From e4579b93e454112808e0801552edffd64a2d159e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 13:35:00 -0800 Subject: [PATCH] fix(library/elaborator): try first projection before imitation in the higher-order unifier 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 --- src/library/elaborator/elaborator.cpp | 28 +++++++++++++-------------- tests/lean/induct.lean | 6 ++++++ tests/lean/induct.lean.expected.out | 8 ++++++++ 3 files changed, 28 insertions(+), 14 deletions(-) create mode 100644 tests/lean/induct.lean create mode 100644 tests/lean/induct.lean.expected.out diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 7db68e73f..6a00621f7 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -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); + } } /** diff --git a/tests/lean/induct.lean b/tests/lean/induct.lean new file mode 100644 index 000000000..240616b30 --- /dev/null +++ b/tests/lean/induct.lean @@ -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) _ diff --git a/tests/lean/induct.lean.expected.out b/tests/lean/induct.lean.expected.out new file mode 100644 index 000000000..6067a56ec --- /dev/null +++ b/tests/lean/induct.lean.expected.out @@ -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