feat: prop instance yields theorems (#5856)

This PR adds a feature to the the mutual def elaborator where the
`instance` command yields theorems instead of definitions when the class
is a `Prop`.

Closes #5672

src/Lean/Elab/DefView.lean

@@ -11,19 +11,13 @@ import Lean.Elab.DeclUtil
 namespace Lean.Elab
 
 inductive DefKind where
-  | def | theorem | example | opaque | abbrev
+  | def | instance | theorem | example | opaque | abbrev
   deriving Inhabited, BEq
 
 def DefKind.isTheorem : DefKind → Bool
   | .theorem => true
   | _        => false
 
-def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
-  | .def    => true
-  | .opaque => true
-  | .abbrev => true
-  | _       => false
-
 def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false
@@ -171,7 +165,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
-    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.instance, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 

src/Lean/Elab/MutualDef.lean

@@ -867,7 +867,7 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
   letRecClosures.foldlM (init := preDefs) fun preDefs c => do
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
-    let kind ← if kind.isDefOrAbbrevOrOpaque then
+    let kind ← if kind matches .def | .instance | .opaque | .abbrev then
       -- Convert any proof let recs inside a `def` to `theorem` kind
       withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind

src/Lean/Elab/PreDefinition/Basic.lean

@@ -132,14 +132,21 @@ private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs preDef
+    let mkDefDecl : TermElabM Declaration :=
+      return Declaration.defnDecl {
+          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
+          hints := ReducibilityHints.regular (getMaxHeight (← getEnv) preDef.value + 1)
+          safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
+          all }
+    let mkThmDecl : TermElabM Declaration := do
+      let d := {
+        name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
+      }
+      reportTheoremDiag d
+      return Declaration.thmDecl d
     let decl ←
       match preDef.kind with
-      | DefKind.«theorem» =>
-        let d := {
-          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
-        }
-        reportTheoremDiag d
-        pure <| Declaration.thmDecl d
+      | DefKind.«theorem» => mkThmDecl
       | DefKind.«opaque»  =>
         pure <| Declaration.opaqueDecl {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
@@ -151,12 +158,8 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
           hints := ReducibilityHints.«abbrev»
           safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
           all }
-      | _ => -- definitions and examples
-        pure <| Declaration.defnDecl {
-          name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value
-          hints := ReducibilityHints.regular (getMaxHeight (← getEnv) preDef.value + 1)
-          safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe,
-          all }
+      | DefKind.def | DefKind.example => mkDefDecl
+      | DefKind.«instance» => if ← Meta.isProp preDef.type then mkThmDecl else mkDefDecl
     addDecl decl
     withSaveInfoContext do  -- save new env
       addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)

src/Lean/Elab/PreDefinition/Main.lean

@@ -267,7 +267,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
             logException ex
             let s ← saveState
             try
-              if preDefs.all fun preDef => preDef.kind == DefKind.def || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
+              if preDefs.all fun preDef => (preDef.kind matches DefKind.def | DefKind.instance) || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
                 -- try to add as partial definition
                 try
                   addAndCompilePartial preDefs (useSorry := true)

tests/lean/run/5672.lean

@@ -0,0 +1,27 @@
+/-!
+# `instance` creates a theorem if the class is a `Prop`
+
+https://github.com/leanprover/lean4/issues/5672
+-/
+
+class A : Prop
+
+instance a : A where
+
+/--
+info: theorem a : A :=
+{ }
+-/
+#guard_msgs in #print a
+
+
+/-!
+Uses `def` variable inclusion rules
+-/
+section
+variable (x : Nat)
+instance b : A := by
+  cases x <;> exact {}
+/-- info: b (x : Nat) : A -/
+#guard_msgs in #check b
+end