From b5da143fc09fbd55337a90d247130999e6418ae7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Nov 2014 15:20:19 -0800 Subject: [PATCH] feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions --- src/frontends/lean/inductive_cmd.cpp | 13 ++ src/library/definitional/CMakeLists.txt | 4 +- src/library/definitional/heq.cpp | 27 ++++ src/library/definitional/heq.h | 12 ++ src/library/definitional/no_confusion.cpp | 144 ++++++++++++++++++ src/library/definitional/no_confusion.h | 17 +++ tests/lean/no_confusion_type.lean | 12 ++ .../lean/no_confusion_type.lean.expected.out | 2 + tests/lean/run/nested_begin.lean | 15 +- tests/lean/run/tree.lean | 9 -- tests/lean/run/tree2.lean | 9 -- tests/lean/run/tree3.lean | 9 -- tests/lean/run/vector.lean | 15 +- tests/lean/run/vector2.lean | 13 +- tests/lean/run/vector3.lean | 15 +- 15 files changed, 240 insertions(+), 76 deletions(-) create mode 100644 src/library/definitional/heq.cpp create mode 100644 src/library/definitional/heq.h create mode 100644 src/library/definitional/no_confusion.cpp create mode 100644 src/library/definitional/no_confusion.h create mode 100644 tests/lean/no_confusion_type.lean create mode 100644 tests/lean/no_confusion_type.lean.expected.out diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 49813cf1c..958aeb73a 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -24,6 +24,9 @@ Author: Leonardo de Moura #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" +#include "library/definitional/no_confusion.h" +#include "library/definitional/eq.h" +#include "library/definitional/heq.h" #include "library/definitional/unit.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/util.h" @@ -637,6 +640,8 @@ struct inductive_cmd_fn { environment mk_aux_decls(environment env, buffer const & decls) { bool has_unit = has_unit_decls(env); + bool has_eq = has_eq_decls(env); + bool has_heq = has_heq_decls(env); for (inductive_decl const & d : decls) { name const & n = inductive_decl_name(d); pos_info pos = *m_decl_pos_map.find(n); @@ -647,6 +652,14 @@ struct inductive_cmd_fn { if (has_unit) { env = mk_cases_on(env, inductive_decl_name(d)); save_def_info(name(n, "cases_on"), pos); + if (has_eq && has_heq) { + env = mk_no_confusion(env, inductive_decl_name(d)); + name no_confusion_type_name{n, "no_confusion_type"}; + if (env.find(no_confusion_type_name)) { + save_def_info(no_confusion_type_name, pos); + // save_def_info(name(n, "no_confusion"), pos); + } + } } } return env; diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt index c4392e3d3..07dfa2ece 100644 --- a/src/library/definitional/CMakeLists.txt +++ b/src/library/definitional/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp eq.cpp - projection.cpp) +add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp eq.cpp heq.cpp + no_confusion.cpp projection.cpp) target_link_libraries(definitional ${LEAN_LIBS}) diff --git a/src/library/definitional/heq.cpp b/src/library/definitional/heq.cpp new file mode 100644 index 000000000..7ba9b3d4e --- /dev/null +++ b/src/library/definitional/heq.cpp @@ -0,0 +1,27 @@ +/* +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 "kernel/environment.h" + +namespace lean { +bool has_heq_decls(environment const & env) { + auto d = env.find(name({"heq", "refl"})); + if (!d) + return false; + if (length(d->get_univ_params()) != 1) + return false; + expr type = d->get_type(); + for (unsigned i = 0; i < 2; i++) { + if (!is_pi(type)) + return type; + type = binding_body(type); + } + type = get_app_fn(type); + if (!is_constant(type)) + return false; + return const_name(type) == "heq"; +} +} diff --git a/src/library/definitional/heq.h b/src/library/definitional/heq.h new file mode 100644 index 000000000..fe3fa8302 --- /dev/null +++ b/src/library/definitional/heq.h @@ -0,0 +1,12 @@ +/* +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 "kernel/environment.h" + +namespace lean { +bool has_heq_decls(environment const & env); +} diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp new file mode 100644 index 000000000..7c72261d1 --- /dev/null +++ b/src/library/definitional/no_confusion.cpp @@ -0,0 +1,144 @@ +/* +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 "util/sstream.h" +#include "kernel/environment.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/inductive/inductive.h" +#include "kernel/type_checker.h" +#include "library/protected.h" +#include "library/module.h" + +namespace lean { +static void throw_corrupted(name const & n) { + throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' inductive datatype declaration is corrupted"); +} + +environment mk_no_confusion_type(environment const & env, name const & n) { + optional decls = inductive::is_inductive_decl(env, n); + if (!decls) + throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' is not an inductive datatype"); + name_generator ngen; + 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)); + levels ilvls = param_names_to_levels(tail(lps)); + if (length(ilvls) != length(ind_decl.get_univ_params())) + return env; // type is a proposition + expr ind_type = instantiate_type_univ_params(ind_decl, ilvls); + name eq_name("eq"); + name heq_name("heq"); + name eq_refl_name{"eq", "refl"}; + name heq_refl_name{"heq", "refl"}; + // All inductive datatype parameters and indices are arguments + buffer args; + while (is_pi(ind_type)) { + expr arg = mk_local(ngen.next(), binding_name(ind_type), binding_domain(ind_type), mk_implicit_binder_info()); + args.push_back(arg); + ind_type = instantiate(binding_body(ind_type), arg); + } + if (!is_sort(ind_type) || args.size() < nparams) + throw_corrupted(n); + if (env.impredicative() && is_zero(sort_level(ind_type))) + return env; // do nothing, inductive type is a proposition + unsigned nindices = args.size() - nparams; + // 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()); + 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); + name no_confusion_type_name{n, "no_confusion_type"}; + expr no_confusion_type_type = Pi(args, R); + // Create type former + buffer type_former_args; + for (unsigned i = nparams; i < nparams + nindices; i++) + type_former_args.push_back(args[i]); + type_former_args.push_back(v1); + expr type_former = Fun(type_former_args, R); + // Create cases_on + levels clvls = levels(mk_succ(rlvl), ilvls); + expr cases_on = mk_app(mk_app(mk_constant(cases_decl.get_name(), clvls), nparams, args.data()), type_former); + cases_on = mk_app(cases_on, nindices, args.data() + nparams); + expr cases_on1 = mk_app(cases_on, v1); + expr cases_on2 = mk_app(cases_on, v2); + type_checker tc(env); + expr t1 = tc.infer(cases_on1).first; + expr t2 = tc.infer(cases_on2).first; + buffer outer_cases_on_args; + unsigned idx1 = 0; + while (is_pi(t1)) { + expr minor1 = tc.whnf(binding_domain(t1)).first; + buffer minor1_args; + while (is_pi(minor1)) { + expr arg = mk_local(ngen.next(), binding_name(minor1), binding_domain(minor1), binding_info(minor1)); + minor1_args.push_back(arg); + minor1 = tc.whnf(instantiate(binding_body(minor1), arg)).first; + } + expr curr_t2 = t2; + buffer inner_cases_on_args; + unsigned idx2 = 0; + while (is_pi(curr_t2)) { + expr minor2 = tc.whnf(binding_domain(curr_t2)).first; + buffer minor2_args; + while (is_pi(minor2)) { + expr arg = mk_local(ngen.next(), binding_name(minor2), binding_domain(minor2), binding_info(minor2)); + minor2_args.push_back(arg); + minor2 = tc.whnf(instantiate(binding_body(minor2), arg)).first; + } + if (idx1 != idx2) { + // infeasible case, constructors do not match + inner_cases_on_args.push_back(Fun(minor2_args, P)); + } else { + if (minor1_args.size() != minor2_args.size()) + throw_corrupted(n); + buffer 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); + } + rtype_hyp.push_back(mk_local(ngen.next(), local_pp_name(lhs).append_after("_eq"), h_type, binder_info())); + } + inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), P))); + } + idx2++; + curr_t2 = binding_body(curr_t2); + } + outer_cases_on_args.push_back(Fun(minor1_args, mk_app(cases_on2, inner_cases_on_args))); + idx1++; + t1 = binding_body(t1); + } + expr no_confusion_type_value = Fun(args, mk_app(cases_on1, outer_cases_on_args)); + + bool opaque = false; + bool use_conv_opt = true; + declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value, + opaque, ind_decl.get_module_idx(), use_conv_opt); + environment new_env = module::add(env, check(env, new_d)); + return add_protected(new_env, no_confusion_type_name); +} + +environment mk_no_confusion(environment const & env, name const & n) { + return mk_no_confusion_type(env, n); +} +} diff --git a/src/library/definitional/no_confusion.h b/src/library/definitional/no_confusion.h new file mode 100644 index 000000000..d8585284a --- /dev/null +++ b/src/library/definitional/no_confusion.h @@ -0,0 +1,17 @@ +/* +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 "kernel/environment.h" + +namespace lean { +/** \brief Given an inductive datatype \c n (which is not a proposition) in \c env, add + n.no_confusion_type and n.no_confusion to the environment. + + \remark This procedure assumes the environment contains eq, heq, n.cases_on +*/ +environment mk_no_confusion(environment const & env, name const & n); +} diff --git a/tests/lean/no_confusion_type.lean b/tests/lean/no_confusion_type.lean new file mode 100644 index 000000000..aedb43127 --- /dev/null +++ b/tests/lean/no_confusion_type.lean @@ -0,0 +1,12 @@ +import logic data.nat.basic +open nat + +inductive vector (A : Type) : nat → Type := +vnil : vector A zero, +vcons : Π {n : nat}, A → vector A n → vector A (succ n) + +check vector.no_confusion_type +constants a1 a2 : num +constants v1 v2 : vector num 2 +constant P : Type₁ +eval vector.no_confusion_type P (vector.vcons a1 v1) (vector.vcons a2 v2) diff --git a/tests/lean/no_confusion_type.lean.expected.out b/tests/lean/no_confusion_type.lean.expected.out new file mode 100644 index 000000000..0d4c2ccb3 --- /dev/null +++ b/tests/lean/no_confusion_type.lean.expected.out @@ -0,0 +1,2 @@ +vector.no_confusion_type : Type → vector ?A ?a → vector ?A ?a → Type +(succ (succ zero) = succ (succ zero) → a1 = a2 → v1 == v2 → P) → P diff --git a/tests/lean/run/nested_begin.lean b/tests/lean/run/nested_begin.lean index 60ab2c3db..867e498d7 100644 --- a/tests/lean/run/nested_begin.lean +++ b/tests/lean/run/nested_begin.lean @@ -6,16 +6,6 @@ vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type := - cases_on v₁ - (cases_on v₂ - (P → P) - (λ n₂ h₂ t₂, P)) - (λ n₁ h₁ t₁, cases_on v₂ - P - (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P)) - - definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, begin @@ -28,7 +18,8 @@ namespace vector intros (n, a, v, h), apply (h rfl), - repeat (apply rfl) + repeat (apply rfl), + repeat (apply heq.refl) end, eq.rec_on H₁₂ aux H₁₂ end @@ -38,7 +29,7 @@ namespace vector intro h, apply (no_confusion h), intros, assumption end - theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ := + theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ == v₂ := begin intro h, apply (no_confusion h), intros, eassumption end diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean index 7ac5009fb..bd39ac06b 100644 --- a/tests/lean/run/tree.lean +++ b/tests/lean/run/tree.lean @@ -36,15 +36,6 @@ namespace tree pr₁ general end - definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type := - cases_on t₁ - (λ a₁, cases_on t₂ - (λ a₂, (a₁ = a₂ → P) → P) - (λ l₂ r₂, P)) - (λ l₁ r₁, cases_on t₂ - (λ a₂, P) - (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P)) - set_option pp.universes true check no_confusion_type diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean index 38083fa90..2483ed026 100644 --- a/tests/lean/run/tree2.lean +++ b/tests/lean/run/tree2.lean @@ -36,15 +36,6 @@ namespace tree pr₁ general end - definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type := - cases_on t₁ - (λ a₁, cases_on t₂ - (λ a₂, (a₁ = a₂ → P) → P) - (λ l₂ r₂, P)) - (λ l₁ r₁, cases_on t₂ - (λ a₂, P) - (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P)) - set_option pp.universes true check no_confusion_type diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index 12067f395..be1ff8e62 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -36,15 +36,6 @@ namespace tree pr₁ general end - definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type := - cases_on t₁ - (λ a₁, cases_on t₂ - (λ a₂, (a₁ = a₂ → P) → P) - (λ l₂ r₂, P)) - (λ l₁ r₁, cases_on t₂ - (λ a₂, P) - (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P)) - set_option pp.universes true check no_confusion_type diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index 889be3050..97265936e 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -6,22 +6,13 @@ vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type := - cases_on v₁ - (cases_on v₂ - (P → P) - (λ n₂ h₂ t₂, P)) - (λ n₁ h₁ t₁, cases_on v₂ - P - (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P)) - definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from take H₁₁, cases_on v₁ (assume h : P, h) - (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P), - h rfl rfl rfl), + (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ == t₁ → P), + h rfl rfl !heq.refl), eq.rec aux H₁₂ H₁₂ theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := @@ -29,7 +20,7 @@ namespace vector intro h, apply (no_confusion h), intros, assumption end - theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ := + theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ == v₂ := begin intro h, apply (no_confusion h), intros, eassumption end diff --git a/tests/lean/run/vector2.lean b/tests/lean/run/vector2.lean index f0b8ba6de..e068f923a 100644 --- a/tests/lean/run/vector2.lean +++ b/tests/lean/run/vector2.lean @@ -6,22 +6,13 @@ vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type := - cases_on v₁ - (cases_on v₂ - (P → P) - (λ n₂ h₂ t₂, P)) - (λ n₁ h₁ t₁, cases_on v₂ - P - (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P)) - definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from take H₁₁, cases_on v₁ (assume h : P, h) - (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P), - h rfl rfl rfl), + (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ == t₁ → P), + h rfl rfl !heq.refl), eq.rec aux H₁₂ H₁₂ theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := diff --git a/tests/lean/run/vector3.lean b/tests/lean/run/vector3.lean index 1f871857e..43f07f799 100644 --- a/tests/lean/run/vector3.lean +++ b/tests/lean/run/vector3.lean @@ -6,28 +6,19 @@ vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) namespace vector - definition no_confusion_type {A : Type} {n : nat} (P : Type) (v₁ v₂ : vector A n) : Type := - cases_on v₁ - (cases_on v₂ - (P → P) - (λ n₂ h₂ t₂, P)) - (λ n₁ h₁ t₁, cases_on v₂ - P - (λ n₂ h₂ t₂, (Π (H : n₁ = n₂), h₁ = h₂ → eq.rec_on H t₁ = t₂ → P) → P)) - definition no_confusion {A : Type} {n : nat} {P : Type} {v₁ v₂ : vector A n} : v₁ = v₂ → no_confusion_type P v₁ v₂ := assume H₁₂ : v₁ = v₂, have aux : v₁ = v₁ → no_confusion_type P v₁ v₁, from take H₁₁, cases_on v₁ (assume h : P, h) - (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ = t₁ → P), - h rfl rfl rfl), + (take n₁ h₁ t₁, assume h : (Π (H : n₁ = n₁), h₁ = h₁ → t₁ == t₁ → P), + h rfl rfl !heq.refl), eq.rec aux H₁₂ H₁₂ theorem vcons.inj₁ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → a₁ = a₂ := assume h, no_confusion h (λ n h t, h) - theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ = v₂ := + theorem vcons.inj₂ {A : Type} {n : nat} (a₁ a₂ : A) (v₁ v₂ : vector A n) : vcons a₁ v₁ = vcons a₂ v₂ → v₁ == v₂ := assume h, no_confusion h (λ n h t, t) end vector