feat: add coinductive command to specify coinductive predicates (#10333)

This PR introduces a `coinductive` keyword, that can be used to define
coinductive predicates via a syntax identical to the one for `inductive`
keyword. The machinery relies on the implementation of elaboration of
inductive types and extracts an endomap on the appropriate space of the
predicates from the definition that is then fed to the
`PartialFixpoint`. Upon elaborating definitions, all the constructors
are declared through automatically generated lemmas.

For example, infinite sequence of transitions in a relation, can be
given by the following:
```lean4
section
variable (α : Type)
coinductive infSeq (r : α → α → Prop) : α → Prop where
  | step : r a b → infSeq r b → infSeq r a
  
/--
info: infSeq.coinduct (α : Type) (r : α → α → Prop) (pred : α → Prop) (hyp : ∀ (x : α), pred x → ∃ b, r x b ∧ pred b)
  (x✝ : α) : pred x✝ → infSeq α r x✝
-/
#guard_msgs in
#check infSeq.coinduct

/--
info: infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
-/
#guard_msgs in
#check infSeq.step
end
```
The machinery also supports `mutual` blocks, as well as mixing inductive
and coinductive predicate definitions:
```lean4
mutual
  coinductive tick : Prop where
  | mk : ¬tock → tick

  inductive tock : Prop where
  | mk : ¬tick → tock
end

/--
info: tick.mutual_induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
  (pred_1 → tick) ∧ (tock → pred_2)
-/
#guard_msgs in
#check tick.mutual_induct
```

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Elab/Coinductive.lean

@@ -0,0 +1,490 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+
+module
+
+prelude
+
+public import Lean.Elab.PreDefinition.PartialFixpoint
+public import Lean.Elab.Tactic.Rewrite
+public import Lean.Meta.Tactic.Simp
+public import Lean.Linter.UnusedVariables
+namespace Lean.Elab.Command
+open Lean Meta Elab
+
+builtin_initialize
+  registerTraceClass `Elab.coinductive
+
+/-
+  This file contains the main bits of the implementation of `coinductive` keyword.
+  The main entry point is the `elabCoinductive`.
+
+  At the beginning, elaboration of mutual blocks where some definitions are defined via
+  `coinductive` keyword is the same as of `inductive`. However, in the `elabInductives` we
+  elaborate views, as they were `inductive` types, but just before replacing the free variables
+  with constants and adding it to the kernel, we call `mkFlatInductive` that rewrites the inductives
+  to the "flat" form, that is we add parameters for each of the definitions in the clique
+  and replace recursive calls in constructors with these parameters. For example, the following definition
+
+  ```
+  variable (α : Type)
+  coinductive infSeq (r : α → α → Prop) : α → Prop where
+  | step : r a b → infSeq r b → infSeq r a
+  ```
+
+  yields the following "flat" inductive:
+  ```
+  inductive infSeq._functor (r : α → α → Prop) (infSeq._functor.call : α → Prop) : α → Prop where
+  | step : r a b → infSeq._functor.call b → infSeq r a
+  ```
+
+  Upon such rewrite, the code for adding flat inductives does not diverge much from the usual
+  way its done for inductive declarations, but we omit applying attributes/modifiers and
+  we do not set the syntax references to track those declarations (as this is auxillary piece of
+  data hidden from the user).
+
+  Then, upon adding such flat inductives for each definition in the mutual block to the environment,
+  we use `Meta.MkIffOfInductiveProp` machinery to rewrite those to predicates made of disjunctions
+  and existentials that we will refer to as "existential" form. This form makes it easy to generate
+  user-readable coinduction proof principles and allows to use existing `monotonicity` tactic.
+
+  For example, the above flat inductive corresponds to:
+  ```
+    def infSeq._functor.existential : (α : Type) → (α → α → Prop) → (α → Prop) → α → Prop :=
+      fun α r infSeq._functor.call a => ∃ b, r a b ∧ infSeq._functor.call b
+  ```
+
+  Both forms are connected through the following lemma (that is generated by
+  `Meta.MkIffOfInductive`) machinery:
+  ```
+    infSeq._functor.existential_equiv (α : Type) (r : α → α → Prop)
+      (infSeq._functor.call : α → Prop) (a✝ : α) :
+      infSeq._functor α r infSeq._functor.call a✝ ↔ ∃ b, r a✝ b ∧ infSeq._functor.call b
+  ```
+
+  Those definitions are used to populate `PreDefinition`s that are then passed to `PartialFixpoint`
+  machinery.
+
+  At that stage all predicates (if definitions are monotone) are added to the environment.
+  Note that at this point `PartialFixpoint` machinery applies the attributes and modifiers. We
+  use the syntax references from the original `InductiveView`s and set them to those declarations.
+
+  Moreover, we have following theorem (generated by `generateEqLemmas`) that connets the coinductive
+  predicate to its flat inductive:
+  ```
+    info: infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝
+  ```
+
+  We use these to define all the constructors from the original definition. For example, we obtain:
+  ```
+    infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
+  ```
+
+  Similarly, we obtain the associated `casesOn` lemma (that are generated by `mkCasesOnCoinductive`):
+  ```
+    infSeq.casesOn (α : Type) (r : α → α → Prop) {motive : (a : α) → infSeq α r a → Prop} {a✝ : α} (t : infSeq α r a✝)
+    (step : ∀ {a b : α} (a_1 : r a b) (a_2 : infSeq α r b), motive a (infSeq.step α r a_1 a_2)) : motive a✝ t
+  ```
+
+  At the very end, we make use of the syntax references from the original `InductiveView`s
+  and set them to newly generated constructors. We apply deriving handlers and docstrings.
+  Note that attributes and modifiers are handled earlier by `PartialFixpoint` machinery
+-/
+
+/-- This structure contains the data carried in `InductiveElabStep1` that are solely used in
+mutual coinductive predicate elaboration. -/
+public structure CoinductiveElabData where
+  /-- Declaration Id from the original `InductiveView` -/
+  declId : Syntax
+  /-- Declaration name of the predicate-/
+  declName : Name
+  /-- Ref from the original `InductiveView`-/
+  ref : Syntax
+  /-- Modifiers from the original `InductiveView`-/
+  modifiers : Modifiers
+  /-- Constructor refs from the original `InductiveView`-/
+  ctorSyntax : Array Syntax
+  /-- The flag that is `true` if the predicate was defined via `coinductive` keyword and `false`
+  otherwise. When we elaborate a mutual definition, we allow mixing `coinductive` and `inductive`
+  keywords, and hence we need to record this information.
+  -/
+  isGreatest : Bool
+  deriving Inhabited
+
+
+public def addFunctorPostfix : Name → Name := (·  ++ `_functor)
+
+public def removeFunctorPostfix : Name → Name := (Name.modifyBase · Name.getPrefix)
+
+public def removeFunctorPostfixInCtor : Name → Name :=
+  fun | Name.str p s => Name.str (removeFunctorPostfix p) s
+      | _ => panic! "UnexpectedName"
+
+private def rewriteGoalUsingEq (goal : MVarId) (eq : Expr) (symm : Bool := false) : MetaM MVarId := do
+  let rewriteResult ← goal.rewrite (←goal.getType) eq symm
+  goal.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
+
+/--
+  Generates unfolding lemmas that relate coinductive predicates to their flat inductive forms.
+  These lemmas are essential for the constructor generation process, providing the bridge
+  between the user-facing coinductive predicates and their internal flat representations.
+
+  Example:
+
+  Given a definition:
+  ```
+  coinductive infSeq (r : α → α → Prop) : α → Prop where
+  | step : r a b → infSeq r b → infSeq r a
+  ```
+
+  We generate the following unfolding lemma:
+  ```
+    infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝
+  ```
+-/
+private def generateEqLemmas (infos : Array InductiveVal) : MetaM Unit := do
+  let levels := infos[0]!.levelParams.map mkLevelParam
+  for info in infos do
+    let res ← forallTelescopeReducing info.type fun args _ => do
+      let params := args[:info.numParams - infos.size]
+      let args := args[info.numParams:]
+
+      let lhs := mkConst (removeFunctorPostfix info.name) levels
+      let lhs := mkAppN lhs params
+      let lhs := mkAppN lhs args
+
+      let calls := infos.map fun info => mkAppN (mkConst (removeFunctorPostfix info.name) levels) params
+      let rhs := mkConst info.name levels
+      let rhs := mkAppN rhs (params ++ calls ++ args)
+
+      let goalType ← mkEq lhs rhs
+      let goal ← mkFreshExprMVar goalType
+
+      let goalMVarId := goal.mvarId!
+
+      let .some #[fixEq] ←  getEqnsFor? (removeFunctorPostfix info.name) | throwError "did not generate unfolding theorem"
+      let existentialEquiv := mkConst (info.name ++ `existential_equiv) levels
+
+      let mut fixEq := mkConst fixEq levels
+      fixEq := mkAppN fixEq params
+      for arg in args do
+        fixEq ← mkCongrFun fixEq arg
+
+      let newGoal ← rewriteGoalUsingEq goalMVarId existentialEquiv
+      newGoal.assign fixEq
+
+      let goal ← instantiateMVars goal
+      mkLambdaFVars (params ++ args) goal
+    trace[Elab.coinductive] "res: {res}"
+    addDecl <|
+      .defnDecl <|
+        ←mkDefinitionValInferringUnsafe
+          (name := (removeFunctorPostfix info.name) ++ `functor_unfold)
+          (levelParams := info.levelParams)
+          (type := (←inferType res))
+          (value := res)
+          (hints := .opaque)
+
+/--
+  Generates a constructor for a coinductive predicate that corresponds to constructors
+  in the original `InductiveView`.
+
+  The process:
+  1. Takes the flat inductive constructor type
+  2. Fills recursive call parameters with the actual coinductive predicates
+  3. Converts to existential form using the equivalence lemma
+  4. Applies the unfolding rule to get the final constructor form
+-/
+private def generateCoinductiveConstructor (infos : Array InductiveVal) (ctorSyntax : Syntax)
+    (numParams : Nat) (name : Name) (ctor : ConstructorVal) : TermElabM Unit := do
+  trace[Elab.coinductive] "Generating constructor: {removeFunctorPostfixInCtor ctor.name}"
+  let numPreds := infos.size
+  let predNames := infos.map fun val => removeFunctorPostfix val.name
+  let levelParams := infos[0]!.levelParams.map mkLevelParam
+  /-
+    We start by looking at the type of the constructor of the flat inductive and then by introducing
+    all its parameters to the scope.
+  -/
+  forallBoundedTelescope ctor.type (numParams + numPreds) fun args body => do
+    /-
+      The first `numParams` many items of `args` are parameters from the original definition,
+      while the remaining ones are free variables that correspond to recursive calls.
+    -/
+    let params := args.take numParams
+    let predFVars := args[numParams:]
+    /-
+      We will fill recursive calls in the body with the just defined (co)inductive predicates.
+    -/
+    let mut predicates : Array Expr := predNames.map (mkConst · levelParams)
+    predicates := predicates.map (mkAppN · params)
+    let body := body.replaceFVars predFVars predicates
+    /-
+      Now, we look at the rest of the constructor.
+      We start by collecting its non-parameter premises, as well as inspecting its conclusion.
+    -/
+    let res ← forallTelescope body fun fields bodyExpr => do
+      /-
+        First, we look at conclusion and pick out all arguments that are non-parameters.
+      -/
+      let bodyAppArgs := bodyExpr.getAppArgs[numParams + infos.size:]
+      /-
+        The goal (i.e. right hands side of a constructor) that we are trying to make is just
+        the coinductive predicate with parameters and non-parameter arguments applied.
+      -/
+      let goalType := mkConst (removeFunctorPostfix name) levelParams
+      let mut goalType := mkAppN goalType params
+      goalType := mkAppN goalType bodyAppArgs
+      trace[Elab.coinductive] "The conclusion of the constructor {ctor.name} is {goalType}"
+
+      -- We start by making the metavariable for it, that we will fill
+      let goal ← mkFreshExprMVar <| .some goalType
+      let hole := Expr.mvarId! goal
+      let unfoldEq := mkConst ((removeFunctorPostfix name) ++ `functor_unfold) levelParams
+      let unfoldEq := mkAppN unfoldEq params
+
+      let rewriteResult ← hole.rewrite (←hole.getType) unfoldEq
+
+      let newHole ← hole.replaceTargetEq rewriteResult.eNew rewriteResult.eqProof
+
+      /-
+        Now, all it suffices is to call an approprate constructor of the flat inductive.
+      -/
+      let constructor := mkConst ctor.name levelParams
+      let constructor := mkAppN constructor params
+      let constructor := mkAppN constructor predicates
+      let constructor := mkAppN constructor fields
+      newHole.assign constructor
+      let conclusion ← instantiateMVars goal
+      let conclusion ← mkLambdaFVars fields conclusion
+      mkLambdaFVars params conclusion
+    let type ← inferType res
+    trace[Elab.coinductive] "The elaborated constructor is of the type: {type}"
+    /-
+      We finish by registering the appropriate declaration
+    -/
+    addDecl <|
+      .defnDecl <|
+        ←mkDefinitionValInferringUnsafe
+          (name := removeFunctorPostfixInCtor ctor.name)
+          (levelParams := ctor.levelParams)
+          (type := type)
+          (value := res)
+          (hints:= .opaque)
+    Term.addTermInfo' ctorSyntax res (isBinder := true)
+
+/--
+  Given the number of parameters and the `InductiveVal` containing flat inductives
+  (see `mkFlatInductive`) and `CoinductiveElabData` associated with the mutual coinductive
+  predicates, generates their constructors that correspond to the
+  constructors given in the original syntax.
+-/
+private def generateCoinductiveConstructors (numParams : Nat) (infos : Array InductiveVal)
+    (coinductiveElabData : Array CoinductiveElabData) : TermElabM Unit := do
+  for indType in infos, e in coinductiveElabData do
+    for ctor in indType.ctors, ctorSyntax in e.ctorSyntax do
+      generateCoinductiveConstructor infos ctorSyntax numParams indType.name
+        <| ←getConstInfoCtor ctor
+
+/--
+  Generates `casesOn` eliminators for coinductive predicates.
+  These eliminators allow pattern matching on coinductive predicates,
+  enabling case analysis in proofs.
+-/
+private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
+  let levels := infos[0]!.levelParams.map mkLevelParam
+  let allCtors := infos.flatMap (·.ctors.toArray)
+
+  forallBoundedTelescope infos[0]!.type (infos[0]!.numParams - infos.size) fun params _ => do
+  let predicates := infos.map fun info => mkConst (removeFunctorPostfix info.name) levels
+  let predicates := predicates.map (mkAppN · params)
+  for info in infos do
+    let casesOnName := Lean.mkCasesOnName info.name
+    let casesOnInfo ← getConstInfo casesOnName
+    let originalCasesOn ← mkConstWithLevelParams casesOnName
+    let originalCasesOn := mkAppN originalCasesOn (params ++ predicates)
+
+    let goalTypeWithParamsApplied ← inferType originalCasesOn
+    /-
+      We replace the mentions of the flat inductive with a coinductive predicate
+      and replace all constructors of the original type.
+    -/
+    let goalTypeWithParamsApplied := goalTypeWithParamsApplied.replace (fun e =>
+      if e.isApp then
+        let bodyArgs := e.getAppArgs[info.numParams:]
+        if e.isAppOf info.name then
+          mkAppN (mkConst (removeFunctorPostfix info.name) levels) <| params ++ bodyArgs
+        else
+          if allCtors.any e.isAppOf then
+            let bodyArgs := e.getAppArgs[info.numParams:]
+            mkAppN (mkConst (removeFunctorPostfixInCtor (e.getAppFn.constName)) levels)
+              <| params ++ bodyArgs
+          else none
+      else
+        none
+    )
+    -- The type of `casesOn` of the flat inductive, upon having the parameters applied
+    let originalType ← inferType originalCasesOn
+    -- The equivalence proof, that will be used in the subsequent rewrites
+    let eqProof := mkConst ((removeFunctorPostfix info.name) ++ `functor_unfold) levels
+    /-
+      First, we look at the motive. We construct a free variable `motive`
+      of the type of motive, as it appears in the `goalTypeWithParamsApplied`
+    -/
+    forallBoundedTelescope goalTypeWithParamsApplied (.some 1) fun args goalType => do
+      let #[motive] := args
+        | throwError "Expected one argument"
+      /-
+        Similarly, we pull of the type of the motive, as it appears in the `casesOn`
+        of the flat inductive. We then make an mvar of this type and try to
+        fill it using `motive` fvar.
+      -/
+      let (Expr.forallE _ type _ _) := originalType
+        | throwError "expected to be quantifier"
+      let motiveMVar ← mkFreshExprMVar type
+      /-
+        We intro all the indices and the occurence of the coinductive predicate
+      -/
+      let (fvars, subgoal) ← motiveMVar.mvarId!.introN (info.numIndices + 1)
+      subgoal.withContext do
+        let lastAssumption := fvars[fvars.size -1]!
+
+        -- We perform the rewrite at the hypothesis
+        let rewriteTarget := (←getLCtx).get! lastAssumption
+        let rewriteTarget := rewriteTarget.type
+        let rewriteResult ← subgoal.rewrite rewriteTarget eqProof (symm := true)
+        let replacementResult ← subgoal.replaceLocalDecl lastAssumption
+              rewriteResult.eNew rewriteResult.eqProof
+
+        let newFVars := fvars.modify (fvars.size - 1) fun _ => replacementResult.fvarId
+        let (_, afterReplacing) ← replacementResult.mvarId.revert newFVars
+        -- Now it is in the form that we can assign the `motive` fvar to the goal
+        afterReplacing.assign motive
+        -- Then we apply the metavariable to the `casesOn` of the flat inductive
+        let originalCasesOn := mkApp originalCasesOn motiveMVar
+
+        -- The next arguemnts of the `casesOn` are type indices
+        forallBoundedTelescope goalType info.numIndices fun indices goalType => do
+          /-
+            The types do not change, so we just make free variables for them
+            and apply them to the `casesOn` of the flat inductive
+          -/
+          let originalCasesOn := mkAppN originalCasesOn indices
+          /-
+            The next argument is the occurence of the coinductive predicate.
+            The original `casesOn` of the flat inductive mentions it in
+            unrolled form, so we need to rewrite it.
+          -/
+          forallBoundedTelescope goalType (.some 1) fun targetArgs _ => do
+            /-
+              We again make a free variable of the type as it appears in the desired
+              type of `casesOn` for the coinductive predicate.
+            -/
+            let #[target] := targetArgs | throwError "Expected one argument"
+            /-
+              Then, we fish out the type as it appears in the `casesOn` of the flat
+              inductive, then making a metavariable for it.
+            -/
+            let (Expr.forallE _ type _ _) ← inferType originalCasesOn
+              | throwError "expected to be quantifier"
+            let targetMVar ← mkFreshExprMVar type
+            let targetMVarSubgoal ← rewriteGoalUsingEq targetMVar.mvarId! eqProof (symm := true)
+            targetMVarSubgoal.assign target
+            -- Upon performing the rewrite, we apply the mvar to the flat inductive `casesOn`
+            let originalCasesOn := mkApp originalCasesOn targetMVar
+
+            let originalCasesOn ←
+              mkLambdaFVars (params ++ args ++ indices ++ targetArgs) originalCasesOn
+            let originalCasesOn ← instantiateMVars originalCasesOn
+
+            let levelParams := casesOnInfo.levelParams
+            let casesOnName := mkCasesOnName (removeFunctorPostfix info.name)
+            let casesOnType ← mkForallFVars params goalTypeWithParamsApplied
+            addDecl <|
+              .defnDecl <|
+                ← mkDefinitionValInferringUnsafe
+                    (name := casesOnName)
+                    (levelParams := levelParams)
+                    (type := casesOnType)
+                    (value := originalCasesOn)
+                    (hints := .opaque)
+            -- We apply the attribute so that the `cases` tactic can pick it up
+            liftCommandElabM
+              <| liftTermElabM
+                <| Term.applyAttributes
+                    casesOnName #[{name := `cases_eliminator}, {name := `elab_as_elim}]
+
+/--
+  Main entry point for elaborating mutual coinductive predicates. This function is called after
+  generating a flat inductive and adding it to the environment.
+
+  We look at corresponding existential form of the flat inductive (see `Meta.MkIffOfInductiveProp`),
+  use it to populate `PreDefinition`s that correspond to the predicates, and then we call
+  the `PartialFixpoint` machinery to register them as (co)inductive predicates.
+
+  Finally, we generate constructors for each of the predicates, that correspond to the constructors
+  that were given by the user.
+-/
+public def elabCoinductive (coinductiveElabData : Array CoinductiveElabData) : TermElabM Unit := do
+  trace[Elab.coinductive] "Elaborating: {coinductiveElabData.map (·.declName)}"
+  let infos ← coinductiveElabData.mapM (getConstInfoInduct ·.declName)
+  let levelParams := infos[0]!.levelParams.map mkLevelParam
+  /-
+    We infer original names and types of the predicates.
+    To get such names, we need to remove `._functor` postfix. At the same time,
+    we need to forget about the parameters for recursive calls, to get the original types.
+  -/
+  let originalNumParams := infos[0]!.numParams - infos.size
+  let namesAndTypes : Array (Name × Expr) ← infos.mapM fun info => do
+    let type ← forallTelescope info.type fun args body => do
+      mkForallFVars (args[:originalNumParams] ++ args[info.numParams:]) body
+    return (removeFunctorPostfix (info.name), type)
+  /-
+    We make dummy constants that are used in populating PreDefinitions
+  -/
+  let consts := namesAndTypes.map fun (name, _) => (mkConst name levelParams)
+  /-
+    We create values of each of PreDefinitions, by taking existential (see `Meta.SumOfProducts`)
+    form of the associated flat inductives and applying paramaters, as well as recursive calls
+    (with their parameters passed).
+  -/
+  let preDefVals ← forallBoundedTelescope infos[0]!.type originalNumParams fun params _ => do
+    infos.mapM fun info => do
+      let mut functor := mkConst (info.name ++ `existential) levelParams
+      functor ← unfoldDefinition functor
+      functor := mkAppN functor <| params ++ consts.map (mkAppN · params)
+      mkLambdaFVars params functor
+  /-
+    Finally, we populate the PreDefinitions
+  -/
+  let preDefs : Array PreDefinition := preDefVals.mapIdx fun idx defn =>
+    { ref := coinductiveElabData[idx]!.ref
+      binders := coinductiveElabData[idx]!.ref
+      kind := .def
+      levelParams := infos[0]!.levelParams
+      modifiers := coinductiveElabData[idx]!.modifiers
+      declName := namesAndTypes[idx]!.1
+      type := namesAndTypes[idx]!.2
+      value := defn
+      termination := {
+        ref := coinductiveElabData[idx]!.ref
+        terminationBy?? := .none
+        terminationBy? := .none
+        partialFixpoint? := .some {
+            ref := coinductiveElabData[idx]!.ref
+            term? := .none
+            fixpointType := if coinductiveElabData[idx]!.isGreatest then
+                              .coinductiveFixpoint else .inductiveFixpoint
+        }
+        decreasingBy? := .none
+        extraParams := 0
+      }
+    }
+  partialFixpoint (← getLCtx, ← getLocalInstances) preDefs
+  generateEqLemmas infos
+  generateCoinductiveConstructors originalNumParams infos coinductiveElabData
+  mkCasesOnCoinductive infos
+
+end Lean.Elab.Command

src/Lean/Elab/Declaration.lean

@@ -181,6 +181,7 @@ def elabDeclaration : CommandElab := fun stx => do
       if declKind == ``Lean.Parser.Command.«axiom» then
         elabAxiom modifiers decl
       else if declKind == ``Lean.Parser.Command.«inductive»
+          || declKind == ``Lean.Parser.Command.«coinductive»
           || declKind == ``Lean.Parser.Command.classInductive
           || declKind == ``Lean.Parser.Command.«structure» then
         elabInductive modifiers decl

src/Lean/Elab/Inductive.lean

@@ -23,7 +23,7 @@ def Lean.Parser.Command.classInductive :=
   leading_parser atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ("where" <|> ":=") >> many ctor >> optDeriving
 ```
 -/
-private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : TermElabM InductiveView := do
+private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoinductive : Bool) : TermElabM InductiveView := do
   let isClass := decl.isOfKind ``Parser.Command.classInductive
   let modifiers := if isClass then modifiers.addAttr { name := `class } else modifiers
   let (binders, type?) := expandOptDeclSig decl[2]
@@ -32,6 +32,12 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
   if modifiers.isMeta then
     modifyEnv (addMeta · declName)
   addDeclarationRangesForBuiltin declName modifiers.stx decl
+  /-
+    Relates to issue
+    https://github.com/leanprover/lean4/issues/10503
+  -/
+  if declName.hasMacroScopes && isCoinductive then
+    throwError "Coinductive predicates are not allowed inside of macro scopes"
   let ctors      ← decl[4].getArgs.mapM fun ctor => withRef ctor do
     /-
     ```
@@ -87,6 +93,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term
     binders, type?, ctors
     computedFields
     docString?
+    isCoinductive := isCoinductive
   }
 
 private def isInductiveFamily (numParams : Nat) (indFVar : Expr) : TermElabM Bool := do
