fix(builtin/Nat): name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
645e748302
commit
62bb2ab2f9
4 changed files with 66 additions and 66 deletions
|
|
@ -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.
|
||||
```
|
||||
|
||||
|
|
|
|||
|
|
@ -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 _ _ _))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
Binary file not shown.
Loading…
Reference in a new issue