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

test(tests/lean/run): use 'cases' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-03 15:28:22 -08:00
parent d10bb92a7d
commit 9ae96514e0
1 changed files with 2 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lean/run/inf_tree2.lean
View file

@ -13,21 +13,11 @@ namespace inftree
definition dsub.node.acc {A : Type} (f : nat → inftree A) (hf : ∀a, acc dsub (f a)) definition dsub.node.acc {A : Type} (f : nat → inftree A) (hf : ∀a, acc dsub (f a))
(t : inftree A) (ht : acc dsub t) : acc dsub (node f t) := (t : inftree A) (ht : acc dsub t) : acc dsub (node f t) :=
acc.intro (node f t) (λ (y : inftree A) (hlt : dsub y (node f t)), acc.intro (node f t) (λ (y : inftree A) (hlt : dsub y (node f t)),
have aux : ∀ z, dsub y z → node f t = z → acc dsub y, from by cases hlt; apply (hf a); apply ht)
λ z hlt, dsub.rec_on hlt
(λ f₁ n t₁ (heq : (node f t = node f₁ t₁)),
inftree.no_confusion heq (λ e₁ e₂, eq.rec_on e₁ (hf n)))
(λ f₁ n t₁ (heq : (node f t = node f₁ t₁)),
inftree.no_confusion heq (λ e₁ e₂, eq.rec_on e₂ ht)),
aux (node f t) hlt rfl)
definition dsub.leaf.acc {A : Type} (a : A) : acc dsub (leaf a) := definition dsub.leaf.acc {A : Type} (a : A) : acc dsub (leaf a) :=
acc.intro (leaf a) (λ (y : inftree A) (hlt : dsub y (leaf a)), acc.intro (leaf a) (λ (y : inftree A) (hlt : dsub y (leaf a)),
have aux : ∀ z, dsub y z → leaf a = z → acc dsub y, from by cases hlt)
λz hlt, dsub.rec_on hlt
(λ f n t (heq : leaf a = node f t), inftree.no_confusion heq)
(λ f n t (heq : leaf a = node f t), inftree.no_confusion heq),
aux (leaf a) hlt rfl)
definition dsub.wf (A : Type) : well_founded (@dsub A) := definition dsub.wf (A : Type) : well_founded (@dsub A) :=
well_founded.intro (λ (t : inftree A), well_founded.intro (λ (t : inftree A),