Exercise 3.3

Theorem “Irreflexivity of <”: a < a  ≡  false
Proof:
  By induction on `a : ℕ`:
    Base case:
        0 < 0
      =⟨ “Nothing is less than zero” ⟩
        false
    Induction step:
        suc a < suc a
      =⟨ “<-Isotonicity of successor” ⟩
        a < a
      =⟨ Induction hypothesis ⟩
        false

Theorem “Zero is <-least element”: 0 < a ∨ 0 = a
Proof:
  By induction on `a : ℕ`:
    Base case:
        0 < 0 ∨ 0 = 0
      =⟨ “Reflexivity of =” ⟩
        0 < 0 ∨ true
      =⟨ “Zero of ∨” ⟩
        true
    Induction step:
        0 < suc a ∨ 0 = suc a
      =⟨ “Zero is not successor” ⟩
        0 < suc a ∨ false
      =⟨ “Identity of ∨” ⟩
        0 < suc a
      =⟨ “Zero is less than successor” ⟩
        true

Theorem “Less than successor”: a < suc b  ≡  a < b ∨ a = b
Proof:
    By induction on `a : ℕ`:
      Base case:
          0 < suc b ≡ 0 < b ∨ 0 = b
        =⟨ “Zero is less than successor” ⟩
          true ≡ 0 < b ∨ 0 = b
        =⟨ “Zero is <-least element” ⟩
          true ≡ true
        =⟨ “Reflexivity of ≡” ⟩
          true
      Induction step `suc a < suc b ≡ suc a < b ∨ suc a = b`:
        By induction on `b : ℕ`:
          Base case:
              suc a < suc 0 ≡ suc a < 0 ∨ suc a = 0
            =⟨ “Zero is not successor” ⟩
              suc a < suc 0 ≡ suc a < 0 ∨ false
            =⟨ “Nothing is less than zero” ⟩
              suc a < suc 0 ≡ false ∨ false
            =⟨ “Idempotency of ∨” ⟩
              suc a < suc 0 ≡ false
            =⟨ “<-Isotonicity of successor” ⟩
              a < 0 ≡ false
            =⟨ “Nothing is less than zero” ⟩
              false ≡ false
            =⟨ “Reflexivity of ≡” ⟩
              true
          Induction step `suc a < suc (suc b) ≡ suc a < suc b ∨ suc a = suc b`:
              suc a < suc (suc b) ≡ suc a < suc b ∨ suc a = suc b
            =⟨ “<-Isotonicity of successor” ⟩
              a < suc b ≡ a < b ∨ suc a = suc b
            =⟨ “Cancellation of `suc`” ⟩
              a < suc b ≡ a < b ∨ a = b
            =⟨ Induction hypothesis `a < suc b  ≡  a < b ∨ a = b` ⟩
              true

Theorem “Less than successor”: a < suc a
Proof:
    a < suc a
  =⟨ “Less than successor” ⟩
    a < a ∨ a = a
  =⟨ “Reflexivity of =” ⟩
    a < a ∨ true
  =⟨ “Zero of ∨” ⟩
    true

Theorem “Only zero is less than one”: a < 1  ≡  a = 0
Proof:
    a < 1
  =⟨ “Left-identity of +” ⟩
    a < 0 + 1
  =⟨ “Successor” ⟩
    a < suc 0
  =⟨ “Less than successor” ⟩
    a < 0 ∨ a = 0
  =⟨ “Nothing is less than zero” ⟩
    false ∨ a = 0
  =⟨ “Identity of ∨” ⟩
    a = 0

