feat(definitional/brec_on): add 'mk_below' skeleton

src/frontends/lean/inductive_cmd.cpp

@@ -24,6 +24,7 @@ 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/brec_on.h"
 #include "library/definitional/no_confusion.h"
 #include "library/definitional/util.h"
 #include "frontends/lean/decl_cmds.h"
@@ -640,6 +641,7 @@ struct inductive_cmd_fn {
         bool has_unit = has_unit_decls(env);
         bool has_eq   = has_eq_decls(env);
         bool has_heq  = has_heq_decls(env);
+        // bool has_prod = has_prod_decls(env);
         for (inductive_decl const & d : decls) {
             name const & n = inductive_decl_name(d);
             pos_info pos   = *m_decl_pos_map.find(n);
@@ -657,6 +659,9 @@ struct inductive_cmd_fn {
                         // save_def_info(name(n, "no_confusion"), pos);
                     }
                 }
+                // if (has_prod) {
+                //    env = mk_below(env, inductive_decl_name(d));
+                // }
             }
         }
         return env;

src/library/definitional/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp
-  no_confusion.cpp util.cpp projection.cpp)
+  no_confusion.cpp util.cpp projection.cpp brec_on.cpp)
 
 target_link_libraries(definitional ${LEAN_LIBS})

src/library/definitional/brec_on.cpp

@@ -0,0 +1,89 @@
+/*
+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 "library/definitional/util.h"
+
+namespace lean {
+static void throw_corrupted(name const & n) {
+    throw exception(sstream() << "error in 'brec_on' generation, '" << n << "' inductive datatype declaration is corrupted");
+}
+
+environment mk_below(environment const & env, name const & n) {
+    if (!is_recursive_datatype(env, n))
+        return env;
+    if (is_inductive_predicate(env, n))
+        return env;
+    inductive::inductive_decls decls = *inductive::is_inductive_decl(env, n);
+    name_generator ngen;
+    unsigned nparams       = std::get<1>(decls);
+    declaration ind_decl   = env.get(n);
+    declaration rec_decl   = env.get(inductive::get_elim_name(n));
+    unsigned nindices      = *inductive::get_num_indices(env, n);
+    unsigned nminors       = *inductive::get_num_minor_premises(env, n);
+    unsigned ntypeformers  = length(std::get<2>(decls));
+    level_param_names lps  = rec_decl.get_univ_params();
+    level  lvl             = mk_param_univ(head(lps)); // universe we are eliminating too
+    levels lvls            = param_names_to_levels(tail(lps));
+    levels blvls           = cons(lvl, lvls);
+    level rlvl             = mk_max(mk_level_one(), lvl); // max 1 lvl: result universe of below
+    expr Type_max_1_l      = mk_sort(rlvl);
+    buffer<expr> rec_args;
+    expr type              = rec_decl.get_type();
+
+    name prod_name("prod");
+    name unit_name("unit");
+    expr inner_prod        = mk_constant(prod_name, {lvl,  rlvl});
+    expr outer_prod        = mk_constant(prod_name, {rlvl, rlvl});
+    expr unit              = mk_constant(unit_name, {rlvl});
+
+    to_telescope(ngen, type, rec_args);
+    if (rec_args.size() != nparams + ntypeformers + nminors + nindices + 1)
+        throw_corrupted(n);
+    buffer<expr> args;
+    for (unsigned i = 0; i < nparams + ntypeformers; i++)
+        args.push_back(rec_args[i]);
+    // we ignore minor premises in the below type
+    for (unsigned i = nparams + ntypeformers + nminors; i < rec_args.size(); i++)
+        args.push_back(rec_args[i]);
+
+    // create recursor application
+    levels rec_lvls       = cons(mk_succ(rlvl), lvls);
+    expr rec              = mk_constant(rec_decl.get_name(), rec_lvls);
+    for (unsigned i = 0; i < nparams; i++)
+        rec = mk_app(rec, args[i]);
+    // add type formers
+    for (unsigned i = nparams; i < nparams + ntypeformers; i++) {
+        buffer<expr> targs;
+        to_telescope(ngen, mlocal_type(args[i]), targs);
+        rec = mk_app(rec, Fun(targs, Type_max_1_l));
+    }
+    // add minor premises
+    for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) {
+        // TODO(Leo)
+    }
+    // add indices and major premise
+    for (unsigned i = nparams + ntypeformers; i < args.size(); i++) {
+        rec = mk_app(rec, args[i]);
+    }
+
+
+    name below_name  = name{n, "below"};
+    expr below_type  = Pi(args, Type_max_1_l);
+    expr below_value = Fun(args, rec);
+
+    // TODO(Leo): declare below
+    std::cout << " >> " << below_name  << "\n";
+    std::cout << "    " << below_type  << "\n";
+    std::cout << "    " << below_value << "\n";
+
+    return env;
+}
+}

src/library/definitional/brec_on.h

@@ -0,0 +1,15 @@
+/*
+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.brec_on</tt> (aka below recursion on) to the environment.
+*/
+environment mk_below(environment const & env, name const & n);
+}

src/library/definitional/util.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/find_fn.h"
+#include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
 
 namespace lean {
@@ -39,6 +40,10 @@ bool has_heq_decls(environment const & env) {
     return has_constructor(env, name{"heq", "refl"}, "heq", 2);
 }
 
+bool has_prod_decls(environment const & env) {
+    return has_constructor(env, name{"prod", "mk"}, "prod", 4);
+}
+
 bool is_recursive_datatype(environment const & env, name const & n) {
     optional<inductive::inductive_decls> decls = inductive::is_inductive_decl(env, n);
     if (!decls)
@@ -48,8 +53,9 @@ bool is_recursive_datatype(environment const & env, name const & n) {
             expr type = inductive::intro_rule_type(intro);
             while (is_pi(type)) {
                 if (find(binding_domain(type), [&](expr const & e, unsigned) {
-                            return is_constant(e) && const_name(e) == n; }))
+                            return is_constant(e) && const_name(e) == n; })) {
                     return true;
+                }
                 type = binding_body(type);
             }
         }
@@ -68,4 +74,17 @@ bool is_inductive_predicate(environment const & env, name const & n) {
     }
     return is_sort(type) && is_zero(sort_level(type));
 }
+
+expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
+    while (is_pi(type)) {
+        expr local;
+        if (binfo)
+            local = mk_local(ngen.next(), binding_name(type), binding_domain(type), *binfo);
+        else
+            local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binder_info(type));
+        telescope.push_back(local);
+        type = instantiate(binding_body(type), local);
+    }
+    return type;
+}
 }

src/library/definitional/util.h

@@ -11,6 +11,7 @@ namespace lean {
 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);
 /** \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.
 
@@ -26,4 +27,12 @@ bool is_recursive_datatype(environment const & env, name const & n);
     \remark If \c env does not have Prop (i.e., Type.{0} is not impredicative), then this method always return false.
 */
 bool is_inductive_predicate(environment const & env, name const & n);
+
+/** \brief "Consume" Pi-type \c type. This method creates local constants based on the domain of \c type
+    and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
+    binder_info, otherwise the procedure uses the one attached in the domain.
+    The procedure returns the "body" of type.
+*/
+expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope,
+                  optional<binder_info> const & binfo = optional<binder_info>());
 }