Exercise 5

Theorem (3.59): p ⇒ q ≡ ¬ p ∨ q
Proof:
    p ⇒ q
  =⟨ “Definition of ⇒” ⟩
    p ∧ q ≡ p
  =⟨ “Golden rule” ⟩
    p ∨ q ≡ q
  =⟨ (3.32) ⟩
    ¬ p ∨ q ≡ q ≡ q
  =⟨ “Reflexivity of ≡” ⟩
    ¬ p ∨ q ≡ true
  =⟨ “Identity of ≡” ⟩
    ¬ p ∨ q

Theorem “LADM Ex. 3.45”: p ⇒ q ≡ ¬ p ∨ ¬ q ≡ ¬ p
Proof:
    p ⇒ q ≡ ¬ p ∨ ¬ q ≡ ¬ p
  =⟨ “Definition of ⇒” ⟩
    (p ∧ q) ≡ p ≡ ¬ p ∨ ¬ q ≡ ¬ p
  =⟨ (3.32) ⟩
    (p ∧ q) ≡ p ≡ ¬ p ∨ q
  =⟨ (3.59) ⟩
    (p ∧ q) ≡ p ≡ p ⇒ q
  =⟨ “Definition of ⇒” ⟩
    p ⇒ q ≡ p ⇒ q
  =⟨ “Reflexivity of ≡” ⟩
    true
    
Theorem “A4.1a”: (p ≢ q) ⇒ p ∨ q
Proof:
    (p ≢ q) ⇒ p ∨ q
  =⟨ (3.59) ⟩ 
    ¬ (p ≢ q) ∨ (p ∨ q)
  =⟨ “Definition of ≢” ⟩ 
    ¬ ¬ (p ≡ q) ∨ (p ∨ q)
  =⟨ “Double negation” ⟩ 
    (p ≡ q) ∨ (p ∨ q)
  =⟨ “Distributivity of ∨ over ≡” ⟩ 
    (p ∨ (p ∨ q)) ≡ (q ∨ (p ∨ q))
  =⟨ “Idempotency of ∨” ⟩ 
    (p ∨ q) ≡ (p ∨ q)
  =⟨ “Reflexivity of ≡” ⟩ 
    true

Theorem “A4.1b”:
    (p ∧ q) ∨ (¬ p ∧ r) ≡ (p ⇒ q) ≡ (¬ p ⇒ r)
