feat(library/definitional/cases_on): automatically add 'cases_on'

library/data/bool.lean

@@ -10,9 +10,6 @@ inductive bool : Type :=
   ff : bool,
   tt : bool
 namespace bool
-  protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
-  rec H₁ H₂ b
-
   definition cond {A : Type} (b : bool) (t e : A) :=
   rec_on b e t
 

library/data/list/basic.lean

@@ -21,10 +21,6 @@ notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
 variable {T : Type}
 
-protected theorem cases_on {P : list T → Prop} (l : list T) (Hnil : P nil)
-    (Hcons : ∀ (x : T) (l : list T), P (x::l)) : P l :=
-induction_on l Hnil (take x l IH, Hcons x l)
-
 -- Concat
 -- ------
 

library/data/sum.lean

@@ -20,8 +20,6 @@ namespace sum
 
   variables {A B : Type}
   variables {a a₁ a₂ : A} {b b₁ b₂ : B}
-  protected definition cases_on {P : (A ⊎ B) → Prop} (s : A ⊎ B) (H₁ : ∀a : A, P (inl B a)) (H₂ : ∀b : B, P (inr A b)) : P s :=
-  rec H₁ H₂ s
 
   -- Here is the trick for the theorems that follow:
   -- Fixing a₁, "f s" is a recursive description of "inl B a₁ = s".

library/logic/eq.lean

@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import general_notation .prop
+import general_notation logic.prop data.unit.decl
 
 -- logic.eq
 -- ====================

src/frontends/lean/inductive_cmd.cpp

@@ -23,6 +23,8 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/definitional/rec_on.h"
 #include "library/definitional/induction_on.h"
+#include "library/definitional/cases_on.h"
+#include "library/definitional/unit.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/class.h"
@@ -649,9 +651,12 @@ struct inductive_cmd_fn {
     }
 
     environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
+        bool has_unit = has_unit_decls(env);
         for (inductive_decl const & d : decls) {
             env = mk_rec_on(env, inductive_decl_name(d));
             env = mk_induction_on(env, inductive_decl_name(d));
+            if (has_unit)
+                env = mk_cases_on(env, inductive_decl_name(d));
         }
         return env;
     }

src/library/definitional/CMakeLists.txt

@@ -1,3 +1,3 @@
-add_library(definitional rec_on.cpp induction_on.cpp)
+add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp unit.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})

src/library/definitional/cases_on.cpp

