CalcCheck Instances for COMPSCI&SFWRENG 2DM3, Fall 2019

Introduction to Calculational Proofs

• Example 1.1: Portia's Suitor's Dilemma
• Example 1.2: The Answer
• Exercise 1.1: Calculations using the Equational Theory of Integers
• Exercise 1.2: Boolean Calculations
• Extra Notebook: A Theory of Integers 1
• Homework 1: Simple Calculations in CalcCheck
• Homework Notebook 2.1: Left- and Right-identities and -zeros
• Homework Notebook 2.2: Implication
• Exercise 2.1: Substitutions
• Exercise 2.2: An Equational Theory of Integers
• Exercise 2.3: Proving in the Equational Theory of Integers without Automatic Associativity and Symmetry
• Exercise 2.4: Proving in the Equational Theory of Integers with Rigid Matching
• Exercise 2.5: Proving in the Equational Theory of Integers for Masochists
• Assignment Notebook 1.1: Calculations using the Equational Theory of Integers
• Assignment Notebook 1.2: Boolean Calculations
• Homework 3: Correctness of Assignment Commands

Propositional Calculus, Natural Induction

• Homework 4: Equivalence and Inequivalence following LADM Chapter 3
• Exercise 3.1: Propositional Calculus: From Equivalence to Inequivalence
• Exercise 3.2: Propositional Calculus: Disjunction
• Exercise 3.3: Propositional Calculus: Conjunction
• Assignment Notebook 2.1: Proving Theorems in the Equational Theory of Integers
• Assignment Notebook 2.2: An Alternate Characterisation of Subtraction for the Theory of Integers
• Homework 5: Natural Numbers and Induction
• Exercise 3.4: Natural Numbers and Induction: Addition and Multiplication
• Exercise 4.1: Inequality
• Homework 6: Order on the Natural Numbers
• Exercise 4.2: Implication
• Exercise 4.3: Monus Subtraction
• Exercise 4.4: Knights and Knaves
• Assignment Notebook 3.1: Conjunction
• Assignment Notebook 3.2: Assignment Commands with Boolean Variables
• Homework Notebook 7.1: Implication
• Homework Notebook 7.2: Leibniz as Axiom, Replacement

Structured Proofs and Sum/Product Quantification

• Homework Notebook 8.1: Quantification Expansion
• Homework Notebook 8.2: Quantification Expansion
• Homework Notebook 8.3: Monotonicity
• Exercise 5.1: Some Properties of Multiplication on ℕ
• Exercise 5.2: Strict-order on Natural Numbers
• Exercise 5.3: More Replacement Theorems
• Exercise 5.4: Quantification Expansion
• Reference Notebook 5.1: Sum Quantification in ℕ
• Assignment Notebook 4.1: Implication
• Assignment Notebook 4.2: Replacement
• Assignment Notebook 4.3: Order on ℕ
• Homework 9: Reversed Presentation for Correctness Reasoning
• Exercise 5.5: Implication Chains and Monotonicity
• Exercise 5.6: Simple Proofs `By cases` on ℕ
• Exercise 6.1: Positivity
• Exercise 6.2: Partial Solutions to Exercise 6.1: Positivity
• Exercise 6.3: Order on Integers
• Exercise 6.4: Conditional
• Exercise 6.5: Manipulating Ranges in ℕ
• Exercise 6.6: “Split-off Term” Theorems for Sum Quantification on ℕ

Quantification and Predicate Logic

• Homework 10: Substituting into Quantifications
• Exercise 7.1: Universal Quantification
• Exercise 7.2: Existential Quantification
• Homework Notebook 11.1: Introduction to Instantiation
• Homework Notebook 11.2: Practice with Universal and Existential Quantification in the Setting of ℕ
• Exercise 7.3: Practice with Universal and Existential Quantification in the Setting of ℕ
• Assignment Notebook 5.1: Conditionals
• Assignment Notebook 5.2: Proofs about Sum Quantification on ℕ
• Homework 12: Introduction to Sequences
• Exercise 8.1: Indirect Equality, Maximum, and Minimum on Integers
• Exercise 8.2: Practice with Universal and Existential Quantification in the Setting of ℤ
• Exercise 8.3: Sequences
• Assignment Notebook 6.1: Factorial Counts Permutations
• Assignment Notebook 6.2: Factorial and Exponentiation

Sets and Relations

• Homework Notebook 13.1: Conditional Commands
• Homework Notebook 13.2: Sets
• Exercise 9.1: Formalisation in Predicate Logic
• Exercise 9.2: Sets
• Homework 14: Pairs and Cartesian Products
• Assignment Notebook 7.1: Practice with Universal and Existential Quantification in the Setting of ℤ
• Assignment Notebook 7.2: Sets
• Assignment Notebook 7.3: Correctness of `rev`
• Homework 15: Relations via Set Theory I
• Homework 16: Relations via Set Theory II
• Homework Notebook 17.1: The Polymorphic Identity Relation `Id`
• Exercise 10.1: Relations via Set Theory: Properties of the Basic Operators
• Exercise 10.2: Relation-Algebraic Formalisation
• Homework Notebook 17.2: Relations via Set Theory: Properties of Relations
• Exercise 10.3: Relations via Set Theory: Counterexamples for Non-Properties

Relations, Graphs, etc.

• Homework 18 Notebook 1: Starting Abstract Relation Algebra
• Homework 18 Notebook 2: Continuing Abstract Relation Algebra with Intersection
• Exercise 11.1: Abstract Relation Algebra: Starting from Inclusion, Composition, and Converse
• Exercise 11.2: Continuing Abstract Relation Algebra with Intersection
• Exercise 11.3: Abstract Relation Algebra: Binary Union
• Exercise 11.4: Abstract Relation Algebra: Least Relations
• Assignment 8: Operators Combining Sets and Relations
• Homework Notebook 19.1: Heterogeneous Relation Properties
• Homework Notebook 19.2: Abstract Relation Algebra: More Union Material
• Assignment Notebook 9.1: Partial-Function Application
• Assignment Notebook 9.2: More Relation-algebraic Proofs
• Homework 20: Using the Induction Principle for `suc` in ℕ
• Exercise 12.1: Proving Induction Principles for Natural Numbers
• Exercise 12.2: Abstract Relation Algebra: Arbitrary Unions
• Exercise 12.3: Abstract Relation Algebra: Reflexive-transitive Closure