Theorem “Transitivity of <”: a < b ⇒ b < c ⇒ a < c
Proof:
  By induction on `b : ℕ`:
    Base case:
        a < 0 ⇒ 0 < c ⇒ a < c
      =⟨ “Nothing is less than zero” ⟩
        false ⇒ 0 < c ⇒ a < c
      =⟨ “ex falso quodlibet” ⟩
        true
    Induction step `a < suc b ⇒ suc b < c ⇒ a < c`:
      By induction on `c : ℕ`:
        Base case:
            a < suc b ⇒ suc b < 0 ⇒ a < 0
          =⟨ “Nothing is less than zero” ⟩
            a < suc b ⇒ false ⇒ a < 0
          =⟨ “ex falso quodlibet” ⟩
            a < suc b ⇒ true
          =⟨ “Right-zero of ⇒” ⟩
            true
        Induction step `a < suc b ⇒ suc b < suc c ⇒ a < suc c`:
          By induction on `a : ℕ`:
            Base case:
                0 < suc b ⇒ suc b < suc c ⇒ 0 < suc c
              =⟨ “Zero is less than successor” ⟩
                0 < suc b ⇒ suc b < suc c ⇒ true
              =⟨ “Right-zero of ⇒” ⟩
                true
            Induction step `suc a < suc b ⇒ suc b < suc c ⇒ suc a < suc c`:
                suc a < suc b ⇒ suc b < suc c ⇒ suc a < suc c
              =⟨ “<-Isotonicity of successor” ⟩
                a < b ⇒ b < c ⇒ a < c
              =⟨ Induction hypothesis `a < b ⇒ b < c ⇒ a < c` ⟩
                true

Calculation:
    ∃ i : ℕ ❙ 4 ≤ i < 9 • i · (i + 1) = 12
  ≡⟨ Quantification expansion, Substitution, Evaluation ⟩
    (i · (i + 1) = 12)[i ≔ 4]
    ∨ (i · (i + 1) = 12)[i ≔ 5]
    ∨ (i · (i + 1) = 12)[i ≔ 6]
    ∨ (i · (i + 1) = 12)[i ≔ 7]
    ∨ (i · (i + 1) = 12)[i ≔ 8]
  ≡⟨ Quantification expansion, Substitution, Evaluation ⟩
    (false)
    ∨ (false)
    ∨ (false)
    ∨ (false)
    ∨ (false)
  ≡⟨ “Idempotency of ∨” ⟩
    (false)
    ∨ (false)
    ∨ (false)
  ≡⟨ “Idempotency of ∨” ⟩
    (false) ∨ (false)
  ≡⟨ “Idempotency of ∨” ⟩
    false

Calculation:
    ∀ i : ℕ ❙ 3 ≤ i < 9
            • (i - 5) · (8 - i) < 2 ∨ j = i
  ≡⟨ Quantification expansion, Substitution, Evaluation ⟩
    ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 3]
    ∧ ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 4]
    ∧ ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 5]
    ∧ ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 6]
    ∧ ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 7]
    ∧ ((i - 5) · (8 - i) < 2 ∨ j = i)[i ≔ 8]
  ≡⟨ Quantification expansion, Substitution, Evaluation ⟩
    (0 < 2 ∨ j = 3)
    ∧ (0 < 2 ∨ j = 4)
    ∧ (0 < 2 ∨ j = 5)
    ∧ (2 < 2 ∨ j = 6)
    ∧ (2 < 2 ∨ j = 7)
    ∧ (0 < 2 ∨ j = 8)
  ≡⟨ “Irreflexivity of <” ⟩
    (0 < 2 ∨ j = 3)
    ∧ (0 < 2 ∨ j = 4)
    ∧ (0 < 2 ∨ j = 5)
    ∧ (false ∨ j = 6)
    ∧ (false ∨ j = 7)
    ∧ (0 < 2 ∨ j = 8)
  ≡⟨ Fact `0 < 2` ⟩
    (true ∨ j = 3)
    ∧ (true ∨ j = 4)
    ∧ (true ∨ j = 5)
    ∧ (false ∨ j = 6)
    ∧ (false ∨ j = 7)
    ∧ (true ∨ j = 8)
  ≡⟨ “Zero of ∨” ⟩
    (true)
    ∧ (true)
    ∧ (true)
    ∧ (false ∨ j = 6)
    ∧ (false ∨ j = 7)
    ∧ (true)
  ≡⟨ “Identity of ∨” ⟩
    (true) ∧ ((true) ∧ ((true) ∧ ((j = 6) ∧ ((j = 7) ∧ (true)))))
  ≡⟨ “Identity of ∧” ⟩
    (j = 6) ∧ (j = 7)