johalj11__Jasraj+Johal__2023-11-01_04:14:46.241349_EDT.calcnb — Score: 58/58

Here we redevelop the theory of the natural numbers from scratch — nothing about the natural numbers is preloaded here.

Instead of having the successor operator suc, we base induction on 0 and (_+ 1), using an explicitly stated induction principle instead of built-in “By induction”, which is disabled here. (Evaluation is also not available here.)

Using (_+ 1) instead of suc will make some proofs easier once in particular symmetry of addition is activated. (But not in this notebook.)

Using (_+ 1) instead of suc also brings the presentation closer to what you will see in many other places, including LADM chapter 12.

(All propositional logic and predicate logic are preloaded here, and four hint items are allowed per hint.)


Weak Induction on Natural Numbers


The type ℕ of natural numbers is set up here so that natural-number literals (such as “0” and “1”) can be used as constants of type ℕ, but no operations on ℕ are registered — not even suc.


Addition


Instead of introducing the constructor suc, we will be using addition of 1, so we need to first introduce addition:


1:  Declaration: _+_ : ℕ → ℕ → ℕ

Declaration: _+_ : ℕ → (ℕ → ℕ)   
    — CalcCheck: Operator _+_: Associating to the left; precedence 100
Top-Level Reports:
— CalcCheck: Found assigned item: Declaration _+_: ℕ → (ℕ → ℕ)

With this, we can already formulate a first axiom:


1:  Axiom “Zero is not successor”: 0 = n + 1  ≡  false

Axiom “Zero is not successor”: 0 = n + 1 ≡ false
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom “Zero is not successor”: 0 = n + 1 ≡ false

A different shape of this is occasionally useful:


1:  Theorem “Zero is not successor”: 0 ≠ n + 1
2:  Proof:
3:      0 ≠ n + 1
4:    ≡⟨“Definition of ≠”⟩
5:      0 = n + 1  ≡  false
6:    ≡⟨“Zero is not successor”⟩
7:      true

Theorem “Zero is not successor”: 0 ≠ n + 1
Proof:
        Proving    `0 ≠ n + 1`:
            0 ≠ n + 1
        ≡ ⟨ “Definition of ≠” ⟩
                — CalcCheck: Found “Definition of ≠”, “Definition of ≠”
                — CalcCheck: ─ OK
            0 = n + 1 ≡ false
        ≡ ⟨ “Zero is not successor” ⟩
                — CalcCheck: Found “Zero is not successor”
                — CalcCheck: ─ OK
            true    
    — CalcCheck: All steps OK   
    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Zero is not successor”: 0 ≠ n + 1
— CalcCheck: Proof of Theorem “Zero is not successor”: 0 ≠ n + 1 appears to be correct: 3/3

Addition is defined by just translating the suc-based definition into using (_+ 1) instead:


1:  Axiom “Definition of +”: 0 + n = n
2:  Axiom “Definition of +”: (m + 1) + n = (m + n) + 1

Axiom “Definition of +”: 0 + n = n
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom “Definition of +”: 0 + n = n

Axiom “Definition of +”: (m + 1) + n = (m + n) + 1
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom “Definition of +”: (m + 1) + n = (m + n) + 1

In this version, natural induction corresponding to that implemented by “By induction on var : ℕ” relies on the following induction principle:


1:  Axiom “Induction over ℕ”:
2:     P[n ≔ 0]
3:     ⇒ (∀ n : ℕ ❙ P • P[n ≔ n + 1])
4:     ⇒ (∀ n : ℕ • P)

Axiom “Induction over ℕ”: P[n ≔ 0] ⇒ ((∀ n : ℕ ❙ P • P[n ≔ n + 1] ) ⇒ (∀ n : ℕ • P ))   
    — CalcCheck: Metavariables: P = P〖n〗
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom “Induction over ℕ”: P[n ≔ 0] ⇒ ((∀ n : ℕ ❙ P • P[n ≔ n + 1] ) ⇒ (∀ n : ℕ • P ))

This can be used to prove properties of the shape (∀ n : ℕ • P) by supplying subproofs for the base case P[n ≔ 0] and the induction step (∀ n : ℕ ❙ P • P[n ≔ n + 1]), as demonstrated in the following example:

Important: Using “Induction over ℕ” with two subproofs can only prove universally-quantified goals, that is, goals of shape (∀ n : ℕ • P)!


 1:  Theorem “Right-identity of + (v0)”: ∀ m : ℕ • m + 0 = m
 2:  Proof:
 3:    Using “Induction over ℕ”:
 4:      Subproof for `(m + 0 = m)[m ≔ 0]`:
 5:        By substitution and “Definition of +”
 6:      Subproof for `∀ m : ℕ ❙ m + 0 = m • (m + 0 = m)[m ≔ m + 1]`:
 7:        For any `m : ℕ` satisfying `m + 0 = m`:
 8:            (m + 0 = m)[m ≔ m + 1]
 9:          =⟨ Substitution, “Definition of +” ⟩
10:            (m + 0) + 1 = m + 1
11:          =⟨ Assumption `m + 0 = m`, “Reflexivity of =” ⟩
12:            true

