fix: proposition fields default values

closes #2575

src/Lean/Elab/StructInst.lean

@@ -821,7 +821,9 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
     | some r => reduce structNames r
     | none   => return e.updateProj! (← reduce structNames b)
   | .app f .. =>
-    match (← reduceProjOf? e structNames.contains) with
+    -- Recall that proposition fields are theorems. Thus, we must set transparency to .all
+    -- to ensure they are unfolded here
+    match (← withTransparency .all <| reduceProjOf? e structNames.contains) with
     | some r => reduce structNames r
     | none   =>
       let f := f.getAppFn

src/Lean/Elab/Structure.lean

@@ -713,8 +713,8 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           subobject? :=
             if info.kind == StructFieldKind.subobject then
               match env.find? info.declName with
-              | some (ConstantInfo.defnInfo val) =>
-                match val.type.getForallBody.getAppFn with
+              | some info =>
+                match info.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName
                 | _ => panic! "ill-formed structure"
               | _ => panic! "ill-formed environment"

src/kernel/declaration.cpp

@@ -205,6 +205,10 @@ declaration mk_definition(environment const & env, name const & n, names const &
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Definition), mk_definition_val(env, n, params, t, v, safety)));
 }
 
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
+}
+
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {
     return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Opaque), opaque_val(n, params, t, v, is_unsafe, names(n))));
 }

src/kernel/declaration.h

@@ -223,10 +223,12 @@ inline optional<declaration> none_declaration() { return optional<declaration>()
 inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
 inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
 
+bool use_unsafe(environment const & env, expr const & e);
 declaration mk_definition(name const & n, names const & lparams, expr const & t, expr const & v,
                           reducibility_hints const & hints, definition_safety safety = definition_safety::safe);
 declaration mk_definition(environment const & env, name const & n, names const & lparams, expr const & t, expr const & v,
                           definition_safety safety = definition_safety::safe);
+declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val);
 declaration mk_opaque(name const & n, names const & lparams, expr const & t, expr const & v, bool unsafe);
 declaration mk_axiom(name const & n, names const & lparams, expr const & t, bool unsafe = false);
 declaration mk_inductive_decl(names const & lparams, nat const & nparams, inductive_types const & types, bool is_unsafe);

src/library/constructions/projection.cpp

@@ -86,7 +86,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             throw exception(sstream() << "generating projection '" << proj_name << "', '"
                             << n << "' does not have sufficient data");
         expr result_type   = consume_type_annotations(binding_domain(cnstr_type));
-        if (is_predicate && !type_checker(new_env, lctx).is_prop(result_type)) {
+        bool is_prop       = type_checker(new_env, lctx).is_prop(result_type);
+        if (is_predicate && !is_prop) {
             throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', "
                             << "type is an inductive predicate, but field is not a proposition");
         }
@@ -97,13 +98,24 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         proj_type      = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit);
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
-        declaration new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
+        declaration new_d;
+        if (is_prop) {
+            bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
+            if (unsafe) {
+                // theorems cannot be unsafe
+                new_d = mk_opaque(proj_name, lvl_params, proj_type, proj_val, unsafe);
+            } else {
+                new_d = mk_theorem(proj_name, lvl_params, proj_type, proj_val);
+            }
+        } else {
+            new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val,
                                                            reducibility_hints::mk_abbreviation());
+        }
         new_env = new_env.add(new_d);
-        if (!inst_implicit)
+        if (!inst_implicit && !is_prop)
             new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true);
         new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit);
-        expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
+        expr proj    = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
         cnstr_type   = instantiate(binding_body(cnstr_type), proj);
         i++;
     }

tests/lean/run/2575.lean

@@ -0,0 +1,12 @@
+structure AtLeastThirtySeven where
+  val : Nat
+  le : 37 ≤ val
+
+theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
+
+/--
+info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
+fun self => self.2
+-/
+#guard_msgs in
+#print AtLeastThirtySeven.le