From 62bb2ab2f9b18c85ce2e49dede2e9e3ea0a9a5ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 5 Jan 2014 23:02:09 -0800 Subject: [PATCH] fix(builtin/Nat): name convention Signed-off-by: Leonardo de Moura --- doc/lean/calc.md | 6 +- examples/lean/even.lean | 2 +- src/builtin/Nat.lean | 124 +++++++++++++++++++------------------- src/builtin/obj/Nat.olean | Bin 15943 -> 15933 bytes 4 files changed, 66 insertions(+), 66 deletions(-) diff --git a/doc/lean/calc.md b/doc/lean/calc.md index c502c91339..a73240c637 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -35,7 +35,7 @@ Here is an example := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::plus::comm d 1 + ... = 1 + d : Nat::add::comm d 1 ... = e : symm Ax4. ``` @@ -45,7 +45,7 @@ proof expression using the given tactic or solver. Even when tactics and solvers are not used, we can still use the elaboration engine to fill gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the -`Nat::plus::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us. +`Nat::add::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us. Here is the same example using placeholders. ```lean @@ -53,7 +53,7 @@ Here is the same example using placeholders. := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::plus::comm _ _ + ... = 1 + d : Nat::add::comm _ _ ... = e : symm Ax4. ``` diff --git a/examples/lean/even.lean b/examples/lean/even.lean index a3c7511d83..3f6c6208dc 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -54,7 +54,7 @@ theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) := obtain (w : Nat) (Hw : a = 2*w + 1), from H, exists::intro (w + 1) (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : symm (plus::assoc _ _ _) + ... = 2*w + (1 + 1) : symm (add::assoc _ _ _) ... = 2*w + 2*1 : refl _ ... = 2*(w + 1) : symm (distribute _ _ _)) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 872b4ecf43..b3ed7affbb 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -32,8 +32,8 @@ notation 55 | _ | : id axiom succ::nz (a : Nat) : a + 1 ≠ 0 axiom succ::inj {a b : Nat} (H : a + 1 = b + 1) : a = b -axiom plus::zeror (a : Nat) : a + 0 = a -axiom plus::succr (a b : Nat) : a + (b + 1) = (a + b) + 1 +axiom add::zeror (a : Nat) : a + 0 = a +axiom add::succr (a b : Nat) : a + (b + 1) = (a + b) + 1 axiom mul::zeror (a : Nat) : a * 0 = 0 axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a axiom le::def (a b : Nat) : a ≤ b ⇔ ∃ c, a + c = b @@ -59,40 +59,40 @@ theorem destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0), H2 w (symm Hw)) -theorem plus::zerol (a : Nat) : 0 + a = a +theorem add::zerol (a : Nat) : 0 + a = a := induction a (have 0 + 0 = 0 : trivial) (λ (n : Nat) (iH : 0 + n = n), - calc 0 + (n + 1) = (0 + n) + 1 : plus::succr 0 n + calc 0 + (n + 1) = (0 + n) + 1 : add::succr 0 n ... = n + 1 : { iH }) -theorem plus::succl (a b : Nat) : (a + 1) + b = (a + b) + 1 +theorem add::succl (a b : Nat) : (a + 1) + b = (a + b) + 1 := induction b - (calc (a + 1) + 0 = a + 1 : plus::zeror (a + 1) - ... = (a + 0) + 1 : { symm (plus::zeror a) }) + (calc (a + 1) + 0 = a + 1 : add::zeror (a + 1) + ... = (a + 0) + 1 : { symm (add::zeror a) }) (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), - calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : plus::succr (a + 1) n + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add::succr (a + 1) n ... = ((a + n) + 1) + 1 : { iH } - ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (plus::succr a n) }) + ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add::succr a n) }) -theorem plus::comm (a b : Nat) : a + b = b + a +theorem add::comm (a b : Nat) : a + b = b + a := induction b - (calc a + 0 = a : plus::zeror a - ... = 0 + a : symm (plus::zerol a)) + (calc a + 0 = a : add::zeror a + ... = 0 + a : symm (add::zerol a)) (λ (n : Nat) (iH : a + n = n + a), - calc a + (n + 1) = (a + n) + 1 : plus::succr a n + calc a + (n + 1) = (a + n) + 1 : add::succr a n ... = (n + a) + 1 : { iH } - ... = (n + 1) + a : symm (plus::succl n a)) + ... = (n + 1) + a : symm (add::succl n a)) -theorem plus::assoc (a b c : Nat) : a + (b + c) = (a + b) + c +theorem add::assoc (a b c : Nat) : a + (b + c) = (a + b) + c := induction a - (calc 0 + (b + c) = b + c : plus::zerol (b + c) - ... = (0 + b) + c : { symm (plus::zerol b) }) + (calc 0 + (b + c) = b + c : add::zerol (b + c) + ... = (0 + b) + c : { symm (add::zerol b) }) (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - calc (n + 1) + (b + c) = (n + (b + c)) + 1 : plus::succl n (b + c) + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add::succl n (b + c) ... = ((n + b) + c) + 1 : { iH } - ... = ((n + b) + 1) + c : symm (plus::succl (n + b) c) - ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (plus::succl n b) }) + ... = ((n + b) + 1) + c : symm (add::succl (n + b) c) + ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add::succl n b) }) theorem mul::zerol (a : Nat) : 0 * a = 0 := induction a @@ -106,16 +106,16 @@ theorem mul::succl (a b : Nat) : (a + 1) * b = a * b + b := induction b (calc (a + 1) * 0 = 0 : mul::zeror (a + 1) ... = a * 0 : symm (mul::zeror a) - ... = a * 0 + 0 : symm (plus::zeror (a * 0))) + ... = a * 0 + 0 : symm (add::zeror (a * 0))) (λ (n : Nat) (iH : (a + 1) * n = a * n + n), calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul::succr (a + 1) n ... = a * n + n + (a + 1) : { iH } - ... = a * n + n + a + 1 : plus::assoc (a * n + n) a 1 - ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (plus::assoc (a * n) n a) } - ... = a * n + (a + n) + 1 : { plus::comm n a } - ... = a * n + a + n + 1 : { plus::assoc (a * n) a n } + ... = a * n + n + a + 1 : add::assoc (a * n + n) a 1 + ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add::assoc (a * n) n a) } + ... = a * n + (a + n) + 1 : { add::comm n a } + ... = a * n + a + n + 1 : { add::assoc (a * n) a n } ... = a * (n + 1) + n + 1 : { symm (mul::succr a n) } - ... = a * (n + 1) + (n + 1) : symm (plus::assoc (a * (n + 1)) n 1)) + ... = a * (n + 1) + (n + 1) : symm (add::assoc (a * (n + 1)) n 1)) theorem mul::lhs::one (a : Nat) : 1 * a = a := induction a @@ -149,12 +149,12 @@ theorem distribute (a b c : Nat) : a * (b + c) = a * b + a * c (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul::succl n (b + c) ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : plus::assoc (n * b + n * c) b c - ... = n * b + (n * c + b) + c : { symm (plus::assoc (n * b) (n * c) b) } - ... = n * b + (b + n * c) + c : { plus::comm (n * c) b } - ... = n * b + b + n * c + c : { plus::assoc (n * b) b (n * c) } + ... = n * b + n * c + b + c : add::assoc (n * b + n * c) b c + ... = n * b + (n * c + b) + c : { symm (add::assoc (n * b) (n * c) b) } + ... = n * b + (b + n * c) + c : { add::comm (n * c) b } + ... = n * b + b + n * c + c : { add::assoc (n * b) b (n * c) } ... = (n + 1) * b + n * c + c : { symm (mul::succl n b) } - ... = (n + 1) * b + (n * c + c) : symm (plus::assoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n * c + c) : symm (add::assoc ((n + 1) * b) (n * c) c) ... = (n + 1) * b + (n + 1) * c : { symm (mul::succl n c) }) theorem distribute2 (a b c : Nat) : (a + b) * c = a * c + b * c @@ -174,36 +174,36 @@ theorem mul::assoc (a b c : Nat) : a * (b * c) = a * b * c ... = (n * b + b) * c : symm (distribute2 (n * b) b c) ... = (n + 1) * b * c : { symm (mul::succl n b) }) -theorem plus::inj' (a b c : Nat) : a + b = a + c ⇒ b = c +theorem add::inj' (a b c : Nat) : a + b = a + c ⇒ b = c := induction a (assume H : 0 + b = 0 + c, - calc b = 0 + b : symm (plus::zerol b) + calc b = 0 + b : symm (add::zerol b) ... = 0 + c : H - ... = c : plus::zerol c) + ... = c : add::zerol c) (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), assume H : n + 1 + b = n + 1 + c, let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : symm (plus::assoc n b 1) - ... = n + (1 + b) : { plus::comm b 1 } - ... = n + 1 + b : plus::assoc n 1 b + := (calc n + b + 1 = n + (b + 1) : symm (add::assoc n b 1) + ... = n + (1 + b) : { add::comm b 1 } + ... = n + 1 + b : add::assoc n 1 b ... = n + 1 + c : H - ... = n + (1 + c) : symm (plus::assoc n 1 c) - ... = n + (c + 1) : { plus::comm 1 c } - ... = n + c + 1 : plus::assoc n c 1), + ... = n + (1 + c) : symm (add::assoc n 1 c) + ... = n + (c + 1) : { add::comm 1 c } + ... = n + c + 1 : add::assoc n c 1), L2 : n + b = n + c := succ::inj L1 in iH ◂ L2) -theorem plus::inj {a b c : Nat} (H : a + b = a + c) : b = c -:= (plus::inj' a b c) ◂ H +theorem add::inj {a b c : Nat} (H : a + b = a + c) : b = c +:= (add::inj' a b c) ◂ H -theorem plus::eqz {a b : Nat} (H : a + b = 0) : a = 0 +theorem add::eqz {a b : Nat} (H : a + b = 0) : a = 0 := destruct (λ H1 : a = 0, H1) (λ (n : Nat) (H1 : a = n + 1), absurd::elim (a = 0) H (calc a + b = n + 1 + b : { H1 } - ... = n + (1 + b) : symm (plus::assoc n 1 b) - ... = n + (b + 1) : { plus::comm 1 b } - ... = n + b + 1 : plus::assoc n b 1 + ... = n + (1 + b) : symm (add::assoc n 1 b) + ... = n + (b + 1) : { add::comm 1 b } + ... = n + b + 1 : add::assoc n b 1 ... ≠ 0 : succ::nz (n + b))) theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b @@ -212,34 +212,34 @@ theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b := (le::def a b) ◂ H -theorem le::refl (a : Nat) : a ≤ a := le::intro (plus::zeror a) +theorem le::refl (a : Nat) : a ≤ a := le::intro (add::zeror a) -theorem le::zero (a : Nat) : 0 ≤ a := le::intro (plus::zerol a) +theorem le::zero (a : Nat) : 0 ≤ a := le::intro (add::zerol a) theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2), - le::intro (calc a + (w1 + w2) = a + w1 + w2 : plus::assoc a w1 w2 - ... = b + w2 : { Hw1 } - ... = c : Hw2) + le::intro (calc a + (w1 + w2) = a + w1 + w2 : add::assoc a w1 w2 + ... = b + w2 : { Hw1 } + ... = c : Hw2) -theorem le::plus {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c +theorem le::add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c := obtain (w : Nat) (Hw : a + w = b), from (le::elim H), - le::intro (calc a + c + w = a + (c + w) : symm (plus::assoc a c w) - ... = a + (w + c) : { plus::comm c w } - ... = a + w + c : plus::assoc a w c - ... = b + c : { Hw }) + le::intro (calc a + c + w = a + (c + w) : symm (add::assoc a c w) + ... = a + (w + c) : { add::comm c w } + ... = a + w + c : add::assoc a w c + ... = b + c : { Hw }) theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b := obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le::elim H2), let L1 : w1 + w2 = 0 - := plus::inj (calc a + (w1 + w2) = a + w1 + w2 : { plus::assoc a w1 w2 } - ... = b + w2 : { Hw1 } - ... = a : Hw2 - ... = a + 0 : symm (plus::zeror a)), - L2 : w1 = 0 := plus::eqz L1 - in calc a = a + 0 : symm (plus::zeror a) + := add::inj (calc a + (w1 + w2) = a + w1 + w2 : { add::assoc a w1 w2 } + ... = b + w2 : { Hw1 } + ... = a : Hw2 + ... = a + 0 : symm (add::zeror a)), + L2 : w1 = 0 := add::eqz L1 + in calc a = a + 0 : symm (add::zeror a) ... = a + w1 : { symm L2 } ... = b : Hw1 diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index c120b1d2af57025bc22af2bbe95ce1f8e0e8906b..3db25e1879a908befec2a8b5700bb0cd1abcd861 100644 GIT binary patch delta 171 zcmX?Jv$tl0Ix}-(O3GwyW-Cr0%}`vLoLn^dAd~Rq1b*(x513ge%X71Cp3a=Y4pO%H zKUX*-TwM-^x(=Q_Okm^g$*OP8=Wk*JbF4LtK&DJy&%(OdP*6$=Y?8nBN)~pIjhT5_ glN~i=ChHlqPgXYQ1WRr(NC(>ov_O2bk%cH50N}qil>h($ delta 158 zcmdm6bG&AQIx|Z_PHFLEEoLh)V-kzz<_XN1>|oC3KV0FA5cwKW&B+s(SvR-v>|x>r z>0n6C&&{2DkV$y*2U-5jS^P~9g`3|Cgh@dZWaee50~Lr)4$xrVoT=Tx0x@YXlO#xF cvWUS14zNL~g;hXh5}OYjctfofw9sJ#0FW{_LjV8(