From 469066bd00525bf315af37bec4d19e4cafb1c516 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Jun 2016 18:24:19 -0700 Subject: [PATCH] feat(library/init/meta/contradiction_tactic): use whnf to be able to handle (a + 1 = 0) --- library/init/meta/contradiction_tactic.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean index 1f67b9a21c..49430da367 100644 --- a/library/init/meta/contradiction_tactic.lean +++ b/library/init/meta/contradiction_tactic.lean @@ -34,8 +34,10 @@ private meta_definition contra_constructor_eq : list expr → tactic unit | (H :: Hs) := do t ← infer_type H, match is_eq t with - | some (lhs, rhs) := + | some (lhs_0, rhs_0) := do env ← get_env, + lhs ← whnf lhs_0, + rhs ← whnf rhs_0, if is_constructor_app env lhs = tt ∧ is_constructor_app env rhs = tt ∧ const_name (get_app_fn lhs) ≠ const_name (get_app_fn rhs) @@ -53,3 +55,8 @@ do ctx ← local_context, contra_A_not_A ctx ctx <|> contra_constructor_eq ctx <|> fail "contradiction tactic failed") + +open tactic + +example : ∀ (a b : nat), (0:nat) = 1 → a = b := +by do intros, contradiction