From 5da1b52e47e2d7b6ec72dc4a1dceb0bab1fca6ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 16:49:21 -0800 Subject: [PATCH] feat(library/blast/unit/unit_propagate): make sure unif_propagate works even if 'not' is marked as '[reducible]' --- library/init/simplifier.lean | 4 +-- src/library/blast/unit/unit_propagate.cpp | 19 +++++++------- src/library/blast/util.cpp | 4 +++ src/library/blast/util.h | 1 + tests/lean/run/blast_cc12.lean | 7 +++++ tests/lean/run/blast_unit.lean | 32 +++++++++++++++++++++++ 6 files changed, 55 insertions(+), 12 deletions(-) diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean index 27ca8ccb7..10c7e65ca 100644 --- a/library/init/simplifier.lean +++ b/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 := -iff.intro id id +-- lemma fold_not [simp] : (A → false) ↔ ¬ A := +-- iff.intro id id lemma false_imp [simp] : (false → A) ↔ true := iff.intro (assume H, trivial) diff --git a/src/library/blast/unit/unit_propagate.cpp b/src/library/blast/unit/unit_propagate.cpp index d569490b1..fd8065dba 100644 --- a/src/library/blast/unit/unit_propagate.cpp +++ b/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 & 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); diff --git a/src/library/blast/util.cpp b/src/library/blast/util.cpp index 6a198b6d3..15ba4fb2e 100644 --- a/src/library/blast/util.cpp +++ b/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); } diff --git a/src/library/blast/util.h b/src/library/blast/util.h index 48ad4ca28..b9dae25ff 100644 --- a/src/library/blast/util.h +++ b/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); }} diff --git a/tests/lean/run/blast_cc12.lean b/tests/lean/run/blast_cc12.lean index 6640000d2..2dba59441 100644 --- a/tests/lean/run/blast_cc12.lean +++ b/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 diff --git a/tests/lean/run/blast_unit.lean b/tests/lean/run/blast_unit.lean index 84ea94f01..506ac81b9 100644 --- a/tests/lean/run/blast_unit.lean +++ b/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