@@ -0,0 +1,180 @@
+/*
+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/module.h"
+#include "library/protected.h"
+
+namespace lean {
+static void throw_corrupted(name const & n) {
+    throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' inductive datatype declaration is corrupted");
+}
+
+/** \brief Given a C := As -> Type, return (fun (xs : As), unit) */
+static expr mk_fun_unit(expr const & C, expr const & unit) {
+    if (is_pi(C)) {
+        return mk_lambda(binding_name(C), binding_domain(C), mk_fun_unit(binding_body(C), unit));
+    } else {
+        return unit;
+    }
+}
+
+static bool is_type_former_arg(buffer<name> const & C_names, expr const & arg) {
+    expr const & fn = get_app_fn(arg);
+    return is_local(fn) && std::find(C_names.begin(), C_names.end(), mlocal_name(fn)) != C_names.end();
+}
+
+/** \brief Given minor premise (Pi (a_1 : A_1) ... (a_n : A_n), B)
+    return fun (a_1 : A_1') ... (a_n : A_n'), star),
+    and A_i' is A_i if A_i is not the main type former C_main.
+*/
+static expr mk_fun_star(expr const & minor, buffer<name> const & C_names, name const & C_main,
+                        expr const & unit, expr const & star) {
+    if (is_pi(minor)) {
+        expr const & domain = binding_domain(minor);
+        expr const & body   = binding_body(minor);
+        if (is_type_former_arg(C_names, domain) && mlocal_name(get_app_fn(domain)) != C_main)
+            return mk_lambda(binding_name(minor), unit, mk_fun_star(body, C_names, C_main, unit, star));
+        else
+            return mk_lambda(binding_name(minor), binding_domain(minor), mk_fun_star(body, C_names, C_main, unit, star));
+    } else {
+        return star;
+    }
+}
+
+environment mk_cases_on(environment const & env, name const & n) {
+    optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
+    if (!decls)
+        throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype");
+    name cases_on_name(n, "cases_on");
+    name_generator ngen;
+    name rec_name          = inductive::get_elim_name(n);
+    declaration rec_decl   = env.get(rec_name);
+    declaration ind_decl   = env.get(n);
+    unsigned num_idx_major = *inductive::get_num_indices(env, n) + 1;
+    unsigned num_minors    = *inductive::get_num_minor_premises(env, n);
+    auto idecls            = std::get<2>(*decls);
+    unsigned num_types     = length(idecls);
+    unsigned num_params    = std::get<1>(*decls);
+    buffer<expr> rec_params;
+    expr rec_type = rec_decl.get_type();
+    while (is_pi(rec_type)) {
+        expr local = mk_local(ngen.next(), binding_name(rec_type), binding_domain(rec_type), binding_info(rec_type));
+        rec_type   = instantiate(binding_body(rec_type), local);
+        rec_params.push_back(local);
+    }
+
+    levels lvls       = param_names_to_levels(rec_decl.get_univ_params());
+    bool elim_to_prop = length(rec_decl.get_univ_params()) == length(ind_decl.get_univ_params());
+    level elim_univ   = elim_to_prop ? mk_level_zero() : head(lvls);
+
+    optional<expr> unit;
+    optional<expr> star;
+    // we use unit if num_types > 1
+    if (num_types > 1) {
+        unit = mk_constant(name("unit"), to_list(elim_univ));
+        star = mk_constant(name({"unit", "star"}), to_list(elim_univ));
+    }
+
+    // rec_params order
+    //   As Cs minor_premises indices major-premise
+
+    // cases_on has
+    //   As C[i] indices major-premise minor_premises[i]
+    // That is, it only contains its type former and minor_premises
+
+    buffer<expr> cases_on_params;
+    expr rec_cnst = mk_constant(rec_name, lvls);
+    buffer<expr> rec_args; // arguments for rec used to define cases_on
+
+    // Add params: As
+    for (unsigned i = 0; i < num_params; i++) {
+        cases_on_params.push_back(rec_params[i]);
+        rec_args.push_back(rec_params[i]);
+    }
+
+    // Add C[i]
+    buffer<name> C_names;
+    bool found = false;
+    unsigned i = num_params;
+    name C_main; // name of the main type former
+    for (auto const & d : idecls) {
+        C_names.push_back(mlocal_name(rec_params[i]));
+        if (inductive::inductive_decl_name(d) == n) {
+            cases_on_params.push_back(rec_params[i]);
+            rec_args.push_back(rec_params[i]);
+            C_main = mlocal_name(rec_params[i]);
+            found = true;
+        } else {
+            rec_args.push_back(mk_fun_unit(mlocal_type(rec_params[i]), *unit));
+        }
+        i++;
+    }
+    if (!found)
+        throw_corrupted(n);
+
+    // Add indices and major-premise to rec_params
+    for (unsigned i = 0; i < num_idx_major; i++)
+        cases_on_params.push_back(rec_params[num_params + num_types + num_minors + i]);
+
+    // Ad minor premises to rec_params and rec_args
+    i = num_params + num_types;
+    for (auto const & d : idecls) {
+        bool is_main = inductive::inductive_decl_name(d) == n;
+        for (auto ir : inductive::inductive_decl_intros(d)) {
+            expr const & minor = rec_params[i];
+            if (is_main) {
+                // A cases_on minor premise does not contain "recursive" arguments
+                buffer<expr> minor_non_rec_params;
+                buffer<expr> minor_params;
+                expr minor_type = mlocal_type(minor);
+                while (is_pi(minor_type)) {
+                    expr local = mk_local(ngen.next(), binding_name(minor_type), binding_domain(minor_type),
+                                          binding_info(minor_type));
+                    if (is_type_former_arg(C_names, binding_domain(minor_type))) {
+                        if (mlocal_name(get_app_fn(binding_domain(minor_type))) == C_main) {
+                            minor_params.push_back(local);
+                        } else {
+                            minor_params.push_back(update_mlocal(local, *unit));
+                        }
+                    } else {
+                        minor_params.push_back(local);
+                        minor_non_rec_params.push_back(local);
+                    }
+                    minor_type = instantiate(binding_body(minor_type), local);
+                }
+                expr new_C = update_mlocal(minor, Pi(minor_non_rec_params, minor_type));
+                cases_on_params.push_back(new_C);
+                expr new_C_app = mk_app(new_C, minor_non_rec_params);
+                expr rec_arg   = Fun(minor_params, new_C_app);
+                rec_args.push_back(rec_arg);
+            } else {
+                rec_args.push_back(mk_fun_star(mlocal_type(minor), C_names, C_main, *unit, *star));
+            }
+            i++;
+        }
+    }
+
+    // Add indices and major-premise to rec_args
+    for (unsigned i = 0; i < num_idx_major; i++)
+        rec_args.push_back(rec_params[num_params + num_types + num_minors + i]);
+
+    expr cases_on_type  = Pi(cases_on_params, rec_type);
+    expr cases_on_value = Fun(cases_on_params,  mk_app(rec_cnst, rec_args));
+
+    bool opaque       = false;
+    bool use_conv_opt = true;
+    declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
+                                      opaque, rec_decl.get_module_idx(), use_conv_opt);
+    environment new_env = module::add(env, check(env, new_d));
+    return add_protected(new_env, cases_on_name);
+}
+}

