diff --git a/src/Lean/Elab/Coinductive.lean b/src/Lean/Elab/Coinductive.lean new file mode 100644 index 0000000000..d93edf1f8e --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index d40b951713..1c94563444 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/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 diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 44d098215e..25f9ef4678 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/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 elabInductiveCommand : InductiveElabDescr where - mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do - let view ← inductiveSyntaxToView modifiers stx +def mkInductiveElabDescr (isCoinductive := false) : InductiveElabDescr where +mkInductiveView (modifiers : Modifiers) (stx : Syntax) := do + let view ← inductiveSyntaxToView modifiers stx isCoinductive 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 diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 23b35f92c0..ffebba0a31 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/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 := - Term.withoutSavingRecAppSyntax do +private structure FinalizeInductiveDecl where + 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 - 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 + k vars elabs rs scopeLevelNames - -- 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. - 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) +private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := + withElaboratedHeaders vars elabs fun vars elabs rs scopeLevelNames => do + let res ← mkInductiveDeclCore addAndFinalizeInductiveDecl vars elabs rs scopeLevelNames + addTermInfoViews <| elabs.map (·.view) 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 ← inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx - elabs.forM fun e => checkValidInductiveModifier e.view.modifiers - checkNoInductiveNameConflicts elabs - let res ← elabInductiveViews vars elabs - pure (elabs, res) - elabInductiveViewsPostprocessing (elabs.map (·.view)) res + let elabs ← runTermElabM fun _ => + inductives.mapM fun (modifiers, stx) => mkInductiveView modifiers stx + + let isCoinductive := elabs.any (·.view.isCoinductive) + + if isCoinductive then + 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)] diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 409f00f16f..22e00be245 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/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 /-- diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index dc0d3e19e6..aed457f69a 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/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 diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean index 325a647777..fa7263f3ed 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean +++ b/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 - { name := inductName, levelParams := us, type := eTyp, value := e' } + addDecl <| (←mkThmOrUnsafeDef { 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 diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index b349167f79..79bf3d2469 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/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 /-- diff --git a/src/Lean/Meta/MkIffOfInductiveProp.lean b/src/Lean/Meta/MkIffOfInductiveProp.lean new file mode 100644 index 0000000000..eb7320e58b --- /dev/null +++ b/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 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 029b01a791..4efb49c644 100644 --- a/src/Lean/Parser/Command.lean +++ b/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 diff --git a/tests/lean/run/coinductive_syntax.lean b/tests/lean/run/coinductive_syntax.lean new file mode 100644 index 0000000000..8c03ca45fe --- /dev/null +++ b/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 diff --git a/tests/lean/versoDocMissing.lean.expected.out b/tests/lean/versoDocMissing.lean.expected.out index 050baa15ac..bf8baa66f4 100644 --- a/tests/lean/versoDocMissing.lean.expected.out +++ b/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' diff --git a/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean b/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean index 7314fc152b..ca2715b971 100644 --- a/tests/pkg/user_attr_app/UserAttr/BlaAttr.lean +++ b/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}" +} diff --git a/tests/pkg/user_attr_app/UserAttr/Tst.lean b/tests/pkg/user_attr_app/UserAttr/Tst.lean index f80db320f8..88b5835169 100644 --- a/tests/pkg/user_attr_app/UserAttr/Tst.lean +++ b/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