feat(library,frontends/lean): validate user defined recursors and add attribute to mark them

see issue #492

The user-defined recursors will also be used to implement the blast tactic

src/emacs/lean-syntax.el

@@ -123,7 +123,7 @@
                "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
                "\[whnf\]" "\[multiple-instances\]" "\[none\]"
                "\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
-               "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]"
+               "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[recursor\]"
                "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]"
                "\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]"))
       . 'font-lock-doc-face)

src/frontends/lean/decl_cmds.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/class.h"
 #include "library/abbreviation.h"
 #include "library/equivalence_manager.h"
+#include "library/user_recursors.h"
 #include "library/unfold_macros.h"
 #include "library/definitional/equations.h"
 #include "library/error_handling/error_handling.h"
@@ -359,6 +360,7 @@ struct decl_attributes {
     bool               m_trans;
     bool               m_refl;
     bool               m_subst;
+    bool               m_recursor;
     optional<unsigned> m_priority;
     optional<unsigned> m_unfold_c_hint;
 
@@ -382,6 +384,7 @@ struct decl_attributes {
         m_trans                  = false;
         m_refl                   = false;
         m_subst                  = false;
+        m_recursor               = false;
     }
 
     struct elim_choice_fn : public replace_visitor {
@@ -508,6 +511,9 @@ struct decl_attributes {
             } else if (p.curr_is_token(get_subst_tk())) {
                 p.next();
                 m_subst = true;
+            } else if (p.curr_is_token(get_recursor_tk())) {
+                p.next();
+                m_recursor = true;
             } else {
                 break;
             }
@@ -563,6 +569,8 @@ struct decl_attributes {
             env = add_trans(env, d, m_persistent);
         if (m_subst)
             env = add_subst(env, d, m_persistent);
+        if (m_recursor)
+            env = add_user_recursor(env, d, m_persistent);
         if (m_is_class)
             env = add_class(env, d, m_persistent);
         if (m_has_multiple_instances)

src/frontends/lean/token_table.cpp

@@ -107,7 +107,7 @@ void init_token_table(token_table & t) {
          "definition", "example", "coercion", "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
-         "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]",
+         "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor]",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]",
          "[constructor]", "[unfold-c", "print",
          "end", "namespace", "section", "prelude", "help",

src/frontends/lean/tokens.cpp

@@ -138,6 +138,7 @@ static name * g_symm         = nullptr;
 static name * g_trans        = nullptr;
 static name * g_refl         = nullptr;
 static name * g_subst        = nullptr;
+static name * g_recursor     = nullptr;
 
 void initialize_tokens() {
     g_period       = new name(".");
@@ -248,6 +249,7 @@ void initialize_tokens() {
     g_trans        = new name("[trans]");
     g_refl         = new name("[refl]");
     g_subst        = new name("[subst]");
+    g_recursor     = new name("[recursor]");
     g_attribute    = new name("attribute");
     g_with         = new name("with");
     g_class        = new name("[class]");
@@ -315,6 +317,7 @@ void finalize_tokens() {
     delete g_refl;
     delete g_trans;
     delete g_subst;
+    delete g_recursor;
     delete g_reducible;
     delete g_quasireducible;
     delete g_semireducible;
@@ -512,6 +515,7 @@ name const & get_symm_tk() { return *g_symm; }
 name const & get_trans_tk() { return *g_trans; }
 name const & get_refl_tk() { return *g_refl; }
 name const & get_subst_tk() { return *g_subst; }
+name const & get_recursor_tk() { return *g_recursor; }
 name const & get_reducible_tk() { return *g_reducible; }
 name const & get_quasireducible_tk() { return *g_quasireducible; }
 name const & get_semireducible_tk() { return *g_semireducible; }

src/frontends/lean/tokens.h

@@ -140,4 +140,5 @@ name const & get_symm_tk();
 name const & get_trans_tk();
 name const & get_refl_tk();
 name const & get_subst_tk();
+name const & get_recursor_tk();
 }

src/library/CMakeLists.txt

@@ -13,6 +13,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
   local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp
   app_builder.cpp projection.cpp abbreviation.cpp equivalence_manager.cpp
-  export.cpp)
+  export.cpp user_recursors.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/init_module.cpp

@@ -37,6 +37,7 @@ Author: Leonardo de Moura
 #include "library/normalize.h"
 #include "library/abbreviation.h"
 #include "library/equivalence_manager.h"
+#include "library/user_recursors.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -73,9 +74,11 @@ void initialize_library_module() {
     initialize_normalize();
     initialize_abbreviation();
     initialize_equivalence_manager();
+    initialize_user_recursors();
 }
 
 void finalize_library_module() {
+    finalize_user_recursors();
     finalize_equivalence_manager();
     finalize_abbreviation();
     finalize_normalize();

src/library/user_recursors.cpp

@@ -0,0 +1,250 @@
+/*
+Copyright (c) 2015 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/inductive/inductive.h"
+#include "library/scoped_ext.h"
+#include "library/util.h"
+#include "library/kernel_serializer.h"
+#include "library/user_recursors.h"
+
+namespace lean {
+bool recursor_info::is_minor(unsigned pos) const {
+    if (pos <= get_motive_pos())
+        return false;
+    if (get_first_index_pos() <= pos && pos <= m_major_pos)
+        return false;
+    return true;
+}
+
+recursor_info::recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major,
+                             optional<unsigned> const & motive_univ_pos, bool dep_elim):
+    m_recursor(r), m_type_name(I), m_num_params(num_params), m_num_indices(num_indices), m_major_pos(major),
+    m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim) {}
+recursor_info::recursor_info() {}
+
+void recursor_info::write(serializer & s) const {
+    s << m_recursor << m_type_name << m_num_params << m_num_indices << m_major_pos << m_motive_univ_pos << m_dep_elim;
+}
+
+recursor_info recursor_info::read(deserializer & d) {
+    recursor_info info;
+    d >> info.m_recursor >> info.m_type_name >> info.m_num_params >> info.m_num_indices >> info.m_major_pos
+      >> info.m_motive_univ_pos >> info.m_dep_elim;
+    return info;
+}
+
+static void throw_invalid_motive(expr const & C) {
+    throw exception(sstream() << "invalid user defined recursor, motive '" << C
+                    << "' must have a type of the form (C : Pi (i : B A), I A i -> Type), "
+                    "where A is (possibly empty) sequence of bound variables (aka parameters), "
+                    "(i : B A) is a (possibly empty) telescope (aka indices), "
+                    "and I is a constant");
+}
+
+static void throw_invalid_major(buffer<expr> const & tele, expr const & I, unsigned num_params,
+                                unsigned num_indices, unsigned major_pos) {
+    sstream msg;
+    msg << "invalid user defined recursor, major premise '" << tele[major_pos] << "' is expected to have type " << I;
+    for (unsigned i = 0; i < num_params; i++)
+        msg << " " << tele[i];
+    for (unsigned i = major_pos - num_indices; i < major_pos; i++)
+        msg << " " << tele[i];
+    throw exception(msg);
+}
+
+recursor_info mk_recursor_info(environment const & env, name const & r) {
+    if (auto I = inductive::is_elim_rule(env, r)) {
+        if (*inductive::get_num_type_formers(env, r) > 1)
+            throw exception(sstream() << "unsupported recursor '" << r << "', it has multiple motives");
+        optional<unsigned> motive_univ_pos;
+        if (env.get(name(*I, "rec")).get_num_univ_params() != env.get(name(*I)).get_num_univ_params())
+            motive_univ_pos = 0;
+        return recursor_info(r, *I,
+                             *inductive::get_num_params(env, *I),
+                             *inductive::get_num_indices(env, *I),
+                             *inductive::get_elim_major_idx(env, *I),
+                             motive_univ_pos,
+                             inductive::has_dep_elim(env, *I));
+    }
+    declaration d = env.get(r);
+    type_checker tc(env);
+    buffer<expr> tele;
+    expr rtype    = to_telescope(tc, d.get_type(), tele);
+    buffer<expr> C_args;
+    expr C        = get_app_args(rtype, C_args);
+    if (!is_local(C) || !std::all_of(C_args.begin(), C_args.end(), is_local) || C_args.empty()) {
+        throw exception("invalid user defined recursor, result type must be of the form (C i t), "
+                        "where C and t are bound variables, and i is a (possibly empty) sequence of bound variables");
+    }
+    unsigned num_indices = C_args.size() - 1;
+    unsigned num_params  = 0;
+    for (expr const & x : tele) {
+        if (mlocal_name(x) == mlocal_name(C))
+            break;
+        num_params++;
+    }
+    buffer<expr> C_tele;
+    expr C_rtype  = to_telescope(tc, mlocal_type(C), C_tele);
+    if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) {
+        throw_invalid_motive(C);
+    }
+    optional<unsigned> C_univ_pos;
+    level C_lvl = sort_level(C_rtype);
+    if (!is_standard(env) || !is_zero(C_lvl)) {
+        if (!is_param(C_lvl)) {
+            if (is_standard(env))
+                throw exception("invalid user defined recursor, "
+                                "motive result sort must be Prop or Type.{l} where l is a universe parameter");
+            else
+                throw exception("invalid user defined recursor, "
+                                "motive result sort must be Type.{l} where l is a universe parameter");
+        }
+        name l  = param_id(C_lvl);
+        C_univ_pos = 0;
+        for (name const & l_curr : d.get_univ_params()) {
+            if (l_curr == l)
+                break;
+            C_univ_pos = *C_univ_pos + 1;
+        }
+        lean_assert(*C_univ_pos < length(d.get_univ_params()));
+    }
+
+    buffer<expr> I_args;
+    expr I = get_app_args(mlocal_type(C_tele.back()), I_args);
+    if (!is_constant(I) || I_args.size() != num_params + num_indices) {
+        throw_invalid_motive(C);
+    }
+    for (unsigned i = 0; i < num_params; i++) {
+        if (mlocal_name(I_args[i]) != mlocal_name(tele[i]))
+            throw_invalid_motive(C);
+    }
+    for (unsigned i = 0; i < num_indices; i++) {
+        if (mlocal_name(I_args[num_params + i]) != mlocal_name(C_tele[i]))
+            throw_invalid_motive(C);
+    }
+    expr const & major  = C_args.back();
+    unsigned major_pos  = 0;
+    for (expr const & x : tele) {
+        if (mlocal_name(x) == mlocal_name(major))
+            break;
+        major_pos++;
+    }
+    lean_assert(major_pos < tele.size());
+    if (major_pos < num_indices)
+        throw exception(sstream() << "invalid user defined recursor, indices must occur before major premise '"
+                        << major << "'");
+    recursor_info info(r, const_name(I), num_params, num_indices, major_pos, C_univ_pos, true);
+    unsigned first_index_pos = info.get_first_index_pos();
+    for (unsigned i = 0; i < num_indices; i++) {
+        if (mlocal_name(tele[first_index_pos+i]) != mlocal_name(C_args[i])) {
+            throw exception(sstream() << "invalid user defined recursor, index '" << C_args[i]
+                            << "' expected, but got '" << tele[i] << "'");
+        }
+    }
+    buffer<expr> I_args_major;
+    expr I_major = get_app_args(mlocal_type(tele[major_pos]), I_args_major);
+    if (I != I_major)
+        throw_invalid_major(tele, I, num_params, num_indices, major_pos);
+    for (unsigned i = 0; i < num_params; i++) {
+        if (mlocal_name(I_args_major[i]) != mlocal_name(tele[i]))
+            throw_invalid_major(tele, I, num_params, num_indices, major_pos);
+    }
+    for (unsigned i = 0; i < num_indices; i++) {
+        if (mlocal_name(I_args_major[num_params + i]) != mlocal_name(tele[first_index_pos + i]))
+            throw_invalid_major(tele, I, num_params, num_indices, major_pos);
+    }
+    for (unsigned i = 0; i < tele.size(); i++) {
+        if (info.is_minor(i)) {
+            buffer<expr> minor_tele;
+            expr minor_rtype = to_telescope(tc, mlocal_type(tele[i]), minor_tele);
+            expr minor_C     = get_app_fn(minor_rtype);
+            if (!is_local(minor_C) || mlocal_name(minor_C) != mlocal_name(C))
+                throw exception(sstream() << "invalid user defined recursor, resultant type of minor premise '"
+                                << tele[i] << "' must be of the form (" << C << " ...)");
+        }
+    }
+    return info;
+}
+
+struct recursor_state {
+    name_map<recursor_info> m_recursors;
+    name_map<list<name>>    m_type2recursors;
+
+    void insert(recursor_info const & info) {
+        m_recursors.insert(info.get_name(), info);
+        if (auto l = m_type2recursors.find(info.get_type_name())) {
+            m_type2recursors.insert(info.get_type_name(),
+                                    cons(info.get_name(),
+                                         filter(*l, [&](name const & n) { return n != info.get_name(); })));
+        } else {
+            m_type2recursors.insert(info.get_type_name(), to_list(info.get_name()));
+        }
+    }
+};
+
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
+struct recursor_config {
+    typedef recursor_state  state;
+    typedef recursor_info   entry;
+
+    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
+        s.insert(e);
+    }
+    static name const & get_class_name() {
+        return *g_class_name;
+    }
+    static std::string const & get_serialization_key() {
+        return *g_key;
+    }
+    static void  write_entry(serializer & s, entry const & e) {
+        e.write(s);
+    }
+    static entry read_entry(deserializer & d) {
+        return recursor_info::read(d);
+    }
+    static optional<unsigned> get_fingerprint(entry const & e) {
+        return some(e.get_name().hash());
+    }
+};
+
+template class scoped_ext<recursor_config>;
+typedef scoped_ext<recursor_config> recursor_ext;
+
+environment add_user_recursor(environment const & env, name const & r, bool persistent) {
+    if (inductive::is_elim_rule(env, r))
+        throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor");
+    recursor_info info = mk_recursor_info(env, r);
+    return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent);
+}
+
+recursor_info get_recursor_info(environment const & env, name const & r) {
+    if (auto info = recursor_ext::get_state(env).m_recursors.find(r))
+        return *info;
+    return mk_recursor_info(env, r);
+}
+
+list<name> get_recursors_for(environment const & env, name const & I) {
+    if (auto l = recursor_ext::get_state(env).m_type2recursors.find(I))
+        return *l;
+    else
+        return list<name>();
+}
+
+void initialize_user_recursors() {
+    g_class_name = new name("recursor");
+    g_key        = new std::string("urec");
+    recursor_ext::initialize();
+}
+
+void finalize_user_recursors() {
+    recursor_ext::finalize();
+    delete g_class_name;
+    delete g_key;
+}
+}

src/library/user_recursors.h

@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+/** \brief Information for a user defined recursor */
+class recursor_info {
+    name               m_recursor;
+    name               m_type_name;
+    unsigned           m_num_params;
+    unsigned           m_num_indices;
+    unsigned           m_major_pos;
+    optional<unsigned> m_motive_univ_pos; // if none, then recursor can only eliminate to Prop
+    bool               m_dep_elim;
+
+public:
+    recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major,
+                  optional<unsigned> const & motive_univ_pos, bool dep_elim);
+    recursor_info();
+
+    name const & get_name() const { return m_recursor; }
+    name const & get_type_name() const { return m_type_name; }
+    unsigned get_num_params() const { return m_num_params; }
+    unsigned get_num_indices() const { return m_num_indices; }
+    unsigned get_motive_pos() const { return m_num_params; }
+    unsigned get_first_index_pos() const { return m_major_pos - m_num_indices; }
+    unsigned get_major_pos() const { return m_major_pos; }
+    optional<unsigned> get_motive_univ_pos() const { return m_motive_univ_pos; }
+    bool has_dep_elim() const { return m_dep_elim; }
+    bool is_minor(unsigned pos) const;
+
+    void write(serializer & s) const;
+    static recursor_info read(deserializer & d);
+};
+
+environment add_user_recursor(environment const & env, name const & r, bool persistent);
+recursor_info get_recursor_info(environment const & env, name const & r);
+list<name> get_recursors_for(environment const & env, name const & I);
+void initialize_user_recursors();
+void finalize_user_recursors();
+}

src/library/util.cpp

@@ -218,15 +218,17 @@ expr fun_to_telescope(name_generator & ngen, expr const & e, buffer<expr> & tele
 
 expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
                   constraint_seq & cs) {
-    type = tc.whnf(type, cs);
-    while (is_pi(type)) {
+    expr new_type = tc.whnf(type, cs);
+    while (is_pi(new_type)) {
+        type = new_type;
         expr local;
         if (binfo)
             local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), *binfo);
         else
             local = mk_local(tc.mk_fresh_name(), binding_name(type), binding_domain(type), binding_info(type));
         telescope.push_back(local);
-        type = tc.whnf(instantiate(binding_body(type), local), cs);
+        type     = instantiate(binding_body(type), local);
+        new_type = tc.whnf(type, cs);
     }
     return type;
 }

tests/lean/urec.lean

@@ -0,0 +1,33 @@
+import data.nat data.vector data.list.basic
+
+attribute nat [recursor]
+
+attribute nat.rec [recursor]
+
+attribute nat.rec_on [recursor]
+
+attribute nat.strong_induction_on [recursor]
+
+attribute nat.cases_on [recursor]
+
+attribute vector.cases_on [recursor]
+
+attribute vector.brec_on [recursor]
+
+axiom badrec1 : Π (A : Type) (C : A → Type) (a : A) (l : list A), C a
+
+attribute badrec1 [recursor]
+
+axiom badrec2 : Π (A : Type) (M : list A → Type) (l : list A) (a : nat), M l
+
+attribute badrec2 [recursor]
+
+open list
+axiom myrec : Π (A : Type) (M : list A → Type) (l : list A), M [] → (∀ a, M [a]) → (∀ a₁ a₂, M [a₁, a₂]) → M l
+
+attribute myrec [recursor]
+
+set_option pp.implicit true
+set_option pp.universes true
+
+check @myrec

tests/lean/urec.lean.expected.out

@@ -0,0 +1,7 @@
+urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C i t), where C and t are bound variables, and i is a (possibly empty) sequence of bound variables
+urec.lean:5:0: error: invalid user defined recursor, 'nat.rec' is a builtin recursor
+urec.lean:19:0: error: invalid user defined recursor, motive 'C' must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of bound variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant
+urec.lean:23:0: error: invalid user defined recursor, resultant type of minor premise 'a' must be of the form (M ...)
+myrec.{l_1 l_2} :
+  Π (A : Type.{l_1}) (M : list.{l_1} A → Type.{l_2}) (l : list.{l_1} A),
+    M (@nil.{l_1} A) → (Π (a : A), M [a]) → (Π (a₁ a₂ : A), M [a₁, a₂]) → M l