@@ -311,10 +318,9 @@ where
     throwNamedErrorAt ctorType lean.ctorResultingTypeMismatch "Unexpected resulting type for constructor `{declName}`: \
       Expected a type, but found{indentExpr resultingType}\nof type{lazyMsg}"
 
-@[builtin_inductive_elab Lean.Parser.Command.inductive, builtin_inductive_elab Lean.Parser.Command.classInductive]
+def mkInductiveElabDescr (isCoinductive := false) : InductiveElabDescr where
-def elabInductiveCommand : InductiveElabDescr where
+mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do
-  mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do
+    let view ← inductiveSyntaxToView modifiers stx isCoinductive
-    let view ← inductiveSyntaxToView modifiers stx
     return {
       view
       elabCtors := fun rs r params => do
@@ -322,4 +328,10 @@ def elabInductiveCommand : InductiveElabDescr where
         return { ctors }
     }
 
+@[builtin_inductive_elab Lean.Parser.Command.inductive, builtin_inductive_elab Lean.Parser.Command.classInductive]
+def elabInductiveCommand : InductiveElabDescr := mkInductiveElabDescr
+
+@[builtin_inductive_elab Lean.Parser.Command.coinductive]
+def elabCoinductiveCommand : InductiveElabDescr := mkInductiveElabDescr (isCoinductive := true)
+
 end Lean.Elab.Command

