From 301f3f93aa261364b8d4ce615b670e102b6ab4e7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jun 2016 18:17:14 -0700
Subject: [PATCH] feat(library/init/meta): add `contradiction` tactic

---
 library/init/meta/base_tactic.lean          | 10 +++-
 library/init/meta/contradiction_tactic.lean | 55 +++++++++++++++++++++
 library/init/meta/default.lean              |  2 +-
 library/init/meta/tactic.lean               | 10 ++++
 4 files changed, 74 insertions(+), 3 deletions(-)
 create mode 100644 library/init/meta/contradiction_tactic.lean

diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean
index 4a7186fca9..31d2ef6bb7 100644
--- a/library/init/meta/base_tactic.lean
+++ b/library/init/meta/base_tactic.lean
@@ -57,8 +57,14 @@ namespace tactic
 variables {S A : Type}
 open base_tactic_result
 
-meta_definition fail (e : format) : base_tactic S unit :=
-λ s, exception unit (λ u, e) s
+meta_definition fail (e : string) : base_tactic S A :=
+λ s, exception A (λ u, to_fmt e) s
+
+meta_definition fail_fmt (e : format) : base_tactic S A :=
+λ s, exception A (λ u, e) s
+
+meta_definition failed : base_tactic S A :=
+fail "failed"
 
 meta_definition try (t : base_tactic S A) : base_tactic S unit :=
 λ s, base_tactic_result.cases_on (t s)
diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
new file mode 100644
index 0000000000..1f67b9a21c
--- /dev/null
+++ b/library/init/meta/contradiction_tactic.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic
+
+open expr tactic option bool decidable environment
+
+private meta_definition contra_A_not_A : list expr → list expr → tactic unit
+| []         Hs := failed
+| (H1 :: Rs) Hs :=
+  do t ← infer_type H1,
+     if is_not t = tt
+     then ((do H2 ← find_same_type (app_arg t) Hs,
+               tgt ← target,
+               pr ← mk_app "absurd" [tgt, H2, H1],
+               exact pr) <|> contra_A_not_A Rs Hs)
+     else contra_A_not_A Rs Hs
+
+private meta_definition contra_false : list expr → tactic unit
+| []        := failed
+| (H :: Hs) :=
+  do t ← infer_type H,
+     if is_false t = tt
+     then do tgt ← target,
+             pr  ← mk_app ("false" <.> "rec") [tgt, H],
+             exact pr
+     else contra_false Hs
+
+private meta_definition contra_constructor_eq : list expr → tactic unit
+| []        := failed
+| (H :: Hs) :=
+  do t ← infer_type H,
+     match is_eq t with
+     | some (lhs, rhs) :=
+       do env ← get_env,
+          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)
+          then do tgt    ← target,
+                  I_name ← return (name.get_prefix (const_name (get_app_fn lhs))),
+                  pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, H],
+                  exact pr
+          else contra_constructor_eq Hs
+     | none := contra_constructor_eq Hs
+     end
+
+meta_definition tactic.contradiction : tactic unit :=
+do ctx ← local_context,
+   (contra_false ctx <|>
+    contra_A_not_A ctx ctx <|>
+    contra_constructor_eq ctx <|>
+    fail "contradiction tactic failed")
diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean
index 3cd0203ebc..e1f110f2f3 100644
--- a/library/init/meta/default.lean
+++ b/library/init/meta/default.lean
@@ -6,4 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.name init.meta.options init.meta.format init.meta.rb_map
 import init.meta.level init.meta.expr init.meta.base_tactic init.meta.environment
-import init.meta.tactic
+import init.meta.tactic init.meta.contradiction_tactic
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index fdf7c72ed7..e393a17987 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -135,4 +135,14 @@ meta_definition trace_result : tactic unit :=
 do f ← format_result,
    trace_fmt f
 
+open bool
+/- (find_same_type t es) tries to find in es an expression with type definitionally equal to t -/
+meta_definition find_same_type : expr → list expr → tactic expr
+| e []         := failed
+| e (H :: Hs) :=
+  do t ← infer_type H,
+     b ← unify e t,
+     if b = tt then return H
+     else find_same_type e Hs
+
 end tactic