feat(library/tactic/contradiction_tactic): handle (h1 : p) and (h2 : not p) hypotheses in the contradiction tactic

src/library/tactic/contradiction_tactic.cpp

@@ -25,15 +25,29 @@ tactic contradiction_tactic() {
         substitution subst  = s.get_subst();
         name_generator ngen = s.get_ngen();
         auto tc             = mk_type_checker(env, ngen.mk_child());
+        auto conserv_tc     = mk_type_checker(env, ngen.mk_child(), UnfoldReducible);
         buffer<expr> hyps;
         g.get_hyps(hyps);
         for (expr const & h : hyps) {
             expr h_type = mlocal_type(h);
             h_type      = tc->whnf(h_type).first;
-            expr lhs, rhs;
+            expr lhs, rhs, arg;
             if (is_false(env, h_type)) {
                 assign(subst, g, mk_false_rec(*tc, h, t));
                 return some_proof_state(proof_state(s, tail(gs), subst, ngen));
+            } else if (is_not(env, h_type, arg)) {
+                optional<expr> h_pos;
+                for (expr const & h_prime : hyps) {
+                    constraint_seq cs;
+                    if (conserv_tc->is_def_eq(arg, mlocal_type(h_prime), justification(), cs) && !cs) {
+                        h_pos = h_prime;
+                        break;
+                    }
+                }
+                if (h_pos) {
+                    assign(subst, g, mk_absurd(*tc, t, *h_pos, h));
+                    return some_proof_state(proof_state(s, tail(gs), subst, ngen));
+                }
             } else if (is_eq(h_type, lhs, rhs)) {
                 lhs = tc->whnf(lhs).first;
                 rhs = tc->whnf(rhs).first;

src/library/util.cpp

@@ -276,6 +276,34 @@ expr mk_false_rec(type_checker & tc, expr const & f, expr const & t) {
     }
 }
 
+bool is_not(environment const & env, expr const & e, expr & a) {
+    if (is_app(e)) {
+        expr const & f = app_fn(e);
+        if (!is_constant(f) || const_name(f) != get_not_name())
+            return false;
+        a = app_arg(e);
+        return true;
+    } else if (is_pi(e)) {
+        if (!is_false(env, binding_body(e)))
+            return false;
+        a = binding_domain(e);
+        return true;
+    } else {
+        return false;
+    }
+}
+
+expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e) {
+    level t_lvl  = sort_level(tc.ensure_type(t).first);
+    expr  e_type = tc.infer(e).first;
+    if (is_standard(tc.env())) {
+        return mk_app(mk_constant(get_absurd_name(), {t_lvl}), e_type, t, e, not_e);
+    } else {
+        level e_lvl = sort_level(tc.ensure_type(e_type).first);
+        return mk_app(mk_constant(get_absurd_name(), {e_lvl, t_lvl}), e_type, t, e, not_e);
+    }
+}
+
 optional<expr> lift_down_if_hott(type_checker & tc, expr const & v) {
     if (is_standard(tc.env())) {
         return some_expr(v);

src/library/util.h

@@ -136,6 +136,13 @@ bool is_false(environment const & env, expr const & e);
 /** \brief Return an element of type t given an element \c f : false (in standard mode) and empty (in HoTT) mode */
 expr mk_false_rec(type_checker & tc, expr const & f, expr const & t);
 
+/** \brief Return true if \c e is of the form <tt>(not arg)</tt>, and store \c arg in \c a.
+     Return false otherwise */
+bool is_not(environment const & env, expr const & e, expr & a);
+
+/** \brief Create the term <tt>absurd e not_e : t</tt>. */
+expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e);
+
 expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
 expr mk_refl(type_checker & tc, expr const & a);
 expr mk_symm(type_checker & tc, expr const & H);

tests/lean/hott/contra2.hlean

@@ -0,0 +1,16 @@
+open nat
+
+example (q p : Type) (h₁ : p) (h₂ : ¬ p) : q :=
+by contradiction
+
+example (q p : Type) (h₁ : p) (h₂ : p → empty) : q :=
+by contradiction
+
+example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : ¬ a + b = 0) : q :=
+by contradiction
+
+example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b ≠ 0) : q :=
+by contradiction
+
+example (q : Type) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b = 0 → empty) : q :=
+by contradiction

tests/lean/run/contra2.lean

@@ -0,0 +1,16 @@
+open nat
+
+example (q p : Prop) (h₁ : p) (h₂ : ¬ p) : q :=
+by contradiction
+
+example (q p : Prop) (h₁ : p) (h₂ : p → false) : q :=
+by contradiction
+
+example (q : Prop) (a b : nat) (h₁ : a + b = 0) (h₂ : ¬ a + b = 0) : q :=
+by contradiction
+
+example (q : Prop) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b ≠ 0) : q :=
+by contradiction
+
+example (q : Prop) (a b : nat) (h₁ : a + b = 0) (h₂ : a + b = 0 → false) : q :=
+by contradiction