feat(library/init/meta/contradiction_tactic): add 'exfalso' tactic

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

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

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