Proof:
    (p ∧ q) ∨ (¬ p ∧ r) ≡ (p ⇒ q) ≡ (¬ p ⇒ r)
  =⟨ (3.59) ⟩
    (p ∧ q) ∨ (¬ p ∧ r) ≡ (¬ p ∨ q) ≡ (¬ ¬ p ∨ r)
  =⟨ “Double negation” ⟩
    (p ∧ q) ∨ (¬ p ∧ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Golden rule” ⟩
    (p ≡ q ≡ p ∨ q) ∨ (¬ p ≡ r ≡ ¬ p ∨ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ (3.32) ⟩
    (p ≡ q ≡ p ∨ q) ∨ (¬ p ≡ p ∨ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Distributivity of ∨ over ≡” ⟩
    (p ≡ q ≡ p ∨ q) ∨ ¬ p ≡ (p ≡ q ≡ p ∨ q) ∨ (p ∨ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Distributivity of ∨ over ≡” ⟩
    (p ∨ ¬ p) ≡ (q ≡ p ∨ q) ∨ ¬ p ≡ (p ∨ p ∨ r ≡ (q ≡ p ∨ q) ∨ (p ∨ r)) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Excluded middle” ⟩
    true ≡ (q ≡ p ∨ q) ∨ ¬ p ≡ (p ∨ p ∨ r ≡ (q ≡ p ∨ q) ∨ (p ∨ r)) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Idempotency of ∨” ⟩
    true ≡ (q ≡ p ∨ q) ∨ ¬ p ≡ (p ∨ r ≡ (q ≡ p ∨ q) ∨ (p ∨ r)) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Distributivity of ∨ over ≡” ⟩
    true ≡ q ∨ ¬ p ≡ p ∨ q ∨ ¬ p ≡ (p ∨ r ≡ q ∨ p ∨ r ≡ p ∨ p ∨ q ∨ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Idempotency of ∨” ⟩
    true ≡ q ∨ ¬ p ≡ p ∨ q ∨ ¬ p ≡ (p ∨ r ≡ q ∨ p ∨ r ≡ p ∨ q ∨ r) ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Excluded middle” ⟩
    true ≡ q ∨ ¬ p ≡ true ∨ q ≡ p ∨ r ≡ q ∨ p ∨ r ≡ p ∨ q ∨ r ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Zero of ∨” ⟩
    true ≡ q ∨ ¬ p ≡ true ≡ p ∨ r ≡ q ∨ p ∨ r ≡ p ∨ q ∨ r ≡ (¬ p ∨ q) ≡ (p ∨ r)
  =⟨ “Reflexivity of ≡” ⟩Fact “A4.2a”: n = 2 ⇒ (6 - n · (n + 1)) · m = 0
Proof:
    n = 2 ⇒ (6 - n · (n + 1)) · m = 0
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ ((6 - z · (z + 1)) · m = 0)[z ≔ n]
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ ((6 - z · (z + 1)) · m = 0)[z ≔ 2]
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ (6 - 2 · (2 + 1)) · m = 0
  =⟨ Fact `2 + 1 = 3` ⟩
    n = 2 ⇒ (6 - 2 · 3) · m = 0
  =⟨ Fact `2 · 3 = 6` ⟩
    n = 2 ⇒ (6 - 6) · m = 0
  =⟨ Fact `6 - 6 = 0` ⟩
    n = 2 ⇒ 0 · m = 0
  =⟨ “Zero of ·” ⟩
    n = 2 ⇒ 0 = 0
  =⟨ “Reflexivity of =” ⟩
    n = 2 ⇒ true
  =⟨ “Right-zero of ⇒” ⟩
    true
    true ≡ true ≡ true
  =⟨ “Reflexivity of ≡” ⟩
    true

Fact “A4.2a”: n = 2 ⇒ (6 - n · (n + 1)) · m = 0
Proof:
    n = 2 ⇒ (6 - n · (n + 1)) · m = 0
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ ((6 - z · (z + 1)) · m = 0)[z ≔ n]
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ ((6 - z · (z + 1)) · m = 0)[z ≔ 2]
  =⟨ Substitution, “Replacement” ⟩
    n = 2 ⇒ (6 - 2 · (2 + 1)) · m = 0
  =⟨ Fact `2 + 1 = 3` ⟩
    n = 2 ⇒ (6 - 2 · 3) · m = 0
  =⟨ Fact `2 · 3 = 6` ⟩
    n = 2 ⇒ (6 - 6) · m = 0
  =⟨ Fact `6 - 6 = 0` ⟩
    n = 2 ⇒ 0 · m = 0
  =⟨ “Zero of ·” ⟩
    n = 2 ⇒ 0 = 0
  =⟨ “Reflexivity of =” ⟩
    n = 2 ⇒ true
  =⟨ “Right-zero of ⇒” ⟩
    true

Fact “A4.2b”:
      k = 2 ∧ m = 3 ∧ n = k · k + m
    ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1)
Proof:
    k = 2 ∧ m = 3 ∧ n = k · k + m ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ “Shunting” ⟩
    k = 2 ∧ m = 3 ⇒ n = k · k + m ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ m = 3 ⇒ (n = k · k + z ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))[z ≔ m]
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ m = 3 ⇒ (n = k · k + z ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))[z ≔ m]
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ m = 3 ⇒ (n = k · k + 3 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))
  =⟨ “Symmetry of ∧” ⟩
    m = 3 ∧ k = 2 ⇒ (n = k · k + 3 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ⇒ (n = z · z + 3 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))[z ≔ k]
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ⇒ (n = z · z + 3 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))[z ≔ 2]
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ⇒ (n = 2 · 2 + 3 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1))
  =⟨ Fact `2 · 2 + 3 = 7` ⟩
    m = 3 ∧ k = 2 ⇒ n = 7 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ “Shunting” ⟩
    m = 3 ∧ k = 2 ∧ n = 7 ⇒ (j · n · n + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ∧ n = 7 ⇒ (j · z · z + 1 = (13 - m) · (k + m)  ⇒  j = 1)[z ≔ n]
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ∧ n = 7 ⇒ (j · z · z + 1 = (13 - m) · (k + m)  ⇒  j = 1)[z ≔ 7]
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ k = 2 ∧ n = 7 ⇒ (j · (7 · 7) + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ Fact `7 · 7 = 49` ⟩
    m = 3 ∧ n = 7 ∧ k = 2 ⇒ (j · 49 + 1 = (13 - m) · (k + m)  ⇒  j = 1)
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ n = 7 ∧ k = 2 ⇒ (j · 49 + 1 = (13 - m) · (z + m)  ⇒  j = 1)[z ≔ k]
  =⟨ Substitution, “Replacement” ⟩
    m = 3 ∧ n = 7 ∧ k = 2 ⇒ (j · 49 + 1 = (13 - m) · (z + m)  ⇒  j = 1)[z ≔ 2]
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = (13 - m) · (2 + m)  ⇒  j = 1)
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = (13 - z) · (2 + z)  ⇒  j = 1)[z ≔ m]
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = (13 - z) · (2 + z)  ⇒  j = 1)[z ≔ 3]
  =⟨ Substitution, “Replacement” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = (13 - 3) · (2 + 3)  ⇒  j = 1)
  =⟨ Fact `13 - 3 = 10` ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = 10 · (2 + 3)  ⇒  j = 1)
  =⟨ Fact `2 + 3 = 5` ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = 10 · 5  ⇒  j = 1)
  =⟨ Fact `10 · 5 = 50` ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = 50  ⇒  j = 1)
  =⟨ Fact `49 + 1 = 50` ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 + 1 = 49 + 1  ⇒  j = 1)
  =⟨ “Cancellation of +” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 = 49  ⇒  j = 1)
  =⟨ “Identity of ·” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j · 49 = 1 · 49  ⇒  j = 1)
  =⟨ “Cancellation of ·” with Fact `49 ≠ 0` ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ (j = 1  ⇒  j = 1)
  =⟨ “Reflexivity of ⇒” ⟩
    k = 2 ∧ n = 7 ∧ m = 3 ⇒ true
  =⟨ “Right-zero of ⇒” ⟩
    true