Theorem “Right-identity of + (v0)”: (∀ m : ℕ • m + 0 = m )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `(m + 0 = m)[m ≔ 0]`:
            By Substitution, “Definition of +”               
                — CalcCheck: Found “Definition of +”, “Definition of +”
        Subproof for `(∀ m : ℕ ❙ m + 0 = m • (m + 0 = m)[m ≔ m + 1] )`:
            For any ` m : ℕ` satisfying `m + 0 = m`:           
            — CalcCheck: Assumptions match quantifier range.
                    Proving    `(m + 0 = m)[m ≔ m + 1]`:
                        (m + 0 = m)[m ≔ m + 1]
                    = ⟨ Substitution, “Definition of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: ─ OK
                        (m + 0) + 1 = m + 1
                    = ⟨ Assumption `m + 0 = m`, “Reflexivity of =” ⟩
                            — CalcCheck: Found assumption `m + 0 = m`
                            — CalcCheck: Found (1.2) “Reflexivity of =”
                            — CalcCheck: ─ OK
                        true                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Right-identity of + (v0)”: (∀ m : ℕ • m + 0 = m )
— CalcCheck: Proof of Theorem “Right-identity of + (v0)”: (∀ m : ℕ • m + 0 = m ) appears to be correct: 0/0

The substitutions in the subproof goals can be taken care of automatically, significantly reducing the overhead of this presentation:


 1:  Theorem “Right-identity of + (v1)”: ∀ m : ℕ • m + 0 = m
 2:  Proof:
 3:    Using “Induction over ℕ”:
 4:      Subproof for `0 + 0 = 0`:
 5:        By “Definition of +”
 6:      Subproof for `∀ m : ℕ ❙ m + 0 = m • (m + 1) + 0 = m + 1`:
 7:        For any `m : ℕ` satisfying `m + 0 = m`:
 8:            (m + 1) + 0
 9:          =⟨ “Definition of +” ⟩
10:            (m + 0) + 1
11:          =⟨ Assumption `m + 0 = m` ⟩
12:            m + 1

Theorem “Right-identity of + (v1)”: (∀ m : ℕ • m + 0 = m )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `0 + 0 = 0`:
            By “Definition of +”               
                — CalcCheck: Found “Definition of +”, “Definition of +”
        Subproof for `(∀ m : ℕ ❙ m + 0 = m • (m + 1) + 0 = m + 1 )`:
            For any ` m : ℕ` satisfying `m + 0 = m`:           
            — CalcCheck: Assumptions match quantifier range.
                    Proving    `(m + 1) + 0 = m + 1`:
                        (m + 1) + 0
                    = ⟨ “Definition of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: ─ OK
                        (m + 0) + 1
                    = ⟨ Assumption `m + 0 = m` ⟩
                            — CalcCheck: Found assumption `m + 0 = m`
                            — CalcCheck: ─ OK
                        m + 1                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Right-identity of + (v1)”: (∀ m : ℕ • m + 0 = m )
— CalcCheck: Proof of Theorem “Right-identity of + (v1)”: (∀ m : ℕ • m + 0 = m ) appears to be correct: 0/0

And as long as the subproofs make their goals obvious, the subproof goals can be omitted, too, making the presentation look almost the same as in Homework 5.3:


 1:  Theorem “Right-identity of + (v2)”: ∀ m : ℕ • m + 0 = m
 2:  Proof:
 3:    Using “Induction over ℕ”:
 4:      Subproof:
 5:          0 + 0
 6:        =⟨ “Definition of +” ⟩
 7:          0
 8:      Subproof:
 9:        For any `m : ℕ` satisfying “IndHyp” `m + 0 = m`:
10:            (m + 1) + 0
11:          =⟨ “Definition of +” ⟩
12:            (m + 0) + 1
13:          =⟨ Assumption “IndHyp” ⟩
14:            m + 1

