From 9ae96514e02b7d239b0377f844902249c1d48d0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Dec 2014 15:28:22 -0800 Subject: [PATCH] test(tests/lean/run): use 'cases' tactic --- tests/lean/run/inf_tree2.lean | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/tests/lean/run/inf_tree2.lean b/tests/lean/run/inf_tree2.lean index 77468786f..11636a5bd 100644 --- a/tests/lean/run/inf_tree2.lean +++ b/tests/lean/run/inf_tree2.lean @@ -13,21 +13,11 @@ namespace inftree 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) := 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 - λ 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) + by cases hlt; apply (hf a); apply ht) definition dsub.leaf.acc {A : Type} (a : A) : acc dsub (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 - λ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) + by cases hlt) definition dsub.wf (A : Type) : well_founded (@dsub A) := well_founded.intro (λ (t : inftree A),