feat(library/blast/unit/unit_propagate): make sure unif_propagate works even if 'not' is marked as '[reducible]'

library/init/simplifier.lean

@@ -55,8 +55,8 @@ lemma true_imp [simp] : (true → A) ↔ A :=
 iff.intro (assume H, H trivial)
           (assume a t, a)
 
-lemma fold_not [simp] : (A → false) ↔ ¬ A :=
+-- lemma fold_not [simp] : (A → false) ↔ ¬ A :=
-iff.intro id id
+-- iff.intro id id
 
 lemma false_imp [simp] : (false → A) ↔ true :=
 iff.intro (assume H, trivial)

src/library/blast/unit/unit_propagate.cpp

@@ -25,7 +25,7 @@ bool is_lemma(expr const & _type) {
     expr type = _type;
     bool has_antecedent = false;
     if (!is_prop(type)) return false;
-    while (is_pi(type) && closed(binding_body(type))) {
+    while (is_pi(type) && !is_not(type) && closed(binding_body(type))) {
         has_antecedent = true;
         type = binding_body(type);
     }
@@ -40,15 +40,14 @@ bool is_fact(expr const & type) {
 
 expr flip(expr const & e) {
     expr not_e;
-    if (!blast::is_not(e, not_e)) not_e = get_app_builder().mk_not(e);
+    if (!blast::is_not(e, not_e)) {
+        // we use whnf to make sure we get a uniform representation
+        // even if 'not' is marked '[reducible]'
+        not_e = whnf(get_app_builder().mk_not(e));
+    }
     return not_e;
 }
 
-bool is_not(expr const & e) {
-    expr not_e;
-    return blast::is_not(e, not_e);
-}
-
 static unsigned g_ext_id = 0;
 struct unit_branch_extension : public branch_extension {
     /* We map each lemma to the two facts that it is watching. */
@@ -145,7 +144,7 @@ bool can_propagate(expr const & _type, buffer<expr, 2> & to_watch) {
 
     bool missing_non_Prop = false;
     /* Traverse the A_i */
-    while (is_pi(type) && closed(binding_body(type))) {
+    while (is_pi(type) && !is_not(type) && closed(binding_body(type))) {
         expr arg;
         hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type));
         if (!fact_hidx) {
@@ -207,14 +206,14 @@ action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr const & _
     bool missing_B = false;
 
     /* (3) Traverse the binding domains */
-    while (is_pi(type) && closed(binding_body(type))) {
+    while (is_pi(type) && !is_not(type) && closed(binding_body(type))) {
         hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type));
         if (fact_hidx) {
             proof = mk_app(proof, curr_state().get_hypothesis_decl(*fact_hidx).get_self());
         } else {
             lean_assert(!missing_A);
             missing_A = true;
-            final_type = get_app_builder().mk_not(binding_domain(type));
+            final_type = whnf(get_app_builder().mk_not(binding_domain(type)));
             proof_left = proof;
             type_init_right = binding_body(type);
             proof_init_right = mk_fresh_local(type_init_right);

src/library/blast/util.cpp

@@ -12,6 +12,10 @@ namespace blast {
 bool is_not(expr const & e, expr & a) {
     return ::lean::is_not(env(), e, a);
 }
+bool is_not(expr const & e) {
+    expr not_e;
+    return is_not(e, not_e);
+}
 bool is_false(expr const & e) {
     return ::lean::is_false(env(), e);
 }

src/library/blast/util.h

@@ -10,5 +10,6 @@ namespace lean {
 namespace blast {
 /** \brief Return true iff \c e is of the form (not a) or (a -> false), and false otherwise */
 bool is_not(expr const & e, expr & a);
+bool is_not(expr const & e);
 bool is_false(expr const & e);
 }}

tests/lean/run/blast_cc12.lean

@@ -16,3 +16,10 @@ definition foo3 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :
 by blast
 
 print foo3
+
+attribute not [reducible]
+
+definition foo4 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :=
+by blast
+
+print foo4

tests/lean/run/blast_unit.lean

@@ -41,3 +41,35 @@ example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4
 example (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₃ := by blast
 example (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₂ := by blast
 example (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₁ := by blast
+
+attribute not [reducible]
+
+-- H last, all pos
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₄ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₃ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₂ := by blast
+example (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : B₁ := by blast
+
+example (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₃ := by blast
+example (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₂ := by blast
+example (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) : ¬ A₁ := by blast
+
+-- H first, all neg
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) : ¬ B₄ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) : ¬ B₃ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) : ¬ B₂ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ B₁ := by blast
+
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₃ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₂ := by blast
+example (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) : ¬ ¬ A₁ := by blast
+
+-- H last, all neg
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₄ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₃ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₂ := by blast
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (n3 : ¬ A₃) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ B₁ := by blast
+
+example (n1 : ¬ A₁) (n2 : ¬ A₂) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₃ := by blast
+example (n1 : ¬ A₁) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₂ := by blast
+example (n2 : ¬ A₂) (n3 : ¬ A₃) (b1 : B₁) (b2 : B₂) (b3 : B₃) (b4 : B₄) (H : ¬ A₁ → ¬ A₂ → ¬ A₃ → ¬ B₁ ∨ ¬ B₂ ∨ ¬ B₃ ∨ ¬ B₄) : ¬ ¬ A₁ := by blast