Theorem “Right-identity of + (v2)”: (∀ m : ℕ • m + 0 = m )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `0 + 0 = 0`:
                Proving    `0 + 0 = 0`:
                    0 + 0
                = ⟨ “Definition of +” ⟩
                        — CalcCheck: Found “Definition of +”, “Definition of +”
                        — CalcCheck: ─ OK
                    0            
            — CalcCheck: All steps OK           
            — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ m : ℕ ❙ m + 0 = m • (m + 1) + 0 = m + 1 )`:
            For any ` m : ℕ` satisfying “IndHyp” `m + 0 = m`:           
            — CalcCheck: Assumptions match quantifier range.
                    Proving    `(m + 1) + 0 = m + 1`:
                        (m + 1) + 0
                    = ⟨ “Definition of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: ─ OK
                        (m + 0) + 1
                    = ⟨ Assumption “IndHyp” ⟩
                            — CalcCheck: Found assumption “IndHyp”
                            — CalcCheck: ─ OK
                        m + 1                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Right-identity of + (v2)”: (∀ m : ℕ • m + 0 = m )
— CalcCheck: Proof of Theorem “Right-identity of + (v2)”: (∀ m : ℕ • m + 0 = m ) appears to be correct: 0/0

And if a theorem statement without explicit universal quantification is desired, one can just adapt this proof accordingly:


 1:  Theorem “Right-identity of +”:  m + 0 = m
 2:  Proof:
 3:        m + 0 = m
 4:      ≡ ⟨ Substitution ⟩
 5:        (m + 0 = m)[m ≔ m]
 6:      ⇐ ⟨ “Instantiation” ⟩
 7:        ∀ m : ℕ • m + 0 = m
 8:    Proof for this:
 9:      Using “Induction over ℕ”:
10:        Subproof:
11:            0 + 0
12:          =⟨ “Definition of +” ⟩
13:            0
14:        Subproof:
15:          For any `m : ℕ` satisfying “IndHyp” `m + 0 = m`:
16:              (m + 1) + 0
17:            =⟨ “Definition of +” ⟩
18:              (m + 0) + 1
19:            =⟨ Assumption “IndHyp” ⟩
20:              m + 1

Theorem “Right-identity of +”: m + 0 = m
Proof:
            Proving    `m + 0 = m`:
                m + 0 = m
            ≡ ⟨ Substitution ⟩
                    — CalcCheck: ─ OK
                (m + 0 = m)[m ≔ m]
            ⇐ ⟨ “Instantiation” ⟩
                    — CalcCheck: Found (9.13) “Instantiation”, (9.13.2) “Instantiation”, (9.13.1) “Instantiation”
                    — CalcCheck: ─ OK
                (∀ m : ℕ • m + 0 = m )        
        — CalcCheck: All steps OK       
        — CalcCheck: Calculation matches goal ─ OK
    Proof for `(∀ m : ℕ • m + 0 = m )`:
        Using “Induction over ℕ”:           
            — CalcCheck: Found “Induction over ℕ”
            Subproof for `0 + 0 = 0`:
                    Proving    `0 + 0 = 0`:
                        0 + 0
                    = ⟨ “Definition of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: ─ OK
                        0                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
            Subproof for `(∀ m : ℕ ❙ m + 0 = m • (m + 1) + 0 = m + 1 )`:
                For any ` m : ℕ` satisfying “IndHyp” `m + 0 = m`:               
                — CalcCheck: Assumptions match quantifier range.
                        Proving    `(m + 1) + 0 = m + 1`:
                            (m + 1) + 0
                        = ⟨ “Definition of +” ⟩
                                — CalcCheck: Found “Definition of +”, “Definition of +”
                                — CalcCheck: ─ OK
                            (m + 0) + 1
                        = ⟨ Assumption “IndHyp” ⟩
                                — CalcCheck: Found assumption “IndHyp”
                                — CalcCheck: ─ OK
                            m + 1                    
                    — CalcCheck: All steps OK                   
                    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Right-identity of +”: m + 0 = m
— CalcCheck: Proof of Theorem “Right-identity of +”: m + 0 = m appears to be correct: 0/0

(However, as long as no explicit substitution needs to be provided, the version with explicit universal quantification, “Right-identity of + (v2)”, is just as useful as the version without, due to automatic instantiation as explained in H10.)


Using the built-in induction support for natural induction that you are familiar with from H5.1, Ex3.5, etc., the theorem “Adding the successor” could be shown as follows:

Theorem “Adding the successor”: m + (suc n) = suc (m + n)
Proof:
  By induction on `m : ℕ`:
    Base case: By “Definition of +”
    Induction step:
        (suc m) + (suc n)
      =⟨ “Definition of +” ⟩
        suc (m + (suc n))
      =⟨ Induction hypothesis ⟩
        suc (suc (m + n))
      =⟨ “Definition of +” ⟩
        suc ((suc m) + n)

For turning this into a proof using “Induction over ℕ”, this will be proving a goal of shape “∀ m : ℕ • ...”.

Since mixing explicit and implicit universal quantification is somewhat dubious stylistically, and also can induce technical problems, a natural way to state theorems here will actually quantify all variables explicitly — this mainly means that additional “For any” structures will be needed in the proofs:


 1:  Theorem “Adding the successor”:
 2:      ∀ m • ∀ n • m + (n + 1) = (m + n) + 1
 3:  Proof:
 4:  
 5:    Using “Induction over ℕ”:
 6:      Subproof for `∀ n • 0 + (n + 1) = (0 + n) + 1`:
 7:        For any `n : ℕ`:
 8:            0 + (n + 1) = (0 + n) + 1
 9:          =⟨ “Definition of +” ⟩
10:            n + 1 = n + 1
11:          ≡⟨ “Reflexivity of =” ⟩
12:            true
13:      Subproof for `∀ m ❙ (∀ n • m + (n + 1) = (m + n) + 1)
14:                        • (∀ n • (m + 1) + (n + 1) = ((m + 1) + n) + 1)`:
15:        For any `m : ℕ` satisfying “IndHyp” `∀ n • m + (n + 1) = (m + n) + 1`:
16:          For any `n : ℕ`:
17:              (m + 1) + (n + 1) = ((m + 1) + n) + 1
18:            =⟨ “Definition of +” ⟩
19:              (m + (n + 1)) + 1 = ((m + n) + 1) + 1
20:            =⟨ Assumption “IndHyp” ⟩
21:              ((m + n) + 1) + 1 = ((m + n) + 1) + 1
22:            ≡⟨ “Reflexivity of =” ⟩
23:              true

Theorem “Adding the successor”: (∀ m • (∀ n • m + (n + 1) = (m + n) + 1 ) )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `(∀ n • 0 + (n + 1) = (0 + n) + 1 )`:
            For any ` n : ℕ`:
                    Proving    `0 + (n + 1) = (0 + n) + 1`:
                        0 + (n + 1) = (0 + n) + 1
                    = ⟨ “Definition of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: ─ OK
                        n + 1 = n + 1
                    ≡ ⟨ “Reflexivity of =” ⟩
                            — CalcCheck: Found (1.2) “Reflexivity of =”
                            — CalcCheck: ─ OK
                        true                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ m ❙ (∀ n • m + (n + 1) = (m + n) + 1 ) • (∀ n • (m + 1) + (n + 1) = ((m + 1) + n) + 1 ) )`:
            For any ` m : ℕ` satisfying “IndHyp” `(∀ n • m + (n + 1) = (m + n) + 1 )`:           
            — CalcCheck: Assumptions match quantifier range.
                For any ` n : ℕ`:
                        Proving    `(m + 1) + (n + 1) = ((m + 1) + n) + 1`:
                            (m + 1) + (n + 1) = ((m + 1) + n) + 1
                        = ⟨ “Definition of +” ⟩
                                — CalcCheck: Found “Definition of +”, “Definition of +”
                                — CalcCheck: ─ OK
                            (m + (n + 1)) + 1 = ((m + n) + 1) + 1
                        = ⟨ Assumption “IndHyp” ⟩
                                — CalcCheck: Found assumption “IndHyp”
                                — CalcCheck: ─ OK
                            ((m + n) + 1) + 1 = ((m + n) + 1) + 1
                        ≡ ⟨ “Reflexivity of =” ⟩
                                — CalcCheck: Found (1.2) “Reflexivity of =”
                                — CalcCheck: ─ OK
                            true                    
                    — CalcCheck: All steps OK                   
                    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Adding the successor”: (∀ m • (∀ n • m + (n + 1) = (m + n) + 1 ) )
