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

refactor(library/data/nat/basic): use no_confusion construction to simplify proofs

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-08 19:00:40 -08:00
parent ac5a963db3
commit b97d437011
1 changed files with 2 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
library/data/nat/basic.lean
View file

@ -48,14 +48,7 @@ num.rec zero
-- -------------------------
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
assume H : succ n = 0,
have H2 : true = false, from
let f := (nat.rec false (fun a b, true)) in
calc
true = f (succ n) : rfl
... = f 0 : H
... = false : rfl,
absurd H2 true_ne_false
assume H, no_confusion H
-- add_rewrite succ_ne_zero
@ -86,10 +79,7 @@ or.elim (zero_or_succ_pred n)
(take H3 : n = succ (pred n), H2 (pred n) H3)
theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
calc
n = pred (succ n) : pred.succ
... = pred (succ m) : H
... = m : pred.succ
no_confusion H (λe, e)
theorem succ.ne_self {n : ℕ} : succ n ≠ n :=
induction_on n