feat(library/tactic): add absurd_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/basic_thms.cpp

@@ -9,6 +9,8 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/basic_thms.h"
 
+#include "kernel/kernel_exception.h"
+
 namespace lean {
 
 MK_CONSTANT(trivial,            name("Trivial"));
@@ -21,6 +23,7 @@ MK_CONSTANT(double_neg_elim_fn, name("DoubleNegElim"));
 MK_CONSTANT(mt_fn,              name("MT"));
 MK_CONSTANT(contrapos_fn,       name("Contrapos"));
 MK_CONSTANT(false_imp_any_fn,   name("FalseImpAny"));
+MK_CONSTANT(absurd_imp_any_fn,  name("AbsurdImpAny"));
 MK_CONSTANT(eq_mp_fn,           name("EqMP"));
 MK_CONSTANT(not_imp1_fn,        name("NotImp1"));
 MK_CONSTANT(not_imp2_fn,        name("NotImp2"));
@@ -117,6 +120,11 @@ void import_basic_thms(environment & env) {
     env.add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)),
                     Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a)));
 
+    // AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c
+    env.add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c),
+                    Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}},
+                        MP(False, c, FalseImpAny(c), Absurd(a, H1, H2))));
+
     // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b
     env.add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b),
                     Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}},

src/library/basic_thms.h

@@ -45,8 +45,14 @@ expr mk_contrapos_fn();
 inline expr Contrapos(expr const & a, expr const & b, expr const & H) { return mk_app(mk_contrapos_fn(), a, b, H); }
 
 expr mk_false_imp_any_fn();
-/** \brief (Theorem) a : Bool, H : False |- a */
-inline expr FalseImpAny(expr const & a, expr const & H) { return mk_app(mk_false_imp_any_fn(), a, H); }
+/** \brief (Theorem) a : Bool |- false => a */
+inline expr FalseImpAny(expr const & a) { return mk_app(mk_false_imp_any_fn(), a); }
+
+expr mk_absurd_imp_any_fn();
+/** \brief (Theorem) {a c : Bool}, H1 : a, H2 : Not(a) |- AbsurdImpAny(a, H1, H2) : c */
+inline expr AbsurdImpAny(expr const & a, expr const & c, expr const & H1, expr const & H2) {
+    return mk_app(mk_absurd_imp_any_fn(), a, c, H1, H2);
+}
 
 expr mk_eq_mp_fn();
 /** \brief (Theorem) {a b : Bool}, H1 : a = b, H2 : a |- EqMP(a, b, H1, H2) : b */

src/library/tactic/boolean.cpp

@@ -239,6 +239,39 @@ tactic disj_hyp_tactic() {
         });
 }
 
+tactic absurd_tactic() {
+    return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
+            list<std::pair<name, expr>> proofs;
+            goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> goal {
+                    expr const & c  = g.get_conclusion();
+                    for (auto const & p1 : g.get_hypotheses()) {
+                        check_interrupted();
+                        expr a;
+                        if (is_not(p1.second, a)) {
+                            for (auto const & p2 : g.get_hypotheses()) {
+                                if (p2.second == a) {
+                                    expr pr = AbsurdImpAny(a, c, mk_constant(p2.first), mk_constant(p1.first));
+                                    proofs.emplace_front(gname, pr);
+                                    return goal(); // remove goal
+                                }
+                            }
+                        }
+                    }
+                    return g; // keep goal
+                });
+            if (empty(proofs))
+                return none_proof_state(); // tactic failed
+            proof_builder pb     = s.get_proof_builder();
+            proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+                    proof_map new_m(m);
+                    for (auto const & np : proofs) {
+                        new_m.insert(np.first, np.second);
+                    }
+                    return pb(new_m, a);
+                });
+            return some(proof_state(s, new_gs, new_pb));
+        });
+}
 
 static int mk_conj_tactic(lua_State * L) {
     int nargs = lua_gettop(L);
@@ -265,10 +298,15 @@ static int mk_disj_hyp_tactic(lua_State * L) {
         return push_tactic(L, disj_hyp_tactic(to_name_ext(L, 1), to_name_ext(L, 2)));
 }
 
+static int mk_absurd_tactic(lua_State * L) {
+    return push_tactic(L, absurd_tactic());
+}
+
 void open_boolean(lua_State * L) {
     SET_GLOBAL_FUN(mk_conj_tactic,     "conj_tactic");
     SET_GLOBAL_FUN(mk_imp_tactic,      "imp_tactic");
     SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
     SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tactic");
+    SET_GLOBAL_FUN(mk_absurd_tactic,   "absurd_tactic");
 }
 }

src/library/tactic/boolean.h

@@ -13,5 +13,6 @@ tactic imp_tactic(name const & H_name = name("H"), bool all = true);
 tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name);
 tactic disj_hyp_tactic(name const & hyp_name);
 tactic disj_hyp_tactic();
+tactic absurd_tactic();
 void open_boolean(lua_State * L);
 }

tests/lean/tactic8.lean

@@ -0,0 +1,8 @@
+Theorem T (a b : Bool) : a \/ b => (not b) => a := _.
+     apply imp_tactic
+     apply imp_tactic
+     apply disj_hyp_tactic
+     apply assumption_tactic
+     apply absurd_tactic
+     done
+Show Environment 1.

tests/lean/tactic8.lean.expected.out

@@ -0,0 +1,6 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T
+Theorem T (a b : Bool) : a ∨ b ⇒ ¬ b ⇒ a :=
+    Discharge
+        (λ H : a ∨ b, Discharge (λ H::1 : ¬ b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))