— CalcCheck: Proof of Theorem “Adding the successor”: (∀ m • (∀ n • m + (n + 1) = (m + n) + 1 ) ) appears to be correct: 5/5

Convert the following proof of “Symmetry of +”, which is not accepted here due to disabled support for “By induction” and absence of suc, to the format used above:

Theorem “Symmetry of +”: m + n = n + m
Proof:
  By induction on `m : ℕ`:
    Base case:
        0 + n
      =⟨ “Definition of +” ⟩
        n
      =⟨ “Right-identity of +” ⟩
        n + 0
    Induction step:
        (suc m) + n
      =⟨ “Definition of +” ⟩
        suc (m + n)
      =⟨ Induction hypothesis ⟩
        suc (n + m)
      =⟨ “Adding the successor” ⟩
        n + (suc m)

 1:  Theorem “Symmetry of +”:
 2:      ∀ m • ∀ n • m + n = n + m
 3:  Proof:
 4:    Using “Induction over ℕ”:
 5:      Subproof for `∀ n • 0 + n = n + 0`:
 6:        For any `n`:
 7:            0 + n = n + 0
 8:          =⟨ “Definition of +” , “Right-identity of +” ⟩
 9:            n = n
10:          ≡⟨ “Reflexivity of =” ⟩
11:            true
12:      Subproof for `∀ m ❙ (∀ n • m + n = n + m)
13:                        • (∀ n • (m + 1) + n = n + (m + 1))`:
14:        For any `m : ℕ` satisfying “IndHyp” `(∀ n • m + n = n + m)`:
15:          For any `n`:
16:              (m + 1) + n = n + (m + 1)
17:            =⟨ “Definition of +” , “Adding the successor” ⟩
18:              (m + n) + 1 = (n + m) + 1
19:            =⟨ Assumption “IndHyp” ⟩
20:              (n + m) + 1 = (n + m) + 1
21:            ≡⟨ “Reflexivity of =” ⟩
22:              true

