From 069e5edf6bd376b6314faab6ede098a262e0e2bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Jan 2014 12:01:01 -0800 Subject: [PATCH] fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic Signed-off-by: Leonardo de Moura --- src/builtin/heq.lean | 3 ++ src/builtin/obj/heq.olean | Bin 2402 -> 2543 bytes src/library/heq_decls.cpp | 1 + src/library/heq_decls.h | 3 ++ src/library/simplifier/simplifier.cpp | 57 +++++++++++-------------- src/library/simplifier/simplifier.h | 43 ++++++++++++++----- src/library/tactic/simplify_tactic.cpp | 18 ++++++-- tests/lean/errmsg1.lean.expected.out | 2 +- tests/lean/simp.lean.expected.out | 8 ++-- tests/lean/simp3.lean.expected.out | 8 ++-- tests/lean/simp6.lean.expected.out | 2 +- 11 files changed, 88 insertions(+), 57 deletions(-) diff --git a/src/builtin/heq.lean b/src/builtin/heq.lean index 9912bc3ee9..4547ea64f0 100644 --- a/src/builtin/heq.lean +++ b/src/builtin/heq.lean @@ -13,6 +13,9 @@ theorem to_heq {A : TypeU} {a b : A} (H : a = b) : a == b theorem hrefl {A : TypeU} (a : A) : a == a := to_heq (refl a) +theorem heqt_elim {a : Bool} (H : a == true) : a +:= eqt_elim (to_eq H) + axiom hsymm {A B : TypeU} {a : A} {b : B} : a == b → b == a axiom htrans {A B C : TypeU} {a : A} {b : B} {c : C} : a == b → b == c → a == c diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index 64d04753f2f2318d8386096790c8d3d2afae5732..b32c74f30040025325b2c98e062cc8d232818185 100644 GIT binary patch literal 2543 zcmZWr+fEcg5bf@fWn91uctfMcz(QhtKoa!{v#e3z0W@-nMk5X|D;sxrV0Iwz>LoG$ zfq!eAQ`0j8OhR$Gs=B)RR8>RLjiY|M(~V93*-q~uNi*|3PWy4!CT#qj1y=9@Y%q%lB8?QO7DOQ2xskDl0{i3>0@c#!UA{A2Ur>t zo$!q9{21zdWI1bx3OgORPP=W)43@(<6+fm9VIjhXl?eDMI-f@ea4u?Po+v6>nQ)=uPQp21d7 zavzSC{Y?@vMf}c85HvDDJG5|=${g7*m3F9DkohI#&EogrH&UxfZPB3&r`jg9zC?4f3Y8CQkNTbCI32{stxB(mMTFZ)GE*8h z3j@Nu+>6_WPw}c5)*Vp0VM;bz`=}qEWMnvib`el1Nqp-Gp)FOBTDS>=RW2LQjY9C< zCOb`V;HWcd%~3G_%vRI<{w0PAa6jS zH<+gXq)z4sZs2KbCGt;at5nPy8X2=$`c6l>MV~%D+Waxcv5) QK)Lw-zwYn7!9RKb0f8>SRR910 literal 2402 zcmZWrT~8B16rGusb}irs_=UzNC?_3n`iy{{es5 zd(PeI4$#EwnLBsxJ#+4z)vS{y-DbO!n&M~MC#P92H^*tOn|4gG+D>wFk@SpfrDvw% zmQCdLE>F|1Miwi2vf>is1X=+6Y~)t5tYggD$tfK$&f4uPPx5xw#nQS)gQw;rER9J9 ztnsrbL!Zwqwf5<-Gm&dIo5svySw&U+F*O(q6W6U|z%TH59qQXAnX;!#6QBCCSM;^Mhg$Q0~S4 z0^_n5+2Iv@Pk6?wfBOzNWu{2!5kmiixo{qKrFMs0$3D&uM^l= z%aI~)3@(4yh87+f+G4aouVls+1sw=>Fbj8h7N+KFzJyzPqh<46((Q+LUqLWL_~3!6 zQS$@@9B@m3XM$2})&h2vj+b#!DIuha-3E-tc}mmbsen>J>LBa>>V>41U*V9xWuKSr zkf0UaTdTOHtOksmKt|;uW7gD&4S%vBKwUtEnEvR}G?-R!KBj#KxXFa1&dFEV%hNc+ zjU_~@0D5m8q*qC8GN4SS-s^hIA)D%9?RmF-k@otjaa%GgvLnXrXSpdiz798#{QY6t zH2nH)nW~@PT1aAXSB}x70iJ+mh2onWEE$i@&!5qS9W1)%Ha#Mh2 z7376R=oc7@!Y&pst(2-pNU3Zom3k=^kL~*TS(I!Q)e9fZRzJ8OD)CNWfS-Q3u3yd* zX5-ec-_q|b1pOq3n9Mi{%(>2Wcp=WuXB4G2J3bXxzv0(O;nUf`Iwj=A2ZY=3t`Y74 zUJ~vCZj89qeE{?Kb%ehlLs3e5fo1T4n8ErDjP`4!cr6V9MVln$Ao#klMM0lp*MDoQ z3V}Q=82LBWm?N0)r6M&6oex9z5Wx6vKu2?=JjZ_*@4|BhQx@b6X!Hg%jGxk%$z)fo z#!;gF47Mu8wBaUmE|hTr)OW{v>ZRxbWLfQ|pR;vgIKnyOD@r;Y|BAp}rtIb$iiTq* zC^2<}l@CTQh7CU$3j(wgg2D$wa(Y4Jh|5g)@~Ha9H=O^5SrPKbU*d->`2GLbJ^Y0K GSN#WdBCkIH diff --git a/src/library/heq_decls.cpp b/src/library/heq_decls.cpp index 574f7d645b..d96b03b869 100644 --- a/src/library/heq_decls.cpp +++ b/src/library/heq_decls.cpp @@ -11,6 +11,7 @@ MK_CONSTANT(heq_eq_fn, name("heq_eq")); MK_CONSTANT(to_eq_fn, name("to_eq")); MK_CONSTANT(to_heq_fn, name("to_heq")); MK_CONSTANT(hrefl_fn, name("hrefl")); +MK_CONSTANT(heqt_elim_fn, name("heqt_elim")); MK_CONSTANT(hsymm_fn, name("hsymm")); MK_CONSTANT(htrans_fn, name("htrans")); MK_CONSTANT(hcongr_fn, name("hcongr")); diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index e86409bb44..32336d3c2f 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -21,6 +21,9 @@ inline expr mk_to_heq_th(expr const & e1, expr const & e2, expr const & e3, expr expr mk_hrefl_fn(); bool is_hrefl_fn(expr const & e); inline expr mk_hrefl_th(expr const & e1, expr const & e2) { return mk_app({mk_hrefl_fn(), e1, e2}); } +expr mk_heqt_elim_fn(); +bool is_heqt_elim_fn(expr const & e); +inline expr mk_heqt_elim_th(expr const & e1, expr const & e2) { return mk_app({mk_heqt_elim_fn(), e1, e2}); } expr mk_hsymm_fn(); bool is_hsymm_fn(expr const & e); inline expr mk_hsymm_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({mk_hsymm_fn(), e1, e2, e3, e4, e5}); } diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index de0a945082..0c6357f2b2 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -121,20 +121,6 @@ static name g_unique = name::mk_internal_unique_name(); class simplifier_cell::imp { friend class simplifier_cell; friend class simplifier; - struct result { - expr m_expr; // the result of a simplification step - optional m_proof; // a proof that the result is equal to the input (when m_proofs_enabled) - bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality) - result() {} - explicit result(expr const & out, bool heq_proof = false): - m_expr(out), m_heq_proof(heq_proof) {} - result(expr const & out, expr const & pr, bool heq_proof = false): - m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} - result(expr const & out, optional const & pr, bool heq_proof = false): - m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} - bool is_heq_proof() const { return m_heq_proof; } - result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof); } - }; typedef std::vector rule_sets; typedef expr_map cache; @@ -931,6 +917,8 @@ class simplifier_cell::imp { if (!d_res.m_proof) { // No proof available. So d should be definitionally equal to True d_proof = mk_trivial(); + } else if (d_res.m_heq_proof) { + d_proof = mk_heqt_elim_th(d, *d_res.m_proof); } else { d_proof = mk_eqt_elim_th(d, *d_res.m_proof); } @@ -1502,7 +1490,7 @@ public: m_next_idx = 0; } - expr_pair operator()(expr const & e, context const & ctx, optional const & menv) { + result operator()(expr const & e, context const & ctx, optional const & menv) { set_ctx(ctx); if (m_menv.update(menv)) m_cache.clear(); @@ -1510,7 +1498,10 @@ public: m_depth = 0; try { auto r = simplify(e); - return mk_pair(r.m_expr, get_proof(r)); + if (m_proofs_enabled && !r.get_proof()) + return r.update_proof(get_proof(r)); + else + return r; } catch (stack_space_exception & ex) { throw simplifier_stack_space_exception(); } @@ -1522,7 +1513,7 @@ simplifier_cell::simplifier_cell(ro_environment const & env, options const & o, m_ptr(new imp(env, o, num_rs, rs, monitor)) { } -expr_pair simplifier_cell::operator()(expr const & e, context const & ctx, optional const & menv) { +simplifier_cell::result simplifier_cell::operator()(expr const & e, context const & ctx, optional const & menv) { return m_ptr->operator()(e, ctx, menv); } void simplifier_cell::clear() { return m_ptr->m_cache.clear(); } @@ -1547,17 +1538,17 @@ ro_simplifier::ro_simplifier(weak_ref const & r) { m_ptr = r.lock(); } -expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_rs, rewrite_rule_set const * rs, - optional const & menv, - std::shared_ptr const & monitor) { +simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, + unsigned num_rs, rewrite_rule_set const * rs, + optional const & menv, + std::shared_ptr const & monitor) { return simplifier(env, opts, num_rs, rs, monitor)(e, ctx, menv); } -expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_ns, name const * ns, - optional const & menv, - std::shared_ptr const & monitor) { +simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, + unsigned num_ns, name const * ns, + optional const & menv, + std::shared_ptr const & monitor) { buffer rules; for (unsigned i = 0; i < num_ns; i++) rules.push_back(get_rewrite_rule_set(env, ns[i])); @@ -1736,16 +1727,17 @@ static int mk_simplifier(lua_State * L) { static int simplifier_apply(lua_State * L) { int nargs = lua_gettop(L); - expr_pair r; + simplifier::result r; if (nargs == 2) r = to_simplifier(L, 1)(to_expr(L, 2), context(), none_ro_menv()); else if (nargs == 3) r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), none_ro_menv()); else r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), some_ro_menv(to_metavar_env(L, 4))); - push_expr(L, r.first); - push_expr(L, r.second); - return 2; + push_expr(L, r.get_expr()); + push_optional_expr(L, r.get_proof()); + lua_pushboolean(L, r.is_heq_proof()); + return 3; } static int simplifier_clear(lua_State * L) { to_simplifier(L, 1)->clear(); return 0; } @@ -1790,9 +1782,10 @@ static int simplify_core(lua_State * L, ro_shared_environment const & env) { if (nargs >= 5) ctx = to_context(L, 5); auto r = simplify(e, env, ctx, opts, rules.size(), rules.data()); - push_expr(L, r.first); - push_expr(L, r.second); - return 2; + push_expr(L, r.get_expr()); + push_optional_expr(L, r.get_proof()); + lua_pushboolean(L, r.is_heq_proof()); + return 3; } static int simplify(lua_State * L) { diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index 29102d174f..5924e2922e 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -21,10 +21,30 @@ class simplifier_cell { class imp; std::unique_ptr m_ptr; public: + /** + \brief Simplification result + */ + class result { + friend class imp; + expr m_expr; // new expression + optional m_proof; // a proof that the m_expr is equal to the input (when m_proofs_enabled) + bool m_heq_proof; // true if the proof has type lhs == rhs (i.e., it is a heterogeneous equality) + explicit result(expr const & out, bool heq_proof = false):m_expr(out), m_heq_proof(heq_proof) {} + result(expr const & out, expr const & pr, bool heq_proof = false):m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} + result(expr const & out, optional const & pr, bool heq_proof = false): + m_expr(out), m_proof(pr), m_heq_proof(heq_proof) {} + result update_expr(expr const & new_e) const { return result(new_e, m_proof, m_heq_proof); } + result update_proof(expr const & new_pr) const { return result(m_expr, new_pr, m_heq_proof); } + public: + result() {} + expr get_expr() const { return m_expr; } + optional get_proof() const { return m_proof; } + bool is_heq_proof() const { return m_heq_proof; } + }; + simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, std::shared_ptr const & monitor); - - expr_pair operator()(expr const & e, context const & ctx, optional const & menv); + result operator()(expr const & e, context const & ctx, optional const & menv); void clear(); unsigned get_depth() const; @@ -38,11 +58,12 @@ class simplifier { friend class ro_simplifier; std::shared_ptr m_ptr; public: + typedef simplifier_cell::result result; simplifier(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, std::shared_ptr const & monitor); simplifier_cell * operator->() const { return m_ptr.get(); } simplifier_cell & operator*() const { return *(m_ptr.get()); } - expr_pair operator()(expr const & e, context const & ctx, optional const & menv) { + result operator()(expr const & e, context const & ctx, optional const & menv) { return (*m_ptr)(e, ctx, menv); } }; @@ -116,13 +137,13 @@ public: virtual void rethrow() const; }; -expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts, - unsigned num_rs, rewrite_rule_set const * rs, - optional const & menv = none_ro_menv(), - std::shared_ptr const & monitor = std::shared_ptr()); -expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_ns, name const * ns, - optional const & menv = none_ro_menv(), - std::shared_ptr const & monitor = std::shared_ptr()); +simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts, + unsigned num_rs, rewrite_rule_set const * rs, + optional const & menv = none_ro_menv(), + std::shared_ptr const & monitor = std::shared_ptr()); +simplifier::result simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, + unsigned num_ns, name const * ns, + optional const & menv = none_ro_menv(), + std::shared_ptr const & monitor = std::shared_ptr()); void open_simplifier(lua_State * L); } diff --git a/src/library/tactic/simplify_tactic.cpp b/src/library/tactic/simplify_tactic.cpp index 6dfa1347ca..5fe14af0c8 100644 --- a/src/library/tactic/simplify_tactic.cpp +++ b/src/library/tactic/simplify_tactic.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/sexpr/option_declarations.h" #include "kernel/type_checker.h" #include "kernel/kernel.h" +#include "library/heq_decls.h" #include "library/simplifier/simplifier.h" #include "library/tactic/tactic.h" @@ -51,12 +52,21 @@ static optional simplify_tactic(ro_environment const & env, io_stat rule_sets.push_back(get_rewrite_rule_set(env, ns[i])); } - expr conclusion = g.get_conclusion(); - auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv)); - expr new_conclusion = r.first; - expr eq_proof = r.second; + expr conclusion = g.get_conclusion(); + auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv)); + expr new_conclusion = r.get_expr(); if (new_conclusion == g.get_conclusion()) return optional(s); + expr eq_proof; + if (!r.get_proof()) { + // TODO(Leo): we should create a "by simplifier" proof + // For now, we just fail + return none_proof_state(); + } else { + eq_proof = *r.get_proof(); + } + if (r.is_heq_proof()) + eq_proof = mk_to_eq_th(Bool, conclusion, new_conclusion, eq_proof); bool solved = is_true(new_conclusion); goals rest_gs = tail(s.get_goals()); goals new_gs; diff --git a/tests/lean/errmsg1.lean.expected.out b/tests/lean/errmsg1.lean.expected.out index d67bf020e8..9add47b4f3 100644 --- a/tests/lean/errmsg1.lean.expected.out +++ b/tests/lean/errmsg1.lean.expected.out @@ -8,6 +8,6 @@ errmsg1.lean:4:10: error: invalid expression, it still contains metavariables af errmsg1.lean:5:11: error: failed to synthesize metavar M::0, it could not be synthesized by type inference and its type is not a proposition λ (A : Type) (x : A), ?M::0 errmsg1.lean:6:3: error: unsolved metavar M::0 -errmsg1.lean:8:0: error: invalid definition, type still contains metavariables after elaboration +errmsg1.lean:8:0: error: failed to synthesize metavar M::1, it could not be synthesized by type inference and its type is not a proposition ∀ x : ?M::1, @eq ?M::1 x x errmsg1.lean:8:22: error: unsolved metavar M::1 diff --git a/tests/lean/simp.lean.expected.out b/tests/lean/simp.lean.expected.out index 5a184d68ce..5ca054bac4 100644 --- a/tests/lean/simp.lean.expected.out +++ b/tests/lean/simp.lean.expected.out @@ -8,7 +8,7 @@ Assumed: b Axfg : ∀ x : ℕ, g x x = x Axf1 : ∀ x : ℕ, f (f x) = x -a trans (congr2 (g a) (Axf1 a)) (Axfg a) -g a a congr2 (g a) (Axf1 a) -a trans (congr2 (g a) (Axf1 a)) (Axfg a) -a trans (congr2 (g a) (Axf1 a)) (Axfg a) +a trans (congr2 (g a) (Axf1 a)) (Axfg a) false +g a a congr2 (g a) (Axf1 a) false +a trans (congr2 (g a) (Axf1 a)) (Axfg a) false +a trans (congr2 (g a) (Axf1 a)) (Axfg a) false diff --git a/tests/lean/simp3.lean.expected.out b/tests/lean/simp3.lean.expected.out index da69ab0548..2407e2647a 100644 --- a/tests/lean/simp3.lean.expected.out +++ b/tests/lean/simp3.lean.expected.out @@ -30,7 +30,7 @@ trans (congr (congr2 (λ x : ℕ, eq ((λ x : ℕ, x + 10) x)) (congr2 (λ x : ℕ, x + 10) (if_a_a (a > 0) b))) (eq_id (b + 10)) a * a + (a * b + (b * a + b * b)) -⊤ → ⊥ refl (⊤ → ⊥) -⊤ → ⊤ refl (⊤ → ⊤) -⊥ → ⊥ refl (⊥ → ⊥) -⊥ refl ⊥ +⊤ → ⊥ refl (⊤ → ⊥) false +⊤ → ⊤ refl (⊤ → ⊤) false +⊥ → ⊥ refl (⊥ → ⊥) false +⊥ refl ⊥ false diff --git a/tests/lean/simp6.lean.expected.out b/tests/lean/simp6.lean.expected.out index aa1e36a658..be42381745 100644 --- a/tests/lean/simp6.lean.expected.out +++ b/tests/lean/simp6.lean.expected.out @@ -2,4 +2,4 @@ Set: pp::unicode Assumed: a Assumed: b -⊤ trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b)) +⊤ trans (congr2 (eq (a + b)) (Nat::add_comm b a)) (eq_id (a + b)) false