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

feat(library/definitional): add no_confusion construction that is compatible with the HoTT library

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-08 22:11:48 -08:00
parent 41c6914e48
commit 58432d0968
8 changed files with 130 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -723,6 +723,7 @@ struct inductive_cmd_fn {
bool has_eq = has_eq_decls(env);
bool has_heq = has_heq_decls(env);
bool has_prod = has_prod_decls(env);
bool has_lift = has_lift_decls(env);
for (inductive_decl const & d : decls) {
name const & n = inductive_decl_name(d);
pos_info pos = *m_decl_pos_map.find(n);
@ -735,7 +736,7 @@ struct inductive_cmd_fn {
if (has_unit) {
env = mk_cases_on(env, n);
save_def_info(name(n, "cases_on"), pos);
if (has_eq && has_heq) {
if (has_eq && ((env.prop_proof_irrel() && has_heq) || (!env.prop_proof_irrel() && has_lift))) {
env = mk_no_confusion(env, n);
save_if_defined(name{n, "no_confusion_type"}, pos);
save_if_defined(name(n, "no_confusion"), pos);

6
src/frontends/lean/structure_cmd.cpp
View file

@ -809,7 +809,11 @@ struct structure_cmd_fn {
}
void declare_no_confustion() {
if (!has_eq_decls(m_env) || !has_heq_decls(m_env))
if (!has_eq_decls(m_env))
return;
if (m_env.impredicative() && !has_heq_decls(m_env))
return;
if (!m_env.impredicative() && !has_lift_decls(m_env))
return;
m_env = mk_no_confusion(m_env, m_name);
name no_confusion_name(m_name, "no_confusion");

97
src/library/definitional/no_confusion.cpp
View file

@ -26,15 +26,22 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
if (is_inductive_predicate(env, n))
return optional<environment>(); // type is a proposition
name_generator ngen;
bool impredicative = env.impredicative();
unsigned nparams = std::get<1>(*decls);
declaration ind_decl = env.get(n);
declaration cases_decl = env.get(name(n, "cases_on"));
level_param_names lps = cases_decl.get_univ_params();
level rlvl = mk_param_univ(head(lps));
level plvl = mk_param_univ(head(lps));
levels ilvls = param_names_to_levels(tail(lps));
level rlvl;
expr ind_type = instantiate_type_univ_params(ind_decl, ilvls);
level ind_lvl = get_datatype_level(ind_type);
if (impredicative)
rlvl = plvl;
else
rlvl = mk_max(plvl, ind_lvl);
if (length(ilvls) != length(ind_decl.get_univ_params()))
return optional<environment>(); // type does not have only a restricted eliminator
expr ind_type = instantiate_type_univ_params(ind_decl, ilvls);
name eq_name("eq");
name heq_name("heq");
// All inductive datatype parameters and indices are arguments
@ -47,14 +54,19 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
// Create inductive datatype
expr I = mk_app(mk_constant(n, ilvls), args);
// Add (P : Type)
expr P = mk_local(ngen.next(), "P", mk_sort(rlvl), binder_info());
expr P = mk_local(ngen.next(), "P", mk_sort(plvl), binder_info());
args.push_back(P);
// add v1 and v2 elements of the inductive type
expr v1 = mk_local(ngen.next(), "v1", I, binder_info());
expr v2 = mk_local(ngen.next(), "v2", I, binder_info());
args.push_back(v1);
args.push_back(v2);
expr R = mk_sort(rlvl);
expr R = mk_sort(rlvl);
expr Pres;
if (impredicative)
Pres = P;
else
Pres = mk_app(mk_constant("lift", {plvl, ind_lvl}), P);
name no_confusion_type_name{n, "no_confusion_type"};
expr no_confusion_type_type = Pi(args, R);
// Create type former
@ -85,27 +97,33 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
expr minor2 = to_telescope(tc, binding_domain(curr_t2), minor2_args);
if (idx1 != idx2) {
// infeasible case, constructors do not match
inner_cases_on_args.push_back(Fun(minor2_args, P));
inner_cases_on_args.push_back(Fun(minor2_args, Pres));
} else {
if (minor1_args.size() != minor2_args.size())
throw_corrupted(n);
buffer<expr> rtype_hyp;
// add equalities
for (unsigned i = 0; i < minor1_args.size(); i++) {
expr lhs = minor1_args[i];
expr rhs = minor2_args[i];
expr lhs_type = mlocal_type(lhs);
expr rhs_type = mlocal_type(rhs);
level l = sort_level(tc.ensure_type(lhs_type).first);
expr h_type;
if (tc.is_def_eq(lhs_type, rhs_type).first) {
h_type = mk_app(mk_constant(eq_name, to_list(l)), lhs_type, lhs, rhs);
} else {
h_type = mk_app(mk_constant(heq_name, to_list(l)), lhs_type, lhs, rhs_type, rhs);
if (env.prop_proof_irrel()) {
// proof irrelevance version using heterogeneous equality
for (unsigned i = 0; i < minor1_args.size(); i++) {
expr lhs = minor1_args[i];
expr rhs = minor2_args[i];
expr lhs_type = mlocal_type(lhs);
expr rhs_type = mlocal_type(rhs);
level l = sort_level(tc.ensure_type(lhs_type).first);
expr h_type;
if (tc.is_def_eq(lhs_type, rhs_type).first) {
h_type = mk_app(mk_constant(eq_name, to_list(l)), lhs_type, lhs, rhs);
} else {
h_type = mk_app(mk_constant(heq_name, to_list(l)), lhs_type, lhs, rhs_type, rhs);
}
rtype_hyp.push_back(mk_local(ngen.next(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info()));
}
rtype_hyp.push_back(mk_local(ngen.next(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info()));
} else {
// we use telescope equality (with casts) when proof irrelevance is not available
mk_telescopic_eq(tc, minor1_args, minor2_args, rtype_hyp);
}
inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), P)));
inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), Pres)));
}
idx2++;
curr_t2 = binding_body(curr_t2);
@ -130,13 +148,17 @@ environment mk_no_confusion(environment const & env, name const & n) {
return env;
environment new_env = *env1;
type_checker tc(new_env);
bool impredicative = env.impredicative();
inductive::inductive_decls decls = *inductive::is_inductive_decl(new_env, n);
unsigned nparams = std::get<1>(decls);
name_generator ngen;
declaration ind_decl = env.get(n);
declaration no_confusion_type_decl = new_env.get(name{n, "no_confusion_type"});
declaration cases_decl = new_env.get(name(n, "cases_on"));
level_param_names lps = no_confusion_type_decl.get_univ_params();
levels ls = param_names_to_levels(lps);
expr ind_type = instantiate_type_univ_params(ind_decl, tail(ls));
level ind_lvl = get_datatype_level(ind_type);
expr no_confusion_type_type = instantiate_type_univ_params(no_confusion_type_decl, ls);
name eq_name("eq");
name heq_name("heq");
@ -152,9 +174,14 @@ environment mk_no_confusion(environment const & env, name const & n) {
expr v1 = args[args.size()-2];
expr v2 = args[args.size()-1];
expr v_type = mlocal_type(v1);
expr lift_up;
if (!impredicative) {
lift_up = mk_app(mk_constant(name{"lift", "up"}, {head(ls), ind_lvl}), P);
}
level v_lvl = sort_level(tc.ensure_type(v_type).first);
expr eq_v = mk_app(mk_constant(eq_name, to_list(v_lvl)), v_type);
expr H12 = mk_local(ngen.next(), "H12", mk_app(eq_v, v1, v2), binder_info());
lean_assert(impredicative != inductive::has_dep_elim(env, eq_name));
args.push_back(H12);
name no_confusion_name{n, "no_confusion"};
expr no_confusion_ty = Pi(args, range);
@ -181,7 +208,11 @@ environment mk_no_confusion(environment const & env, name const & n) {
expr no_confusion_type_app = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), no_confusion_type_args);
expr type_former = Fun(type_former_args, no_confusion_type_app);
// create cases_on
levels clvls = ls;
levels clvls;
if (impredicative)
clvls = ls;
else
clvls = cons(mk_max(head(ls), ind_lvl), tail(ls));
expr cases_on = mk_app(mk_app(mk_constant(cases_decl.get_name(), clvls), nparams, args.data()), type_former);
cases_on = mk_app(mk_app(cases_on, nindices, args.data() + nparams), v1);
expr cot = tc.infer(cases_on).first;
@ -197,23 +228,32 @@ environment mk_no_confusion(environment const & env, name const & n) {
buffer<expr> eq_args;
expr eq_fn = get_app_args(binding_domain(Ht), eq_args);
if (const_name(eq_fn) == eq_name) {
refl_args.push_back(mk_app(mk_constant(eq_refl_name, const_levels(eq_fn)), eq_args[0], eq_args[1]));
refl_args.push_back(mk_app(mk_constant(eq_refl_name, const_levels(eq_fn)), eq_args[0], eq_args[2]));
} else {
refl_args.push_back(mk_app(mk_constant(heq_refl_name, const_levels(eq_fn)), eq_args[0], eq_args[1]));
}
Ht = binding_body(Ht);
}
expr pr = mk_app(H, refl_args);
if (!impredicative)
pr = mk_app(lift_up, pr);
cases_on = mk_app(cases_on, Fun(minor_args, pr));
cot = binding_body(cot);
}
expr gen = Fun(H11, cases_on);
expr gen = cases_on;
if (impredicative)
gen = Fun(H11, gen);
// Now, we use gen to build the final proof using eq.rec
//
// eq.rec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12
//
name eq_rec_name{"eq", "rec"};
expr eq_rec = mk_app(mk_constant(eq_rec_name, {head(ls), v_lvl}), v_type, v1);
level eq_rec_l1;
if (impredicative)
eq_rec_l1 = head(ls);
else
eq_rec_l1 = mk_max(head(ls), ind_lvl);
expr eq_rec = mk_app(mk_constant(eq_rec_name, {eq_rec_l1, v_lvl}), v_type, v1);
// create eq_rec type_former
// (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a)
expr a = mk_local(ngen.next(), "a", v_type, binder_info());
@ -222,12 +262,17 @@ environment mk_no_confusion(environment const & env, name const & n) {
no_confusion_type_args.pop_back();
no_confusion_type_args.push_back(a);
expr no_confusion_type_app_1a = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), no_confusion_type_args);
expr rec_type_former = Fun(a, Pi(H1a, no_confusion_type_app_1a));
// finalize eq_rec
eq_rec = mk_app(mk_app(eq_rec, rec_type_former, gen, v2, H12), H12);
if (impredicative) {
expr rec_type_former = Fun(a, Pi(H1a, no_confusion_type_app_1a));
// finalize eq_rec
eq_rec = mk_app(mk_app(eq_rec, rec_type_former, gen, v2, H12), H12);
} else {
expr rec_type_former = Fun(a, Fun(H1a, no_confusion_type_app_1a));
// finalize eq_rec
eq_rec = mk_app(eq_rec, rec_type_former, gen, v2, H12);
}
//
expr no_confusion_val = Fun(args, eq_rec);
bool opaque = false;
bool use_conv_opt = true;
declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,

6
src/library/definitional/no_confusion.h
View file

@ -11,9 +11,9 @@ namespace lean {
/** \brief Given an inductive datatype \c n (which is not a proposition) in \c env, add
<tt>n.no_confusion_type</tt> and <tt>n.no_confusion</tt> to the environment.
\remark This procedure assumes the environment contains eq, heq, n.cases_on</tt>
\remark Return none if did not create constructions because type is a proposition.
\remark This procedure assumes the environment contains eq, n.cases_on</tt>.
If the environment has an impredicative Prop, it also assumes heq is defined.
If the environment does not have an impredicative Prop, then it also assumes lift is defined.
*/
environment mk_no_confusion(environment const & env, name const & n);
}

15
src/library/definitional/util.cpp
View file

@ -47,6 +47,10 @@ bool has_prod_decls(environment const & env) {
return has_constructor(env, name{"prod", "mk"}, "prod", 4);
}
bool has_lift_decls(environment const & env) {
return has_constructor(env, name{"lift", "up"}, "lift", 2);
}
bool is_recursive_datatype(environment const & env, name const & n) {
optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
if (!decls)
@ -261,7 +265,7 @@ expr mk_pr1(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and
expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs) {
expr A = tc.infer(lhs).first;
expr A = tc.whnf(tc.infer(lhs).first).first;
level lvl = sort_level(tc.ensure_type(A).first);
return mk_app(mk_constant(*g_eq_name, {lvl}), A, lhs, rhs);
}
@ -321,4 +325,13 @@ void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> &
}
return mk_telescopic_eq(tc, t, s, eqs);
}
level mk_max(levels const & ls) {
if (!ls)
return mk_level_zero();
else if (!tail(ls))
return head(ls);
else
return mk_max(head(ls), mk_max(tail(ls)));
}
}