Theorem “Symmetry of +”: (∀ m • (∀ n • m + n = n + m ) )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `(∀ n • 0 + n = n + 0 )`:
            For any ` n`:
                    Proving    `0 + n = n + 0`:
                        0 + n = n + 0
                    = ⟨ “Definition of +”, “Right-identity of +” ⟩
                            — CalcCheck: Found “Definition of +”, “Definition of +”
                            — CalcCheck: Found “Right-identity of +”
                            — CalcCheck: ─ OK
                        n = n
                    ≡ ⟨ “Reflexivity of =” ⟩
                            — CalcCheck: Found (1.2) “Reflexivity of =”
                            — CalcCheck: ─ OK
                        true                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ m ❙ (∀ n • m + n = n + m ) • (∀ n • (m + 1) + n = n + (m + 1) ) )`:
            For any ` m : ℕ` satisfying “IndHyp” `(∀ n • m + n = n + m )`:           
            — CalcCheck: Assumptions match quantifier range.
                For any ` n`:
                        Proving    `(m + 1) + n = n + (m + 1)`:
                            (m + 1) + n = n + (m + 1)
                        = ⟨ “Definition of +”, “Adding the successor” ⟩
                                — CalcCheck: Found “Definition of +”, “Definition of +”
                                — CalcCheck: Found “Adding the successor”
                                — CalcCheck: ─ OK
                            (m + n) + 1 = (n + m) + 1
                        = ⟨ Assumption “IndHyp” ⟩
                                — CalcCheck: Found assumption “IndHyp”
                                — CalcCheck: ─ OK
                            (n + m) + 1 = (n + m) + 1
                        ≡ ⟨ “Reflexivity of =” ⟩
                                — CalcCheck: Found (1.2) “Reflexivity of =”
                                — CalcCheck: ─ OK
                            true                    
                    — CalcCheck: All steps OK                   
                    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Symmetry of +”: (∀ m • (∀ n • m + n = n + m ) )
— CalcCheck: Proof of Theorem “Symmetry of +”: (∀ m • (∀ n • m + n = n + m ) ) appears to be correct: 7/7

Prove “Associativity of +” by induction over k:


 1:  Theorem “Associativity of +”: ∀ k • ∀ m • ∀ n • (k + m) + n = k + (m + n)
 2:  Proof:
 3:    Using “Induction over ℕ”:
 4:      Subproof for `∀ m • ∀ n • (0 + m) + n = 0 + (m + n)`:
 5:        For any `m`:
 6:          For any `n`:
 7:              (0 + m) + n = 0 + (m + n)
 8:            =⟨ “Definition of +” ⟩
 9:              m + n = m + n
10:            =⟨ “Reflexivity of =” ⟩
11:              true
12:      Subproof for `∀ k ❙ (∀ m • ∀ n • (k + m) + n = k + (m + n))
13:                        • (∀ m • ∀ n • ((k + 1) + m) + n = (k + 1) + (m + n))`:
14:        For any `k : ℕ` satisfying “IndHyp” `(∀ m • ∀ n • (k + m) + n = k + (m + n))`:
15:          For any `m`:
16:            For any `n`:
17:                ((k + 1) + m) + n = (k + 1) + (m + n)
18:              =⟨ “Definition of +” ⟩
19:                ((k + m) + 1) + n = (k + (m + n)) + 1
20:              =⟨ “Definition of +” ⟩
21:                ((k + m) + n) + 1 = (k + (m + n)) + 1
22:              =⟨ Assumption “IndHyp” ⟩
23:                (k + (m + n)) + 1 = (k + (m + n)) + 1
24:              ≡⟨ “Reflexivity of =” ⟩
25:                true

Theorem “Associativity of +”: (∀ k • (∀ m • (∀ n • (k + m) + n = k + (m + n) ) ) )
Proof:
    Using “Induction over ℕ”:       
        — CalcCheck: Found “Induction over ℕ”
        Subproof for `(∀ m • (∀ n • (0 + m) + n = 0 + (m + n) ) )`:
            For any ` m`:
                For any ` n`:
                        Proving    `(0 + m) + n = 0 + (m + n)`:
                            (0 + m) + n = 0 + (m + n)
                        = ⟨ “Definition of +” ⟩
                                — CalcCheck: Found “Definition of +”, “Definition of +”
                                — CalcCheck: ─ OK
                            m + n = m + n
                        = ⟨ “Reflexivity of =” ⟩
                                — CalcCheck: Found (1.2) “Reflexivity of =”
                                — CalcCheck: ─ OK
                            true                    
                    — CalcCheck: All steps OK                   
                    — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ k ❙ (∀ m • (∀ n • (k + m) + n = k + (m + n) ) ) • (∀ m • (∀ n • ((k + 1) + m) + n = (k + 1) + (m + n) ) ) )`:
            For any ` k : ℕ` satisfying “IndHyp” `(∀ m • (∀ n • (k + m) + n = k + (m + n) ) )`:           
            — CalcCheck: Assumptions match quantifier range.
                For any ` m`:
                    For any ` n`:
                            Proving    `((k + 1) + m) + n = (k + 1) + (m + n)`:
                                ((k + 1) + m) + n = (k + 1) + (m + n)
                            = ⟨ “Definition of +” ⟩
                                    — CalcCheck: Found “Definition of +”, “Definition of +”
                                    — CalcCheck: ─ OK
                                ((k + m) + 1) + n = (k + (m + n)) + 1
                            = ⟨ “Definition of +” ⟩
                                    — CalcCheck: Found “Definition of +”, “Definition of +”
                                    — CalcCheck: ─ OK
                                ((k + m) + n) + 1 = (k + (m + n)) + 1
                            = ⟨ Assumption “IndHyp” ⟩
                                    — CalcCheck: Found assumption “IndHyp”
                                    — CalcCheck: ─ OK
                                (k + (m + n)) + 1 = (k + (m + n)) + 1
                            ≡ ⟨ “Reflexivity of =” ⟩
                                    — CalcCheck: Found (1.2) “Reflexivity of =”
                                    — CalcCheck: ─ OK
                                true                        
                        — CalcCheck: All steps OK                       
                        — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Associativity of +”: (∀ k • (∀ m • (∀ n • (k + m) + n = k + (m + n) ) ) )
— CalcCheck: Proof of Theorem “Associativity of +”: (∀ k • (∀ m • (∀ n • (k + m) + n = k + (m + n) ) ) ) appears to be correct: 12/12