Theorem “Predecessor of non-zero”: n ≠ 0 ⇒ suc (pred n) = n
Proof:
  By induction on `n : ℕ`:
    Base case:
        0 ≠ 0 ⇒ suc (pred 0) = 0
      =⟨ “Definition of ≠” ⟩
        ¬ (0 = 0) ⇒ suc (pred 0) = 0
      =⟨ “Reflexivity of =” ⟩
        ¬ true ⇒ suc (pred 0) = 0
      =⟨ “Definition of `false`” ⟩
        false ⇒ suc (pred 0) = 0
      =⟨ “ex falso quodlibet” ⟩
        true
    Induction step:
        suc n ≠ 0 ⇒ suc (pred (suc (n))) = suc n
      =⟨ “Predecessor of successor” ⟩
        suc n ≠ 0 ⇒ suc (n) = suc n
      =⟨ “Reflexivity of =” ⟩
        suc n ≠ 0 ⇒ true
      =⟨ “Right-zero of ⇒” ⟩
        true

Theorem “Isotonicity of +”: a + b ≤ a + c  ≡  b ≤ c
Proof:
  By induction on `a : ℕ`:
    Base case:
        0 + b ≤ 0 + c  ≡  b ≤ c
      =⟨ “Identity of +” ⟩
        b ≤ c  ≡  b ≤ c
      =⟨ “Reflexivity of ≡” ⟩ 
        true
    Induction step:
        suc a + b ≤ suc a + c  ≡  b ≤ c
      =⟨ “Definition of + for `suc`” ⟩
        suc (a + b) ≤ suc (a + c)  ≡  b ≤ c
      =⟨ “Isotonicity of successor” ⟩
        a + b ≤ a + c  ≡  b ≤ c
      =⟨ Induction hypothesis ⟩
        b ≤ c  ≡  b ≤ c
      =⟨ “Reflexivity of ≡” ⟩
        true

