CalcCheck Instances for COMPSCI 2LC3, Fall 2024

(Accessing the notebooks from here bypasses the McMaster LMS “Avenue”, so you won't be able to save, nor see your previous saves.)

Introduction to Calculational Proofs

• Example 1.1: The Answer
• Homework 1: Simple Calculations in CalcCheck
• Exercise 1.1: Simple Calculations in CalcCheck
• Exercise 1.2: An Equational Theory of Integers
• Exercise 1.3: Calculations with Boolean Operators
• Exercise 1.4: Substitution
• Homework 2: Substitution
• Exercise 2.1: Re-Proving the Equational Theory of Integers with Rigid Matching
• Exercise 2.2: Re-Proving the Integer Theorems without Automatic Associativity and Symmetry
• Exercise 2.3: Re-Proving the Integer Theorems for Masochists
• Exercise 2.4: Propositional Calculus: From Equivalence to Inequivalence
• Exercise 2.5: Propositional Calculus: Disjunction
• Exercise 2.6: Propositional Calculus: Conjunction
• Extra Exercise 2.7: Knights and Knaves
• Homework 3: Correctness of Assignment Commands
• Homework 4 Notebook 1: Natural Numbers and Induction
• Homework 4 Notebook 2: Propositional Calculus
• Homework 5 Notebook 1: Leibniz as Axiom, Replacement
• Homework 5 Notebook 2: Calculations with Monotonicity and Antitonicity
• Exercise 3.1: Implication
• Exercise 3.2: Natural Numbers and Induction: Addition and Multiplication
• Exercise 3.3: Monus Subtraction
• Exercise 3.4: Assignment Commands with Boolean Variables
• Homework 6 Notebook 1: Quantification Expansion 1
• Homework 6 Notebook 2: Quantification Expansion 2
• Homework 6 Notebook 3: Quantification Expansion 3
• Homework 6 Notebook 4: Structured Proofs in the Propositional Calculus
• Reference Notebook 4.1: Inequality
• Exercise 4.1: Leibniz as Axiom, Replacement
• Exercise 4.2: Calculations with Monotonicity and Antitonicity
• Exercise 4.3: Equality and Predecessors in ℕ
• Exercise 4.4: Simple Proofs `By cases` on ℕ
• Exercise 4.5: Positivity
• Exercise 4.6: Partial Solutions to Exercise 4.5: Positivity
• Exercise 4.7: Order on Integers

Quantification and Predicate Logic

• Homework 7: Substituting into Quantifications
• Reference Notebook 4.2: General Quantification Following LADM Chapter 8
• Reference Notebook 4.3: General Quantification Material, Instantiated for ∀
• Reference Notebook 4.4: General Quantification Material, Instantiated for ∃
• Reference Notebook 4.5: General Quantification Material, Instantiated for ∑ on ℕ
• Reference Notebook 4.6: General Quantification Material, Instantiated for ∏ on ℕ
• Reference Notebook 4.7: Universal Quantification (LADM 9.1)
• Reference Notebook 4.8: Existential Quantification (LADM 9.2)
• Homework 8 Notebook 1: Introduction to Instantiation
• Homework 8 Notebook 2: Practice with Universal and Existential Quantification
• Exercise 5.1: Manipulating Ranges in ℤ
• Exercise 5.2: Practice with ∀ and ∃
• Exercise 5.3: Indirect Equality, Maximum, and Minimum on ℤ
• Exercise 5.4: “Mixed Monotonicity”
• Exercise 5.5: Sum Quantification in ℤ
• Assignment 1 Notebook 1: Conditional Commands
• Assignment 1 Notebook 2: Correctness of `while` Loops
• Exercise 6.1: Introduction to Sequences
• Exercise 6.2: Sequences Continued
• Exercise 6.3: Sets
• Exercise 6.4: Set Theory
• Reference Notebook 6.1: Set Theory
• Exercise 6.5: Pairs and Cartesian Products
• Exercise 6.6: Correctness of `while` Loops
• Homework 9 Notebook 1: Using Explicit Induction Principles
• Homework 9 Notebook 2: Binary Trees
• Exercise 7.1: Multiplication on ℕ Using Explicit Induction Principle
• Exercise 7.2: Binary Trees
• Exercise 7.3: Correctness of `elem`

Relations, Graphs, etc.

• Homework 10 Notebook 1: Pairs
• Homework 10 Notebook 2: Cartesian Product of Sets
• Homework 10 Notebook 3: Relations via Set Theory: Definitions
• Homework 11: Some Properties of Relation Operations in Set Theory
• Exercise 8.1: Typed Universal Sets
• Exercise 8.2: Relations via Set Theory: More Properties
• Reference Notebook 8.1: Properties of the Basic Relation Operations
• Exercise 8.3: Properties of Relations Shown as Simple Graphs
• Assignment 2 Notebook 1: Correctness of `rev`
• Assignment 2 Notebook 2: Absolute Value in ℤ
• Homework 12: Heterogeneous Relation Properties
• Exercise 9.1: Correctness of `elem` with Ghost Variable
• Reference Notebook 9.1: Operators Combining Sets and Relations
• Exercise 9.2: Operators Combining Sets and Relations
• Reference Notebook 9.2: Abstract Relation Algebra: Starting from ⊆ and ⨾
• Reference Notebook 9.3: Abstract Relation Algebra: Continuing with Converse after ⊆ and ⨾
• Reference Notebook 9.4: Continuing Abstract Relation Algebra with Intersection
• Exercise 9.3: Starting Abstract Relation Algebra from ⊆, ⨾, and 𝕀
• Exercise 9.4: Abstract Relation Algebra: Continuing with Converse after ⊆ and ⨾
• Exercise 9.5: Continuing Abstract Relation Algebra with Intersection
• Exercise 9.6: More Relation-algebraic Proofs
• Reference Notebook 9.5: Abstract Relation Algebra: Binary Union
• Homework 13: Abstract Relation Algebra: More Union Material
• Exercise 10.1: Partial-Function Application
• Reference Notebook 10.1: Abstract Relation Algebra: Least Relations
• Reference Notebook 10.2: Abstract Relation Algebra: Arbitrary Unions
• Exercise 10.2: Abstract Relation Algebra: Reflexive-transitive Closure
• Exercise 10.3: Verification Condition Generation
• Reference Notebook 11.1: Abstract Kleene Algebra
• Exercise 11.1: Abstract Kleene Algebra
• Reference Notebook 11.2: Subidentity Relations in Set Theory
• Reference Notebook 11.3: Domain in Abstract Relation Algebra
• Homework 14: Domain in Abstract Relation Algebra
• Reference Notebook 11.4: Z Arrows
• Exercise 11.2: Correctness of Array Modifications
• Exercise 11.3: Expression Datatypes for Relational Semantics
• Exercise 11.4: Relational Semantics: Partial Correctness
• Reference Notebook “Function Extensionality”
• Reference Notebook “Function Prelude”
• Reference and Practice Notebook 12.1: More on Subidentity Relations in Set Theory
• Assignment 3: Relational Semantics
• Exercise 12.1: PLTL