Note that symmetry and associativity of addition are not activated here, so their uses will need to be made explicit below where necessary.


Sequences


We introduce the sequence type and its constructors also without setup for “By induction on `xs : Seq A`”:


1:  Declaration: Seq : Type → Type

Declaration: Seq : Type → Type
Top-Level Reports:
— CalcCheck: Found assigned item: Declaration Seq: Type → Type 

1:  Declaration: 𝜖 : Seq A
2:  Declaration: _◃_ : A → Seq A → Seq A

Declaration: 𝜖 : Seq A
Top-Level Reports:
— CalcCheck: Found assigned item: Declaration 𝜖: Seq A

Declaration: _◃_ : A → (Seq A → Seq A)   
    — CalcCheck: Operator _◃_: Associating to the right; precedence 60
Top-Level Reports:
— CalcCheck: Found assigned item: Declaration _◃_: A → (Seq A → Seq A) 

1:  Axiom (13.3) “Cons is not empty”: x ◃ xs ≠ 𝜖

Axiom (13.3) “Cons is not empty”: x ◃ xs ≠ 𝜖
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom (13.3) “Cons is not empty”: x ◃ xs ≠ 𝜖 

1:  Theorem “Cons is not empty”: x ◃ xs = 𝜖  ≡  false
2:  Proof:
3:      x ◃ xs = 𝜖  ≡ false
4:    ≡⟨ “Definition of ≠” ⟩
5:      x ◃ xs ≠ 𝜖
6:    ≡⟨ “Cons is not empty” ⟩
7:      true

Theorem “Cons is not empty”: x ◃ xs = 𝜖 ≡ false
Proof:
        Proving    `x ◃ xs = 𝜖 ≡ false`:
            x ◃ xs = 𝜖 ≡ false
        ≡ ⟨ “Definition of ≠” ⟩
                — CalcCheck: Found “Definition of ≠”, “Definition of ≠”
                — CalcCheck: ─ OK
            x ◃ xs ≠ 𝜖
        ≡ ⟨ “Cons is not empty” ⟩
                — CalcCheck: Found (13.3) “Cons is not empty”
                — CalcCheck: ─ OK
            true    
    — CalcCheck: All steps OK   
    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem “Cons is not empty”: x ◃ xs = 𝜖 ≡ false
— CalcCheck: Proof of Theorem “Cons is not empty”: x ◃ xs = 𝜖 ≡ false appears to be correct: 3/3 

1:  Axiom (13.4) “Equality of ◃” “Injectivity of ◃” “Cancellation of ◃”:
2:     x ◃ xs  =  y ◃ ys   ≡   x = y  ∧  xs = ys

Axiom (13.4) “Equality of ◃” “Injectivity of ◃” “Cancellation of ◃”: x ◃ xs = y ◃ ys ≡ x = y ∧ xs = ys
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom (13.4) “Equality of ◃” “Injectivity of ◃” “Cancellation of ◃”: x ◃ xs = y ◃ ys ≡ x = y ∧ xs = ys

We provide the ◃-based induction principle for sequences in the following shape:


1:  Axiom “Induction over sequences”:
2:      P[xs ≔ 𝜖]
3:      ⇒ (∀ xs : Seq A ❙ P • (∀ x : A • P[xs ≔ x ◃ xs]))
4:      ⇒ (∀ xs : Seq A • P)

Axiom “Induction over sequences”: P[xs ≔ 𝜖] ⇒ ((∀ xs : Seq A ❙ P • (∀ x : A • P[xs ≔ x ◃ xs] ) ) ⇒ (∀ xs : Seq A • P ))   
    — CalcCheck: Metavariables: A = A〖〗, P = P〖xs〗   
    — CalcCheck: Proviso: ¬occurs(`x`, `P`), ¬occurs(`xs`, `A`)
Top-Level Reports:
— CalcCheck: Found assigned item: Axiom “Induction over sequences”: P[xs ≔ 𝜖] ⇒ ((∀ xs : Seq A ❙ P • (∀ x : A • P[xs ≔ x ◃ xs] ) ) ⇒ (∀ xs : Seq A • P ))

The lecture showed a proof of “Tail is different”; you can reproduce that here, or bring a different proof into Using “Induction over sequences” shape:


 1:  Theorem (13.7) “Tail is different”:
 2:                   ∀ xs : Seq A • ∀ x : A • x ◃ xs ≠ xs
 3:  Proof:
 4:    Using “Induction over sequences”:
 5:      Subproof for `∀ x : A • x ◃ 𝜖 ≠ 𝜖`:
 6:        For any `x`:
 7:            x ◃ 𝜖 ≠ 𝜖
 8:          ≡⟨ “Cons is not empty” ⟩
 9:            true
