CalcCheck Instances for COMPSCI 2LC3, Fall 2025

(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

• Homework 1: Getting Started with CalcCheck
• Example 1.1: Universal and Existential Quantification
• Example 1.2: The Answer
• Homework 2: Expressions and Calculations
• Exercise 1.1: Simple Calculations in CalcCheck
• Exercise 1.2: An Equational Theory of Integers
• Exercise 1.3: Substitution
• Exercise 1.4: Re-Proving the Equational Theory of Integers with Rigid Matching
• Exercise 1.5: Re-Proving the Integer Theorems without Automatic Associativity and Symmetry
• Exercise 1.6: Re-Proving the Integer Theorems for Masochists

Propositional Calculus, Natural Induction, and Getting Started with Command Correctness

• Homework 3: Correctness of Assignment Commands
• Homework 4: First Steps in Propositional Calculus following LADM Chapter 3
• Exercise 2.1: Propositional Calculus: From Equivalence to Inequivalence
• Exercise 2.2: Propositional Calculus: Disjunction
• Exercise 2.3: Propositional Calculus: Conjunction
• Exercise 2.4: Implication
• Extra Exercise 2.5: Knights and Knaves
• Exercise 2.6: Assignment Commands with Boolean Variables
• Homework 5: Leibniz as Axiom, Replacement
• Homework 6: Structured Proofs in the Propositional Calculus
• Assignment 1 Notebook 1: Propositional Calculus
• Assignment 1 Notebook 2: Assignment Commands with Boolean Variables
• Homework 7: Natural Numbers and Induction
• Exercise 3.1: Leibniz as Axiom, Replacement
• Exercise 3.2: Natural Numbers and Induction: Addition and Multiplication
• Exercise 3.3: Monus Subtraction
• Homework 8: Calculations with Monotonicity and Antitonicity
• Homework 9: Correctness of `while` Loops
• Exercise 4.1: Calculations with Monotonicity and Antitonicity
• Reference Notebook Inequality
• Exercise 4.2: Positivity
• Exercise 4.3: Partial Solutions to Exercise 4.2: Positivity
• Exercise 4.4: Order on Integers

Quantification and Predicate Logic

• Homework 10 Notebook 1: Quantification Expansion 1
• Homework 10 Notebook 2: Quantification Expansion 2
• Homework 10 Notebook 3: Quantification Expansion 3
• Homework 11: Substituting into Quantifications
• Reference Notebook: General Quantification Following LADM Chapter 8
• Reference Notebook: General Quantification Instantiated for ∀
• Reference Notebook: General Quantification Instantiated for ∃
• Reference Notebook: General Quantification Instantiated for ∑ on ℕ
• Reference Notebook: General Quantification Instantiated for ∏ on ℕ
• Reference Notebook: Universal Quantification (LADM 9.1)
• Reference Notebook: Existential Quantification (LADM 9.2)
• Homework 12: Introduction to Instantiation
• Exercise 5.1: Oddities
• Exercise 5.2: Equality and Predecessors in ℕ
• Exercise 5.3: Simple Proofs `By cases` on ℕ
• Exercise 5.4: Manipulating Ranges in ℤ
• Exercise 5.5: Sum Quantification in ℤ
• Homework 13: Practice with Universal and Existential Quantification
• Exercise 6.1: Introduction to Sequences
• Exercise 6.2: Sequences Continued
• Exercise 6.3: Practice with ∀ and ∃
• Exercise 6.4: Indirect Equality, Maximum, and Minimum on ℤ
• Exercise 6.5: “Mixed Monotonicity”
• Exercise 6.6: Correctness of `while` Loops

Sets and Relations

• Reference Notebook “Set Theory”
• Homework 14: Set Theory Basics
• Exercise 7.1: Set Theory
• Exercise 7.2: Pairs and Cartesian Products
• Homework 15 Notebook 1: Cartesian Products of Sets
• Homework 15 Notebook 2: Relations via Set Theory: Definitions
• Exercise 7.3: Typed Universal Sets
• Homework 16: Some Properties of Relation Operations in Set Theory
• Exercise 7.4: Relations via Set Theory: More Properties
• Reference Notebook “Basic Relation Operation Properties”
• Exercise 8.1: Properties of Relations Shown as Simple Graphs
• Homework 17: Heterogeneous Relation Properties
• Reference Notebook “Operators Combining Sets and Relations”
• Exercise 8.2: Operators Combining Sets and Relations
• Homework 18: Using Explicit Induction Principles
• Homework 19: Binary Trees
• Homework 19 (variant): Binary Trees
• Exercise 9.1: Multiplication on ℕ Using Explicit Induction Principle
• Exercise 9.2: Binary Trees
• Exercise 9.2 (variant): Binary Trees
• Reference Notebook “Induction Principles for ℕ”
• Reference Notebook “Well-foundedness of ℕ”
• Reference Notebook “Subidentity Relations in Set Theory”
• Assignment 2 Notebook 1: Partial-Function Application
• Assignment 2 Notebook 2: Conditional Commands
• Assignment 2 Notebook 3: Proofs about Sum Quantification on ℕ
• Reference Notebook “Z Arrows”
• Exercise 9.3: Sequences Misc.
• Exercise 9.4: Sum Quantification Misc.
• Homework 20: Bags
• Exercise 10.2: Bags