michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/blast/unit): quantified and non-Prop facts

Browse source
This commit is contained in:
Daniel Selsam 2015-11-28 15:01:10 -08:00 committed by Leonardo de Moura
parent c604333af2
commit 0df4556eb5
2 changed files with 21 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/blast/unit/unit_action.cpp
View file

@ -29,13 +29,13 @@ bool is_lemma(expr const & _type) {
has_antecedent = true;
type = binding_body(type);
}
if (has_antecedent && !is_pi(type)) return true;
if (has_antecedent) 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);
return !is_lemma(type);
}
expr flip(expr const & e) {
@ -143,11 +143,14 @@ bool can_propagate(expr const & _type, buffer<expr, 2> & to_watch) {
unsigned num_watching = 0;
unit_branch_extension & ext = get_extension();
bool missing_non_Prop = false;
/* 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) {
/* We do not support non-Prop antecedents since we cannot negate them */
if (!is_prop(binding_domain(type))) missing_non_Prop = true;
to_watch.push_back(binding_domain(type));
num_watching++;
if (num_watching == 2) return false;
@ -173,7 +176,7 @@ bool can_propagate(expr const & _type, buffer<expr, 2> & to_watch) {
num_watching++;
if (num_watching == 2) return false;
}
return true;
return !missing_non_Prop;
}
action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr const & _proof) {
@ -184,7 +187,6 @@ action_result unit_lemma(hypothesis_idx hidx, expr const & _type, expr const & _
list<expr> 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); });
}

15
tests/lean/run/blast_unit_edges.lean Normal file
View file

@ -0,0 +1,15 @@
-- Testing all possible cases of [unit_action]
set_option blast.recursor false
universes l1 l2
variables {A B C : Prop}
variables {X : Type.{l1}} {Y : Type.{l2}}
variables {P : Y → Prop}
-- Types as antecedents
example (H : X → A) (x : X) : A := by blast
example (H : X → A → B) (x : X) (nb : ¬ B) : ¬ A := by blast
example (H : A → X → B → C) (x : X) (a : A) (nc : ¬ C) : ¬ B := by blast
-- Universally quantified facts
example (H : A → X → B → ∀ y : Y, P y) (x : X) (a : A) (nc : ¬ ∀ y : Y, P y) : ¬ B := by blast
example (H : A → X → B → ¬ ∀ y : Y, P y) (x : X) (a : A) (nc : ∀ y : Y, P y) : ¬ B := by blast