10:      Subproof for `∀ xs : Seq A ❙ (∀ x : A • x ◃ xs ≠ xs)
11:                        • (∀ z : A • (∀ x : A • x ◃ z ◃ xs ≠ z ◃ xs))`:
12:        For any `xs : Seq A` satisfying “IndHyp” `(∀ x : A • x ◃ xs ≠ xs)`:
13:          For any `z : A`:
14:            For any `x : A`:
15:                x ◃ (z ◃ xs) ≠ z ◃ xs
16:              =⟨ “Definition of ≠” ⟩
17:                ¬ (x ◃ (z ◃ xs) = z ◃ xs)
18:              ≡⟨ “Equality of ◃” ⟩
19:                ¬ ((x = z) ∧ ((z ◃ xs) = xs))
20:              ≡⟨ “De Morgan”⟩
21:                ¬ (x = z) ∨ ¬ (z ◃ xs = xs)
22:              ≡⟨ “Definition of ≠” ⟩
23:                ¬ (x = z) ∨ (z ◃ xs ≠ xs)
24:              ≡⟨ Assumption “IndHyp” ⟩
25:                ¬ (x = z) ∨ true
26:              ≡⟨ “Zero of ∨” ⟩
27:                true

Theorem (13.7) “Tail is different”: (∀ xs : Seq A • (∀ x : A • x ◃ xs ≠ xs ) )   
    — CalcCheck: Metavariables: A = A〖〗   
    — CalcCheck: Proviso: ¬occurs(`xs`, `A`)
