feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled

not (not (not a)) -> not a

hott/init/logic.hlean

@@ -25,6 +25,9 @@ assume H : empty, H
 definition not_not_intro {a : Type} (Ha : a) : ¬¬a :=
 assume Hna : ¬a, absurd Ha Hna
 
+theorem not_of_not_not_not {a : Type} (H : ¬¬¬a) : ¬a :=
+λ Ha, absurd (not_not_intro Ha) H
+
 definition not.elim {a : Type} (H₁ : ¬a) (H₂ : a) : empty := H₁ H₂
 
 definition not.intro {a : Type} (H : a → empty) : ¬a := H

library/init/logic.lean

@@ -340,6 +340,9 @@ iff.intro
 theorem not_not_intro (Ha : a) : ¬¬a :=
 assume Hna : ¬a, Hna Ha
 
+theorem not_of_not_not_not (H : ¬¬¬a) : ¬a :=
+λ Ha, absurd (not_not_intro Ha) H
+
 theorem not_true [simp] : (¬ true) ↔ false :=
 iff_false_intro (not_not_intro trivial)
 

src/library/blast/actions/simple_actions.cpp

@@ -41,6 +41,21 @@ static optional<expr> try_not_refl_relation(hypothesis const & h) {
     return none_expr();
 }
 
+static unsigned consume_not(expr & e) {
+    unsigned n = 0;
+    while (is_not(e, e))
+        n++;
+    return n;
+}
+
+static void reduce_nots(expr & pr, unsigned & num_not) {
+    app_builder & b      = get_app_builder();
+    while (num_not > 2) {
+        pr = b.mk_app(get_not_of_not_not_not_name(), 2, pr);
+        num_not -= 2;
+    }
+}
+
 action_result assumption_contradiction_actions(hypothesis_idx hidx) {
     state const & s      = curr_state();
     app_builder & b      = get_app_builder();
@@ -59,21 +74,24 @@ action_result assumption_contradiction_actions(hypothesis_idx hidx) {
         return action_result(*pr);
     }
     expr p1 = type;
-    bool is_neg1 = is_not(type, p1);
+    unsigned num_not1 = consume_not(p1);
     /* try to find complement */
     for (hypothesis_idx hidx2 : s.get_head_related(hidx)) {
         hypothesis const & h2 = s.get_hypothesis_decl(hidx2);
-        expr type2 = h2.get_type();
-        expr p2    = type2;
-        bool is_neg2 = is_not(type2, p2);
-        if (is_neg1 != is_neg2) {
+        expr p2    = h2.get_type();
+        unsigned num_not2 = consume_not(p2);
+        if ((num_not1 % 2) != (num_not2 % 2)) {
             if (is_def_eq(p1, p2)) {
                 trace_action("contradiction");
-                if (is_neg1) {
-                    return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h2.get_self(), h.get_self()}));
+                expr pr1 = h.get_self();
+                expr pr2 = h2.get_self();
+                reduce_nots(pr1, num_not1);
+                reduce_nots(pr2, num_not2);
+                if (num_not1 > num_not2) {
+                    return action_result(b.mk_app(get_absurd_name(), {s.get_target(), pr2, pr1}));
                 } else {
                     lean_assert(is_neg2);
-                    return action_result(b.mk_app(get_absurd_name(), {s.get_target(), h.get_self(), h2.get_self()}));
+                    return action_result(b.mk_app(get_absurd_name(), {s.get_target(), pr1, pr2}));
                 }
             }
         }

src/library/blast/state.cpp

@@ -711,7 +711,7 @@ hypothesis_idx_set state::get_direct_forward_deps(hypothesis_idx hidx) const {
 }
 
 static optional<head_index> to_head_index(expr type) {
-    is_not(type, type);
+    while (is_not(type, type));
     expr const & f = get_app_fn(type);
     if (is_constant(f) || is_local(f))
         return optional<head_index>(head_index(f));

src/library/constants.cpp

@@ -85,6 +85,7 @@ name const * g_ne = nullptr;
 name const * g_neg = nullptr;
 name const * g_not = nullptr;
 name const * g_not_of_iff_false = nullptr;
+name const * g_not_of_not_not_not = nullptr;
 name const * g_num = nullptr;
 name const * g_num_zero = nullptr;
 name const * g_num_pos = nullptr;
@@ -272,6 +273,7 @@ void initialize_constants() {
     g_neg = new name{"neg"};
     g_not = new name{"not"};
     g_not_of_iff_false = new name{"not_of_iff_false"};
+    g_not_of_not_not_not = new name{"not_of_not_not_not"};
     g_num = new name{"num"};
     g_num_zero = new name{"num", "zero"};
     g_num_pos = new name{"num", "pos"};
@@ -460,6 +462,7 @@ void finalize_constants() {
     delete g_neg;
     delete g_not;
     delete g_not_of_iff_false;
+    delete g_not_of_not_not_not;
     delete g_num;
     delete g_num_zero;
     delete g_num_pos;
@@ -647,6 +650,7 @@ name const & get_ne_name() { return *g_ne; }
 name const & get_neg_name() { return *g_neg; }
 name const & get_not_name() { return *g_not; }
 name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; }
+name const & get_not_of_not_not_not_name() { return *g_not_of_not_not_not; }
 name const & get_num_name() { return *g_num; }
 name const & get_num_zero_name() { return *g_num_zero; }
 name const & get_num_pos_name() { return *g_num_pos; }

src/library/constants.h

@@ -87,6 +87,7 @@ name const & get_ne_name();
 name const & get_neg_name();
 name const & get_not_name();
 name const & get_not_of_iff_false_name();
+name const & get_not_of_not_not_not_name();
 name const & get_num_name();
 name const & get_num_zero_name();
 name const & get_num_pos_name();

src/library/constants.txt

@@ -80,6 +80,7 @@ ne
 neg
 not
 not_of_iff_false
+not_of_not_not_not
 num
 num.zero
 num.pos

tests/lean/run/blast_multiple_nots.lean

@@ -0,0 +1,29 @@
+constants a b c d : Prop
+
+set_option blast.strategy "unit"
+
+example (H : ¬ a → ¬ b → ¬ c ∨ ¬ d) : ¬ a → c → d → ¬ b → false :=
+by blast
+
+set_option blast.strategy "preprocess"
+
+example : ¬¬¬¬¬a → ¬¬a → false :=
+by blast
+
+example : ¬¬¬¬¬a → ¬¬¬¬a → false :=
+by blast
+
+example : ¬¬¬¬¬a → a → false :=
+by blast
+
+example : ¬¬a → ¬¬¬¬¬a → false :=
+by blast
+
+example : ¬¬¬¬¬a → ¬¬¬¬¬¬¬¬a → false :=
+by blast
+
+example : ¬¬¬¬¬a → a → false :=
+by blast
+
+example : ¬¬¬¬¬¬¬¬a → ¬¬¬¬¬a → false :=
+by blast