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

fix(library/unifier): non-termination

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-04 10:32:01 -07:00
parent a97f82be1a
commit b94ce412ae
2 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/unifier.cpp
View file

@ -596,19 +596,16 @@ struct unifier_fn {
rhs = m_tc.whnf(rhs); rhs = m_tc.whnf(rhs);
lhs = m_tc.whnf(lhs); lhs = m_tc.whnf(lhs);
// We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) {
add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
return true;
}
// If lhs or rhs were updated, then invoke is_def_eq again. // If lhs or rhs were updated, then invoke is_def_eq again.
if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) { if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
// some metavariables were instantiated, try is_def_eq again // some metavariables were instantiated, try is_def_eq again
return is_def_eq(lhs, rhs, new_jst); return is_def_eq(lhs, rhs, new_jst);
} }
if (is_meta(lhs) && is_meta(rhs)) { // We delay constraints where lhs or rhs are of the form (elim ... (?m ...))
if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) {
add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
} else if (is_meta(lhs) && is_meta(rhs)) {
// flex-flex constraints are delayed the most. // flex-flex constraints are delayed the most.
add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs); add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs);
} else if (is_meta(lhs) || is_meta(rhs)) { } else if (is_meta(lhs) || is_meta(rhs)) {

8
tests/lean/run/tactic23.lean
View file

@ -26,5 +26,11 @@ check 2 + 3
-- Define an assump as an alias for the eassumption tactic -- Define an assump as an alias for the eassumption tactic
definition assump : tactic := eassumption definition assump : tactic := eassumption
theorem T {p : nat → Bool} {a : nat } (H : p (a+1)) : ∃ x, p (succ x) theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
:= by apply exists_intro; assump := by apply exists_intro; assump
definition is_zero [inline] (n : nat)
:= nat_rec true (λ n r, false) n
theorem T2 : ∃ a, (is_zero a) = true
:= by apply exists_intro; apply refl