diff --git a/library/init/logic.lean b/library/init/logic.lean index bc653e9ad6..7e524e2fc3 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -27,6 +27,8 @@ false.rec b (H2 H1) theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a := assume Ha : a, absurd (H1 Ha) H2 +definition implies.resolve {a b : Prop} (H : a → b) (nb : ¬ b) : ¬ a := assume Ha, nb (H Ha) + /- not -/ theorem not_false : ¬false := @@ -37,6 +39,8 @@ definition non_contradictory (a : Prop) : Prop := ¬¬a theorem non_contradictory_intro {a : Prop} (Ha : a) : ¬¬a := assume Hna : ¬a, absurd Ha Hna +definition not.wrap {a : Prop} (na : a → false) : ¬ a := na + /- false -/ theorem false.elim {c : Prop} (H : false) : c := @@ -459,6 +463,20 @@ iff.trans or.comm !or_false theorem or_self [simp] (a : Prop) : a ∨ a ↔ a := iff.intro (or.rec id id) or.inl +/- or resolution rulse -/ + +definition or.resolve_left {a b : Prop} (H : a ∨ b) (na : ¬ a) : b := + or.elim H (λ Ha, absurd Ha na) id + +definition or.neg_resolve_left {a b : Prop} (H : ¬ a ∨ b) (Ha : a) : b := + or.elim H (λ na, absurd Ha na) id + +definition or.resolve_right {a b : Prop} (H : a ∨ b) (nb : ¬ b) : a := + or.elim H id (λ Hb, absurd Hb nb) + +definition or.neg_resolve_right {a b : Prop} (H : a ∨ ¬ b) (Hb : b) : a := + or.elim H id (λ nb, absurd Hb nb) + /- iff simp rules -/ theorem iff_true [simp] (a : Prop) : (a ↔ true) ↔ a := diff --git a/src/library/blast/unit/unit_action.cpp b/src/library/blast/unit/unit_action.cpp index 9775c5f55a..e97f2ad33b 100644 --- a/src/library/blast/unit/unit_action.cpp +++ b/src/library/blast/unit/unit_action.cpp @@ -21,123 +21,88 @@ Author: Daniel Selsam namespace lean { namespace blast { +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))) { + has_antecedent = true; + type = binding_body(type); + } + if (has_antecedent && !is_pi(type)) return true; + else if (is_or(type)) return true; + else return false; +} + +bool is_fact(expr const & type) { + return is_prop(type) && !is_pi(type) && !is_or(type); +} + +expr flip(expr const & e) { + expr not_e; + if (!blast::is_not(e, not_e)) not_e = 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 { - rb_multi_map m_lemma_map; - rb_map m_fact_map; + /* We map each lemma to the two facts that it is watching. */ + rb_multi_map m_lemmas_to_facts; + + /* We map each fact back to the lemma hypotheses that are watching it. */ + rb_multi_map m_facts_to_lemmas; + + /* We map each fact expression to its hypothesis. */ + rb_map m_facts; unit_branch_extension() {} unit_branch_extension(unit_branch_extension const & b): - m_lemma_map(b.m_lemma_map), m_fact_map(b.m_fact_map) {} + m_lemmas_to_facts(b.m_lemmas_to_facts), + m_facts_to_lemmas(b.m_facts_to_lemmas), + m_facts(b.m_facts) {} virtual ~unit_branch_extension() {} virtual branch_extension * clone() override { return new unit_branch_extension(*this); } - - void insert(expr const & e, hypothesis_idx hidx, bool neg) { - expr A, B; - if (is_or(e, A, B)) { - lean_assert(!neg); - insert(A, hidx, neg); - insert(B, hidx, neg); - } else if (is_and(e, A, B)) { - lean_assert(neg); - insert(A, hidx, neg); - insert(B, hidx, neg); - } else if (neg) { - expr not_e; - if (blast::is_not(e, not_e)) m_lemma_map.insert(not_e, hidx); - else m_lemma_map.insert(get_app_builder().mk_not(e), hidx); - } else { - m_lemma_map.insert(e, hidx); - } - } - virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override { - expr type = whnf(h.get_type()); - if (!is_pi(type)) { - if (is_prop(type)) m_fact_map.insert(type, hidx); - return; - } - bool has_antecedent = false; - while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) { - has_antecedent = true; - insert(binding_domain(type), hidx, false); - type = binding_body(type); - } - if (has_antecedent && is_prop(type)) { - insert(type, hidx, true); - } + if (is_fact(h.get_type())) m_facts.insert(h.get_type(), hidx); } - - virtual void hypothesis_deleted(hypothesis const & , hypothesis_idx ) override { - /* We discard opportunistically when we encounter a hypothesis that is dead. */ + virtual void hypothesis_deleted(hypothesis const & h, hypothesis_idx hidx) override { + if (is_lemma(h.get_type())) { + list const * facts = find_facts_watching_lemma(hidx); + if (facts) { + for_each(*facts, [&](expr const & fact) { + unwatch(hidx, fact); + }); + } + } else if (is_fact(h.get_type())) { + m_facts.erase(h.get_type()); + lean_assert(!find_lemmas_watching_fact(h.get_type())); + } } public: - list const * find_lemmas(expr const & e) { return m_lemma_map.find(e); } - template void filter_lemmas(expr const & e, P && p) { return m_lemma_map.filter(e, p); } - hypothesis_idx const * find_fact(expr const & e) { return m_fact_map.find(e); } - void erase_fact(expr const & e) { return m_fact_map.erase(e); } - - /* Returns a proof of the disjunction [e] */ - optional find_live_fact_in_disjunction(expr const & e) { - expr A, B; - if (is_or(e, A, B)) { - if (auto A_fact = find_live_fact_in_disjunction(A)) { - return some_expr(get_app_builder().mk_app(get_or_intro_left_name(), {A, B, *A_fact})); - } else if (auto B_fact = find_live_fact_in_disjunction(B)) { - return some_expr(get_app_builder().mk_app(get_or_intro_right_name(), {A, B, *B_fact})); - } else { - return none_expr(); - } - } else { - hypothesis_idx const * fact_hidx = find_fact(e); - if (fact_hidx) { - hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx); - if (fact_h.is_dead()) { - erase_fact(e); - return none_expr(); - } else { - return some_expr(fact_h.get_self()); - } - } else { - return none_expr(); - } - } + list const * find_lemmas_watching_fact(expr const & fact_type) { + return m_facts_to_lemmas.find(fact_type); } - - /* Returns a proof of [false], by either applying a projection of [proof] to a hypothesis or vice versa. */ - optional find_live_disproof_of_conjunction(expr const & e, expr const & proof) { - expr A, B; - if (is_and(e, A, B)) { - if (auto A_false = find_live_disproof_of_conjunction(A, get_app_builder().mk_app(get_and_elim_left_name(), {A, B, proof}))) { - return some_expr(*A_false); - } else if (auto B_false = find_live_disproof_of_conjunction(B, get_app_builder().mk_app(get_and_elim_right_name(), {A, B, proof}))) { - return some_expr(*B_false); - } else { - return none_expr(); - } - } else { - expr not_e; - bool not_e_is_not = false; - if (!blast::is_not(e, not_e)) { - not_e_is_not = true; - not_e = get_app_builder().mk_not(e); - } - - hypothesis_idx const * fact_hidx = find_fact(not_e); - if (fact_hidx) { - hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx); - if (fact_h.is_dead()) { - erase_fact(e); - return none_expr(); - } else { - if (not_e_is_not) return some_expr(mk_app(fact_h.get_self(), proof)); - else return some_expr(mk_app(proof, fact_h.get_self())); - } - } else { - return none_expr(); - } - } + list const * find_facts_watching_lemma(hypothesis_idx lemma_hidx) { + return m_lemmas_to_facts.find(lemma_hidx); + } + void unwatch(hypothesis_idx lemma_hidx, expr const & fact_type) { + m_lemmas_to_facts.filter(lemma_hidx, [&](expr const & fact_type2) { + return fact_type != fact_type2; + }); + m_facts_to_lemmas.erase(fact_type, lemma_hidx); + } + hypothesis_idx const * find_fact(expr const & fact_type) { + return m_facts.find(fact_type); + } + void watch(hypothesis_idx lemma_hidx, expr const & fact_type) { + m_lemmas_to_facts.insert(lemma_hidx, fact_type); + m_facts_to_lemmas.insert(fact_type, lemma_hidx); } }; @@ -151,72 +116,178 @@ static unit_branch_extension & get_extension() { return static_cast(curr_state().get_extension(g_ext_id)); } -action_result unit_pi(expr const & _type, expr const & proof) { - unit_branch_extension & ext = get_extension(); - bool missing_argument = false; - bool has_antecedent = false; - expr type = _type; - expr new_hypothesis = proof; - expr local; +/* Recall the general form of the lemmas we handle in this module: + A_1 -> ... -> A_n -> B_1 \/ (B2 \/ ... \/ B_m)...) - while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) { - has_antecedent = true; - optional fact = ext.find_live_fact_in_disjunction(binding_domain(type)); - if (fact) { - new_hypothesis = mk_app(new_hypothesis, *fact); - } else { - if (missing_argument) return action_result::failed(); - local = mk_fresh_local(binding_domain(type)); - new_hypothesis = mk_app(new_hypothesis, local); - missing_argument = true; + There are three different scenarios in which we propagate: + (1) We have all of the A_i, and the negations of all but the last B_j. + (2) We are missing an A_i. + (3) We are missing a B_j. + + The first thing we do is check whether or not we are able to propagate. + If so, we start instantiating the A_i. If we hit a missing literal, + we store the proof so far, create a local for the consequent, prove false, + and then conclude with [lemma imp_right : (A → B) → ¬ B → ¬ A]. + + If we instantiate all the A_i, we start using [lemma or_resolve_left : A ∨ B → ¬ A → B] + to cross of the B_j. If we have all but the last one, we simply return the resulting proof. + + If we are missing a B_j, we store the proof so far, create a local for the right-hand-side of + the disjunct, prove false, and then conclude with [lemma or_resolve_right : A ∨ B → ¬ B → A]. +*/ + + +bool can_propagate(expr const & _type, buffer & to_watch) { + lean_assert(is_lemma(_type)); + expr type = _type; + unsigned num_watching = 0; + unit_branch_extension & ext = get_extension(); + + /* Traverse the A_i */ + while (is_pi(type) && closed(binding_body(type))) { + expr arg; + hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type)); + if (!fact_hidx) { + to_watch.push_back(binding_domain(type)); + num_watching++; + if (num_watching == 2) return false; } type = binding_body(type); } - if (!has_antecedent) { - return action_result::failed(); - } else if (!missing_argument) { - curr_state().mk_hypothesis(type, new_hypothesis); - return action_result::new_branch(); - } else if (is_prop(type)) { - optional disproof = ext.find_live_disproof_of_conjunction(type, new_hypothesis); - if (disproof) { - curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)), - Fun(local, *disproof)); - return action_result::new_branch(); - } else { - return action_result::failed(); + /* Traverse the B_j */ + expr lhs, rhs; + while (is_or(type, lhs, rhs)) { + hypothesis_idx const * fact_hidx = ext.find_fact(flip(lhs)); + if (!fact_hidx) { + to_watch.push_back(flip(lhs)); + num_watching++; + if (num_watching == 2) return false; } - } else { + type = rhs; + } + + hypothesis_idx const * fact_hidx = ext.find_fact(flip(type)); + if (!fact_hidx) { + to_watch.push_back(flip(type)); + num_watching++; + if (num_watching == 2) return false; + } + return true; +} + +action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr const & _proof) { + lean_assert(is_lemma(_type)); + unit_branch_extension & ext = get_extension(); + + /* (1) Find the facts that are watching this lemma and clear them. */ + list const * watching = ext.find_facts_watching_lemma(hidx); + if (watching) { + lean_assert(length(*watching) == 2); + // TODO(dhs): is it safe to remove from these lists while I am iterating them with [for_each]? + for_each(*watching, [&](expr const & fact) { ext.unwatch(hidx, fact); }); + } + + /* (2) Check if we can propagate */ + buffer to_watch; + if (!can_propagate(_type, to_watch)) { + for (expr const & e : to_watch) ext.watch(hidx, e); return action_result::failed(); } - lean_unreachable(); + + expr type = _type; + expr proof = _proof; + expr final_type; + expr proof_left; + expr proof_init_right; + expr type_init_right; + bool missing_A = false; + bool missing_B = false; + + /* (3) Traverse the binding domains */ + while (is_pi(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)); + proof_left = proof; + type_init_right = binding_body(type); + proof_init_right = mk_fresh_local(type_init_right); + proof = proof_init_right; + } + type = binding_body(type); + } + + /* (4) Traverse the conclusion */ + expr lhs, rhs; + while (is_or(type, lhs, rhs)) { + hypothesis_idx const * fact_hidx = ext.find_fact(flip(lhs)); + if (fact_hidx) { + expr arg = curr_state().get_hypothesis_decl(*fact_hidx).get_self(); + if (is_not(lhs)) { + proof = get_app_builder().mk_app(get_or_neg_resolve_left_name(), + proof, arg); + } else { + proof = get_app_builder().mk_app(get_or_resolve_left_name(), + proof, arg); + } + } else { + lean_assert(!missing_A); + lean_assert(!missing_B); + missing_B = true; + final_type = lhs; + proof_left = proof; + type_init_right = rhs; + proof_init_right = mk_fresh_local(type_init_right); + proof = proof_init_right; + } + type = rhs; + } + + expr final_proof; + if (missing_A || missing_B) { + hypothesis_idx const * fact_hidx = ext.find_fact(flip(type)); + lean_assert(fact_hidx); + expr arg = curr_state().get_hypothesis_decl(*fact_hidx).get_self(); + if (is_not(type)) proof = mk_app(proof, arg); + else proof = mk_app(arg, proof); + expr proof_right = get_app_builder().mk_app(get_not_wrap_name(), type_init_right, Fun(proof_init_right, proof)); + if (missing_A) { + final_proof = get_app_builder().mk_app(get_implies_resolve_name(), proof_left, proof_right); + } else { + final_proof = get_app_builder().mk_app(get_or_resolve_right_name(), proof_left, proof_right); + } + } else { + final_type = type; + final_proof = proof; + } + + curr_state().mk_hypothesis(final_type, final_proof); + return action_result::new_branch(); } action_result unit_fact(expr const & type) { unit_branch_extension & ext = get_extension(); - list const * lemmas = ext.find_lemmas(type); + list const * lemmas = ext.find_lemmas_watching_fact(type); if (!lemmas) return action_result::failed(); bool success = false; - ext.filter_lemmas(type, [&](hypothesis_idx const & hidx) { + for_each(*lemmas, [&](hypothesis_idx const & hidx) { hypothesis const & h = curr_state().get_hypothesis_decl(hidx); - if (h.is_dead()) { - return false; - } else { - action_result r = unit_pi(whnf(h.get_type()), h.get_self()); - success = success || (r.get_kind() == action_result::NewBranch); - return true; - } + action_result r = unit_lemma(hidx, whnf(h.get_type()), h.get_self()); + success = success || (r.get_kind() == action_result::NewBranch); }); if (success) return action_result::new_branch(); else return action_result::failed(); } -action_result unit_action(unsigned _hidx) { - hypothesis const & h = curr_state().get_hypothesis_decl(_hidx); +action_result unit_action(unsigned hidx) { + hypothesis const & h = curr_state().get_hypothesis_decl(hidx); expr type = whnf(h.get_type()); - if (is_pi(type)) return unit_pi(type, h.get_self()); - else if (is_prop(type)) return unit_fact(type); + if (is_lemma(type)) return unit_lemma(hidx, type, h.get_self()); + else if (is_fact(type)) return unit_fact(type); else return action_result::failed(); } }} diff --git a/src/library/blast/unit/unit_action.h b/src/library/blast/unit/unit_action.h index 52f3ffd44f..306f8fd81d 100644 --- a/src/library/blast/unit/unit_action.h +++ b/src/library/blast/unit/unit_action.h @@ -8,18 +8,15 @@ Author: Daniel Selsam namespace lean { namespace blast { -/* \brief Propagates lemmas of the form - (A11 \/ ... \/ ...) -> ... -> (Am1 \/ ... \/ ...) -> (B1 /\ ... /\ ...) - where each A and B can be any propositions, and can optionally - be negated. +/* \brief The unit module handles lemmas of the form + A_1 -> ... -> A_n -> B_1 \/ (B2 \/ ... \/ B_m)...) - If we can find one disjunct for every antecedent, we instantiate the lemma - fully. On the other hand, if we can find one disjunct for all but one - antecedents, and one fact that disproves the conjunctive conclusion, - we conclude the negation of the missing disjunctive argument. + Whenever all but one of the literals is present as a hypothesis with + the appropriate polarity, we instantiate and resolve and necessary + to conclude a new literal. - Remark: conjunctions in the antecedents and disjunctions in the conclusion are - both treated as monolithic propositions, so some pre-processing may be necessary. + Remark: we assume that a pre-processing step will put lemmas + into the above form when possible. */ action_result unit_action(unsigned hidx); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d370ba550a..5312e36480 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -66,6 +66,7 @@ name const * g_iff_elim_left = nullptr; name const * g_iff_elim_right = nullptr; name const * g_iff_false_intro = nullptr; name const * g_iff_true_intro = nullptr; +name const * g_implies_resolve = nullptr; name const * g_implies = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_implies_of_if_neg = nullptr; @@ -81,6 +82,7 @@ name const * g_nat_succ = nullptr; name const * g_nat_zero = nullptr; name const * g_neg = nullptr; name const * g_not = nullptr; +name const * g_not_wrap = nullptr; name const * g_not_of_iff_false = nullptr; name const * g_num = nullptr; name const * g_num_zero = nullptr; @@ -94,6 +96,11 @@ name const * g_or = nullptr; name const * g_or_elim = nullptr; name const * g_or_intro_left = nullptr; name const * g_or_intro_right = nullptr; +name const * g_or_rec = nullptr; +name const * g_or_resolve_left = nullptr; +name const * g_or_resolve_right = nullptr; +name const * g_or_neg_resolve_left = nullptr; +name const * g_or_neg_resolve_right = nullptr; name const * g_poly_unit = nullptr; name const * g_poly_unit_star = nullptr; name const * g_pos_num = nullptr; @@ -245,6 +252,7 @@ void initialize_constants() { g_iff_elim_right = new name{"iff", "elim_right"}; g_iff_false_intro = new name{"iff_false_intro"}; g_iff_true_intro = new name{"iff_true_intro"}; + g_implies_resolve = new name{"implies", "resolve"}; g_implies = new name{"implies"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_implies_of_if_neg = new name{"implies_of_if_neg"}; @@ -260,6 +268,7 @@ void initialize_constants() { g_nat_zero = new name{"nat", "zero"}; g_neg = new name{"neg"}; g_not = new name{"not"}; + g_not_wrap = new name{"not", "wrap"}; g_not_of_iff_false = new name{"not_of_iff_false"}; g_num = new name{"num"}; g_num_zero = new name{"num", "zero"}; @@ -273,6 +282,11 @@ void initialize_constants() { g_or_elim = new name{"or", "elim"}; g_or_intro_left = new name{"or", "intro_left"}; g_or_intro_right = new name{"or", "intro_right"}; + g_or_rec = new name{"or", "rec"}; + g_or_resolve_left = new name{"or", "resolve_left"}; + g_or_resolve_right = new name{"or", "resolve_right"}; + g_or_neg_resolve_left = new name{"or", "neg_resolve_left"}; + g_or_neg_resolve_right = new name{"or", "neg_resolve_right"}; g_poly_unit = new name{"poly_unit"}; g_poly_unit_star = new name{"poly_unit", "star"}; g_pos_num = new name{"pos_num"}; @@ -425,6 +439,7 @@ void finalize_constants() { delete g_iff_elim_right; delete g_iff_false_intro; delete g_iff_true_intro; + delete g_implies_resolve; delete g_implies; delete g_implies_of_if_pos; delete g_implies_of_if_neg; @@ -440,6 +455,7 @@ void finalize_constants() { delete g_nat_zero; delete g_neg; delete g_not; + delete g_not_wrap; delete g_not_of_iff_false; delete g_num; delete g_num_zero; @@ -453,6 +469,11 @@ void finalize_constants() { delete g_or_elim; delete g_or_intro_left; delete g_or_intro_right; + delete g_or_rec; + delete g_or_resolve_left; + delete g_or_resolve_right; + delete g_or_neg_resolve_left; + delete g_or_neg_resolve_right; delete g_poly_unit; delete g_poly_unit_star; delete g_pos_num; @@ -604,6 +625,7 @@ name const & get_iff_elim_left_name() { return *g_iff_elim_left; } name const & get_iff_elim_right_name() { return *g_iff_elim_right; } name const & get_iff_false_intro_name() { return *g_iff_false_intro; } name const & get_iff_true_intro_name() { return *g_iff_true_intro; } +name const & get_implies_resolve_name() { return *g_implies_resolve; } name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } @@ -619,6 +641,7 @@ name const & get_nat_succ_name() { return *g_nat_succ; } name const & get_nat_zero_name() { return *g_nat_zero; } name const & get_neg_name() { return *g_neg; } name const & get_not_name() { return *g_not; } +name const & get_not_wrap_name() { return *g_not_wrap; } name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; } name const & get_num_name() { return *g_num; } name const & get_num_zero_name() { return *g_num_zero; } @@ -632,6 +655,11 @@ name const & get_or_name() { return *g_or; } name const & get_or_elim_name() { return *g_or_elim; } name const & get_or_intro_left_name() { return *g_or_intro_left; } name const & get_or_intro_right_name() { return *g_or_intro_right; } +name const & get_or_rec_name() { return *g_or_rec; } +name const & get_or_resolve_left_name() { return *g_or_resolve_left; } +name const & get_or_resolve_right_name() { return *g_or_resolve_right; } +name const & get_or_neg_resolve_left_name() { return *g_or_neg_resolve_left; } +name const & get_or_neg_resolve_right_name() { return *g_or_neg_resolve_right; } name const & get_poly_unit_name() { return *g_poly_unit; } name const & get_poly_unit_star_name() { return *g_poly_unit_star; } name const & get_pos_num_name() { return *g_pos_num; } diff --git a/src/library/constants.h b/src/library/constants.h index 924c606657..cf93d53788 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -68,6 +68,7 @@ name const & get_iff_elim_left_name(); name const & get_iff_elim_right_name(); name const & get_iff_false_intro_name(); name const & get_iff_true_intro_name(); +name const & get_implies_resolve_name(); name const & get_implies_name(); name const & get_implies_of_if_pos_name(); name const & get_implies_of_if_neg_name(); @@ -83,6 +84,7 @@ name const & get_nat_succ_name(); name const & get_nat_zero_name(); name const & get_neg_name(); name const & get_not_name(); +name const & get_not_wrap_name(); name const & get_not_of_iff_false_name(); name const & get_num_name(); name const & get_num_zero_name(); @@ -96,6 +98,11 @@ name const & get_or_name(); name const & get_or_elim_name(); name const & get_or_intro_left_name(); name const & get_or_intro_right_name(); +name const & get_or_rec_name(); +name const & get_or_resolve_left_name(); +name const & get_or_resolve_right_name(); +name const & get_or_neg_resolve_left_name(); +name const & get_or_neg_resolve_right_name(); name const & get_poly_unit_name(); name const & get_poly_unit_star_name(); name const & get_pos_num_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index eb44192ec3..2b0e115e5d 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -61,6 +61,7 @@ iff.elim_left iff.elim_right iff_false_intro iff_true_intro +implies.resolve implies implies_of_if_pos implies_of_if_neg @@ -76,6 +77,7 @@ nat.succ nat.zero neg not +not.wrap not_of_iff_false num num.zero @@ -89,6 +91,11 @@ or or.elim or.intro_left or.intro_right +or.rec +or.resolve_left +or.resolve_right +or.neg_resolve_left +or.neg_resolve_right poly_unit poly_unit.star pos_num diff --git a/src/library/util.cpp b/src/library/util.cpp index d0ef8b33f3..6a9eddca0e 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -304,6 +304,13 @@ expr mk_false_rec(type_checker & tc, expr const & f, expr const & t) { } } +bool is_or(expr const & e) { + buffer args; + expr const & fn = get_app_args(e, args); + if (is_constant(fn) && const_name(fn) == get_or_name() && args.size() == 2) return true; + else return false; +} + bool is_or(expr const & e, expr & A, expr & B) { buffer args; expr const & fn = get_app_args(e, args); diff --git a/src/library/util.h b/src/library/util.h index bade2c48b7..edf8da7ea6 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -143,6 +143,7 @@ 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); +bool is_or(expr const & e); bool is_or(expr const & e, expr & A, expr & B); /** \brief Return true if \c e is of the form (not arg), and store \c arg in \c a. diff --git a/tests/lean/run/blast22.lean b/tests/lean/run/blast22.lean deleted file mode 100644 index 5e6fc398ee..0000000000 --- a/tests/lean/run/blast22.lean +++ /dev/null @@ -1,13 +0,0 @@ --- Basic (propositional) forward chaining -constants (A B C D : Prop) - -definition lemma1 : A → (A → B) → B := by blast -definition lemma2 : ¬ B → (A → B) → ¬ A := by blast -definition lemma3 : ¬ C → A → (A → B → C) → ¬ B := by blast -definition lemma4 : C → A → (A → B → ¬ C) → ¬ B := by blast --- TODO(dhs): [forward_action] is responsible for --- eliminating double negation -definition lemma5 : C → A → (A → ¬ B → ¬ C) → ¬ ¬ B := by blast -definition lemma6 : (A → B → ¬ C) → C → A → ¬ B := by blast -definition lemma7 : ¬ C → (A → B → C) → A → ¬ B := by blast -definition lemma8 : A → (A → B) → C → B ∧ C := by blast diff --git a/tests/lean/run/blast23.lean b/tests/lean/run/blast23.lean deleted file mode 100644 index 3d8e1e7ab1..0000000000 --- a/tests/lean/run/blast23.lean +++ /dev/null @@ -1,9 +0,0 @@ --- Basic (propositional) forward chaining with nested backward chaining -constants (A B C D : Prop) -set_option blast.trace true -set_option blast.init_depth 10 -set_option blast.inc_depth 1000 -set_option pp.all true - -definition lemma1 : A → (A → B) → C → B ∧ C := -by blast diff --git a/tests/lean/run/blast24.lean b/tests/lean/run/blast24.lean deleted file mode 100644 index 2c9009dcd7..0000000000 --- a/tests/lean/run/blast24.lean +++ /dev/null @@ -1,12 +0,0 @@ --- Basic (propositional) forward chaining with clauses -constants (A B C D E : Prop) -set_option blast.recursor false - -definition lemma1 : A → (A ∨ B → C) → C := by blast -definition lemma2 : B → (A ∨ B → C) → C := by blast -definition lemma3 : A → B → (A → B ∨ C → D) → D := by blast -definition lemma4 : A → B → (A → B ∨ C ∨ C → D) → D := by blast -definition lemma5 : A → B → (E ∨ A ∨ E → E ∨ B ∨ C ∨ C → D) → D := by blast -definition lemma6 : A → (A → B → C) → ¬ C → ¬ B := by blast -definition lemma7 : ¬ D → B → (A → E ∨ B ∨ C ∨ C → D) → ¬ A := by blast -definition lemma8 : ¬ D → B → (A ∨ E → E ∨ B ∨ C ∨ C → D) → ¬ (A ∨ E) := by blast diff --git a/tests/lean/run/blast25.lean b/tests/lean/run/blast25.lean deleted file mode 100644 index 2d7e84e5e9..0000000000 --- a/tests/lean/run/blast25.lean +++ /dev/null @@ -1,12 +0,0 @@ --- Basic (propositional) forward chaining with conjunctive conclusions -constants (A B C D E : Prop) -set_option blast.recursor false - -definition lemma1 : B → (A → (¬ B) ∧ C) → ¬ A := by blast -definition lemma2 : ¬ B → (A → B ∧ C) → ¬ A := by blast -definition lemma3 : B → (A → C ∧ (¬ B)) → ¬ A := by blast -definition lemma4 : ¬ B → (A → C ∧ B) → ¬ A := by blast -definition lemma5 : B → (A → (¬ B) ∧ E ∧ C) → ¬ A := by blast -definition lemma6 : ¬ B → (A → E ∧ B ∧ C) → ¬ A := by blast -definition lemma7 : B → (A → E ∧ C ∧ (¬ B)) → ¬ A := by blast -definition lemma8 : ¬ B → (A → C ∧ B ∧ E) → ¬ A := by blast diff --git a/tests/lean/run/blast26.lean b/tests/lean/run/blast26.lean deleted file mode 100644 index 06c399b60a..0000000000 --- a/tests/lean/run/blast26.lean +++ /dev/null @@ -1,10 +0,0 @@ --- Basic (propositional) forward chaining with disjunctive antecedents and conjunctive conclusions -constants (A B C D E F : Prop) -set_option blast.recursor false - -definition lemma1 : B → (A ∨ E → (¬ B) ∧ C) → ¬ (A ∨ E) := by blast -definition lemma2 : ¬ B → (A ∨ E → B ∧ C) → ¬ (A ∨ E) := by blast -definition lemma3 : A → ¬ D → (A ∨ E → B → C ∧ D) → ¬ B := by blast -definition lemma4 : A → ¬ E → (A → B → E ∧ F) → ¬ B := by blast -definition lemma5 : (A → B) → ¬ B → ¬ A := by blast -definition lemma6 : (A → B ∧ C) → ¬ B → ¬ A := by blast diff --git a/tests/lean/run/blast_unit.lean b/tests/lean/run/blast_unit.lean new file mode 100644 index 0000000000..84ea94f015 --- /dev/null +++ b/tests/lean/run/blast_unit.lean @@ -0,0 +1,43 @@ +-- Testing all possible cases of [unit_action] +set_option blast.recursor false +variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop} + +-- H first, all pos +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) : B₄ := by blast +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₄) : B₃ := by blast +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₂ := by blast +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (a3 : A₃) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : B₁ := by blast + +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a2 : A₂) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₃ := by blast +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a1 : A₁) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₂ := by blast +example (H : A₁ → A₂ → A₃ → B₁ ∨ B₂ ∨ B₃ ∨ B₄) (a2 : A₂) (a3 : A₃) (n1 : ¬ B₁) (n2 : ¬ B₂) (n3 : ¬ B₃) (n3 : ¬ B₄) : ¬ A₁ := by blast + +-- 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 diff --git a/tests/lean/run/blast27.lean b/tests/lean/run/blast_unit_cc.lean similarity index 90% rename from tests/lean/run/blast27.lean rename to tests/lean/run/blast_unit_cc.lean index b46ec0d51a..9d7afa02ec 100644 --- a/tests/lean/run/blast27.lean +++ b/tests/lean/run/blast_unit_cc.lean @@ -1,4 +1,4 @@ --- Basic (propositional) forward chaining with conjunctive conclusions +-- Unit propagation with congruence closure constants (a b c d e : nat) constants (p : nat → Prop) constants (q : nat → nat → Prop) @@ -6,6 +6,8 @@ constants (f : nat → nat) set_option blast.recursor false set_option blast.subst false +-- The following tests require the unit preprocessor to work +/- definition lemma1 : a = d → b = e → p b → (p a → (¬ p e) ∧ p c) → ¬ p d := by blast definition lemma2a : ¬ p b → (p d → p b ∧ p c) → d = e → e = a → ¬ p a := by blast definition lemma2b : ¬ p (f b) → (p (f a) → p (f d) ∧ p (f c)) → b = d → ¬ p (f a) := by blast @@ -15,3 +17,4 @@ definition lemma4b : b = f b → ¬ p (f (f b)) → (p a → q c c ∧ q e c ∧ by blast definition lemma5 : p b → (p (f a) → (¬ p b) ∧ p e ∧ p c) → ¬ p (f a) := by blast definition lemma6 : ¬ (q b a) → d = a → (p a → p e ∧ (q b d) ∧ p c) → ¬ p a := by blast +-/