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 c120b1d2af..3db25e1879 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