michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(builtin/Nat): use obtain-from instead of ExistsElim, and use more user-friendly argument order for Induction

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-03 10:33:57 -08:00
parent 9f3706e365
commit 5b5cebe750
3 changed files with 139 additions and 145 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

110
src/builtin/Nat.lean
View file

@ -37,22 +37,20 @@ Axiom PlusSucc (a b : Nat) : a + (b + 1) = (a + b) + 1.
Axiom MulZero (a : Nat) : a * 0 = 0. Axiom MulZero (a : Nat) : a * 0 = 0.
Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a. Axiom MulSucc (a b : Nat) : a * (b + 1) = a * b + a.
Axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b. Axiom LeDef (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b.
Axiom Induction {P : Nat → Bool} (Hb : P 0) (iH : Π (n : Nat) (H : P n), P (n + 1)) (a : Nat) : P a. Axiom Induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : Π (n : Nat) (iH : P n), P (n + 1)) : P a.
Theorem ZeroNeOne : 0 ≠ 1 := Trivial. Theorem ZeroNeOne : 0 ≠ 1 := Trivial.
Theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a Theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a
:= Induction (show 0 ≠ 0 ⇒ ∃ b, b + 1 = 0, := Induction a
assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) (assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H)
(λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n),
assume H : n + 1 ≠ 0, assume H : n + 1 ≠ 0,
DisjCases (EM (n = 0)) DisjCases (EM (n = 0))
(λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 }))
(λ Hne0 : n ≠ 0, (λ Hne0 : n ≠ 0,
ExistsElim (MP iH Hne0) obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0),
(λ (w : Nat) (Hw : w + 1 = n), ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))).
ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))))
a.
Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a
:= MP (NeZeroPred' a) H. := MP (NeZeroPred' a) H.
@ -60,54 +58,55 @@ Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a
Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B
:= DisjCases (EM (a = 0)) := DisjCases (EM (a = 0))
(λ Heq0 : a = 0, H1 Heq0) (λ Heq0 : a = 0, H1 Heq0)
(λ Hne0 : a ≠ 0, ExistsElim (NeZeroPred Hne0) (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0),
(λ (w : Nat) (Hw : w + 1 = a), H2 w (Symm Hw))). H2 w (Symm Hw)).
Theorem ZeroPlus (a : Nat) : 0 + a = a Theorem ZeroPlus (a : Nat) : 0 + a = a
:= Induction (show 0 + 0 = 0, Trivial) := Induction a
(show 0 + 0 = 0, Trivial)
(λ (n : Nat) (iH : 0 + n = n), (λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n calc 0 + (n + 1) = (0 + n) + 1 : PlusSucc 0 n
... = n + 1 : { iH }) ... = n + 1 : { iH }).
a.
Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1 Theorem SuccPlus (a b : Nat) : (a + 1) + b = (a + b) + 1
:= Induction (calc (a + 1) + 0 = a + 1 : PlusZero (a + 1) := Induction b
(calc (a + 1) + 0 = a + 1 : PlusZero (a + 1)
... = (a + 0) + 1 : { Symm (PlusZero a) }) ... = (a + 0) + 1 : { Symm (PlusZero a) })
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : PlusSucc (a + 1) n
... = ((a + n) + 1) + 1 : { iH } ... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }) ... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), Symm (PlusSucc a n) }).
b.
Theorem PlusComm (a b : Nat) : a + b = b + a Theorem PlusComm (a b : Nat) : a + b = b + a
:= Induction (calc a + 0 = a : PlusZero a := Induction b
(calc a + 0 = a : PlusZero a
... = 0 + a : Symm (ZeroPlus a)) ... = 0 + a : Symm (ZeroPlus a))
(λ (n : Nat) (iH : a + n = n + a), (λ (n : Nat) (iH : a + n = n + a),
calc a + (n + 1) = (a + n) + 1 : PlusSucc a n calc a + (n + 1) = (a + n) + 1 : PlusSucc a n
... = (n + a) + 1 : { iH } ... = (n + a) + 1 : { iH }
... = (n + 1) + a : Symm (SuccPlus n a)) ... = (n + 1) + a : Symm (SuccPlus n a)).
b.
Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c Theorem PlusAssoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= Induction (calc 0 + (b + c) = b + c : ZeroPlus (b + c) := Induction a
(calc 0 + (b + c) = b + c : ZeroPlus (b + c)
... = (0 + b) + c : { Symm (ZeroPlus b) }) ... = (0 + b) + c : { Symm (ZeroPlus b) })
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c), (λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c) calc (n + 1) + (b + c) = (n + (b + c)) + 1 : SuccPlus n (b + c)
... = ((n + b) + c) + 1 : { iH } ... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c) ... = ((n + b) + 1) + c : Symm (SuccPlus (n + b) c)
... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }) ... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, Symm (SuccPlus n b) }).
a.
Theorem ZeroMul (a : Nat) : 0 * a = 0 Theorem ZeroMul (a : Nat) : 0 * a = 0
:= Induction (show 0 * 0 = 0, Trivial) := Induction a
(show 0 * 0 = 0, Trivial)
(λ (n : Nat) (iH : 0 * n = 0), (λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n calc 0 * (n + 1) = (0 * n) + 0 : MulSucc 0 n
... = 0 + 0 : { iH } ... = 0 + 0 : { iH }
... = 0 : Trivial) ... = 0 : Trivial).
a.
Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
:= Induction (calc (a + 1) * 0 = 0 : MulZero (a + 1) := Induction b
(calc (a + 1) * 0 = 0 : MulZero (a + 1)
... = a * 0 : Symm (MulZero a) ... = a * 0 : Symm (MulZero a)
... = a * 0 + 0 : Symm (PlusZero (a * 0))) ... = a * 0 + 0 : Symm (PlusZero (a * 0)))
(λ (n : Nat) (iH : (a + 1) * n = a * n + n), (λ (n : Nat) (iH : (a + 1) * n = a * n + n),
@ -118,35 +117,34 @@ Theorem SuccMul (a b : Nat) : (a + 1) * b = a * b + b
... = a * n + (a + n) + 1 : { PlusComm n a } ... = a * n + (a + n) + 1 : { PlusComm n a }
... = a * n + a + n + 1 : { PlusAssoc (a * n) a n } ... = a * n + a + n + 1 : { PlusAssoc (a * n) a n }
... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) } ... = a * (n + 1) + n + 1 : { Symm (MulSucc a n) }
... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)) ... = a * (n + 1) + (n + 1) : Symm (PlusAssoc (a * (n + 1)) n 1)).
b.
Theorem OneMul (a : Nat) : 1 * a = a Theorem OneMul (a : Nat) : 1 * a = a
:= Induction (show 1 * 0 = 0, Trivial) := Induction a
(show 1 * 0 = 0, Trivial)
(λ (n : Nat) (iH : 1 * n = n), (λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n calc 1 * (n + 1) = 1 * n + 1 : MulSucc 1 n
... = n + 1 : { iH }) ... = n + 1 : { iH }).
a.
Theorem MulOne (a : Nat) : a * 1 = a Theorem MulOne (a : Nat) : a * 1 = a
:= Induction (show 0 * 1 = 0, Trivial) := Induction a
(show 0 * 1 = 0, Trivial)
(λ (n : Nat) (iH : n * 1 = n), (λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1 calc (n + 1) * 1 = n * 1 + 1 : SuccMul n 1
... = n + 1 : { iH }) ... = n + 1 : { iH }).
a.
Theorem MulComm (a b : Nat) : a * b = b * a Theorem MulComm (a b : Nat) : a * b = b * a
:= Induction (calc a * 0 = 0 : MulZero a := Induction b
(calc a * 0 = 0 : MulZero a
... = 0 * a : Symm (ZeroMul a)) ... = 0 * a : Symm (ZeroMul a))
(λ (n : Nat) (iH : a * n = n * a), (λ (n : Nat) (iH : a * n = n * a),
calc a * (n + 1) = a * n + a : MulSucc a n calc a * (n + 1) = a * n + a : MulSucc a n
... = n * a + a : { iH } ... = n * a + a : { iH }
... = (n + 1) * a : Symm (SuccMul n a)) ... = (n + 1) * a : Symm (SuccMul n a)).
b.
Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c
:= Induction (calc 0 * (b + c) = 0 : ZeroMul (b + c) := Induction a
(calc 0 * (b + c) = 0 : ZeroMul (b + c)
... = 0 + 0 : Trivial ... = 0 + 0 : Trivial
... = 0 * b + 0 : { Symm (ZeroMul b) } ... = 0 * b + 0 : { Symm (ZeroMul b) }
... = 0 * b + 0 * c : { Symm (ZeroMul c) }) ... = 0 * b + 0 * c : { Symm (ZeroMul c) })
@ -159,8 +157,7 @@ Theorem Distribute (a b c : Nat) : a * (b + c) = a * b + a * c
... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) } ... = n * b + b + n * c + c : { PlusAssoc (n * b) b (n * c) }
... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) } ... = (n + 1) * b + n * c + c : { Symm (SuccMul n b) }
... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c) ... = (n + 1) * b + (n * c + c) : Symm (PlusAssoc ((n + 1) * b) (n * c) c)
... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }) ... = (n + 1) * b + (n + 1) * c : { Symm (SuccMul n c) }).
a.
Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
:= calc (a + b) * c = c * (a + b) : MulComm (a + b) c := calc (a + b) * c = c * (a + b) : MulComm (a + b) c
@ -169,18 +166,19 @@ Theorem Distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c
... = a * c + b * c : { MulComm c b }. ... = a * c + b * c : { MulComm c b }.
Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c
:= Induction (calc 0 * (b * c) = 0 : ZeroMul (b * c) := Induction a
(calc 0 * (b * c) = 0 : ZeroMul (b * c)
... = 0 * c : Symm (ZeroMul c) ... = 0 * c : Symm (ZeroMul c)
... = (0 * b) * c : { Symm (ZeroMul b) }) ... = (0 * b) * c : { Symm (ZeroMul b) })
(λ (n : Nat) (iH : n * (b * c) = n * b * c), (λ (n : Nat) (iH : n * (b * c) = n * b * c),
calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c) calc (n + 1) * (b * c) = n * (b * c) + (b * c) : SuccMul n (b * c)
... = n * b * c + (b * c) : { iH } ... = n * b * c + (b * c) : { iH }
... = (n * b + b) * c : Symm (Distribute2 (n * b) b c) ... = (n * b + b) * c : Symm (Distribute2 (n * b) b c)
... = (n + 1) * b * c : { Symm (SuccMul n b) }) ... = (n + 1) * b * c : { Symm (SuccMul n b) }).
a.
Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c
:= Induction (assume H : 0 + b = 0 + c, := Induction a
(assume H : 0 + b = 0 + c,
calc b = 0 + b : Symm (ZeroPlus b) calc b = 0 + b : Symm (ZeroPlus b)
... = 0 + c : H ... = 0 + c : H
... = c : ZeroPlus c) ... = c : ZeroPlus c)
@ -195,8 +193,7 @@ Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c
... = n + (c + 1) : { PlusComm 1 c } ... = n + (c + 1) : { PlusComm 1 c }
... = n + c + 1 : PlusAssoc n c 1), ... = n + c + 1 : PlusAssoc n c 1),
L2 : n + b = n + c := SuccInj L1 L2 : n + b = n + c := SuccInj L1
in MP iH L2) in MP iH L2).
a.
Theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c Theorem PlusInj {a b c : Nat} (H : a + b = a + c) : b = c
:= MP (PlusInj' a b c) H. := MP (PlusInj' a b c) H.
@ -222,27 +219,22 @@ Theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a).
Theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a). Theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a).
Theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c Theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
:= ExistsElim (LeElim H1) := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1),
(λ (w1 : Nat) (Hw1 : a + w1 = b), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2),
ExistsElim (LeElim H2)
(λ (w2 : Nat) (Hw2 : b + w2 = c),
LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2
... = b + w2 : { Hw1 } ... = b + w2 : { Hw1 }
... = c : Hw2))). ... = c : Hw2).
Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c
:= ExistsElim (LeElim H) := obtain (w : Nat) (Hw : a + w = b), from (LeElim H),
(λ (w : Nat) (Hw : a + w = b),
LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w)
... = a + (w + c) : { PlusComm c w } ... = a + (w + c) : { PlusComm c w }
... = a + w + c : PlusAssoc a w c ... = a + w + c : PlusAssoc a w c
... = b + c : { Hw })). ... = b + c : { Hw }).
Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
:= ExistsElim (LeElim H1) := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1),
(λ (w1 : Nat) (Hw1 : a + w1 = b), obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2),
ExistsElim (LeElim H2)
(λ (w2 : Nat) (Hw2 : b + w2 = a),
let L1 : w1 + w2 = 0 let L1 : w1 + w2 = 0
:= PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 }
... = b + w2 : { Hw1 } ... = b + w2 : { Hw1 }
@ -251,7 +243,7 @@ Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b
L2 : w1 = 0 := PlusEq0 L1 L2 : w1 = 0 := PlusEq0 L1
in calc a = a + 0 : Symm (PlusZero a) in calc a = a + 0 : Symm (PlusZero a)
... = a + w1 : { Symm L2 } ... = a + w1 : { Symm L2 }
... = b : Hw1)). ... = b : Hw1.
SetOpaque ge true. SetOpaque ge true.
SetOpaque lt true. SetOpaque lt true.

2
src/builtin/kernel.lean
View file

@ -106,6 +106,8 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b
:= Subst H2 H1. := Subst H2 H1.
(* assume is a 'macro' that expands into a Discharge *)
Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
:= assume Ha, MP H2 (MP H1 Ha). := assume Ha, MP H2 (MP H1 Ha).

BIN
src/builtin/obj/Nat.olean
View file

Binary file not shown.