2014-01-28 09:15:28 +00:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
|
Imported 'tactic'
|
|
|
|
|
|
Using: Nat
|
|
|
|
|
|
Proved: add_assoc
|
|
|
|
|
|
Nat::add_zerol : ∀ a : ℕ, 0 + a = a
|
|
|
|
|
|
Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
|
2014-02-02 02:27:14 +00:00
|
|
|
|
@eq_id : ∀ (A : (Type U)) (a : A), a = a ↔ ⊤
|
2014-01-28 09:15:28 +00:00
|
|
|
|
theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
|
|
|
|
|
|
Nat::induction_on
|
|
|
|
|
|
a
|
|
|
|
|
|
(let have_expr : 0 + (b + c) = 0 + b + c :=
|
|
|
|
|
|
eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c)))
|
|
|
|
|
|
(congr1 c (congr2 Nat::add (Nat::add_zerol b))))
|
|
|
|
|
|
(eq_id (b + c)))
|
|
|
|
|
|
in have_expr)
|
|
|
|
|
|
(λ (n : ℕ) (iH : n + (b + c) = n + b + c),
|
|
|
|
|
|
let have_expr : n + 1 + (b + c) = n + 1 + b + c :=
|
|
|
|
|
|
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
|
|
|
|
|
|
(trans (congr1 c (congr2 Nat::add (Nat::add_succl n b)))
|
|
|
|
|
|
(Nat::add_succl (n + b) c)))
|
|
|
|
|
|
(eq_id (n + b + c + 1)))
|
|
|
|
|
|
in have_expr)
|
