feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command

src/frontends/lean/structure_cmd.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/module.h"
 #include "library/aliases.h"
+#include "library/annotation.h"
 #include "library/coercion.h"
 #include "library/explicit.h"
 #include "library/protected.h"
@@ -106,7 +107,9 @@ struct structure_cmd_fn {
     buffer<expr>                m_fields;
     std::vector<rename_vector>  m_renames;
     std::vector<field_map>      m_field_maps;
+    bool                        m_explicit_universe_params;
     bool                        m_infer_result_universe;
+    bool                        m_inductive_predicate;
     levels                      m_ctx_levels; // context levels for creating aliases
     buffer<expr>                m_ctx_locals; // context local constants for creating aliases
 
@@ -115,7 +118,9 @@ struct structure_cmd_fn {
 
     structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_namespace(get_namespace(m_env)) {
         m_tc = mk_type_checker(m_env);
+        m_explicit_universe_params = false;
         m_infer_result_universe    = false;
+        m_inductive_predicate      = false;
         m_gen_eta     = get_structure_eta_thm(p.get_options());
         m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options());
     }
@@ -127,9 +132,11 @@ struct structure_cmd_fn {
         m_name = m_namespace + m_name;
         buffer<name> ls_buffer;
         if (parse_univ_params(m_p, ls_buffer)) {
+            m_explicit_universe_params = true;
             m_infer_result_universe    = false;
             m_level_names.append(ls_buffer);
         } else {
+            m_explicit_universe_params = false;
             m_infer_result_universe    = true;
         }
         m_modifiers.parse(m_p);
@@ -239,8 +246,15 @@ struct structure_cmd_fn {
         if (m_p.curr_is_token(get_colon_tk())) {
             m_p.next();
             m_type = m_p.parse_expr();
+            while (is_annotation(m_type))
+                m_type = get_annotation_arg(m_type);
+            m_inductive_predicate = m_env.impredicative() && is_zero(sort_level(m_type));
             if (!is_sort(m_type))
                 throw parser_error("invalid 'structure', 'Type' expected", pos);
+
+            if (m_inductive_predicate)
+                m_infer_result_universe = false;
+
             if (m_infer_result_universe) {
                 if (!is_placeholder(sort_level(m_type)))
                     throw parser_error("invalid 'structure', resultant universe level is computed "
@@ -248,10 +262,6 @@ struct structure_cmd_fn {
             } else {
                 if (has_placeholder(m_type))
                     throw_explicit_universe(pos);
-                level l = sort_level(m_type);
-                if (m_env.impredicative() && !is_not_zero(l))
-                    throw parser_error("invalid 'structure', the resultant universe level should not be zero "
-                                       "for any universe parameter assignment", pos);
             }
         } else {
             if (!m_infer_result_universe)
@@ -462,7 +472,7 @@ struct structure_cmd_fn {
 
     /** \brief Add params, fields and references to parent structures into parser local scope */
     void add_locals() {
-        if (!m_infer_result_universe) {
+        if (m_explicit_universe_params) {
             for (name const & l : m_level_names)
                 m_p.add_local_level(l, mk_param_univ(l));
         }
@@ -948,9 +958,11 @@ struct structure_cmd_fn {
         declare_projections();
         declare_auxiliary();
         declare_coercions();
+        if (!m_inductive_predicate) {
             declare_eta();
             declare_proj_over_mk();
             declare_no_confustion();
+        }
         return m_env;
     }
 };

src/library/definitional/projection.cpp

@@ -192,9 +192,10 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
     expr intro_type              = inductive::intro_rule_type(intro);
     name rec_name                = inductive::get_elim_name(n);
     declaration ind_decl         = env.get(n);
-    if (env.impredicative() && is_prop(ind_decl.get_type()))
-        throw exception(sstream() << "projection generation, '" << n << "' is a proposition");
     declaration rec_decl         = env.get(rec_name);
+    bool is_predicate            = env.impredicative() && is_prop(ind_decl.get_type());
+    bool elim_to_prop            = rec_decl.get_num_univ_params() == ind_decl.get_num_univ_params();
+    bool dep_elim                = inductive::has_dep_elim(env, n);
     level_param_names lvl_params = ind_decl.get_univ_params();
     levels lvls                  = param_names_to_levels(lvl_params);
     buffer<expr> params; // datatype parameters
@@ -222,16 +223,20 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         if (!is_pi(intro_type))
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
+        type_checker tc(new_env);
         expr result_type   = binding_domain(intro_type);
+        if (is_predicate && !tc.is_prop(result_type).first) {
+            throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
+                            << "type is an inductive predicate, but field is not a proposition");
+        }
         buffer<expr> proj_args;
         proj_args.append(params);
         proj_args.push_back(c);
-        expr type_former   = Fun(c, result_type);
+        expr type_former   = dep_elim ? Fun(c, result_type) : result_type;
         expr minor_premise = Fun(intro_type_args, mk_var(intro_type_args.size() - i - 1));
         expr major_premise = c;
-        type_checker tc(new_env);
         level l            = sort_level(tc.ensure_sort(tc.infer(result_type).first).first);
-        levels rec_lvls    = append(to_list(l), lvls);
+        levels rec_lvls    = elim_to_prop ? lvls : append(to_list(l), lvls);
         expr rec           = mk_constant(rec_name, rec_lvls);
         buffer<expr> rec_args;
         rec_args.append(params);

tests/lean/bad_structures.lean

@@ -7,6 +7,6 @@ structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type :=
 structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{l} :=
 (pr1 : A) (pr2 : B)
 
-structure prod.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
+structure prod2.{l} (A : Type.{l}) (B : Type.{l}) : Type.{max 1 l} :=
 (pr1 : A) (pr2 : B)
 end foo

tests/lean/bad_structures.lean.expected.out

@@ -1,3 +1,2 @@
 bad_structures.lean:1:71: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
 bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
-bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment

tests/lean/bad_structures2.lean

@@ -29,3 +29,6 @@ structure bla2 extends Type
 
 structure bla2 : Prop :=
 (x : Prop)
+
+structure bla3 : Prop :=
+(x : nat)

tests/lean/bad_structures2.lean.expected.out

@@ -8,4 +8,5 @@ bad_structures2.lean:18:2: error: invalid field, identifier expected
 bad_structures2.lean:23:36: error: invalid 'structure' renaming, parent structure 'foo' does not contain field 'y'
 bad_structures2.lean:25:23: error: invalid 'structure' extends, 'nat' is not a structure
 bad_structures2.lean:27:23: error: invalid 'structure', expression must be a 'parent' structure
-bad_structures2.lean:30:15: error: invalid 'structure', 'Type' expected
+bad_structures2.lean:30:0: error: failed to generate projection 'bla2.x' for 'bla2', type is an inductive predicate, but field is not a proposition
+bad_structures2.lean:33:0: error: failed to generate projection 'bla3.x' for 'bla3', type is an inductive predicate, but field is not a proposition

tests/lean/proj.lean.expected.out

@@ -1,5 +1,4 @@
 proj.lean:7:0: error: projection generation, 'or' does not have a single constructor
-proj.lean:8:0: error: projection generation, 'and' is a proposition
 proj.lean:9:0: error: projection generation, 'eq.refl' is not an inductive datatype
 proj.lean:10:0: error: projection generation, 'eq' is an indexed inductive datatype family
 proj.lean:11:0: error: projection generation, 'vector' is an indexed inductive datatype family

tests/lean/run/pred_using_structure_cmd.lean

@@ -0,0 +1,13 @@
+variable {A : Type}
+
+structure has_refl (R : A → A → Prop) : Prop :=
+(refl : ∀ a, R a a)
+
+structure is_equiv (R : A → A → Prop) extends has_refl R : Prop :=
+(symm : ∀ a b, R a b → R b a)
+(trans : ∀ a b c, R a b → R b c → R a c)
+
+check @is_equiv.refl
+check @is_equiv.symm
+check @is_equiv.trans
+check @is_equiv.to_has_refl