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

fix(library/elaborator): try first projection before imitation in the higher-order unifier

Browse source 
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-06 13:35:00 -08:00
parent ef321e730f
commit e4579b93e4
3 changed files with 28 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/library/elaborator/elaborator.cpp
View file

@ -908,20 +908,6 @@ class elaborator::imp {
arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs));
push_active(ucs);
}
// Add projections
for (unsigned i = 1; i < num_a; i++) {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
state new_state(m_state);
justification new_assumption = mk_assumption();
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
expr new_a = arg(a, i);
expr new_b = b;
if (!is_lhs)
swap(new_a, new_b);
push_new_constraint(new_state.m_active_cnstrs, is_eq(c), ctx, new_a, new_b, new_assumption);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, proj, new_assumption);
new_cs->push_back(new_state, new_assumption);
}
// Add imitation
state new_state(m_state);
justification new_assumption = mk_assumption();
@ -987,6 +973,20 @@ class elaborator::imp {
}
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, imitation, new_assumption);
new_cs->push_back(new_state, new_assumption);
// Add projections
for (unsigned i = 1; i < num_a; i++) {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
state new_state(m_state);
justification new_assumption = mk_assumption();
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
expr new_a = arg(a, i);
expr new_b = b;
if (!is_lhs)
swap(new_a, new_b);
push_new_constraint(new_state.m_active_cnstrs, is_eq(c), ctx, new_a, new_b, new_assumption);
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, proj, new_assumption);
new_cs->push_back(new_state, new_assumption);
}
}
/**

6
tests/lean/induct.lean Normal file
View file

@ -0,0 +1,6 @@
import macros
import tactic
using Nat
theorem add_comm2 (a b : Nat) : a + b = b + a
:= induction_on b (by skip) _

8
tests/lean/induct.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Imported 'macros'
Imported 'tactic'
Using: Nat
induct.lean:7:0: error: invalid tactic command, unexpected end of file
Proof state:
a : ℕ, b : ℕ, n : ℕ, iH : a + n = n + a ⊢ a + (n + 1) = n + 1 + a