Proof:
    Using “Induction over sequences”:       
        — CalcCheck: Found “Induction over sequences”
        Subproof for `(∀ x : A • x ◃ 𝜖 ≠ 𝜖 )`:
            For any ` x`:
                    Proving    `x ◃ 𝜖 ≠ 𝜖`:
                        x ◃ 𝜖 ≠ 𝜖
                    ≡ ⟨ “Cons is not empty” ⟩
                            — CalcCheck: Found “Cons is not empty”, (13.3) “Cons is not empty”
                            — CalcCheck: ─ OK
                        true                
                — CalcCheck: All steps OK               
                — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ xs : Seq A ❙ (∀ x : A • x ◃ xs ≠ xs ) • (∀ z : A • (∀ x : A • x ◃ (z ◃ xs) ≠ z ◃ xs ) ) )`:
            For any ` xs : Seq A` satisfying “IndHyp” `(∀ x : A • x ◃ xs ≠ xs )`:           
            — CalcCheck: Assumptions match quantifier range.
                For any ` z : A`:
                    For any ` x : A`:
                            Proving    `x ◃ (z ◃ xs) ≠ z ◃ xs`:
                                x ◃ (z ◃ xs) ≠ z ◃ xs
                            = ⟨ “Definition of ≠” ⟩
                                    — CalcCheck: Found “Definition of ≠”, “Definition of ≠”
                                    — CalcCheck: ─ OK
                                ¬ (x ◃ (z ◃ xs) = z ◃ xs)
                            ≡ ⟨ “Equality of ◃” ⟩
                                    — CalcCheck: Found (13.4) “Equality of ◃”
                                    — CalcCheck: ─ OK
                                ¬ (x = z ∧ z ◃ xs = xs)
                            ≡ ⟨ “De Morgan” ⟩
                                    — CalcCheck: Found (3.47a) “De Morgan”, (3.47b) “De Morgan”, (3.47c) “De Morgan”, (3.47d) “De Morgan”
                                    — CalcCheck: ─ OK
                                ¬ (x = z) ∨ ¬ (z ◃ xs = xs)
                            ≡ ⟨ “Definition of ≠” ⟩
                                    — CalcCheck: Found “Definition of ≠”, “Definition of ≠”
                                    — CalcCheck: ─ OK
                                ¬ (x = z) ∨ z ◃ xs ≠ xs
                            ≡ ⟨ Assumption “IndHyp” ⟩
                                    — CalcCheck: Found assumption “IndHyp”
                                    — CalcCheck: ─ OK
                                ¬ (x = z) ∨ true
                            ≡ ⟨ “Zero of ∨” ⟩
                                    — CalcCheck: Found (3.29) “Zero of ∨”
                                    — CalcCheck: ─ OK
                                true                        
                        — CalcCheck: All steps OK                       
                        — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem (13.7) “Tail is different”: (∀ xs : Seq A • (∀ x : A • x ◃ xs ≠ xs ) )
— CalcCheck: Proof of Theorem (13.7) “Tail is different”: (∀ xs : Seq A • (∀ x : A • x ◃ xs ≠ xs ) ) appears to be correct: 13/13

Prove also the following:


 1:  Theorem (13.6) “Cons decomposition”:
 2:      ∀ xs : Seq A •  xs = 𝜖  ∨  (∃ y • ∃ ys • xs = y ◃ ys)
 3:  Proof:
 4:    Using “Induction over sequences”:
 5:      Subproof for `𝜖 = 𝜖  ∨  (∃ y • ∃ ys • 𝜖 = y ◃ ys)`:
 6:           𝜖 = 𝜖  ∨  (∃ y • ∃ ys • 𝜖 = y ◃ ys)
 7:         ≡⟨ “Reflexivity of =” ⟩
 8:           true ∨ (∃ y • ∃ ys • 𝜖 = y ◃ ys)
 9:         ≡⟨ “Zero of ∨” ⟩
10:           true
11:      Subproof for `∀ xs : Seq A ❙ (xs = 𝜖  ∨  (∃ y • ∃ ys • xs = y ◃ ys))
12:                        • (∀ z : A • (z ◃ xs = 𝜖  ∨  (∃ y • ∃ ys • z ◃ xs = y ◃ ys)))`:
13:        For any `xs : Seq A` satisfying “IndHyp” `(xs = 𝜖  ∨  (∃ y • ∃ ys • xs = y ◃ ys))`:
14:          For any `z`:      
15:              (z ◃ xs) = 𝜖  ∨  (∃ y • ∃ ys • (z ◃ xs) = y ◃ ys)
16:            =⟨ “Cons is not empty”, “Identity of ∨” ⟩
17:              ∃ y • ∃ ys • (z ◃ xs) = y ◃ ys
18:            ⇐⟨ “∃-Introduction” ⟩
19:              (∃ ys • (z ◃ xs) = y ◃ ys)[y ≔ z]
20:            =⟨ Substitution ⟩
21:              ∃ ys • (z ◃ xs) = z ◃ ys
22:            ⇐⟨ “∃-Introduction” ⟩
23:              (z ◃ xs = z ◃ ys)[ys ≔ xs]
24:            =⟨ Substitution, “Reflexivity of =” ⟩
25:              true

Theorem (13.6) “Cons decomposition”: (∀ xs : Seq A • xs = 𝜖 ∨ (∃ y • (∃ ys • xs = y ◃ ys ) ) )   
    — CalcCheck: Metavariables: A = A〖〗
Proof:
    Using “Induction over sequences”:       
        — CalcCheck: Found “Induction over sequences”
        Subproof for `𝜖 = 𝜖 ∨ (∃ y • (∃ ys • 𝜖 = y ◃ ys ) )`:
                Proving    `𝜖 = 𝜖 ∨ (∃ y • (∃ ys • 𝜖 = y ◃ ys ) )`:
                    𝜖 = 𝜖 ∨ (∃ y • (∃ ys • 𝜖 = y ◃ ys ) )
                ≡ ⟨ “Reflexivity of =” ⟩
                        — CalcCheck: Found (1.2) “Reflexivity of =”
                        — CalcCheck: ─ OK
                    true ∨ (∃ y • (∃ ys • 𝜖 = y ◃ ys ) )
                ≡ ⟨ “Zero of ∨” ⟩
                        — CalcCheck: Found (3.29) “Zero of ∨”
                        — CalcCheck: ─ OK
                    true            
            — CalcCheck: All steps OK           
            — CalcCheck: Calculation matches goal ─ OK
        Subproof for `(∀ xs : Seq A ❙ xs = 𝜖 ∨ (∃ y • (∃ ys • xs = y ◃ ys ) ) • (∀ z : A • z ◃ xs = 𝜖 ∨ (∃ y • (∃ ys • z ◃ xs = y ◃ ys ) ) ) )`:
            For any ` xs : Seq A` satisfying “IndHyp” `xs = 𝜖 ∨ (∃ y • (∃ ys • xs = y ◃ ys ) )`:           
            — CalcCheck: Assumptions match quantifier range.
                For any ` z`:
                        Proving    `z ◃ xs = 𝜖 ∨ (∃ y • (∃ ys • z ◃ xs = y ◃ ys ) )`:
                            z ◃ xs = 𝜖 ∨ (∃ y • (∃ ys • z ◃ xs = y ◃ ys ) )
                        = ⟨ “Cons is not empty”, “Identity of ∨” ⟩
                                — CalcCheck: Found “Cons is not empty”, (13.3) “Cons is not empty”
                                — CalcCheck: Found (3.30) “Identity of ∨”
                                — CalcCheck: ─ OK
                            (∃ y • (∃ ys • z ◃ xs = y ◃ ys ) )
                        ⇐ ⟨ “∃-Introduction” ⟩
                                — CalcCheck: Found (9.28) “∃-Introduction”, (9.28.1) “∃-Introduction”
                                — CalcCheck: ─ OK
                            (∃ ys • z ◃ xs = y ◃ ys )[y ≔ z]
                        = ⟨ Substitution ⟩
                                — CalcCheck: ─ OK
                            (∃ ys • z ◃ xs = z ◃ ys )
                        ⇐ ⟨ “∃-Introduction” ⟩
                                — CalcCheck: Found (9.28) “∃-Introduction”, (9.28.1) “∃-Introduction”
                                — CalcCheck: ─ OK
                            (z ◃ xs = z ◃ ys)[ys ≔ xs]
                        = ⟨ Substitution, “Reflexivity of =” ⟩
                                — CalcCheck: Found (1.2) “Reflexivity of =”
                                — CalcCheck: ─ OK
                            true                    
                    — CalcCheck: All steps OK                   
                    — CalcCheck: Calculation matches goal ─ OK
Top-Level Reports:
— CalcCheck: Found assigned item: Theorem (13.6) “Cons decomposition”: (∀ xs : Seq A • xs = 𝜖 ∨ (∃ y • (∃ ys • xs = y ◃ ys ) ) )
— CalcCheck: Proof of Theorem (13.6) “Cons decomposition”: (∀ xs : Seq A • xs = 𝜖 ∨ (∃ y • (∃ ys • xs = y ◃ ys ) ) ) appears to be correct: 15/15