Logic & proof c17.4 and start of c17.5

c17_exercises.lean

open nat

def plus' : ℕ → ℕ  → ℕ
| m 0 := m
| m (succ n) := succ (plus' m n)

def plus'' : ℕ → ℕ  → ℕ
| m 0 := m
| m (succ n) := plus'' (succ m) n

theorem plus_succ'  (n m : ℕ)  : plus'  m (succ n) = succ (plus' m n) := rfl
theorem plus_succ'' (n m : ℕ)  : plus'' m (succ n) = plus'' (succ m) n := rfl

theorem add_succ' (n m : ℕ) : m + (n + 1) = (m + n) + 1 := rfl
theorem add_zero' (m : ℕ) : m + 0 = m := rfl
theorem zero_add' (m : ℕ) : 0 + m = m
:= nat.rec_on m
   (show 0 + 0 = 0, from rfl)
   (λ m, λ ih,
    show 0 + (m + 1) = (m + 1),
    by calc 0 + (m + 1)
          = (0 + m) + 1 : rfl
      ... = m + 1       : by rw ih
   )

theorem mul_zero' (m : ℕ) : m * 0 = 0 := rfl
theorem mul_succ' (n m : ℕ) : n * (m + 1) = (n * m) + n := rfl
theorem mul_one' (n : ℕ) : n * 1 = n :=
nat.rec_on n
 (show 0 * 1 = 0, from mul_zero 1)
 (λ n, λ ih,
  show (n + 1) * 1 = (n + 1),
   from calc (n + 1) * 1
           = (n + 1) * 0 + (n + 1) : by rw mul_succ'
       ... = (n + 1)               : by rw [mul_zero', zero_add']
 )

theorem succ_add' (m n : ℕ) : (m + 1) + n = (m + n) + 1
:= nat.rec_on n
  (show (succ m) + 0 = succ(m + 0),
   from rfl)
  (λ n, λ ih, 
   show (m + 1) + (n + 1) = m + n + 1 + 1,
   by calc (m + 1) + (n + 1)
          = m + 1 + n + 1    : rfl
      ... = (m + n + 1) + 1  : by rw ih)

theorem add_assoc' (m n k : nat) : m + n + k = m + (n + k) :=
nat.rec_on k
  (show m + n + 0 = m + (n + 0), by rw [add_zero', add_zero'])
  (assume k,
    assume ih : m + n + k = m + (n + k),
    show (m + n) + (k + 1) = m + (n + (k + 1)),
    from calc (m + n) + (k + 1)
            = (m + n + k) + 1    : by rw add_succ'
        ... = succ (m + (n + k)) : by rw ih 
        ... = m + (n + k + 1)    : by rw add_succ')

theorem add_comm' (m n : nat) : m + n = n + m :=
nat.rec_on n
  (show m + 0 = 0 + m, by rewrite [add_zero', zero_add'])
  (assume n,
    assume ih : m + n = n + m,
    show m + succ n = succ n + m,
    from calc m + succ n
            = succ (m + n) : by rw add_succ'
        ... = succ (n + m) : by rw ih
        ... = succ n + m   : by rw succ_add')

theorem add_swap' (n m k : ℕ) : n + (m + k) = m + (n + k)
:= show n + (m + k) = m + (n + k), 
   from calc n + (m + k)
           = n + m + k   : by rw add_assoc'
       ... = m + n + k   : by rw add_comm' n m
       ... = m + (n + k) : by rw add_assoc'

theorem succ_mul' (n m : ℕ) : (n + 1) * m = (n * m) + m := 
nat.rec_on m
  (show (succ n) * 0 = (n * 0) + 0, by rw [mul_zero',mul_zero',zero_add'])
  (λ m, λ ih,
   have h1 : (n + 1) * (m + 1) = succ (n * m + (m + n)), 
   from calc (n + 1) * (m + 1)
           = (n + 1) * m + (n + 1) : by rw mul_succ'
       ... = succ((n + 1) * m + n) : by rw add_succ'
       ... = succ(n * m + m + n)   : by rw ih
       ... = succ(n * m + (m + n)) : by rw add_assoc'
       ,
   have h2 : (n * (m + 1)) + (succ m) = succ (n * m + (m + n)), 
   from calc (n * (m + 1)) + (succ m)
           = succ(n * (m + 1) + m) : by rw add_succ'
       ... = succ(m + n * (m + 1)) : by rw add_comm'
       ... = succ(m + (n * m + n)) : by rw mul_succ'
       ... = succ(n * m + (m + n)) : by rw add_swap'
       ,
   show (n + 1) * (m + 1) = (n * (m + 1)) + (m + 1),
   from calc (n + 1) * (m + 1)
           = succ (n * m + (m + n))   : by rw h1
       ... = (n * (m + 1)) + (succ m) : by rw eq.symm(h2)
  )

-- c17_4_6
theorem dist' (m n k : ℕ) : m * (n + k) = (m * n) + (m * k)
:= nat.rec_on k
   (show m * (n + 0) = (m * n) + (m * 0),
    by rw [add_zero', mul_zero', add_zero'])
   (λ k, λ ih,
    show m * (n + (k + 1)) = (m * n) + (m * (k + 1)),
    from calc m * (n + (k + 1)) 
            = m * ((n + k) + 1)     : by rw add_succ'
        ... = m * (n + k) + m       : by rw mul_succ'
        ... = m * n + m * k + m     : by rw ih
        ... = m * n + (m * k + m)   : by rw add_assoc' (m * n) (m * k) m
        ... = m * n + (m * (k + 1)) : by rw eq.symm(mul_succ' m k)
   )

-- c16_4_7
theorem zero_mul' (m : ℕ) : 0 * m = 0 :=
nat.rec_on m
 (show 0 * 0 = 0, by rw mul_zero')
 (λ m, λ ih, 
  show 0 * (m + 1) = 0, by rw [mul_succ', add_zero', ih])


-- c17_4_10
theorem mul_comm' (n m : ℕ) : n * m = m * n :=
nat.rec_on m
  (show n * 0  = 0 * n, by rw [mul_zero', zero_mul'])
  (λ m, λ ih,
   show n * (m + 1) = (m + 1) * n,
      from calc n * (m + 1)
              = n * m + n   : by rw mul_succ'
          ... = m * n + n   : by rw ih
          ... = (m + 1) * n : by rw succ_mul')

-- c17_4_8
theorem one_mul' (m : ℕ) : 1 * m = m :=
by rw [mul_comm', mul_one']

-- c17_4_9
theorem mul_assoc' (m n k:ℕ) : (m * n) * k = m * (n * k)
:= nat.rec_on m
  (show (0 * n) * k = 0 * (n * k), 
   from calc
     (0 * n) * k = 0 * (n * k) : by rw [zero_mul', zero_mul', zero_mul'])
  (λ m, λ ih,
    have foo : _, 
    from calc ((m + 1) * n) * k
            = (m * n + n) * k     : by rw succ_mul'
        ... = k * (m * n + n)     : by rw mul_comm'
        ... = k * (m * n) + k * n : by rw dist'
        ... = m * n * k + k * n   : by rw mul_comm'
        ... = m * n * k + n * k   : by rw mul_comm' k n
        ,
    have bar : _,
    from calc (m + 1) * (n * k)
            = m * (n * k) + n * k : by rw succ_mul'
        ... = m * n * k + n * k   : by rw eq.symm ih
        ,

    show ((m + 1) * n) * k = (m + 1) * (n * k),
    from calc ((m + 1) * n) * k
           = m * n * k + n * k   : by rw foo
        ...= (m + 1) * (n * k)   : by rw eq.symm bar                
  )

def LEQ (m n : ℕ) := ∃k, m + k = n
def GEQ (n m : ℕ) := m ≤ n 
def LT  (m n : ℕ) : Prop := m ≤ n ∧ m ≠ n 

local infix ≤ := LEQ
local infix ≥ := GEQ
local infix < := LT

theorem irrflLT (n : nat) : ¬ n < n :=
(λ (nn : n < n),
 have n ≠ n, from and.right nn,
 have n = n, from rfl,
 show false, from ‹n ≠ n› ‹n = n›
)

def reflexive' {A:Type} (R : A → A → Prop) : Prop :=
∀ x, R x x

def leq_rfl (n : ℕ): n ≤ n := exists.intro 0 (add_zero n)

def reflexiveLeq' : reflexive' (≤) := leq_rfl

def reflexiveLeq : reflexive (≤) := leq_rfl

def leq_trans (n m k : ℕ) : n ≤ m → m ≤ k → n ≤ k
:=
(λ nm_leq,
 λ mk_leq,
   exists.elim nm_leq (λ nm nm_leq,
      exists.elim mk_leq (λ mk mk_leq,        
      have h : _,
      from calc n + (nm + mk)
              = n + nm + mk : by rw eq.symm (add_assoc n nm mk)
          ... = m + mk      : by rw nm_leq
          ... = k           : by rw mk_leq
          ,
      exists.intro (nm + mk) h
      )
   )
)

def transitiveLeq : transitive (≤)
:= leq_trans