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

feat(frontends/lean): treat "proof t qed" as alias for "by exact t"

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-05 11:10:34 -08:00
parent bd0f209659
commit 039afb4578
12 changed files with 30 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
hott/algebra/precategory/yoneda.hlean
View file

@ -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) :

4
hott/init/axioms/funext_varieties.hlean
View file

@ -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,

2
src/frontends/lean/CMakeLists.txt
View file

@ -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)

3
src/frontends/lean/builtin_exprs.cpp
View file

@ -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;
}

19
src/frontends/lean/elaborator.cpp
View file

@ -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<expr> const & t, cons
return m;
}
expr elaborator::visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_proof_qed_annotation(e));
info_manager * im = nullptr;
if (infom())
im = &m_pre_info_data;
pair<expr, constraint_seq> 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<bool> let(m_no_info, true);
return visit(get_annotation_arg(e), cs);

1
src/frontends/lean/elaborator.h
View file

@ -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<expr> const & t, constraint_seq & cs);
expr visit_by(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs);
expr add_implict_args(expr e, constraint_seq & cs, bool relax);
pair<expr, expr> ensure_fun(expr f, constraint_seq & cs);

57
src/frontends/lean/proof_qed_elaborator.cpp
View file

@ -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 <tt>(cs union (m =?= e))</tt>.
*/
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<expr, constraint_seq> tcs = tc->infer(e);
expr e_type = tcs.first;
justification new_j = mk_type_mismatch_jst(e, e_type, meta_type);
pair<bool, constraint_seq> 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<constraint> 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);
}
}

22
src/frontends/lean/proof_qed_elaborator.h
View file

@ -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 <tt>(cs union (m =?= e))</tt>.
\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);
}

6
src/library/annotation.cpp
View file

@ -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;

4
src/library/annotation.h
View file

@ -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();

4
tests/lean/run/div2.lean
View file

@ -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,

6
tests/lean/run/proof_qed_nested_tac.lean Normal file
View file

@ -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