Theorem “Monotonicity of +”: a ≤ b ⇒ c ≤ d ⇒ a + c ≤ b + d
Proof:
    a ≤ b ⇒ c ≤ d ⇒ a + c ≤ b + d
  =⟨ “Isotonicity of +” ⟩ 
    a + c ≤ b + c ⇒ b + c ≤ b + d ⇒ a + c ≤ b + d
  =⟨ “Transitivity of ≤” ⟩ 
    true

Theorem “Monotonicity of predecessor”:
    a ≤ b ⇒ pred a ≤ pred b
Proof: 
  By induction on `a : ℕ`:
    Base case:
        0 ≤ b ⇒ pred 0 ≤ pred b
      =⟨ “Predecessor of zero” ⟩ 
        0 ≤ b ⇒ 0 ≤ pred b
      =⟨ “Zero is least element” ⟩ 
        true ⇒ true
      =⟨ “Reflexivity of ⇒” ⟩ 
        true
    Induction step `suc a ≤ b ⇒ pred (suc(a)) ≤ pred b`:
      By induction on `b : ℕ`:
        Base case `suc a ≤ 0 ⇒ pred (suc(a)) ≤ pred 0`:
            suc a ≤ 0 ⇒ pred (suc(a)) ≤ pred 0
          =⟨ “Predecessor of successor” ⟩
            suc a ≤ 0 ⇒ a ≤ pred 0
          =⟨ “Predecessor of zero” ⟩
            suc a ≤ 0 ⇒ a ≤ 0
          =⟨ “Successor is not at most zero” ⟩
            false ⇒ a ≤ 0
          =⟨ “ex falso quodlibet” ⟩
            true
        Induction step `suc a ≤ suc b ⇒ pred (suc(a)) ≤ pred (suc (b))`:
            suc a ≤ suc b ⇒ pred (suc(a)) ≤ pred (suc (b))
          ≡⟨ “Isotonicity of successor” ⟩
            a ≤ b ⇒ pred (suc(a)) ≤ pred (suc (b))
          ≡⟨ “Predecessor of successor” ⟩
            a ≤ b ⇒ a ≤ b
          ≡⟨ “Reflexivity of ⇒” ⟩
            true

Theorem “Successor is non-decreasing”: a ≤ suc a
Proof:
  By induction on `a : ℕ`:
    Base case:
        0 ≤ suc 0
      =⟨ “Zero is least element” ⟩
        true
    Induction step:
        suc a ≤ suc suc a
      =⟨ “Isotonicity of successor” ⟩
        a ≤ suc a
      =⟨ Induction hypothesis ⟩
        true

Theorem “Subtraction is non-increasing”: a - b ≤ a
Proof:
  By induction on `a : ℕ`:
    Base case:
        0 - b ≤ 0
      =⟨ “Subtraction from zero” ⟩
        0 ≤ 0
      =⟨ “Reflexivity of ≤” ⟩
        true
    Induction step `suc a - b ≤ suc a`:
      By induction on `b : ℕ`:
        Base case `suc a - 0 ≤ suc a`:
              suc a - 0 ≤ suc a
            =⟨ “Right-identity of subtraction” ⟩
              suc a ≤ suc a
            =⟨ “Reflexivity of ≤” ⟩
              true
        Induction step `suc a - suc b ≤ suc a`:
              suc a - suc b ≤ suc a
            =⟨ “Subtraction of successor from successor” ⟩
              a - b ≤ suc a
            =⟨ “Left-identity of ⇒” ⟩
              true ⇒ a - b ≤ suc a
            =⟨ “Left-identity of ⇒” ⟩
              true ⇒ true ⇒ a - b ≤ suc a
            =⟨ “Successor is non-decreasing” ⟩
              true ⇒ a ≤ suc a ⇒ a - b ≤ suc a
            =⟨ Induction hypothesis `a - b ≤ a` ⟩
              a - b ≤ a ⇒ a ≤ suc a ⇒ a - b ≤ suc a
            =⟨ “Transitivity of ≤” ⟩
              true