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

doc(examples/wf): use 'have' construct in wf example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-03-03 18:29:19 -08:00
parent 26bf21b91d
commit f8a12363f2
1 changed files with 35 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
examples/lean/wf.lean
View file

@ -13,14 +13,38 @@ theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf
obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
-- The main "trick" is to define Q x as ¬ P x.
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
let Q : A → Bool := λ x, ¬ P x,
Qw : ∃ w, Q w := exists_intro w Hw,
Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b := Hwf Q Qw
in obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), from Qwf,
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
let s1 : ∀ b, R b r → P b := take b : A, assume H : R b r,
-- We are using Hr to derive ¬ ¬ P b
not_not_elim (and_elimr Hr b H),
s2 : P r := iH r s1,
s3 : ¬ P r := and_eliml Hr
in absurd s2 s3)
let Q : A → Bool := λ x, ¬ P x in
have Qw : ∃ w, Q w,
from exists_intro w Hw,
have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b,
from Hwf Q Qw,
obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
from Qwf,
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
have s1 : ∀ b, R b r → P b,
from take b : A, assume H : R b r,
-- We are using Hr to derive ¬ ¬ P b
not_not_elim (and_elimr Hr b H),
have s2 : P r,
from iH r s1,
have s3 : ¬ P r,
from and_eliml Hr,
show false,
from absurd s2 s3)
-- More compact proof
theorem wf_induction2 {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x)
: ∀ x, P x
:= by_contradiction (assume N : ¬ ∀ x, P x,
obtain (w : A) (Hw : ¬ P w), from not_forall_elim N,
-- The main "trick" is to define Q x as ¬ P x.
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r)
let Q : A → Bool := λ x, ¬ P x in
obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b),
from Hwf Q (exists_intro w Hw),
-- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction.
have s1 : ∀ b, R b r → P b,
from take b : A, assume H : R b r,
-- We are using Hr to derive ¬ ¬ P b
not_not_elim (and_elimr Hr b H),
absurd (iH r s1) (and_eliml Hr))