src/Lean/Elab/MutualInductive.lean

@@ -14,7 +14,9 @@ public import Lean.Meta.Constructions
 public import Lean.Meta.CollectFVars
 public import Lean.Meta.SizeOf
 public import Lean.Meta.Injective
+public import Lean.Meta.MkIffOfInductiveProp
 public import Lean.Elab.Command
+public import Lean.Elab.Coinductive
 public import Lean.Elab.DefView
 public import Lean.Elab.DeclUtil
 public import Lean.Elab.Deriving.Basic
@@ -114,6 +116,7 @@ structure InductiveView where
   derivingClasses : Array DerivingClassView
   /-- The declaration docstring, and whether it's Verso -/
   docString?      : Option (TSyntax ``Lean.Parser.Command.docComment × Bool)
+  isCoinductive : Bool := false
   deriving Inhabited
 
 /-- Elaborated header for an inductive type before fvars for each inductive are added to the local context. -/
@@ -851,7 +854,7 @@ private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr
 /-- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration,
    and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/
 private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name)
-    (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
+    (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) (applyVariables : Bool := true) : TermElabM (List InductiveType) :=
   let indFVar2Const := mkIndFVar2Const views indFVars levelNames
   indTypes.mapM fun indType => do
     let ctors ← indType.ctors.mapM fun ctor => do
@@ -861,7 +864,7 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars :
             none
           else match indFVar2Const[e]? with
             | none   => none
-            | some c => mkAppN c (params.extract 0 numVars)
+            | some c => if applyVariables then mkAppN c (params.extract 0 numVars) else c
         instantiateMVars (← mkForallFVars params type)
       return { ctor with type }
     return { indType with ctors }
@@ -875,99 +878,252 @@ private structure FinalizeContext where
   localInsts : LocalInstances
   replaceIndFVars : Expr → MetaM Expr
 
-private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext :=
+private structure FinalizeInductiveDecl where
-  Term.withoutSavingRecAppSyntax do
+  decl : Declaration
+  indFvars : Array Expr
+  numParams : Int
+  rs : Array PreElabHeaderResult
+
+/--
+  For nested inductive types, the kernel adds a variable number of auxiliary recursors.
+  Let the elaborator know about them as well. (Other auxiliaries have already been
+  registered by `addDecl` via `Declaration.getNames`.)
+  NOTE: If we want to make inductive elaboration parallel, this should switch to using
+  reserved names.
+-/
+private def addAuxRecs (indTypes : List InductiveType) : TermElabM Unit := do
+  for indType in indTypes do
+    let mut i := 1
+    while true do
+      let auxRecName := indType.name ++ `rec |>.appendIndexAfter i
+      let env ← getEnv
+      let some const := env.toKernelEnv.find? auxRecName | break
+      let res ← env.addConstAsync auxRecName .recursor
+      res.commitConst res.asyncEnv (info? := const)
+      res.commitCheckEnv res.asyncEnv
+      setEnv res.mainEnv
+      i := i + 1
+
+private def mkReplaceIndFVars (views : Array InductiveView) (indFVars : Array Expr)
+   (levelParams : List Name) (vars : Array Expr) : Expr → MetaM Expr := fun e => do
+    let indFVar2Const := mkIndFVar2Const views indFVars levelParams
+    return (← instantiateMVars e).replace fun e' =>
+      if !e'.isFVar then
+        none
+      else
+        match indFVar2Const[e']? with
+        | none   => none
+        | some c => mkAppN c vars
+
+private def buildFinalizeContext (elabs' : Array InductiveElabStep2) (levelParams : List Name)
+    (vars params : Array Expr) (views : Array InductiveView) (newIndFVars : Array Expr)
+    (rs : Array ElabHeaderResult) : TermElabM FinalizeContext := do
+  let lctx := rs.foldl (init := ← getLCtx) fun lctx r =>
+    lctx.modifyLocalDecl r.indFVar.fvarId! fun decl =>
+      decl.setUserName (`_indFVar ++ decl.userName)
+
+  pure {
+    elabs := elabs',
+    levelParams,
+    params := vars ++ params,
+    replaceIndFVars := mkReplaceIndFVars views newIndFVars levelParams vars,
+    mctx := ← getMCtx,
+    lctx,
+    localInsts := ← getLocalInstances
+  }
+
+def replaceIndFVars (numParams : Nat) (oldFVars : Array Expr) (calls : Array Expr) : Expr → Expr := fun e =>
+  let replacementMap : ExprMap Expr := {}
+  let replacementMap := replacementMap.insertMany <| oldFVars.zip calls
+  e.replace (fun e =>
+    if e.isApp || numParams == 0 then
+      if let some replacement := replacementMap.get? e.getAppFn then
+        mkAppN replacement <| e.getAppArgs.extract numParams
+      else
+        .none
+    else
+      .none
+    )
+
+/--
+  Given a list of `InductiveType` structures and some local variables of `mkInductiveDecl`,
+  rewrites the inductive types and their constructors in a way that signature contains parameters
+  representing the types being defined, and all the recursive occurrences of the inductive types
+  in constructor are replaced by applications of these parameters.
+
+  This function is used to implement coinductive predicates. For more details, see the comment in
+  `Elab.Coinductive`
+
+  Upon rewriting the inductive types, it adds the new inductive declaration to the environment,
+  following the same pattern as `mkInductiveDecl`.
+
+  We assume that numVars <= numParams, where numVars is the number of local variables.
+-/
+private def mkFlatInductive (views : Array InductiveView)
+  (indFVars : Array Expr) (levelParams : List Name) (numVars : Nat)
+  (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
+
+  let namesAndTypes := indTypes.map fun indType => (indType.name.append `call, indType.type)
+  let namesAndTypes := namesAndTypes.toArray
+
+  -- We update the type of all inductive types, so they have recursive calls added as parameters
+  let newTypes ← namesAndTypes.mapM fun (_, indType) =>
+    forallBoundedTelescope indType numParams fun indTypeParams indTypeBody => do
+
+      -- We first go through all types in the mutual block and get rid of their parameters
+      -- by substiuting free variables
+      let typesWithAppliedParams ← namesAndTypes.mapM fun (newName, curIndType) => do
+        forallBoundedTelescope curIndType numParams fun curIntTypeParams curIndTypeBody => do
+          return (newName, curIndTypeBody.replaceFVars curIntTypeParams indTypeParams)
+      withLocalDeclsDND typesWithAppliedParams fun newParams => do
+       mkForallFVars (indTypeParams ++ newParams) indTypeBody
+  let rs ← newTypes.mapIdxM fun idx newType => do
+    return PreElabHeaderResult.mk views[idx]! levelParams (numParams + views.size) newType #[]
+
+  -- We now reuse the machinery for bringing in indFVars to the context
+  withInductiveLocalDecls rs fun newParams newIndFVars => do
+    let indTypes ← indTypes.mapIdxM fun indTypeIdx indType => do
+      let updatedCtors ← indType.ctors.mapM fun ctor => do
+        -- We first use new set of parameters
+        let updatedCtor ← instantiateForall ctor.type (newParams.take numParams)
+        let updatedCtor ← forallTelescope updatedCtor fun ctorArgs ctorBody => do
+            -- We assume that the conclusion is an application of the fvar
+          guard <| ctorBody.isApp || numParams == 0
+
+          -- We first get non-parameter arguments of the body
+          let bodyArgs := ctorBody.getAppArgs.extract (numParams - numVars)
+
+          -- And make a new conclusion with new indFVar. We pass new parameters and old non-parameter arguments
+          let ctorBody := mkAppN (newIndFVars[indTypeIdx]!) (newParams ++ bodyArgs)
+          mkForallFVars ctorArgs ctorBody
+
+        -- Then we replace indFVars in the premises of the rule
+        let calls := newParams.extract numParams
+        let updatedCtor := replaceIndFVars (numParams - numVars) indFVars calls updatedCtor
+
+        -- Finally, we need to abstract away the parameters
+        let updatedCtor ← mkForallFVars newParams updatedCtor
+        return { ctor with type := updatedCtor}
+      return { indType with type := newTypes[indTypeIdx]!, ctors := updatedCtors}
+
+    let indTypes ← replaceIndFVarsWithConsts views newIndFVars levelParams numVars (numParams + views.size) indTypes (applyVariables := false)
+    let decl := Declaration.inductDecl levelParams (numParams + views.size) indTypes false
+    Term.ensureNoUnassignedMVars decl
+    addDecl decl
+
+private structure AddAndFinalizeContext where
+  views : Array InductiveView
+  elabs' : Array InductiveElabStep2
+  indFVars : Array Expr
+  vars : Array Expr
+  levelParams : List Name
+  numVars : Nat
+  numParams : Nat
+  indTypes : List InductiveType
+  isUnsafe : Bool
+  rs : Array ElabHeaderResult
+  params : Array Expr
+  isCoinductive : Bool
+
+private def addAndFinalizeInductiveDecl (context : AddAndFinalizeContext) : TermElabM FinalizeContext := do
+    let indTypes ← replaceIndFVarsWithConsts context.views context.indFVars context.levelParams context.numVars context.numParams context.indTypes
+    let decl := Declaration.inductDecl context.levelParams context.numParams indTypes context.isUnsafe
+    Term.ensureNoUnassignedMVars decl
+    addDecl decl
+    addAuxRecs indTypes
+    buildFinalizeContext context.elabs' context.levelParams context.vars context.params context.views context.indFVars context.rs
+
+private def addTermInfoViews (views : Array InductiveView) : TermElabM Unit := -- save new env
+  withSaveInfoContext do -- save new env
+    for view in views do
+      do Term.addTermInfo' view.declId (← mkConstWithLevelParams view.declName) (isBinder := true)
+      for ctor in view.ctors do
+        if (ctor.declId.getPos? (canonicalOnly := true)).isSome then do
+          Term.addTermInfo' ctor.declId (← mkConstWithLevelParams ctor.declName) (isBinder := true)
+          enableRealizationsForConst ctor.declName
+
+private def mkInductiveDeclCore
+  (callback : AddAndFinalizeContext → TermElabM α) (vars : Array Expr)
+  (elabs : Array InductiveElabStep1) (rs : Array PreElabHeaderResult) (scopeLevelNames : List Name) : TermElabM α := do
+  let views := elabs.map (·.view)
+  let view0 := views[0]!
+  let isCoinductive := views.any (·.isCoinductive)
+  if isCoinductive then
+    unless (←rs.allM (forallTelescopeReducing ·.type fun args body => pure body.isProp)) do
+      throwErrorAt view0.declId "`coinductive` keyword can only be used to define predicates"
+  let allUserLevelNames := rs[0]!.levelNames
+  let isUnsafe          := view0.modifiers.isUnsafe
+  let res ← withInductiveLocalDecls rs fun params indFVars => do
+        trace[Elab.inductive] "indFVars: {indFVars}"
+        let rs := Array.zipWith (fun r indFVar => { r with indFVar : ElabHeaderResult }) rs indFVars
+        let mut indTypesArray : Array InductiveType := #[]
+        let mut elabs' := #[]
+        for h : i in *...views.size do
+          Term.addLocalVarInfo views[i].declId indFVars[i]!
+          let r     := rs[i]!
+          let elab' ← elabs[i]!.elabCtors rs r params
+          elabs'    := elabs'.push elab'
+          indTypesArray := indTypesArray.push { name := r.view.declName, type := r.type, ctors := elab'.ctors }
+        Term.synthesizeSyntheticMVarsNoPostponing
+        let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
+        trace[Elab.inductive] "numExplicitParams: {numExplicitParams}"
+        let indTypes := indTypesArray.toList
+        let u ← getResultingUniverse indTypes
+        let univToInfer? ← shouldInferResultUniverse u
+        withUsed elabs' vars indTypes fun vars => do
+          let numVars   := vars.size
+          let numParams := numVars + numExplicitParams
+          let indTypes ← updateParams vars indTypes
+          -- allow general access to private data for steps that do no elaboration
+          let indTypes ←
+            withoutExporting do
+              if let some univToInfer := univToInfer? then
+                updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer)
+              else
+                propagateUniversesToConstructors numParams indTypes
+                levelMVarToParam indTypes none
+          withoutExporting do
+            checkResultingUniverses views elabs' numParams indTypes
+          elabs'.forM fun elab' => elab'.finalizeTermElab
+          let usedLevelNames := collectLevelParamsInInductive indTypes
+          match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
+          | .error msg      => throwErrorAt view0.declId msg
+          | .ok levelParams =>
+            callback {
+              views := views
+              elabs' := elabs'
+              indFVars := indFVars
+              vars := vars
+              levelParams := levelParams
+              indTypes := indTypes
+              isUnsafe := isUnsafe
+              rs := rs
+              params := params
+              isCoinductive := isCoinductive
+              numVars := numVars
+              numParams := numParams
+            }
+  return res
+
+private def withElaboratedHeaders (vars : Array Expr) (elabs : Array InductiveElabStep1)
+  (k : Array Expr → Array InductiveElabStep1 → Array PreElabHeaderResult → List Name → TermElabM α ) : TermElabM α :=
+Term.withoutSavingRecAppSyntax do
   let views := elabs.map (·.view)
   let view0 := views[0]!
   let scopeLevelNames ← Term.getLevelNames
   InductiveElabStep1.checkLevelNames views
   let allUserLevelNames := view0.levelNames
-  let isUnsafe          := view0.modifiers.isUnsafe
   withRef view0.ref <| Term.withLevelNames allUserLevelNames do
     let rs ← elabHeaders views
     Term.synthesizeSyntheticMVarsNoPostponing
     ElabHeaderResult.checkLevelNames rs
-    let allUserLevelNames := rs[0]!.levelNames
     trace[Elab.inductive] "level names: {allUserLevelNames}"
-    let res ← withInductiveLocalDecls rs fun params indFVars => do
+    k vars elabs rs scopeLevelNames
-      trace[Elab.inductive] "indFVars: {indFVars}"
-      let rs := Array.zipWith (fun r indFVar => { r with indFVar : ElabHeaderResult }) rs indFVars
-      let mut indTypesArray : Array InductiveType := #[]
-      let mut elabs' := #[]
-      for h : i in *...views.size do
-        Term.addLocalVarInfo views[i].declId indFVars[i]!
-        let r     := rs[i]!
-        let elab' ← elabs[i]!.elabCtors rs r params
-        elabs'    := elabs'.push elab'
-        indTypesArray := indTypesArray.push { name := r.view.declName, type := r.type, ctors := elab'.ctors }
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let numExplicitParams ← fixedIndicesToParams params.size indTypesArray indFVars
-      trace[Elab.inductive] "numExplicitParams: {numExplicitParams}"
-      let indTypes := indTypesArray.toList
-      let u ← getResultingUniverse indTypes
-      let univToInfer? ← shouldInferResultUniverse u
-      withUsed elabs' vars indTypes fun vars => do
-        let numVars   := vars.size
-        let numParams := numVars + numExplicitParams
-        let indTypes ← updateParams vars indTypes
-        -- allow general access to private data for steps that do no elaboration
-        let indTypes ←
-          withoutExporting do
-            if let some univToInfer := univToInfer? then
-              updateResultingUniverse views numParams (← levelMVarToParam indTypes univToInfer)
-            else
-              propagateUniversesToConstructors numParams indTypes
-              levelMVarToParam indTypes none
-        withoutExporting do
-          checkResultingUniverses views elabs' numParams indTypes
-        elabs'.forM fun elab' => elab'.finalizeTermElab
-        let usedLevelNames := collectLevelParamsInInductive indTypes
-        match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
-        | .error msg      => throwErrorAt view0.declId msg
-        | .ok levelParams => do
-          let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
-          let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
-          Term.ensureNoUnassignedMVars decl
-          addDecl decl
 
-          -- For nested inductive types, the kernel adds a variable number of auxiliary recursors.
+private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext :=
-          -- Let the elaborator know about them as well. (Other auxiliaries have already been
+  withElaboratedHeaders vars elabs fun vars elabs rs scopeLevelNames => do
-          -- registered by `addDecl` via `Declaration.getNames`.)
+    let res ← mkInductiveDeclCore addAndFinalizeInductiveDecl vars elabs rs scopeLevelNames
-          -- NOTE: If we want to make inductive elaboration parallel, this should switch to using
+    addTermInfoViews <| elabs.map (·.view)
-          -- reserved names.
-          for indType in indTypes do
-            let mut i := 1
-            while true do
-              let auxRecName := indType.name ++ `rec |>.appendIndexAfter i
-              let env ← getEnv
-              let some const := env.toKernelEnv.find? auxRecName | break
-              let res ← env.addConstAsync auxRecName .recursor
-              res.commitConst res.asyncEnv (info? := const)
-              res.commitCheckEnv res.asyncEnv
-              setEnv res.mainEnv
-              i := i + 1
-
-          let replaceIndFVars (e : Expr) : MetaM Expr := do
-            let indFVar2Const := mkIndFVar2Const views indFVars levelParams
-            return (← instantiateMVars e).replace fun e' =>
-              if !e'.isFVar then
-                none
-              else
-                match indFVar2Const[e']? with
-                | none   => none
-                | some c => mkAppN c vars
-          -- Now the indFVars are (mostly) unnecessary, so rename them to prevent shadowing in messages.
-          -- Inductive elaborators might still have some indFVars around, but they should use `replaceIndFVars` as soon as possible during their `finalize` procedure.
-          let lctx := rs.foldl (init := ← getLCtx) (fun lctx r => lctx.modifyLocalDecl r.indFVar.fvarId! fun decl => decl.setUserName (`_indFVar ++ decl.userName))
-          pure {
-            elabs := elabs', levelParams, params := vars ++ params, replaceIndFVars,
-            mctx := ← getMCtx, lctx, localInsts := ← getLocalInstances }
-    withSaveInfoContext do -- save new env
-      for view in views do
-        Term.addTermInfo' view.declId (← mkConstWithLevelParams view.declName) (isBinder := true)
-        for ctor in view.ctors do
-          if (ctor.declId.getPos? (canonicalOnly := true)).isSome then
-            Term.addTermInfo' ctor.declId (← mkConstWithLevelParams ctor.declName) (isBinder := true)
     return res
 
 private def mkAuxConstructions (declNames : Array Name) : TermElabM Unit := do
@@ -987,6 +1143,14 @@ private def mkAuxConstructions (declNames : Array Name) : TermElabM Unit := do
   for n in declNames do
     if hasUnit && hasProd then mkBRecOn n
 
+def updateViewWithFunctorName (view : InductiveView) : InductiveView :=
+  let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (addFunctorPostfix ctor.declName.getPrefix)})
+  {view with declName := addFunctorPostfix view.declName, ctors := newCtors}
+
+def updateViewRemovingFunctorName (view : InductiveView) : InductiveView :=
+  let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (removeFunctorPostfix ctor.declName.getPrefix)})
+  {view with declName := addFunctorPostfix view.declName, ctors := newCtors}
+
 private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
   let view0 := elabs[0]!.view
   let ref := view0.ref
@@ -1007,23 +1171,39 @@ private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabS
         enableRealizationsForConst ctor.declName
     return res
 
+private def elabFlatInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM Unit := do
+  let view0 := elabs[0]!.view
+  let ref := view0.ref
+  Term.withDeclName view0.declName do withRef ref do
+  withExporting (isExporting := !isPrivateName view0.declName) do
+    withElaboratedHeaders vars elabs <| mkInductiveDeclCore (fun context =>
+     mkFlatInductive context.views context.indFVars context.levelParams context.numVars context.numParams context.indTypes)
+    -- This might be too coarse, consider reconsidering on construction-by-construction basis
+    withoutExporting (when := view0.ctors.any (isPrivateName ·.declName)) do
+      mkAuxConstructions (elabs.map (·.view.declName))
+    -- Note that the below applies to the flat inductive
+    for e in elabs do
+      enableRealizationsForConst e.view.declName
+
 /-- Ensures that there are no conflicts among or between the type and constructor names defined in `elabs`. -/
-private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) : TermElabM Unit := do
+private def checkNoInductiveNameConflicts (elabs : Array InductiveElabStep1) (isCoinductive : Bool := false) : TermElabM Unit := do
   let throwErrorsAt (init cur : Syntax) (msg : MessageData) : TermElabM Unit := do
     logErrorAt init msg
     throwErrorAt cur msg
   -- Maps names of inductive types to to `true` and those of constructors to `false`, along with syntax refs
   let mut uniqueNames : Std.HashMap Name (Bool × Syntax) := {}
+  let declString := if isCoinductive then "coinductive predicate" else "inductive type"
+  trace[Elab.inductive] "deckString: {declString}"
   for { view, .. } in elabs do
     let typeDeclName := privateToUserName view.declName
     if let some (prevNameIsType, prevRef) := uniqueNames[typeDeclName]? then
-      let declKinds := if prevNameIsType then "multiple inductive types" else "an inductive type and a constructor"
+      let declKinds := if prevNameIsType then "multiple " ++ declString ++ "s" else "an " ++ declString ++ " and a constructor"
       throwErrorsAt prevRef view.declId m!"Cannot define {declKinds} with the same name `{typeDeclName}`"
     uniqueNames := uniqueNames.insert typeDeclName (true, view.declId)
     for ctor in view.ctors do
       let ctorName := privateToUserName ctor.declName
       if let some (prevNameIsType, prevRef) := uniqueNames[ctorName]? then
-        let declKinds := if prevNameIsType then "an inductive type and a constructor" else "multiple constructors"
+        let declKinds := if prevNameIsType then "an {declString} and a constructor" else "multiple constructors"
         throwErrorsAt prevRef ctor.declId m!"Cannot define {declKinds} with the same name `{ctorName}`"
       uniqueNames := uniqueNames.insert ctorName (false, ctor.declId)
 
@@ -1067,13 +1247,15 @@ private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM U
             declNames := declNames.push view.declName
         classView.applyHandlers declNames
 
-private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res : FinalizeContext) : CommandElabM Unit := do
+private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res : FinalizeContext)
+     : CommandElabM Unit := do
   let view0 := views[0]!
   let ref := view0.ref
   applyComputedFields views -- NOTE: any generated code before this line is invalid
   liftTermElabM <| withMCtx res.mctx <| withLCtx res.lctx res.localInsts do
     let finalizers ← res.elabs.mapM fun elab' => elab'.prefinalize res.levelParams res.params res.replaceIndFVars
-    for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking
+    for view in views do withRef view.declId <|
+      Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking
     for elab' in finalizers do elab'.finalize
   applyDerivingHandlers views
   -- Docstrings are added during postprocessing to allow them to have checked references to
@@ -1089,16 +1271,64 @@ private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res
             addDocStringOf verso ctor.declName ctor.binders doc
 
   runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
-    for view in views do withRef view.declId <| Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+    for view in views do withRef view.declId <|
+      unless (views.any (·.isCoinductive)) do
+        Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+
+private def elabInductiveViewsPostprocessingCoinductive (views : Array InductiveView)
+     : CommandElabM Unit := do
+  let views := views.map updateViewRemovingFunctorName
+  let view0 := views[0]!
+  let ref := view0.ref
+
+  applyDerivingHandlers views
+  -- Docstrings are added during postprocessing to allow them to have checked references to
+  -- the type and its constructors, but before attributes to enable e.g. `@[inherit_doc X]`
+  runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
+    for view in views do
+      withRef view.declId do
+        if let some (doc, verso) := view.docString? then
+          addDocStringOf verso view.declName view.binders doc
+      for ctor in view.ctors do
+        withRef ctor.declId do
+          if let some (doc, verso) := ctor.modifiers.docString? then
+            addDocStringOf verso ctor.declName ctor.binders doc
+
+  runTermElabM fun _ => Term.withDeclName view0.declName do withRef ref do
+    for view in views do withRef view.declId <|
+      unless (views.any (·.isCoinductive)) do
+        Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation
+
+def InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabData where
+  declId := e.view.declId
+  declName := e.view.declName
+  ref := e.view.ref
+  modifiers := e.view.modifiers
+  ctorSyntax := e.view.ctors.map (·.ref)
+  isGreatest := e.view.isCoinductive
 
 def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit := do
-  let (elabs, res) ← runTermElabM fun vars => do
+  let elabs ← runTermElabM fun _ =>
-    let elabs ← inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx
+      inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx
-    elabs.forM fun e => checkValidInductiveModifier e.view.modifiers
+
-    checkNoInductiveNameConflicts elabs
+  let isCoinductive := elabs.any (·.view.isCoinductive)
-    let res ← elabInductiveViews vars elabs
+
-    pure (elabs, res)
+  if isCoinductive then
-  elabInductiveViewsPostprocessing (elabs.map (·.view)) res
+    runTermElabM fun vars => do
+      checkNoInductiveNameConflicts elabs (isCoinductive := true)
+      let flatElabs := elabs.map fun e => {e with view := updateViewWithFunctorName e.view}
+      flatElabs.forM fun e => checkValidInductiveModifier e.view.modifiers
+      elabFlatInductiveViews vars flatElabs
+      discard <| flatElabs.mapM fun e => MetaM.run' do mkSumOfProducts e.view.declName
+      elabCoinductive (flatElabs.map InductiveViewToCoinductiveElab)
+      addTermInfoViews <| elabs.map (·.view)
+    elabInductiveViewsPostprocessingCoinductive (elabs.map (·.view))
+  else
+    let res ← runTermElabM fun vars => do
+      elabs.forM fun e => checkValidInductiveModifier e.view.modifiers
+      checkNoInductiveNameConflicts elabs
+      elabInductiveViews vars elabs
+    elabInductiveViewsPostprocessing (elabs.map (·.view)) res
 
 def elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   elabInductives #[(modifiers, stx)]

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -432,10 +432,10 @@ where
   doRealize name info type := withOptions (tactic.hygienic.set · false) do
     let value ← mkEqnProof declName type tryRefl
     let (type, value) ← removeUnusedEqnHypotheses type value
-    addDecl <| Declaration.thmDecl {
+    addDecl <| (←mkThmOrUnsafeDef {
       name, type, value
       levelParams := info.levelParams
-    }
+    })
     inferDefEqAttr name
 
 /--

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -103,10 +103,13 @@ where
       let type ← mkForallFVars xs type
       let type ← letToHave type
       let value ← mkLambdaFVars xs goal
-      addDecl <| Declaration.thmDecl {
+
-        name, type, value
+      addDecl <| (←mkThmOrUnsafeDef {
+        name := name
         levelParams := info.levelParams
-      }
+        type := type
+        value := value
+      })
 
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix

src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean

@@ -61,7 +61,7 @@ The optional parameter `reducePremise` (false by default) indicates whether we n
 -/
 def unfoldPredRel (predType : Expr) (lhs rhs : Expr) (fixpointType : PartialFixpointType) (reducePremise : Bool := false) : MetaM Expr := do
   guard <| isLatticeTheoretic fixpointType
-  forallTelescope predType fun ts _ => do
+  forallTelescopeReducing predType fun ts _ => do
     let mut lhs : Expr := mkAppN lhs ts
     let rhs : Expr := mkAppN rhs ts
     if reducePremise then
@@ -281,8 +281,7 @@ def deriveInduction (name : Name) (isMutual : Bool) : MetaM Unit := do
     -- Prune unused level parameters, preserving the original order
     let us := infos[0]!.levelParams.filter (params.contains ·)
 
-    addDecl <| Declaration.thmDecl
+    addDecl <| (←mkThmOrUnsafeDef { name := inductName, levelParams := us, type := eTyp, value := e' })
-      { name := inductName, levelParams := us, type := eTyp, value := e' }
 
 def isInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false

src/Lean/Meta/Eqns.lean

@@ -186,10 +186,10 @@ where doRealize name info := do
     -- Note: if this definition was added using `def`, then `letToHave` has already been applied to the body.
     let type  ← letToHave type
     let value ← mkLambdaFVars xs (← mkEqRefl lhs)
-    addDecl <| Declaration.thmDecl {
+    addDecl <| (←mkThmOrUnsafeDef {
       name, type, value
       levelParams := info.levelParams
-    }
+    })
     inferDefEqAttr name -- should always succeed
 
 /--

src/Lean/Meta/MkIffOfInductiveProp.lean

@@ -0,0 +1,380 @@
+/-
+Copyright (c) 2018 Johannes Hölzl, David Renshaw. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Johannes Hölzl, David Renshaw, Wojciech Różowski
+-/
+
+module
+
+prelude
+
+public import Lean.Elab.Tactic
+
+namespace Lean.Meta
+
+open Lean Meta Elab
+
+/-- Has the effect of `refine ⟨e₁,e₂,⋯, ?_⟩`.
+-/
+private def MVarId.existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
+  es.foldlM (fun mv e ↦ do
+      let (subgoals,_) ← Elab.Term.TermElabM.run <| Elab.Tactic.run mv do
+        Elab.Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
+      let [sg1, sg2] := subgoals | throwError "expected two subgoals"
+      sg1.assign e
+      pure sg2)
+    mvar
+
+/--
+Apply the `n`-th constructor of the target type,
+checking that it is an inductive type,
+and that there are the expected number of constructors.
+-/
+private def MVarId.nthConstructor
+    (name : Name) (idx : Nat) (expected? : Option Nat := none) (goal : MVarId) :
+    MetaM (List MVarId) := do
+  goal.withContext do
+    goal.checkNotAssigned name
+    matchConstInduct (← goal.getType').getAppFn
+      (fun _ => throwTacticEx name goal "target is not an inductive datatype")
+      fun ival us => do
+        if let some e := expected? then unless ival.ctors.length == e do
+          throwTacticEx name goal
+            s!"{name} tactic works for inductive types with exactly {e} constructors"
+        if h : idx < ival.ctors.length then
+          goal.apply <| mkConst ival.ctors[idx] us
+        else
+          throwTacticEx name goal s!"index {idx} out of bounds, only {ival.ctors.length} constructors"
+
+/-- `select m n` runs `right` `m` times; if `m < n`, then it also runs `left` once.
+Fails if `n < m`. -/
+private def select (m n : Nat) (goal : MVarId) : MetaM MVarId :=
+  match m,n with
+  | 0, 0             => pure goal
+  | 0, (_ + 1)       => do
+    let [new_goal] ← MVarId.nthConstructor `left 0 (some 2) goal
+      | throwError "expected only one new goal"
+    pure new_goal
+  | (m + 1), (n + 1) => do
+    let [new_goal] ← MVarId.nthConstructor `right 1 (some 2) goal
+      | throwError "expected only one new goal"
+    select m n new_goal
+  | _, _             => failure
+
+/-- `compactRelation bs as_ps`: Produce a relation of the form:
+```lean
+R := fun as ↦ ∃ bs, ⋀_i a_i = p_i[bs]
+```
+This relation is user-visible, so we compact it by removing each `b_j` where a `p_i = b_j`, and
+hence `a_i = b_j`. We need to take care when there are `p_i` and `p_j` with `p_i = p_j = b_k`.
+-/
+private partial def compactRelation :
+    List Expr → List (Expr × Expr) → List (Option Expr) × List (Expr × Expr) × (Expr → Expr)
+| [],    as_ps => ([], as_ps, id)
+| b::bs, as_ps =>
+  match as_ps.span (fun ⟨_, p⟩ ↦ p != b) with
+    | (_, []) => -- found nothing in ps equal to b
+      let (bs, as_ps', subst) := compactRelation bs as_ps
+      (b::bs, as_ps', subst)
+    | (ps₁, (a, _) :: ps₂) => -- found one that matches b. Remove it.
+      let i := fun e ↦ e.replaceFVar b a
+      let (bs, as_ps', subst) :=
+        compactRelation (bs.map i) ((ps₁ ++ ps₂).map (fun ⟨a, p⟩ ↦ (a, i p)))
+      (none :: bs, as_ps', i ∘ subst)
+
+private def updateLambdaBinderInfoD! (e : Expr) : Expr :=
+  match e with
+  | .lam n domain body _ => .lam n domain body .default
+  | _           => panic! "lambda expected"
+
+/-- Generates an expression of the form `∃ (args), inner`. `args` is assumed to be a list of fvars.
+When possible, `p ∧ q` is used instead of `∃ (_ : p), q`. -/
+private def mkExistsList (args : List Expr) (inner : Expr) : MetaM Expr :=
+  args.foldrM
+    (fun arg i:Expr => do
+      let t ← inferType arg
+      let l := (← inferType t).sortLevel!
+      if arg.occurs i || l != Level.zero
+        then pure (mkApp2 (.const `Exists [l]) t
+          (updateLambdaBinderInfoD! <| ← mkLambdaFVars #[arg] i))
+        else pure <| mkApp2 (mkConst `And) t i)
+    inner
+
+/-- `mkOpList op empty [x1, x2, ...]` is defined as `op x1 (op x2 ...)`.
+  Returns `empty` if the list is empty. -/
+private def mkOpList (op : Expr) (empty : Expr) : List Expr → Expr
+  | []        => empty
+  | [e]       => e
+  | (e :: es) => mkApp2 op e <| mkOpList op empty es
+
+/-- `mkAndList [x1, x2, ...]` is defined as `x1 ∧ (x2 ∧ ...)`, or `True` if the list is empty. -/
+private def mkAndList : List Expr → Expr := mkOpList (mkConst `And) (mkConst `True)
+
+/-- `mkOrList [x1, x2, ...]` is defined as `x1 ∨ (x2 ∨ ...)`, or `False` if the list is empty. -/
+private def mkOrList : List Expr → Expr := mkOpList (mkConst `Or) (mkConst `False)
+
+/-- Drops the final element of a list. -/
+private def List.init : List α → List α
+  | []     => []
+  | [_]    => []
+  | a::l => a::init l
+
+/-- Auxiliary data associated with a single constructor of an inductive declaration.
+-/
+private structure Shape : Type where
+  /-- For each forall-bound variable in the type of the constructor, minus
+  the "params" that apply to the entire inductive type, this list contains `true`
+  if that variable has been kept after `compactRelation`.
+
+  For example, `List.Chain.nil` has type
+  ```lean
+    ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []`
+  ```
+  and the first two variables `α` and `R` are "params", while the `a : α` gets
+  eliminated in a `compactRelation`, so `variablesKept = [false]`.
+
+  `List.Chain.cons` has type
+  ```lean
+    ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
+       R a b → List.Chain R b l → List.Chain R a (b :: l)
+  ```
+  and the `a : α` gets eliminated, so `variablesKept = [false,true,true,true,true]`.
+  -/
+  variablesKept : List Bool
+
+  /-- The number of equalities, or `none` in the case when we've reduced something
+  of the form `p ∧ True` to just `p`.
+  -/
+  neqs : Option Nat
+
+/-- Converts an inductive constructor `c` into a `Shape` that will be used later in
+while proving the iff theorem, and a proposition representing the constructor.
+-/
+private def constrToProp (univs : List Level) (params : List Expr) (idxs : List Expr) (c : Name) :
+    MetaM (Shape × Expr) := do
+  let type := (← getConstInfo c).instantiateTypeLevelParams univs
+  let type' ← Meta.forallBoundedTelescope type (params.length) fun fvars ty ↦ do
+    pure <| ty.replaceFVars fvars params.toArray
+  Meta.forallTelescope type' fun fvars ty ↦ do
+    let idxs_inst := ty.getAppArgs.toList.drop params.length
+    let (bs, eqs, subst) := compactRelation fvars.toList (idxs.zip idxs_inst)
+    let eqs ← eqs.mapM (fun ⟨idx, inst⟩ ↦ do
+      let ty ← idx.fvarId!.getType
+      let instTy ← inferType inst
+      let u := (← inferType ty).sortLevel!
+      if ← isDefEq ty instTy
+      then pure (mkApp3 (.const `Eq [u]) ty idx inst)
+      else pure (mkApp4 (.const `HEq [u]) ty idx instTy inst))
+    let (n, r) ← match bs.filterMap id, eqs with
+    | [], [] => do
+      pure (some 0, (mkConst `True))
+    | bs', [] => do
+      let t : Expr ← bs'.getLast!.fvarId!.getType
+      let l := (← inferType t).sortLevel!
+      if l == Level.zero then do
+        let r ← mkExistsList (List.init bs') t
+        pure (none, subst r)
+      else do
+        let r ← mkExistsList bs' (mkConst `True)
+        pure (some 0, subst r)
+    | bs', _ => do
+      let r ← mkExistsList bs' (mkAndList eqs)
+      pure (some eqs.length, subst r)
+    pure (⟨bs.map Option.isSome, n⟩, r)
+
+/-- Splits the goal `n` times via `refine ⟨?_,?_⟩`, and then applies `constructor` to
+close the resulting subgoals.
+-/
+private def splitThenConstructor (mvar : MVarId) (n : Nat) : MetaM Unit :=
+match n with
+| 0   => do
+  let (subgoals',_) ← Term.TermElabM.run <| Tactic.run mvar do
+    Tactic.evalTactic (← `(tactic| constructor))
+  let [] := subgoals' | throwError "expected no subgoals"
+  pure ()
+| n + 1 => do
+  let (subgoals,_) ← Term.TermElabM.run <| Tactic.run mvar do
+    Tactic.evalTactic (← `(tactic| refine ⟨?_,?_⟩))
+  let [sg1, sg2] := subgoals | throwError "expected two subgoals"
+  let (subgoals',_) ← Term.TermElabM.run <| Tactic.run sg1 do
+    Tactic.evalTactic (← `(tactic| constructor))
+  let [] := subgoals' | throwError "expected no subgoals"
+  splitThenConstructor sg2 n
+
+/-- Proves the left to right direction of a generated iff theorem.
+`shape` is the output of a call to `constrToProp`.
+-/
+private def toCases (mvar : MVarId) (shape : List Shape) : MetaM Unit :=
+do
+  let ⟨h, mvar'⟩ ← mvar.intro1
+  let subgoals ← mvar'.cases h
+  let _ ← (shape.zip subgoals.toList).zipIdx.mapM fun ⟨⟨⟨shape, t⟩, subgoal⟩, p⟩ ↦ do
+    let vars := subgoal.fields
+    let si := (shape.zip vars.toList).filterMap (fun ⟨c,v⟩ ↦ if c then some v else none)
+    let mvar'' ← select p (subgoals.size - 1) subgoal.mvarId
+    match t with
+    | none => do
+      let v := vars[shape.length - 1]!
+      let mv ← MVarId.existsi mvar'' (List.init si)
+      mv.assign v
+    | some n => do
+      let mv ← MVarId.existsi mvar'' si
+      splitThenConstructor mv (n - 1)
+  pure ()
+
+/-- Calls `cases` on `h` (assumed to be a binary sum) `n` times, and returns
+the resulting subgoals and their corresponding new hypotheses.
+-/
+def nCasesSum (n : Nat) (mvar : MVarId) (h : FVarId) : MetaM (List (FVarId × MVarId)) :=
+match n with
+| 0 => pure [(h, mvar)]
+| n' + 1 => do
+  let #[sg1, sg2] ← mvar.cases h | throwError "expected two case subgoals"
+  let #[Expr.fvar fvar1] ← pure sg1.fields | throwError "expected fvar"
+  let #[Expr.fvar fvar2] ← pure sg2.fields | throwError "expected fvar"
+  let rest ← nCasesSum n' sg2.mvarId fvar2
+  pure ((fvar1, sg1.mvarId)::rest)
+
+/-- Calls `cases` on `h` (assumed to be a binary product) `n` times, and returns
+the resulting subgoal and the new hypotheses.
+-/
+private def nCasesProd (n : Nat) (mvar : MVarId) (h : FVarId) : MetaM (MVarId × List FVarId) :=
+match n with
+| 0 => pure (mvar, [h])
+| n' + 1 => do
+  let #[sg] ← mvar.cases h | throwError "expected one case subgoals"
+  let #[Expr.fvar fvar1, Expr.fvar fvar2] ← pure sg.fields | throwError "expected fvar"
+  let (mvar', rest) ← nCasesProd n' sg.mvarId fvar2
+  pure (mvar', fvar1::rest)
+
+/--
+Iterate over two lists, if the first element of the first list is `false`, insert `none` into the
+result and continue with the tail of first list. Otherwise, wrap the first element of the second
+list with `some` and continue with the tails of both lists. Return when either list is empty.
+
+Example:
+```
+listBoolMerge [false, true, false, true] [0, 1, 2, 3, 4] = [none, (some 0), none, (some 1)]
+```
+-/
+private def listBoolMerge : List Bool → List α → List (Option α)
+  | [], _ => []
+  | false :: xs, ys => none :: listBoolMerge xs ys
+  | true :: xs, y :: ys => some y :: listBoolMerge xs ys
+  | true :: _, [] => []
+
+/-- Proves the right to left direction of a generated iff theorem.
+-/
+private def toInductive (mvar : MVarId) (cs : List Name)
+    (gs : List Expr) (s : List Shape) (h : FVarId) :
+    MetaM Unit := do
+  match s.length with
+  | 0       => do let _ ← mvar.cases h
+                  pure ()
+  | (n + 1) => do
+      let subgoals ← nCasesSum n mvar h
+      let _ ← (cs.zip (subgoals.zip s)).mapM fun ⟨constr_name, ⟨h, mv⟩, bs, e⟩ ↦ do
+        let n := (bs.filter id).length
+        let (mvar', _fvars, numHEqs) ← match e with
+        | none =>
+            let (id, fvarIds) ← nCasesProd (n-1) mv h
+            pure ⟨id, fvarIds, 0⟩
+        | some 0 => do let ⟨mvar', fvars⟩ ← nCasesProd n mv h
+                          let mvar'' ← mvar'.tryClear fvars.getLast!
+                          pure ⟨mvar'', fvars, 0⟩
+        | some (e + 1) => do
+          let (mv', fvars) ← nCasesProd n mv h
+          let lastfv := fvars.getLast!
+          let (mv2, fvars') ← nCasesProd e mv' lastfv
+          let numHEqs ← mv2.withContext do
+            let fvarTypes ← fvars'.mapM (·.getType)
+            let res := fvarTypes.map (·.isAppOf `HEq)
+            let res := res.filter id
+            pure res.length
+
+          /- `fvars'.foldlM subst mv2` fails when we have dependent equalities (`HEq`).
+          `subst` will change the dependent hypotheses, so that the `uniq` local names
+          are wrong afterwards. Instead we revert them and pull them out one-by-one. -/
+          let (_, mv3) ← mv2.revert fvars'.toArray
+          let mv4 ← fvars'.foldlM (fun mv _ ↦ do
+            let ⟨fv, mv'⟩ ← mv.intro1
+            let #[res] ← mv'.cases fv | throwError "expected one case subgoal"
+            return res.mvarId) mv3
+          pure (mv4, fvars, numHEqs)
+        mvar'.withContext do
+          let fvarIds := (← getLCtx).getFVarIds.toList
+          let gs := fvarIds.take gs.length
+          let hs := fvarIds.extract (fvarIds.length - (n + numHEqs)) (fvarIds.length - numHEqs)
+          let m := gs.map some ++ listBoolMerge bs hs
+          let args ← m.mapM fun a ↦
+            match a with
+            | some v => pure (mkFVar v)
+            | none => mkFreshExprMVar none
+          let c ← mkConstWithLevelParams constr_name
+          let e := mkAppN c args.toArray
+          let t ← inferType e
+          let mt ← mvar'.getType
+          let _ ← isDefEq t mt -- infer values for those mvars we just made
+          mvar'.assign e
+
+/--
+  Generates existential form of a prop-valued inductive type and proves the equivalence.
+-/
+private def mkIffOfInductivePropImpl (inductVal : InductiveVal) (rel : Name) : MetaM Unit := do
+  let constrs := inductVal.ctors
+  let params := inductVal.numParams
+  let type := inductVal.type
+
+  let univNames := inductVal.levelParams
+  let univs := univNames.map mkLevelParam
+  /- we use these names for our universe parameters, maybe we should construct a copy of them
+  using `uniq_name` -/
+
+  let (thmTy, shape, existential) ← Meta.forallTelescopeReducing type fun fvars ty ↦ do
+    if !ty.isProp then throwError "mk_iff only applies to prop-valued declarations"
+    let lhs := mkAppN (mkConst inductVal.name univs) fvars
+    let fvars' := fvars.toList
+    let shape_rhss ← constrs.mapM (constrToProp univs (fvars'.take params) (fvars'.drop params))
+    let (shape, rhss) := shape_rhss.unzip
+    let existential := mkOrList rhss
+    let existential ← mkLambdaFVars fvars existential
+    pure (← mkForallFVars fvars (mkApp2 (mkConst `Iff) lhs (mkOrList rhss)), shape, existential)
+
+  trace[Meta.MkIffOfInductiveProp] "Existential form is: {existential}"
+  trace[Meta.MkIffOfInductiveProp] "The type of proof of equivalence: {thmTy}"
+
+  let mvar ← mkFreshExprMVar (some thmTy)
+  let mvarId := mvar.mvarId!
+  let (fvars, mvarId') ← mvarId.intros
+  let [mp, mpr] ← mvarId'.apply (mkConst `Iff.intro) | throwError "failed to split goal"
+
+  toCases mp shape
+  let ⟨mprFvar, mpr'⟩ ← mpr.intro1
+  toInductive mpr' constrs ((fvars.toList.take params).map .fvar) shape mprFvar
+
+  let proof ← instantiateMVars mvar
+  addDecl <| (←mkThmOrUnsafeDef {
+    name := rel
+    levelParams := univNames
+    type := thmTy
+    value := proof
+  })
+
+  addDecl <| .defnDecl (←mkDefinitionValInferringUnsafe
+    (inductVal.name ++ `existential) inductVal.levelParams
+    (←inferType existential) existential .opaque)
+
+
+public def mkSumOfProducts (declName : Name) : MetaM Unit := do
+    trace[Meta.MkIffOfInductiveProp] "Generating existential form of {declName}"
+    let .inductInfo infos ← getConstInfo declName | throwError "Needs to be a definition"
+    mkIffOfInductivePropImpl infos (declName ++ `existential_equiv)
+
+builtin_initialize
+  registerTraceClass `Meta.MkIffOfInductiveProp
+
+end Lean.Meta

src/Lean/Parser/Command.lean

@@ -237,6 +237,9 @@ for more information.
 @[builtin_doc] def «inductive» := leading_parser
   "inductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
   many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
+@[builtin_doc] def «coinductive» := leading_parser
+  "coinductive " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> optional (symbol " :=" <|> " where") >>
+  many ctor >> optional (ppDedent ppLine >> computedFields) >> optDeriving
 def classInductive   := leading_parser
   atomic (group (symbol "class " >> "inductive ")) >>
   recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >>
@@ -278,7 +281,7 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def declaration := leading_parser
   declModifiers false >>
   («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
-   «inductive» <|> classInductive <|> «structure»)
+   «inductive» <|> «coinductive» <|> classInductive <|> «structure»)
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover termParser skip) ", "
 def sectionHeader := leading_parser

tests/lean/run/coinductive_syntax.lean

@@ -0,0 +1,252 @@
+-- set_option trace.Elab.coinductive true
+set_option pp.proofs true
+section
+variable (α : Type)
+
+/--
+docstring
+-/
+coinductive infSeq (r : α → α → Prop) : α → Prop where
+  | step : r a b → infSeq r b → infSeq r a
+
+/--
+info: infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
+-/
+#guard_msgs in
+#check infSeq.step
+
+theorem casesOnTest (r : α → α → Prop) (a : α) : infSeq α r a → ∃ b, r a b := by
+  intro h
+  cases h
+  case step b _ hr => exists b
+
+-- `match` support does not work yet
+/--
+error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
+
+Hint: These are similar:
+  'Lean.Order.iterates.below.step',
+  'Lean.Order.iterates.step',
+  'Nat.le.below.step',
+  'Nat.le.step',
+  'infSeq._functor.step'
+---
+error: Case tag `rhs` not found.
+
+Note: There are no cases to select.
+-/
+#guard_msgs in
+theorem casesOnTest' (r : α → α → Prop) (a : α) : infSeq α r a → ∃ b, r a b := by
+  intro h
+  match h with
+  | step  b _ hr => exists b
+
+/--
+info: infSeq.casesOn (α : Type) (r : α → α → Prop) {motive : (a : α) → infSeq α r a → Prop} {a✝ : α} (t : infSeq α r a✝)
+  (step : ∀ {a b : α} (a_1 : r a b) (a_2 : infSeq α r b), motive a (infSeq.step α r a_1 a_2)) : motive a✝ t
+-/
+#guard_msgs in
+#check infSeq.casesOn
+
+/--
+info: infSeq.functor_unfold (α : Type) (r : α → α → Prop) (a✝ : α) : infSeq α r a✝ = infSeq._functor α r (infSeq α r) a✝
+-/
+#guard_msgs in
+#check infSeq.functor_unfold
+
+/-- info: infSeq (α : Type) (r : α → α → Prop) : α → Prop -/
+#guard_msgs in
+#check infSeq
+
+/--
+info: inductive infSeq._functor : (α : Type) → (α → α → Prop) → (α → Prop) → α → Prop
+number of parameters: 3
+constructors:
+infSeq._functor.step : ∀ (α : Type) (r : α → α → Prop) (infSeq._functor.call : α → Prop) {a b : α},
+  r a b → infSeq._functor.call b → infSeq._functor α r infSeq._functor.call a
+-/
+#guard_msgs in
+#print infSeq._functor
+
+/--
+info: def infSeq._functor.existential : (α : Type) → (α → α → Prop) → (α → Prop) → α → Prop :=
+fun α r infSeq._functor.call a => ∃ b, r a b ∧ infSeq._functor.call b
+-/
+#guard_msgs in
+#print infSeq._functor.existential
+
+/--
+info: infSeq._functor.existential_equiv (α : Type) (r : α → α → Prop) (infSeq._functor.call : α → Prop) (a✝ : α) :
+  infSeq._functor α r infSeq._functor.call a✝ ↔ ∃ b, r a✝ b ∧ infSeq._functor.call b
+-/
+#guard_msgs in
+#check infSeq._functor.existential_equiv
+
+/--
+info: infSeq.coinduct (α : Type) (r : α → α → Prop) (pred : α → Prop) (hyp : ∀ (a : α), pred a → ∃ b, r a b ∧ pred b)
+  (a✝ : α) : pred a✝ → infSeq α r a✝
+-/
+#guard_msgs in
+#check infSeq.coinduct
+
+/--
+info: infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a
+-/
+#guard_msgs in
+#check infSeq.step
+end
+
+section
+mutual
+  coinductive tick : Prop where
+  | mk : ¬tock → tick
+
+  inductive tock : Prop where
+  | mk : ¬tick → tock
+end
+
+/--
+info: tick._functor.casesOn {tick._functor.call tock._functor.call : Prop}
+  {motive_1 : tick._functor tick._functor.call tock._functor.call → Prop}
+  (t : tick._functor tick._functor.call tock._functor.call)
+  (mk : ∀ (a : ¬tock._functor.call), motive_1 (tick._functor.mk tick._functor.call tock._functor.call a)) : motive_1 t
+-/
+#guard_msgs in
+#check tick._functor.casesOn
+
+/-- info: tick.mk : ¬tock → tick -/
+#guard_msgs in
+#check tick.mk
+
+/-- info: tock.mk : ¬tick → tock -/
+#guard_msgs in
+#check tock.mk
+
+/-- info: tock._functor (tick._functor.call tock._functor.call : Prop) : Prop -/
+#guard_msgs in
+#check tock._functor
+
+/-- info: tock._functor.existential (tick._functor.call tock._functor.call : Prop) : Prop -/
+#guard_msgs in
+#check tock._functor.existential
+
+/--
+info: tick.coinduct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
+  pred_1 → tick
+-/
+#guard_msgs in
+#check tick.coinduct
+
+/--
+info: tock._functor.existential_equiv (tick._functor.call tock._functor.call : Prop) :
+  tock._functor tick._functor.call tock._functor.call ↔ ¬tick._functor.call
+-/
+#guard_msgs in
+#check tock._functor.existential_equiv
+
+/--
+info: tock.induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) : tock → pred_2
+-/
+#guard_msgs in
+#check tock.induct
+
+/--
+info: tick.mutual_induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
+  (pred_1 → tick) ∧ (tock → pred_2)
+-/
+#guard_msgs in
+#check tick.mutual_induct
+end
+
+/-- error: `coinductive` keyword can only be used to define predicates -/
+#guard_msgs in
+coinductive my_nat  where
+  | zero : my_nat
+  | succ : my_nat → my_nat
+
+def Set := Nat → Prop
+
+coinductive Foo : Set where
+
+/--
+info: Foo.coinduct (pred : Set) (hyp : ∀ (a : Nat), pred a → False) (a✝ : Nat) : pred a✝ → Foo a✝
+-/
+#guard_msgs in
+#check Foo.coinduct
+
+coinductive Bar : Set where
+  | make : Bar 42
+
+/--
+info: Bar.coinduct (pred : Set) (hyp : ∀ (a : Nat), pred a → a = 42) (a✝ : Nat) : pred a✝ → Bar a✝
+-/
+#guard_msgs in
+#check Bar.coinduct
+
+
+coinductive dependentTest : (n : Nat) → (Vector α n) → Prop  where
+  | mk (x : α) : dependentTest m v → dependentTest (m+1) (v.push x)
+
+/--
+info: dependentTest.coinduct.{u_1} {α : Type u_1} (pred : (n : Nat) → Vector α n → Prop)
+  (hyp : ∀ (n : Nat) (a : Vector α n), pred n a → ∃ m v x, pred m v ∧ n = m + 1 ∧ a ≍ v.push x) (n : Nat)
+  (a✝ : Vector α n) : pred n a✝ → dependentTest n a✝
+-/
+#guard_msgs in
+#check dependentTest.coinduct
+
+/-
+  Duplicated parameters and dependent types
+-/
+coinductive dependentTest2 : (n : Nat) → (m : Nat) → (Vector α (m + n)) → (Vector α (m + n)) → Prop  where
+  | mk (x : α) : dependentTest2 0 n v v → dependentTest2 0 (n + 1) (v.push x) (v.push x)
+
+coinductive dependentTest3 : (α : Type) → (ls : List α) → (vec : Vector α ls.length) → (Vector α vec.size) → Prop where
+  | mk : dependentTest3 Nat [a] (Vector.singleton a) (Vector.singleton a)
+  | mk2 : dependentTest3 String ["hi"] (Vector.singleton b) (Vector.singleton c)
+
+/--
+info: dependentTest3.casesOn
+  {motive :
+    (α : Type) →
+      (ls : List α) → (vec : Vector α ls.length) → (a : Vector α vec.size) → dependentTest3 α ls vec a → Prop}
+  {α : Type} {ls : List α} {vec : Vector α ls.length} {a✝ : Vector α vec.size} (t : dependentTest3 α ls vec a✝)
+  (mk : ∀ {a : Nat}, motive Nat [a] (Vector.singleton a) (Vector.singleton a) dependentTest3.mk)
+  (mk2 : ∀ {b c : String}, motive String ["hi"] (Vector.singleton b) (Vector.singleton c) dependentTest3.mk2) :
+  motive α ls vec a✝ t
+-/
+#guard_msgs in
+#check dependentTest3.casesOn
+
+coinductive test1  (r: α → α → Prop) : α → α → Prop where
+  | mk : r a b → test1 r a b → test1 r a a
+  | mk2 : test1 r a a
+
+coinductive test2  (r: α → α → Prop) : α → α → Prop where
+  | mk : r a b → test2 r b b → test2 r a a
+
+/--
+error: Cannot define an coinductive predicate and a constructor with the same name `A.mk`
+---
+error: Cannot define an coinductive predicate and a constructor with the same name `A.mk`
+-/
+#guard_msgs in
+mutual
+  coinductive A : Prop where
+    | mk : A.mk → A
+  coinductive A.mk : Prop where
+    | mk : A → A.mk
+end
+
+macro "test%" : command => `(command|
+  coinductive MacroTest : Prop where | mk : MacroTest
+)
+
+/-- error: Coinductive predicates are not allowed inside of macro scopes -/
+#guard_msgs in
+test%
+
+namespace unsafe_test
+unsafe coinductive infSeq2 (r : α → α → Prop) : α → Prop where
+  | step : r a b → infSeq2 r b → infSeq2 r a
+end unsafe_test

tests/lean/versoDocMissing.lean.expected.out

@@ -1 +1 @@
-versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
+versoDocMissing.lean:10:0: error: unexpected end of input; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_error_explanation', 'register_tactic_tag', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'

tests/pkg/user_attr_app/UserAttr/BlaAttr.lean

@@ -3,3 +3,10 @@ import Lean
 open Lean
 
 initialize blaAttr : TagAttribute ← registerTagAttribute `bla "simple user defined attribute"
+
+initialize registerBuiltinAttribute {
+  name := `testPred
+  descr := "Dummy attribute for testing"
+  add := fun declName _stx _kind => do
+    logInfo s!"Applied @testPred to {declName}"
+}

tests/pkg/user_attr_app/UserAttr/Tst.lean

@@ -2,3 +2,6 @@ import UserAttr.BlaAttr
 
 @[bla] def f (x : Nat) := x + 2
 @[bla] def g (x : Nat) := x + 1
+
+@[testPred] coinductive infSeq (r : α → α → Prop) : α → Prop where
+  | mk : r a b → infSeq r b → infSeq r a