From 154f02ca32444b39f9821026870f7ce7ab9dbf2e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2016 17:35:53 -0700
Subject: [PATCH] feat(library/init/meta/contradiction_tactic): add 'exfalso'
 tactic

---
 library/init/meta/contradiction_tactic.lean | 12 ++++++++----
 library/init/meta/tactic.lean               | 17 +++++++++++++++--
 tests/lean/run/exfalso1.lean                | 15 ++++++++-------
 3 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean
index 5da1a435c5..496621a507 100644
--- a/library/init/meta/contradiction_tactic.lean
+++ b/library/init/meta/contradiction_tactic.lean
@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import init.meta.tactic
 
+namespace tactic
+
 open expr tactic option bool decidable environment
 
 private meta_definition contra_A_not_A : list expr → list expr → tactic unit
@@ -53,14 +55,16 @@ private meta_definition contra_constructor_eq : list expr → tactic unit
      | none := contra_constructor_eq Hs
      end
 
-meta_definition tactic.contradiction : tactic unit :=
+meta_definition contradiction : tactic unit :=
 do ctx ← local_context,
    (contra_false ctx <|>
     contra_A_not_A ctx ctx <|>
     contra_constructor_eq ctx <|>
     fail "contradiction tactic failed")
 
-open tactic
+meta_definition exfalso : tactic unit :=
+do fail_if_no_goals,
+   assert "Hfalse" (expr.const "false" []),
+   swap, contradiction
 
-example : ∀ (a b : nat), (0:nat) = 1 → a = b :=
-by do intros, contradiction
+end tactic
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index df7dc72353..33bd8786f3 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -205,9 +205,22 @@ meta_definition all_goals (tac : tactic unit) : tactic unit :=
 do gs ← get_goals,
    all_goals_core tac gs []
 
+meta_definition when (c : Prop) [decidable c] (tac : tactic unit) : tactic unit :=
+if c then tac else skip
+
+meta_definition fail_if_no_goals : tactic unit :=
+do n ← num_goals,
+   when (n = 0) (fail "tactic failed, there are no goals to be solved")
+
 meta_definition now : tactic unit :=
 do n ← num_goals,
-   if n = 0 then skip
-   else fail "now tactic failed, there are unsolved goals"
+   when (n ≠ 0) (fail "now tactic failed, there are unsolved goals")
 
+/- Swap first two goals, do nothing if tactic state does not have at least two goals -/
+meta_definition swap : tactic unit :=
+do gs ← get_goals,
+   match gs with
+   | g₁ :: g₂ :: rs := set_goals (g₂ :: g₁ :: rs)
+   | _              := skip
+   end
 end tactic
diff --git a/tests/lean/run/exfalso1.lean b/tests/lean/run/exfalso1.lean
index 746f475f0b..c75ca12927 100644
--- a/tests/lean/run/exfalso1.lean
+++ b/tests/lean/run/exfalso1.lean
@@ -1,10 +1,11 @@
-exit
-open nat
+open tactic nat
 
 example (a b : nat) : a = 0 → b = 1 → a = b → a + b * b ≤ 10000 :=
-begin
-  intro a0 b1 ab,
-  exfalso, state,
-  rewrite [a0 at ab, b1 at ab],
+by do
+  intro_lst ["a0", "a1", "ab"],
+  exfalso,
+  trace_state,
+  subst "a",
+  subst "b",
+  trace_state,
   contradiction
-end