3
src/library/definitional/util.h
View file

@ -12,6 +12,7 @@ bool has_unit_decls(environment const & env);
bool has_eq_decls(environment const & env);
bool has_heq_decls(environment const & env);
bool has_prod_decls(environment const & env);
bool has_lift_decls(environment const & env);
/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
That is, it must be an inductive datatype AND contain a recursive constructor.
@ -83,6 +84,8 @@ expr mk_eq(type_checker & tc, expr const & lhs, expr const & rhs);
void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> const & s, buffer<expr> & eqs);
void mk_telescopic_eq(type_checker & tc, buffer<expr> const & t, buffer<expr> & eqs);
level mk_max(levels const & ls);
void initialize_definitional_util();
void finalize_definitional_util();
}

15
tests/lean/hott/noc.hlean Normal file
View file

@ -0,0 +1,15 @@
set_option pp.beta true
structure foo :=
mk :: (A : Type) (B : A → Type) (a : A) (b : B a)
namespace foo
definition foo.inj₁
{A₁ : Type} {B₁ : A₁ → Type} {a₁ : A₁} {b₁ : B₁ a₁}
{A₂ : Type} {B₂ : A₂ → Type} {a₂ : A₂} {b₂ : B₂ a₂}
(H : foo.mk A₁ B₁ a₁ b₁ = foo.mk A₂ B₂ a₂ b₂)
: A₁ = A₂
:= lift.down (no_confusion H (λ e₁ e₂ e₃ e₄, e₁))
end foo

17
tests/lean/hott/noc_list.hlean Normal file
View file

@ -0,0 +1,17 @@
inductive list (A : Type) : Type :=
nil {} : list A,
cons : A → list A → list A
namespace list
open lift
theorem nil_ne_cons {A : Type} (a : A) (v : list A) : nil ≠ cons a v :=
λ H, down (no_confusion H)
theorem cons.inj₁ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → a₁ = a₂ :=
λ H, down (no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₁))
theorem cons.inj₂ {A : Type} (a₁ a₂ : A) (v₁ v₂ : list A) : cons a₁ v₁ = cons a₂ v₂ → v₁ = v₂ :=
λ H, down (no_confusion H (λ (h₁ : a₁ = a₂) (h₂ : v₁ = v₂), h₂))
end list