feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions

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

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

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";
+}
+}

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);
+}

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<inductive::inductive_decls> 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<expr> 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<expr> 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<expr> outer_cases_on_args;
+    unsigned idx1 = 0;
+    while (is_pi(t1)) {
+        expr minor1 = tc.whnf(binding_domain(t1)).first;
+        buffer<expr> 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<expr> inner_cases_on_args;
+        unsigned idx2 = 0;
+        while (is_pi(curr_t2)) {
+            expr minor2 = tc.whnf(binding_domain(curr_t2)).first;
+            buffer<expr> 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<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);
+                    }
+                    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);
+}
+}

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
+    <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>
+*/
+environment mk_no_confusion(environment const & env, name const & n);
+}

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)

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

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

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
 

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
 

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
 

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

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₂ :=

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