From 039afb4578146044b9b17900fab92beb9ad3d76a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2015 11:10:34 -0800 Subject: [PATCH] feat(frontends/lean): treat "proof t qed" as alias for "by exact t" --- hott/algebra/precategory/yoneda.hlean | 33 ++++++------ hott/init/axioms/funext_varieties.hlean | 4 +- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_exprs.cpp | 3 +- src/frontends/lean/elaborator.cpp | 19 ------- src/frontends/lean/elaborator.h | 1 - src/frontends/lean/proof_qed_elaborator.cpp | 57 --------------------- src/frontends/lean/proof_qed_elaborator.h | 22 -------- src/library/annotation.cpp | 6 --- src/library/annotation.h | 4 -- tests/lean/run/div2.lean | 4 +- tests/lean/run/proof_qed_nested_tac.lean | 6 +++ 12 files changed, 30 insertions(+), 131 deletions(-) delete mode 100644 src/frontends/lean/proof_qed_elaborator.cpp delete mode 100644 src/frontends/lean/proof_qed_elaborator.h create mode 100644 tests/lean/run/proof_qed_nested_tac.lean diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index a340d18f2..87e1becb6 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -20,18 +20,18 @@ namespace yoneda (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2) : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 := calc - _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc - ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : assoc - ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : assoc - ... = _ : assoc + _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : by rewrite -assoc + ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : by rewrite -assoc + ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _) + ... = _ : by rewrite (assoc f2 f3 f4) --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set := functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2) (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1)) - proof - (λ(x : Cᵒᵖ ×c C), eq_of_homotopy (λ(h : homset x.1 x.2), !id_left ⬝ !id_right)) - qed + begin + intro x, apply eq_of_homotopy, intro h, exact (!id_left ⬝ !id_right) + end begin intros (x, y, z, g, f), apply eq_of_homotopy, intro h, exact (representable_functor_assoc g.2 f.2 h f.1 g.1), @@ -48,22 +48,23 @@ namespace functor functor.mk (λd, F (c,d)) (λd d' g, F (id, g)) (λd, !respect_id) - (λd₁ d₂ d₃ g' g, proof calc + (λd₁ d₂ d₃ g' g, calc F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : {(id_comp c)⁻¹} ... = F ((id,g') ∘ (id, g)) : idp - ... = F (id,g') ∘ F (id, g) : respect_comp F qed) + ... = F (id,g') ∘ F (id, g) : by rewrite (respect_comp F)) + local abbreviation Fob := @functor_curry_ob definition functor_curry_hom ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' := nat_trans.mk (λd, F (f, id)) - (λd d' g, proof calc + (λd d' g, calc F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F - ... = F (f, g ∘ id) : {id_left f} - ... = F (f, g) : {id_right g} - ... = F (f ∘ id, g) : {(id_right f)⁻¹} - ... = F (f ∘ id, id ∘ g) : {(id_left g)⁻¹} - ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ - qed) + ... = F (f, g ∘ id) : by rewrite id_left + ... = F (f, g) : by rewrite id_right + ... = F (f ∘ id, g) : by rewrite id_right + ... = F (f ∘ id, id ∘ g) : by rewrite id_left + ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ) + local abbreviation Fhom := @functor_curry_hom definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) : diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index 776a8bf01..46026758a 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -97,9 +97,9 @@ theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} := λ A B f g, let eq_to_f := (λ g' x, f = g') in let sim2path := homotopy_ind f eq_to_f idp in - have t1 : sim2path f (homotopy.refl f) = idp, + assert t1 : sim2path f (homotopy.refl f) = idp, proof homotopy_ind_comp f eq_to_f idp qed, - have t2 : apD10 (sim2path f (homotopy.refl f)) = (homotopy.refl f), + assert t2 : apD10 (sim2path f (homotopy.refl f)) = (homotopy.refl f), proof ap apD10 t1 qed, have sect : apD10 ∘ (sim2path g) ∼ id, proof (homotopy_ind f (λ g' x, apD10 (sim2path g' x) = x) t2) g qed, diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 990c2b0b9..7f93527b3 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -5,7 +5,7 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp -coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp +coercion_elaborator.cpp info_tactic.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp parse_tactic_location.cpp parse_rewrite_tactic.cpp type_util.cpp elaborator_exception.cpp) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index e726adda8..b76f8acaa 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -271,8 +271,9 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & } static expr parse_proof_qed_core(parser & p, pos_info const & pos) { - expr r = p.save_pos(mk_proof_qed_annotation(p.parse_expr()), pos); + expr r = p.parse_expr(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); + r = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos); return r; } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a4adb7f96..9d4579998 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -46,7 +46,6 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/elaborator.h" -#include "frontends/lean/proof_qed_elaborator.h" #include "frontends/lean/calc_proof_elaborator.h" #include "frontends/lean/info_tactic.h" #include "frontends/lean/begin_end_ext.h" @@ -287,8 +286,6 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra return visit_by(e, some_expr(t), cs); } else if (is_calc_annotation(e)) { return visit_calc_proof(e, some_expr(t), cs); - } else if (is_proof_qed_annotation(e)) { - return visit_proof_qed(e, some_expr(t), cs); } else { return visit(e, cs); } @@ -336,20 +333,6 @@ expr elaborator::visit_calc_proof(expr const & e, optional const & t, cons return m; } -expr elaborator::visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs) { - lean_assert(is_proof_qed_annotation(e)); - info_manager * im = nullptr; - if (infom()) - im = &m_pre_info_data; - pair ecs = visit(get_annotation_arg(e)); - expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); - register_meta(m); - constraint c = mk_proof_qed_cnstr(env(), m, ecs.first, ecs.second, m_unifier_config, - im, m_relax_main_opaque); - cs += c; - return m; -} - static bool is_implicit_pi(expr const & e) { if (!is_pi(e)) return false; @@ -1329,8 +1312,6 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit_by(e, none_expr(), cs); } else if (is_calc_annotation(e)) { return visit_calc_proof(e, none_expr(), cs); - } else if (is_proof_qed_annotation(e)) { - return visit_proof_qed(e, none_expr(), cs); } else if (is_no_info(e)) { flet let(m_no_info, true); return visit(get_annotation_arg(e), cs); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index e30227ac0..4437f434d 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -111,7 +111,6 @@ class elaborator : public coercion_info_manager { expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs); expr visit_choice(expr const & e, optional const & t, constraint_seq & cs); expr visit_by(expr const & e, optional const & t, constraint_seq & cs); - expr visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs); expr visit_calc_proof(expr const & e, optional const & t, constraint_seq & cs); expr add_implict_args(expr e, constraint_seq & cs, bool relax); pair ensure_fun(expr f, constraint_seq & cs); diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp deleted file mode 100644 index f405a1769..000000000 --- a/src/frontends/lean/proof_qed_elaborator.cpp +++ /dev/null @@ -1,57 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/unifier.h" -#include "library/reducible.h" -#include "library/metavar_closure.h" -#include "frontends/lean/util.h" -#include "frontends/lean/info_manager.h" -namespace lean { -/** \brief Create a "choice" constraint that postpone the - solving the constraints (cs union (m =?= e)). -*/ -constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e, - constraint_seq const & cs, unifier_config const & cfg, - info_manager * im, bool relax) { - justification j = mk_failed_to_synthesize_jst(env, m); - auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, - name_generator const & _ngen) { - name_generator ngen(_ngen); - type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax)); - pair tcs = tc->infer(e); - expr e_type = tcs.first; - justification new_j = mk_type_mismatch_jst(e, e_type, meta_type); - pair dcs = tc->is_def_eq(e_type, meta_type, new_j); - if (!dcs.first) - throw unifier_exception(new_j, s); - constraint_seq new_cs = cs + tcs.second + dcs.second; - buffer cs_buffer; - new_cs.linearize(cs_buffer); - metavar_closure cls(meta); - cls.add(meta_type); - cls.mk_constraints(s, j, relax, cs_buffer); - cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax)); - - unifier_config new_cfg(cfg); - new_cfg.m_discard = false; - unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); - auto p = seq.pull(); - lean_assert(p); - substitution new_s = p->first.first; - constraints postponed = map(p->first.second, - [&](constraint const & c) { - // we erase internal justifications - return update_justification(c, j); - }); - if (im) - im->instantiate(new_s); - constraints r = cls.mk_constraints(new_s, j, relax); - return append(r, postponed); - }; - bool owner = false; - return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax); -} -} diff --git a/src/frontends/lean/proof_qed_elaborator.h b/src/frontends/lean/proof_qed_elaborator.h deleted file mode 100644 index 6d1febf4d..000000000 --- a/src/frontends/lean/proof_qed_elaborator.h +++ /dev/null @@ -1,22 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/unifier.h" -#include "frontends/lean/info_manager.h" - -namespace lean { -/** \brief Create a "choice" constraint that postpone the - solving the constraints (cs union (m =?= e)). - - \remark A proof-qed block may instantiate meta-variables in the - info_manager. Thus, we provide the info_manager to make sure - this assignments are reflected on it. -*/ -constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e, - constraint_seq const & cs, unifier_config const & cfg, - info_manager * im, bool relax); -} diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index c905254be..0973359f5 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -125,14 +125,11 @@ expr copy_annotations(expr const & from, expr const & to) { static name * g_have = nullptr; static name * g_show = nullptr; -static name * g_proof_qed = nullptr; expr mk_have_annotation(expr const & e) { return mk_annotation(*g_have, e); } expr mk_show_annotation(expr const & e) { return mk_annotation(*g_show, e); } -expr mk_proof_qed_annotation(expr const & e) { return mk_annotation(*g_proof_qed, e); } bool is_have_annotation(expr const & e) { return is_annotation(e, *g_have); } bool is_show_annotation(expr const & e) { return is_annotation(e, *g_show); } -bool is_proof_qed_annotation(expr const & e) { return is_annotation(e, *g_proof_qed); } void initialize_annotation() { g_annotation = new name("annotation"); @@ -140,11 +137,9 @@ void initialize_annotation() { g_annotation_macros = new annotation_macros(); g_have = new name("have"); g_show = new name("show"); - g_proof_qed = new name("proof-qed"); register_annotation(*g_have); register_annotation(*g_show); - register_annotation(*g_proof_qed); register_macro_deserializer(get_annotation_opcode(), [](deserializer & d, unsigned num, expr const * args) { @@ -157,7 +152,6 @@ void initialize_annotation() { } void finalize_annotation() { - delete g_proof_qed; delete g_show; delete g_have; delete g_annotation_macros; diff --git a/src/library/annotation.h b/src/library/annotation.h index d6c124e2c..2d874f275 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -57,14 +57,10 @@ expr copy_annotations(expr const & from, expr const & to); expr mk_have_annotation(expr const & e); /** \brief Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */ expr mk_show_annotation(expr const & e); -/** \brief Tag \c e as a 'proof-qed'-expression. 'proof-qed' is a pre-registered annotation. */ -expr mk_proof_qed_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_have_annotation. */ bool is_have_annotation(expr const & e); /** \brief Return true iff \c e was created using #mk_show_annotation. */ bool is_show_annotation(expr const & e); -/** \brief Return true iff \c e was created using #mk_proof_qed_annotation. */ -bool is_proof_qed_annotation(expr const & e); /** \brief Return the serialization 'opcode' for annotation macros. */ std::string const & get_annotation_opcode(); diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean index 6cc938d20..e03c137c6 100644 --- a/tests/lean/run/div2.lean +++ b/tests/lean/run/div2.lean @@ -74,7 +74,7 @@ nat.case_strong_induction_on m show f' (succ m) x = restrict default measure f (succ m) x, from by_cases -- (measure x < succ m) (assume H1 : measure x < succ m, - have H2a : ∀z, measure z < measure x → f' m z = f z, + assert H2a : ∀z, measure z < measure x → f' m z = f z, proof take z, assume Hzx : measure z < measure x, @@ -90,7 +90,7 @@ nat.case_strong_induction_on m ... = rec_val x f : rec_decreasing (f' m) f x H2a ∎, let m' := measure x in - have H3a : ∀z, measure z < m' → f' m' z = f z, + assert H3a : ∀z, measure z < m' → f' m' z = f z, proof take z, assume Hzx : measure z < measure x, diff --git a/tests/lean/run/proof_qed_nested_tac.lean b/tests/lean/run/proof_qed_nested_tac.lean new file mode 100644 index 000000000..c27e731cf --- /dev/null +++ b/tests/lean/run/proof_qed_nested_tac.lean @@ -0,0 +1,6 @@ +example (a b c : nat) (f : nat → nat → nat) (H₁ : a = b) (H₂ : b = c) : f (f a a) (f b b) = f (f c c) (f c c) := +assert h : a = c, from eq.trans H₁ H₂, +proof + calc f (f a a) (f b b) = f (f c c) (f b b) : by rewrite h + ... = f (f c c) (f c c) : by rewrite H₂ +qed