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

fix(frontends/lean/placeholder_elaborator): do not truncate stream of

Browse source 
solutions during class-instance resolution, closes #183

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
This commit is contained in:
Leonardo de Moura 2014-09-12 15:56:02 -07:00
parent b482f27543
commit b7023ce1d8
2 changed files with 24 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/category.lean
View file

@ -112,9 +112,9 @@ namespace category
(Hl : is_section f) (Hr : is_retraction f) : is_iso f :=
is_iso.mk (subst (section_eq_retraction Hl Hr) retraction_compose) compose_section
-- theorem inverse_unique {A B : ob} {f : mor A B} (H H' : is_iso f)
-- : @inverse _ _ f H = @inverse _ _ f H' :=
-- left_inverse_eq_right_inverse inverse_compose compose_inverse
theorem inverse_unique {A B : ob} {f : mor A B} (H H' : is_iso f)
: @inverse _ _ f H = @inverse _ _ f H' :=
left_inverse_eq_right_inverse inverse_compose compose_inverse
theorem retraction_of_id {A : ob} : retraction_of (ID A) = id :=
left_inverse_eq_right_inverse retraction_compose id_compose

47
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/lazy_list_fn.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/unifier.h"
@ -288,32 +289,26 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first;
justification new_j = mj.second;
try {
constraint c = mk_placeholder_cnstr(C, new_meta, is_strict);
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
unify_result_seq seq = unify(env, 1, &c, ngen, new_cfg);
auto p = seq.pull();
if (!p)
return lazy_list<constraints>();
substitution new_s = p->first.first;
constraints postponed = map(p->first.second,
[&](constraint const & c) {
// we erase internal justifications
return update_justification(c, new_j);
});
if (!new_s.is_expr_assigned(mlocal_name(get_app_fn(new_meta)))) {
lazy_list<constraints>(constraints());
}
metavar_closure cls(new_meta);
cls.add(meta_type);
bool relax = C->m_relax;
constraints cs = cls.mk_constraints(new_s, new_j, relax);
return lazy_list<constraints>(append(cs, postponed));
} catch (exception & ex) {
return lazy_list<constraints>();
}
return lazy_list<constraints>();
constraint c = mk_placeholder_cnstr(C, new_meta, is_strict);
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
new_cfg.m_use_exceptions = false;
unify_result_seq seq = unify(env, 1, &c, ngen, new_cfg);
return map2<constraints>(seq, [=](pair<substitution, constraints> const & p) {
substitution new_s = p.first;
if (!new_s.is_expr_assigned(mlocal_name(get_app_fn(new_meta))))
constraints();
constraints postponed = map(p.second,
[&](constraint const & c) {
// we erase internal justifications
return update_justification(c, new_j);
});
metavar_closure cls(new_meta);
cls.add(meta_type);
bool relax = C->m_relax;
constraints cs = cls.mk_constraints(new_s, new_j, relax);
return append(cs, postponed);
});
};
bool owner = false;
bool relax = C->m_relax;