src/library/definitional/cases_on.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 in \c env, add
+    <tt>n.cases_on</tt> to the environment.
+
+    \remark Throws an exception if \c n is not an inductive datatype.
+*/
+environment mk_cases_on(environment const & env, name const & n);
+}

src/library/definitional/unit.cpp

@@ -0,0 +1,21 @@
+/*
+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_unit_decls(environment const & env) {
+    auto d = env.find(name({"unit", "star"}));
+    if (!d)
+        return false;
+    if (length(d->get_univ_params()) != 1)
+        return false;
+    expr const & type = d->get_type();
+    if (!is_constant(type))
+        return false;
+    return const_name(type) == "unit";
+}
+}

src/library/definitional/unit.h

@@ -0,0 +1,11 @@
+/*
+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_unit_decls(environment const & env);
+}

tests/lean/interactive/num2.input.expected.out

@@ -10,6 +10,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
 pos_num.num_bits|pos_num → pos_num
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
@@ -27,6 +28,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
 -- ENDFINDP
@@ -39,6 +41,7 @@ pos_num.induction_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C
 pos_num.bit1|pos_num → pos_num
 pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n)
 pos_num.one|pos_num
+pos_num.cases_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C (pos_num.bit0 a)) → ?C n
 pos_num.rec_on|Π (n : pos_num), ?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → ?C n
 pos_num|Type
 -- ENDFINDP

tests/lean/run/sum_bug.lean

@@ -21,10 +21,6 @@ have H1 : f (inl B a1), from rfl,
 have H2 : f (inl B a2), from subst H H1,
 H2
 
-definition cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B)
-  (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
-sum.rec H1 H2 s
-
 theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
 let f := λs, rec_on s (λa', a = a') (λb, false) in
 have H1 : f (inl B a), from rfl,

tests/lean/run/tree.lean

@@ -11,12 +11,6 @@ star : one
 set_option pp.universes true
 
 namespace tree
-  section
-    variables {A : Type} {C : tree A → Type}
-    definition cases_on  (t : tree A) (e₁ : Πa, C (leaf a)) (e₂ : Πt₁ t₂, C (node t₁ t₂)) : C t :=
-    rec e₁ (λt₁ t₂ r₁ r₂, e₂ t₁ t₂) t
-  end
-
   section
     universe variables l₁ l₂
     variable {A : Type.{l₁}}