From 70150897341d472fd537056f60fad333caedfcbc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2014 10:49:36 -0800 Subject: [PATCH] fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices Signed-off-by: Leonardo de Moura --- src/library/simplifier/simplifier.cpp | 126 ++++++++++++++------------ tests/lean/simp24.lean.expected.out | 2 +- tests/lean/simp25.lean | 13 +++ tests/lean/simp25.lean.expected.out | 10 ++ tests/lean/simp26.lean | 19 ++++ tests/lean/simp26.lean.expected.out | 21 +++++ 6 files changed, 131 insertions(+), 60 deletions(-) create mode 100644 tests/lean/simp25.lean create mode 100644 tests/lean/simp25.lean.expected.out create mode 100644 tests/lean/simp26.lean create mode 100644 tests/lean/simp26.lean.expected.out diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 8e29a6c0d2..6d24fab848 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -130,7 +130,7 @@ class simplifier_fn { cache m_cache; max_sharing_fn m_max_sharing; congr_thms m_congr_thms; - unsigned m_contextual_depth; // number of contextual simplification steps in the current branch + unsigned m_next_idx; // index used to create fresh constants unsigned m_num_steps; // number of steps performed // Configuration @@ -145,19 +145,18 @@ class simplifier_fn { bool m_memoize; unsigned m_max_steps; - struct set_context { - flet m_set; - freset m_reset_cache; - set_context(simplifier_fn & s, context const & new_ctx):m_set(s.m_ctx, new_ctx), m_reset_cache(s.m_cache) {} - }; - struct updt_rule_set { - rewrite_rule_set & m_rs; + simplifier_fn & m_fn; rewrite_rule_set m_old; - updt_rule_set(rewrite_rule_set & rs, expr const & fact, expr const & proof):m_rs(rs), m_old(m_rs) { - m_rs.insert(g_local, fact, proof); + freset m_reset_cache; // must reset the cache whenever we update the rule set. + updt_rule_set(simplifier_fn & fn, expr const & fact, expr const & proof): + m_fn(fn), m_old(m_fn.m_rule_sets[0]), m_reset_cache(m_fn.m_cache) { + m_fn.m_rule_sets[0].insert(g_local, fact, proof); + } + ~updt_rule_set() { + m_fn.m_rule_sets[0] = m_old; + // Remark: m_reset_cache destructor will restore the cache } - ~updt_rule_set() { m_rs = m_old; } }; @@ -465,22 +464,21 @@ class simplifier_fn { if (!m_proofs_enabled) { // Contextual reasoning without proofs. expr dummy_proof; // we don't need a proof - updt_rule_set update(m_rule_sets[0], H, dummy_proof); + updt_rule_set update(*this, H, dummy_proof); result res_a = simplify(a); new_args[pos] = res_a.m_out; } else { // We have to introduce H in the context, so first we lift the free variables in \c a - flet set_depth(m_contextual_depth, m_contextual_depth+1); - expr H_proof = mk_constant(name(g_unique, m_contextual_depth)); - updt_rule_set update(m_rule_sets[0], H, H_proof); - freset m_reset_cache(m_cache); // must reset cache for the recursive call because we updated the rule_sets + flet set_depth(m_next_idx, m_next_idx+1); + expr H_proof = mk_constant(name(g_unique, m_next_idx)); + updt_rule_set update(*this, H, H_proof); result res_a = simplify(a); if (!ensure_homogeneous(a, res_a)) return simplify_app_default(e); // fallback to default congruence new_args[pos] = res_a.m_out; proof_args[info.get_pos_at_proof()] = a; proof_args[*info.get_new_pos_at_proof()] = new_args[pos]; - name C_name(g_C, m_contextual_depth); // H_name is a cryptic unique name + name C_name(g_C, m_next_idx); // H_name is a cryptic unique name proof_args[*info.get_proof_pos_at_proof()] = mk_lambda(C_name, H, abstract(get_proof(res_a), H_proof)); } } @@ -826,16 +824,18 @@ class simplifier_fn { lean_assert(is_constant(e)); if (m_unfold || m_eval) { auto obj = m_env->find_object(const_name(e)); - if (m_unfold && should_unfold(obj)) { - expr e = obj->get_value(); - if (m_single_pass) { - return result(e); - } else { - return simplify(e); + if (obj) { + if (m_unfold && should_unfold(obj)) { + expr e = obj->get_value(); + if (m_single_pass) { + return result(e); + } else { + return simplify(e); + } + } + if (m_eval && obj->is_builtin()) { + return result(obj->get_value()); } - } - if (m_eval && obj->is_builtin()) { - return result(obj->get_value()); } } return rewrite(e, result(e)); @@ -904,18 +904,20 @@ class simplifier_fn { // TODO(Leo) return result(e); } else { - set_context set(*this, extend(m_ctx, abst_name(e), abst_domain(e))); - result res_body = simplify(abst_body(e)); + flet set_depth(m_next_idx, m_next_idx+1); + expr fresh_const = mk_constant(name(g_unique, m_next_idx), abst_domain(e)); + expr b_c = instantiate(abst_body(e), fresh_const); + result res_body = simplify(b_c); lean_assert(!res_body.m_heq_proof); - expr new_body = res_body.m_out; - if (is_eqp(new_body, abst_body(e))) + expr new_body = res_body.m_out; + if (is_eqp(new_body, b_c)) return rewrite_lambda(e, result(e)); - expr out = mk_lambda(e, new_body); + expr out = mk_lambda(e, abstract(new_body, fresh_const)); if (!m_proofs_enabled || !res_body.m_proof) return rewrite_lambda(e, result(out)); expr body_type = infer_type(abst_body(e)); expr pr = mk_funext_th(abst_domain(e), mk_lambda(e, body_type), e, out, - mk_lambda(e, *res_body.m_proof)); + mk_lambda(e, abstract(*res_body.m_proof, fresh_const))); return rewrite_lambda(e, result(out, pr)); } } @@ -934,41 +936,38 @@ class simplifier_fn { // And rewrite B to B' using A' result res_d = simplify(d); ensure_homogeneous(d, res_d); - flet set_depth(m_contextual_depth, m_contextual_depth+1); - expr H_proof = mk_constant(name(g_unique, m_contextual_depth)); + flet set_depth(m_next_idx, m_next_idx+1); + expr H_proof = mk_constant(name(g_unique, m_next_idx)); + expr b_c = lower_free_vars(b, 1, 1); result res_b; { - updt_rule_set update(m_rule_sets[0], res_d.m_out, H_proof); - freset m_reset_cache(m_cache); // must reset cache for the recursive call because we updated the rule_sets - set_context set(*this, extend(m_ctx, abst_name(e), res_d.m_out)); - res_b = simplify(b); + updt_rule_set update(*this, res_d.m_out, H_proof); + res_b = simplify(b_c); } - ensure_homogeneous(b, res_b); - if (is_eqp(res_d.m_out, d) && is_eqp(res_b.m_out, b)) + ensure_homogeneous(b_c, res_b); + if (is_eqp(res_d.m_out, d) && is_eqp(res_b.m_out, b_c)) return rewrite(e, result(e)); - expr out = update_pi(e, res_d.m_out, res_b.m_out); + expr out = update_pi(e, res_d.m_out, lift_free_vars(res_b.m_out, 0, 1)); if (!m_proofs_enabled) return rewrite(e, result(out)); - name C_name(g_C, m_contextual_depth); // H_name is a cryptic unique name - expr proof = mk_imp_congr_th(d, lower_free_vars(b, 1, 1), - res_d.m_out, lower_free_vars(res_b.m_out, 1, 1), + name C_name(g_C, m_next_idx); // H_name is a cryptic unique name + expr proof = mk_imp_congr_th(d, b_c, res_d.m_out, res_b.m_out, get_proof(res_d), mk_lambda(C_name, res_d.m_out, abstract(get_proof(res_b), H_proof))); return rewrite(e, result(out, proof)); } else { // Simplify A -> B (when m_contextual == false) result res_d = simplify(d); ensure_homogeneous(d, res_d); - set_context set(*this, extend(m_ctx, abst_name(e), res_d.m_out)); - result res_b = simplify(b); - ensure_homogeneous(b, res_b); - if (is_eqp(res_d.m_out, d) && is_eqp(res_b.m_out, b)) + expr b_c = lower_free_vars(b, 1, 1); + result res_b = simplify(b_c); + ensure_homogeneous(b_c, res_b); + if (is_eqp(res_d.m_out, d) && is_eqp(res_b.m_out, b_c)) return rewrite(e, result(e)); - expr out = update_pi(e, res_d.m_out, res_b.m_out); + expr out = update_pi(e, res_d.m_out, lift_free_vars(res_b.m_out, 0, 1)); if (!m_proofs_enabled) return rewrite(e, result(out)); - expr proof = mk_imp_congr_th(d, lower_free_vars(b, 1, 1), - res_d.m_out, lower_free_vars(res_b.m_out, 1, 1), - get_proof(res_d), mk_lambda(g_H, res_d.m_out, get_proof(res_b))); + expr proof = mk_imp_congr_th(d, b_c, res_d.m_out, res_b.m_out, + get_proof(res_d), mk_lambda(g_H, res_d.m_out, lift_free_vars(get_proof(res_b), 0, 1))); return rewrite(e, result(out, proof)); } } else if (m_has_heq) { @@ -976,19 +975,21 @@ class simplifier_fn { return result(e); } else if (is_prop) { // Simplify (forall x : A, P x) - set_context set(*this, extend(m_ctx, abst_name(e), d)); - result res_body = simplify(b); + flet set_depth(m_next_idx, m_next_idx+1); + expr fresh_const = mk_constant(name(g_unique, m_next_idx), abst_domain(e)); + expr b_c = instantiate(b, fresh_const); + result res_body = simplify(b_c); lean_assert(!res_body.m_heq_proof); expr new_body = res_body.m_out; - if (is_eqp(new_body, b)) + if (is_eqp(new_body, b_c)) return rewrite(e, result(e)); - expr out = mk_pi(abst_name(e), d, new_body); + expr out = mk_pi(abst_name(e), d, abstract(new_body, fresh_const)); if (!m_proofs_enabled || !res_body.m_proof) return rewrite(e, result(out)); expr pr = mk_allext_th(d, mk_lambda(e, b), mk_lambda(e, abst_body(out)), - mk_lambda(e, *res_body.m_proof)); + mk_lambda(e, abstract(*res_body.m_proof, fresh_const))); return rewrite(e, result(out, pr)); } else { // if the environment does not contain heq axioms, then we don't simplify Pi's that are not forall's @@ -1046,6 +1047,13 @@ class simplifier_fn { } } + void set_ctx(context const & ctx) { + if (!is_eqp(m_ctx, ctx)) { + m_cache.clear(); + m_ctx = ctx; + } + } + void set_options(options const & o) { m_proofs_enabled = get_simplifier_proofs(o); m_contextual = get_simplifier_contextual(o); @@ -1071,11 +1079,11 @@ public: } m_rule_sets.insert(m_rule_sets.end(), rs, rs + num_rs); collect_congr_thms(); - m_contextual_depth = 0; + m_next_idx = 0; } expr_pair operator()(expr const & e, context const & ctx) { - set_context set(*this, ctx); + set_ctx(ctx); m_num_steps = 0; auto r = simplify(e); return mk_pair(r.m_out, get_proof(r)); diff --git a/tests/lean/simp24.lean.expected.out b/tests/lean/simp24.lean.expected.out index 80c1e3bdd9..07d65e5757 100644 --- a/tests/lean/simp24.lean.expected.out +++ b/tests/lean/simp24.lean.expected.out @@ -9,4 +9,4 @@ funext (λ x : ℕ, trans (imp_congr (refl (x = a)) (λ H : x = a, eq_id x)) (im λ x : ℕ, ⊤ funext (λ x : ℕ, trans (imp_congr (congr2 (eq x) (Nat::add_zeror a)) (λ H : x = a, eq_id a)) (imp_truer (x = a))) λ x : ℕ, a = 1 → x > 1 -funext (λ x : ℕ, imp_congr (congr1 1 (congr2 eq (Nat::add_zeror a))) (λ C::1 : a = 1, congr2 (Nat::gt x) C::1)) +funext (λ x : ℕ, imp_congr (congr1 1 (congr2 eq (Nat::add_zeror a))) (λ C::2 : a = 1, congr2 (Nat::gt x) C::2)) diff --git a/tests/lean/simp25.lean b/tests/lean/simp25.lean new file mode 100644 index 0000000000..be95735f0a --- /dev/null +++ b/tests/lean/simp25.lean @@ -0,0 +1,13 @@ +rewrite_set simple +add_rewrite eq_id imp_truel imp_truer Nat::add_zeror : simple +(* add_congr_theorem("simple", "and_congrr") *) +variables a b : Nat +variables f : (Nat → Nat → Bool) → Bool + +(* +local t = parse_lean('λ x, x = 1 ∧ f (λ y z, y + z > x)') +local t2, pr = simplify(t, "simple") +print(t2) +print(pr) +get_environment():type_check(pr) +*) diff --git a/tests/lean/simp25.lean.expected.out b/tests/lean/simp25.lean.expected.out new file mode 100644 index 0000000000..a0eb59589f --- /dev/null +++ b/tests/lean/simp25.lean.expected.out @@ -0,0 +1,10 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: f +λ x : ℕ, x = 1 ∧ f (λ y z : ℕ, y + z > 1) +funext (λ x : ℕ, + and_congrr + (λ C::2 : f (λ y z : ℕ, y + z > x), refl (x = 1)) + (λ C::2 : x = 1, congr2 f (funext (λ y : ℕ, funext (λ z : ℕ, congr2 (Nat::gt (y + z)) C::2))))) diff --git a/tests/lean/simp26.lean b/tests/lean/simp26.lean new file mode 100644 index 0000000000..1bb309a90e --- /dev/null +++ b/tests/lean/simp26.lean @@ -0,0 +1,19 @@ +rewrite_set simple +add_rewrite eq_id imp_truel imp_truer Nat::add_zeror : simple +variables a b : Nat +variable f : (Nat → Nat) → Nat +(* +local t = parse_lean('λ x, a + 0 = 1 → x > f (λ y, y + a)') +local t2, pr = simplify(t, "simple") +print(t2) +print(pr) +get_environment():type_check(pr) +*) + +(* +local t = parse_lean('λ x, a + 0 = 1 → x = 2 → x > f (λ y, y + a + x)') +local t2, pr = simplify(t, "simple") +print(t2) +print(pr) +get_environment():type_check(pr) +*) diff --git a/tests/lean/simp26.lean.expected.out b/tests/lean/simp26.lean.expected.out new file mode 100644 index 0000000000..20aaa415e5 --- /dev/null +++ b/tests/lean/simp26.lean.expected.out @@ -0,0 +1,21 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: f +λ x : ℕ, a = 1 → x > f (λ y : ℕ, y + 1) +funext (λ x : ℕ, + imp_congr + (congr1 1 (congr2 eq (Nat::add_zeror a))) + (λ C::2 : a = 1, congr2 (Nat::gt x) (congr2 f (funext (λ y : ℕ, congr2 (Nat::add y) C::2))))) +λ x : ℕ, a = 1 → x = 2 → 2 > f (λ y : ℕ, y + 1 + 2) +funext (λ x : ℕ, + imp_congr + (congr1 1 (congr2 eq (Nat::add_zeror a))) + (λ C::2 : a = 1, + imp_congr + (refl (x = 2)) + (λ C::3 : x = 2, + congr (congr2 Nat::gt C::3) + (congr2 f + (funext (λ y : ℕ, congr (congr2 Nat::add (congr2 (Nat::add y) C::2)) C::3))))))