From f89ed406189a79cd7a3a8fb746919db7bb5aae83 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 14 Mar 2024 15:59:40 +0100 Subject: [PATCH] refactor: ArgsPacker (#3621) This introduces the `ArgsPacker` module and abstraction, to replace the exising `PackDomain`/`PackMutual` code. The motivation was that we now have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the code was spread in various places. The goals are * consistent function naming withing the the `PSigma` handling, the `PSum` handling, and the combined interface * avoid taking a type apart just based on the `PSigma`/`PSum` nesting, to be robust in case the user happens to be using `PSigma`/`PSum` somewhere. Therefore, always pass an `arity` or `numFuncs` or `varNames` around. * keep all the `PSigma`/`PSum` encoding logic contained within one module (`ArgsPacker`), and keep that module independent of its users (so no `EqnInfos` visible here). * pick good variable names when matching on a packed argument * the unary function now is either called `fun1._unary` or `fun1._mutual`, never `fun1._unary._mutual`. This file has less heavy dependencies than `PackMutual` had, so build parallelism is improved as well. --- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 8 +- src/Lean/Elab/PreDefinition/WF/Fix.lean | 16 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 44 +- src/Lean/Elab/PreDefinition/WF/Main.lean | 62 +- .../Elab/PreDefinition/WF/PackDomain.lean | 191 ------ .../Elab/PreDefinition/WF/PackMutual.lean | 250 ++------ src/Lean/Meta/AppBuilder.lean | 21 + src/Lean/Meta/ArgsPacker.lean | 572 ++++++++++++++++++ src/Lean/Meta/ArgsPacker/Basic.lean | 33 + src/Lean/Meta/Tactic/FunInd.lean | 201 +----- tests/lean/guessLex.lean | 9 +- tests/lean/guessLex.lean.expected.out | 12 +- tests/lean/guessLexFailures.lean.expected.out | 42 +- tests/lean/mutwftypemismatch.lean | 28 + .../lean/mutwftypemismatch.lean.expected.out | 14 + tests/lean/run/funind_demo.lean | 4 +- tests/lean/run/funind_mutual_dep.lean | 4 +- tests/lean/run/funind_proof.lean | 2 +- tests/lean/run/funind_tests.lean | 47 +- tests/lean/run/mutwf3.lean | 6 +- tests/lean/run/mutwf4.lean | 2 +- 21 files changed, 863 insertions(+), 705 deletions(-) delete mode 100644 src/Lean/Elab/PreDefinition/WF/PackDomain.lean create mode 100644 src/Lean/Meta/ArgsPacker.lean create mode 100644 src/Lean/Meta/ArgsPacker/Basic.lean create mode 100644 tests/lean/mutwftypemismatch.lean create mode 100644 tests/lean/mutwftypemismatch.lean.expected.out diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index f4e6b35808..85997209d8 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Rewrite import Lean.Meta.Tactic.Split import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Eqns +import Lean.Meta.ArgsPacker.Basic namespace Lean.Elab.WF open Meta @@ -17,6 +18,7 @@ structure EqnInfo extends EqnInfoCore where declNames : Array Name declNameNonRec : Name fixedPrefixSize : Nat + argsPacker : ArgsPacker deriving Inhabited private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do @@ -129,7 +131,8 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) := builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension -def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do +def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) + (argsPacker : ArgsPacker) : MetaM Unit := do /- See issue #2327. Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare @@ -140,7 +143,8 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi let declNames := preDefs.map (·.declName) modifyEnv fun env => preDefs.foldl (init := env) fun env preDef => - eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize } + eqnInfoExt.insert env preDef.declName { preDef with + declNames, declNameNonRec, fixedPrefixSize, argsPacker } def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do if let some info := eqnInfoExt.find? (← getEnv) declName then diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 5f1e9b632c..b60153bbf0 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -8,12 +8,12 @@ import Lean.Util.HasConstCache import Lean.Meta.Match.Match import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.Cleanup +import Lean.Meta.ArgsPacker import Lean.Elab.Tactic.Basic import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural.Basic import Lean.Elab.PreDefinition.Structural.BRecOn -import Lean.Elab.PreDefinition.WF.PackMutual import Lean.Data.Array namespace Lean.Elab.WF @@ -172,19 +172,19 @@ know which function is making the call. The close coupling with how arguments are packed and termination goals look like is not great, but it works for now. -/ -def groupGoalsByFunction (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do +def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Array MVarId) : MetaM (Array (Array MVarId)) := do let mut r := mkArray numFuncs #[] for goal in goals do let (.mdata _ (.app _ param)) ← goal.getType | throwError "MVar does not look like like a recursive call" - let (funidx, _) ← unpackMutualArg numFuncs param + let (funidx, _) ← argsPacker.unpack param r := r.modify funidx (·.push goal) return r -def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do +def solveDecreasingGoals (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do let goals ← getMVarsNoDelayed value let goals ← assignSubsumed goals - let goalss ← groupGoalsByFunction decrTactics.size goals + let goalss ← groupGoalsByFunction argsPacker decrTactics.size goals for goals in goalss, decrTactic? in decrTactics do Lean.Elab.Term.TermElabM.run' do match decrTactic? with @@ -205,8 +205,8 @@ def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Ex Term.reportUnsolvedGoals remainingGoals instantiateMVars value -def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) - (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do +def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker) + (wfRel : Expr) (decrTactics : Array (Option DecreasingBy)) : TermElabM Expr := do let type ← instantiateForall preDef.type prefixArgs let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do let x := x[0]! @@ -229,7 +229,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) let val := preDef.value.beta (prefixArgs.push x) let val ← processSumCasesOn x F val fun x F val => do processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size) - let val ← solveDecreasingGoals decrTactics val + let val ← solveDecreasingGoals argsPacker decrTactics val mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val)) end Lean.Elab.WF diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index d20eebfab0..5a29c302d1 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -9,12 +9,12 @@ import Lean.Meta.Match.MatcherApp.Transform import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Refl import Lean.Meta.Tactic.TryThis +import Lean.Meta.ArgsPacker import Lean.Elab.Quotation import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural.Basic import Lean.Elab.PreDefinition.WF.TerminationHint -import Lean.Elab.PreDefinition.WF.PackMutual import Lean.Data.Array @@ -84,11 +84,11 @@ def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName) /-- -Given the original paramter names from `originalVarNames`, remove the fixed prefix and find +Given the original parameter names from `originalVarNames`, find good variable names to be used when talking about termination arguments: Use user-given parameter names if present; use x1...xn otherwise. -The names ought to accessible (no macro scopes) and new names fresh wrt to the current environment, +The names ought to accessible (no macro scopes) and fresh wrt to the current environment, so that with `showInferredTerminationBy` we can print them to the user reliably. We do that by appending `'` as needed. @@ -97,8 +97,7 @@ shadow each other, and the guessed relation refers to the wrong one. In that case, the user gets to keep both pieces (and may have to rename variables). -/ partial -def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do - let xs := xs.extract fixedPrefixSize xs.size +def naryVarNames (xs : Array Name) : MetaM (Array Name) := do let mut ns : Array Name := #[] for h : i in [:xs.size] do let n := xs[i] @@ -264,8 +263,8 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext /-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive call site. -/ -def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) - : MetaM (Array RecCallWithContext) := withoutModifyingState do +def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) + (argsPacker : ArgsPacker) : MetaM (Array RecCallWithContext) := withoutModifyingState do addAsAxiom unaryPreDef lambdaTelescope unaryPreDef.value fun xs body => do unless xs.size == fixedPrefixSize + 1 do @@ -277,8 +276,8 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti throwError "Insufficient arguments in recursive call" let arg := args[fixedPrefixSize]! trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})" - let (caller, params) ← unpackArg arities param - let (callee, args) ← unpackArg arities arg + let (caller, params) ← argsPacker.unpack param + let (callee, args) ← argsPacker.unpack arg RecCallWithContext.create (← getRef) caller params callee args /-- A `GuessLexRel` described how a recursive call affects a measure; whether it @@ -738,12 +737,14 @@ Try to find a lexicographic ordering of the arguments for which the recursive de terminates. See the module doc string for a high-level overview. -/ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) - (fixedPrefixSize : Nat) : + (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) : MetaM TerminationWF := do + let extraParamss := preDefs.map (·.termination.extraParams) + let arities := argsPacker.varNamess.map (·.size) + let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·) + -- with fixed prefix, used to qualify the measure in buildTermWf. let originalVarNamess ← preDefs.mapM originalVarNames - let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·) - let arities := varNamess.map (·.size) - trace[Elab.definition.wf] "varNames is: {varNamess}" + trace[Elab.definition.wf] "varNames is: {userVarNamess}" let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize) let needsNoSizeOf ← @@ -758,23 +759,30 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) -- If there is only one plausible measure, use that if let #[solution] := measures then - let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf #[solution] + let wf ← buildTermWF originalVarNamess userVarNamess needsNoSizeOf #[solution] reportWF preDefs wf return wf -- Collect all recursive calls and extract their context - let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities + let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker let recCalls := filterSubsumed recCalls let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·) let callMatrix := rcs.map (inspectCall ·) match ← liftMetaM <| solve measures callMatrix with | .some solution => do - let wf ← buildTermWF originalVarNamess varNamess needsNoSizeOf solution - reportWF preDefs wf + let wf ← buildTermWF originalVarNamess userVarNamess needsNoSizeOf solution + + let wf' := trimTermWF extraParamss wf + for preDef in preDefs, term in wf' do + if showInferredTerminationBy.get (← getOptions) then + logInfoAt preDef.ref m!"Inferred termination argument:\n{← term.unexpand}" + if let some ref := preDef.termination.terminationBy?? then + Tactic.TryThis.addSuggestion ref (← term.unexpand) + return wf | .none => - let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs + let explanation ← explainFailure (preDefs.map (·.declName)) userVarNamess rcs Lean.throwError <| "Could not find a decreasing measure.\n" ++ explanation ++ "\n" ++ "Please use `termination_by` to specify a decreasing measure." diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean index b20687ca7a..ec48a2e85a 100644 --- a/src/Lean/Elab/PreDefinition/WF/Main.lean +++ b/src/Lean/Elab/PreDefinition/WF/Main.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura prelude import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.WF.TerminationHint -import Lean.Elab.PreDefinition.WF.PackDomain import Lean.Elab.PreDefinition.WF.PackMutual import Lean.Elab.PreDefinition.WF.Preprocess import Lean.Elab.PreDefinition.WF.Rel @@ -19,29 +18,15 @@ namespace Lean.Elab open WF open Meta -private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) (fixedPrefixSize : Nat) : TermElabM Unit := do +private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do let us := preDefNonRec.levelParams.map mkLevelParam let all := preDefs.toList.map (·.declName) for fidx in [:preDefs.size] do let preDef := preDefs[fidx]! - let value ← lambdaTelescope preDef.value fun xs _ => do - let packedArgs : Array Expr := xs[fixedPrefixSize:] - let mkProd (type : Expr) : MetaM Expr := do - mkUnaryArg type packedArgs - let rec mkSum (i : Nat) (type : Expr) : MetaM Expr := do - if i == preDefs.size - 1 then - mkProd type - else - (← whnfD type).withApp fun f args => do - assert! args.size == 2 - if i == fidx then - return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! (← mkProd args[0]!) - else - let r ← mkSum (i+1) args[1]! - return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r - let Expr.forallE _ domain _ _ := (← instantiateForall preDefNonRec.type xs[:fixedPrefixSize]) | unreachable! - let arg ← mkSum 0 domain - mkLambdaFVars xs (mkApp (mkAppN (mkConst preDefNonRec.declName us) xs[:fixedPrefixSize]) arg) + let value ← forallBoundedTelescope preDef.type (some fixedPrefixSize) fun xs _ => do + let value := mkAppN (mkConst preDefNonRec.declName us) xs + let value ← argsPacker.curryProj value fidx + mkLambdaFVars xs value trace[Elab.definition.wf] "{preDef.declName} := {value}" addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all) @@ -81,23 +66,44 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : else return false +/-- +Collect the names of the varying variables (after the fixed prefix); this also determines the +arity for the well-founded translations, and is turned into an `ArgsPacker`. +We use the term to determine the arity, but take the name from the type, for better names in the +``` +fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n +``` +idiom. +-/ +def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name) := do + -- We take the arity from the term, but the names from the types + let arity ← lambdaTelescope preDef.value fun xs _ => return xs.size + assert! fixedPrefixSize ≤ arity + if arity = fixedPrefixSize then + throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments" + forallBoundedTelescope preDef.type arity fun xs _ => do + assert! xs.size = arity + let xs : Array Expr := xs[fixedPrefixSize:] + xs.mapM (·.fvarId!.getUserName) + def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do let preDefs ← preDefs.mapM fun preDef => return { preDef with value := (← preprocess preDef.value) } - let (unaryPreDef, fixedPrefixSize) ← withoutModifyingEnv do + let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do for preDef in preDefs do addAsAxiom preDef let fixedPrefixSize ← getFixedPrefix preDefs trace[Elab.definition.wf] "fixed prefix: {fixedPrefixSize}" + let varNamess ← preDefs.mapM (varyingVarNames fixedPrefixSize ·) + let argsPacker := { varNamess } let preDefsDIte ← preDefs.mapM fun preDef => return { preDef with value := (← iteToDIte preDef.value) } - let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte - return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize) + return (fixedPrefixSize, argsPacker, ← packMutual fixedPrefixSize argsPacker preDefsDIte) let wf ← do let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.terminationBy?.isSome) if preDefsWith.isEmpty then -- No termination_by anywhere, so guess one - guessLex preDefs unaryPreDef fixedPrefixSize + guessLex preDefs unaryPreDef fixedPrefixSize argsPacker else if preDefsWithout.isEmpty then pure <| preDefsWith.map (·.termination.terminationBy?.get!) else @@ -109,12 +115,14 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do let type ← whnfForall type + unless type.isForall do + throwError "wfRecursion: expected unary function type: {type}" let packedArgType := type.bindingDomain! elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do trace[Elab.definition.wf] "wfRel: {wfRel}" let (value, envNew) ← withoutModifyingEnv' do addAsAxiom unaryPreDef - let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasingBy?)) + let value ← mkFix unaryPreDef prefixArgs argsPacker wfRel (preDefs.map (·.termination.decreasingBy?)) eraseRecAppSyntaxExpr value /- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/ let value ← unfoldDeclsFrom envNew value @@ -126,12 +134,12 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do else withEnableInfoTree false do addNonRec preDefNonRec (applyAttrAfterCompilation := false) - addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize + addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec -- We create the `_unsafe_rec` before we abstract nested proofs. -- Reason: the nested proofs may be referring to the _unsafe_rec. addAndCompilePartialRec preDefs let preDefs ← preDefs.mapM (abstractNestedProofs ·) - registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize + registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker for preDef in preDefs do applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean deleted file mode 100644 index d450e6c9ce..0000000000 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ /dev/null @@ -1,191 +0,0 @@ -/- -Copyright (c) 2021 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -prelude -import Lean.Meta.Tactic.Cases -import Lean.Elab.PreDefinition.Basic - -namespace Lean.Elab.WF -open Meta - -/-- - Given a (dependent) tuple `t` (using `PSigma`) of the given arity. - Return an array containing its "elements". - Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`. - -/ -private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do - let mut result := #[] - let mut t := t - for _ in [:arity - 1] do - result := result.push (mkProj ``PSigma 0 t) - t := mkProj ``PSigma 1 t - result.push t - -/-- Create a unary application by packing the given arguments using `PSigma.mk` -/ -partial def mkUnaryArg (type : Expr) (args : Array Expr) : MetaM Expr := do - go 0 type -where - go (i : Nat) (type : Expr) : MetaM Expr := do - if i < args.size - 1 then - let arg := args[i]! - assert! type.isAppOfArity ``PSigma 2 - let us := type.getAppFn.constLevels! - let α := type.appFn!.appArg! - let β := type.appArg! - assert! β.isLambda - let type := β.bindingBody!.instantiate1 arg - let rest ← go (i+1) type - return mkApp4 (mkConst ``PSigma.mk us) α β arg rest - else - return args[i]! - -/-- Unpacks a unary packed argument created with `mkUnaryArg`. -/ -def unpackUnaryArg {m} [Monad m] [MonadError m] (arity : Nat) (e : Expr) : m (Array Expr) := do - let mut e := e - let mut args := #[] - while args.size + 1 < arity do - if e.isAppOfArity ``PSigma.mk 4 then - args := args.push (e.getArg! 2) - e := e.getArg! 3 - else - throwError "Unexpected expression while unpacking n-ary argument" - args := args.push e - return args - -private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Expr) (value : Expr) : MetaM Expr := do - let mvar ← mkFreshExprSyntheticOpaqueMVar codomain - let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do - if ys.size < xs.size - 1 then - let xDecl ← xs[ys.size]!.fvarId!.getDecl - let xDecl' ← xs[ys.size + 1]!.fvarId!.getDecl - let #[s] ← mvarId.cases y #[{ varNames := [xDecl.userName, xDecl'.userName] }] | unreachable! - go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!) - else - let ys := ys.push (mkFVar y) - mvarId.assign (value.replaceFVars xs ys) - go mvar.mvarId! y.fvarId! #[] - instantiateMVars mvar - -/-- - Convert the given pre-definitions into unary functions. - We "pack" the arguments using `PSigma`. --/ -partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := do - let mut preDefsNew := #[] - let mut arities := #[] - let mut modified := false - for preDef in preDefs do - let (preDefNew, arity, modifiedCurr) ← lambdaTelescope preDef.value fun xs _ => do - if xs.size == fixedPrefix then - throwError "well-founded recursion cannot be used, '{preDef.declName}' does not take any (non-fixed) arguments" - let arity := xs.size - if arity > fixedPrefix + 1 then - let bodyType ← instantiateForall preDef.type xs - let mut d ← inferType xs.back - let ys : Array Expr := xs[:fixedPrefix] - let xs : Array Expr := xs[fixedPrefix:] - for x in xs.pop.reverse do - d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)] - withLocalDeclD (← mkFreshUserName `_x) d fun tuple => do - let elems := mkTupleElems tuple xs.size - let codomain := bodyType.replaceFVars xs elems - let preDefNew:= { preDef with - declName := preDef.declName ++ `_unary - type := (← mkForallFVars (ys.push tuple) codomain) - } - addAsAxiom preDefNew - return (preDefNew, arity, true) - else - return (preDef, arity, false) - modified := modified || modifiedCurr - arities := arities.push arity - preDefsNew := preDefsNew.push preDefNew - if !modified then - return preDefs - -- Update values - for i in [:preDefs.size] do - let preDef := preDefs[i]! - let preDefNew := preDefsNew[i]! - let valueNew ← lambdaTelescope preDef.value fun xs body => do - let ys : Array Expr := xs[:fixedPrefix] - let xs : Array Expr := xs[fixedPrefix:] - let type ← instantiateForall preDefNew.type ys - forallBoundedTelescope type (some 1) fun z codomain => do - let z := z[0]! - let newBody ← mkPSigmaCasesOn z codomain xs body - mkLambdaFVars (ys.push z) (← packApplications newBody arities preDefsNew) - let isBad (e : Expr) : Bool := - match isAppOfPreDef? e with - | none => false - | some i => e.getAppNumArgs > fixedPrefix + 1 || preDefsNew[i]!.declName != preDefs[i]!.declName - if let some bad := valueNew.find? isBad then - if let some i := isAppOfPreDef? bad then - throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i]!.declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]!}" - preDefsNew := preDefsNew.set! i { preDefNew with value := valueNew } - return preDefsNew -where - /-- Return `some i` if `e` is a `preDefs[i]` application -/ - isAppOfPreDef? (e : Expr) : Option Nat := do - let f := e.getAppFn - guard f.isConst - preDefs.findIdx? (·.declName == f.constName!) - - packApplications (e : Expr) (arities : Array Nat) (preDefsNew : Array PreDefinition) : MetaM Expr := do - let pack (e : Expr) (funIdx : Nat) : MetaM Expr := do - let f := e.getAppFn - let args := e.getAppArgs - let fNew := mkConst preDefsNew[funIdx]!.declName f.constLevels! - let fNew := mkAppN fNew args[:fixedPrefix] - let Expr.forallE _ d .. ← whnf (← inferType fNew) | unreachable! - -- NB: Use whnf in case the type is not a manifest forall, but a definition around it - let argNew ← mkUnaryArg d args[fixedPrefix:] - return mkApp fNew argNew - let rec - visit (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := do - checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do - match e with - | Expr.lam n d b c => - withLocalDecl n c (← visit d) fun x => do - mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) - | Expr.forallE n d b c => - withLocalDecl n c (← visit d) fun x => do - mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) - | Expr.letE n t v b _ => - withLetDecl n (← visit t) (← visit v) fun x => do - mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) - | Expr.proj n i s .. => return mkProj n i (← visit s) - | Expr.mdata d b => return mkMData d (← visit b) - | Expr.app .. => visitApp e - | Expr.const .. => visitApp e - | e => return e, - visitApp (e : Expr) : MonadCacheT ExprStructEq Expr MetaM Expr := e.withApp fun f args => do - let args ← args.mapM visit - if let some funIdx := isAppOfPreDef? f then - let numArgs := args.size - let arity := arities[funIdx]! - if numArgs < arity then - -- Partial application - let extra := arity - numArgs - withDefault do forallBoundedTelescope (← inferType e) extra fun xs _ => do - if xs.size != extra then - return (mkAppN f args) -- It will fail later - else - mkLambdaFVars xs (← pack (mkAppN (mkAppN f args) xs) funIdx) - else if numArgs > arity then - -- Over application - let r ← pack (mkAppN f args[:arity]) funIdx - let rType ← inferType r - -- Make sure the new auxiliary definition has only one argument. - withLetDecl (← mkFreshUserName `aux) rType r fun aux => - mkLetFVars #[aux] (mkAppN aux args[arity:]) - else - pack (mkAppN f args) funIdx - else if args.isEmpty then - return f - else - return mkAppN (← visit f) args - visit e |>.run - -end Lean.Elab.WF diff --git a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean index 1f34fe3883..6381664254 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackMutual.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackMutual.lean @@ -4,93 +4,28 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Meta.Tactic.Cases +import Lean.Meta.ArgsPacker import Lean.Elab.PreDefinition.Basic -import Lean.Elab.PreDefinition.WF.PackDomain namespace Lean.Elab.WF open Meta -/-- Combine different function domains `ds` using `PSum`s -/ -private def mkNewDomain (ds : Array Expr) : MetaM Expr := do - let mut r := ds.back - for d in ds.pop.reverse do - r ← mkAppM ``PSum #[d, r] - return r - -private def getCodomainLevel (preDefType : Expr) : MetaM Level := - forallBoundedTelescope preDefType (some 1) fun _ body => getLevel body /-- - Return the universe level for the codomain of the given definitions. - This method produces an error if the codomains are in different universe levels. +Checks that all codomians have the same level, throws an error otherwise. -/ -private def getCodomainsLevel (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) : MetaM Level := do - let r ← getCodomainLevel preDefTypes[0]! - for i in [1:preDefTypes.size] do - let preDef := preDefTypes[i]! - unless (← isLevelDefEq r (← getCodomainLevel preDef)) do - let arity₀ ← lambdaTelescope preDefsOriginal[0]!.value fun xs _ => return xs.size - let arityᵢ ← lambdaTelescope preDefsOriginal[i]!.value fun xs _ => return xs.size - forallBoundedTelescope preDefsOriginal[0]!.type arity₀ fun _ type₀ => - forallBoundedTelescope preDefsOriginal[i]!.type arityᵢ fun _ typeᵢ => +private def checkCodomainsLevel (fixedPrefixSize : Nat) (arities : Array Nat) + (preDefs : Array PreDefinition) : MetaM Unit := do + forallBoundedTelescope preDefs[0]!.type (fixedPrefixSize + arities[0]!) fun _ type₀ => do + let u₀ ← getLevel type₀ + for i in [1:preDefs.size] do + forallBoundedTelescope preDefs[i]!.type (fixedPrefixSize + arities[i]!) fun _ typeᵢ => + unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do withOptions (fun o => pp.sanitizeNames.set o false) do - throwError "invalid mutual definition, result types must be in the same universe level, resulting type for `{preDefsOriginal[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\nand for `{preDefsOriginal[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}" - return r - -/-- - Create the codomain for the new function that "combines" different `preDef` types - See: `packMutual` --/ -private partial def mkNewCoDomain (preDefsOriginal : Array PreDefinition) (preDefTypes : Array Expr) (x : Expr) : MetaM Expr := do - let u ← getCodomainsLevel preDefsOriginal preDefTypes - let rec go (x : Expr) (i : Nat) : MetaM Expr := do - if i < preDefTypes.size - 1 then - let xType ← whnfD (← inferType x) - assert! xType.isAppOfArity ``PSum 2 - let xTypeArgs := xType.getAppArgs - let casesOn := mkConst (mkCasesOnName ``PSum) (mkLevelSucc u :: xType.getAppFn.constLevels!) - let casesOn := mkAppN casesOn xTypeArgs -- parameters - let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive - let casesOn := mkApp casesOn x -- major - let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x => do - mkLambdaFVars #[x] ((← whnf preDefTypes[i]!).bindingBody!.instantiate1 x) - let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1]! fun x => do - mkLambdaFVars #[x] (← go x (i+1)) - return mkApp2 casesOn minor1 minor2 - else - return (← whnf preDefTypes[i]!).bindingBody!.instantiate1 x - go x 0 - -/-- - Combine/pack the values of the different definitions in a single value - `x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`. - See: `packMutual`. - Remark: this method does not replace the nested recursive `preDefValues` applications. - This step is performed by `transform` with the following `post` method. - -/ -private partial def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do - let varNames := preDefValues.map fun val => - assert! val.isLambda - val.bindingName! - let mvar ← mkFreshExprSyntheticOpaqueMVar codomain - let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do - if i < preDefValues.size - 1 then - /- - Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions). - -/ - let givenNames : Array AltVarNames := - if i == preDefValues.size - 2 then - #[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }] - else - #[{ varNames := [varNames[i]!] }] - let #[s₁, s₂] ← mvarId.cases x (givenNames := givenNames) | unreachable! - s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta - go s₂.mvarId s₂.fields[0]!.fvarId! (i+1) - else - mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta - go mvar.mvarId! x.fvarId! 0 - instantiateMVars mvar + throwError m!"invalid mutual definition, result types must be in the same universe " ++ + m!"level, resulting type " ++ + m!"for `{preDefs[0]!.declName}` is{indentExpr type₀} : {← inferType type₀}\n" ++ + m!"and for `{preDefs[i]!.declName}` is{indentExpr typeᵢ} : {← inferType typeᵢ}" /-- Pass the first `n` arguments of `e` to the continuation, and apply the result to the @@ -112,141 +47,54 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr : mkLambdaFVars xs e' /-- -If `arg` is the argument to the `fidx`th of the `numFuncs` in the recursive group, -then `mkMutualArg` packs that argument in `PSum.inl` and `PSum.inr` constructors -to create the mutual-packed argument of type `domain`. +A `post` for `Meta.transform` to replace recursive calls to the original `preDefs` with calls +to the new unary function `newfn`. -/ -partial def mkMutualArg (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr := do - let rec go (i : Nat) (type : Expr) : MetaM Expr := do - if i == numFuncs - 1 then - return arg - else - (← whnfD type).withApp fun f args => do - assert! args.size == 2 - if i == fidx then - return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg - else - let r ← go (i+1) args[1]! - return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r - go 0 domain - -/-- -Unpacks a mutually packed argument, returning the argument and function index. -Inverse of `mkMutualArg`. Cf. `unpackUnaryArg` and `unpackArg`, which does both --/ -def unpackMutualArg {m} [Monad m] [MonadError m] (numFuncs : Nat) (e : Expr) : m (Nat × Expr) := do - let mut funidx := 0 - let mut e := e - while funidx + 1 < numFuncs do - if e.isAppOfArity ``PSum.inr 3 then - e := e.getArg! 2 - funidx := funidx + 1 - else if e.isAppOfArity ``PSum.inl 3 then - e := e.getArg! 2 - break - else - throwError "Unexpected expression while unpacking mutual argument" - return (funidx, e) - -/-- -Given the packed argument of a (possibly) mutual and (possibly) nary call, -return the function index that is called and the arguments individually. - -We expect precisely the expressions produced by `packMutual`, with manifest -`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart -rather than using projectinos. --/ -def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) : - m (Nat × Array Expr) := do - let (funidx, e) ← unpackMutualArg arities.size e - let args ← unpackUnaryArg arities[funidx]! e - return (funidx, args) - - -/-- -Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`. -See: `packMutual` --/ -private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do +private partial def post (fixedPrefix : Nat) (argsPacker : ArgsPacker) (funNames : Array Name) + (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do let f := e.getAppFn if !f.isConst then return TransformStep.done e let declName := f.constName! let us := f.constLevels! - if let some fidx := preDefs.findIdx? (·.declName == declName) then - let e' ← withAppN (fixedPrefix + 1) e fun args => do + if let some fidx := funNames.getIdx? declName then + let arity := fixedPrefix + argsPacker.varNamess[fidx]!.size + let e' ← withAppN arity e fun args => do let fixedArgs := args[:fixedPrefix] - let arg := args[fixedPrefix]! - let packedArg ← mkMutualArg preDefs.size domain fidx arg + let packedArg ← argsPacker.pack domain fidx args[fixedPrefix:] return mkApp (mkAppN (mkConst newFn us) fixedArgs) packedArg return TransformStep.done e' return TransformStep.done e -partial def withFixedPrefix (fixedPrefix : Nat) (preDefs : Array PreDefinition) (k : Array Expr → Array Expr → Array Expr → MetaM α) : MetaM α := - go fixedPrefix #[] (preDefs.map (·.value)) -where - go (i : Nat) (fvars : Array Expr) (vals : Array Expr) : MetaM α := do - match i with - | 0 => k fvars (← preDefs.mapM fun preDef => instantiateForall preDef.type fvars) vals - | i+1 => - withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x => - go i (fvars.push x) (vals.map fun val => val.bindingBody!.instantiate1 x) - /-- - If `preDefs.size > 1`, combine different functions in a single one using `PSum`. - This method assumes all `preDefs` have arity 1, and have already been processed using `packDomain`. - Here is a small example. Suppose the input is - ``` - f x := - match x.2.1, x.2.2.1, x.2.2.2 with - | 0, a, b => a - | Nat.succ n, a, b => (g ⟨x.1, n, a, b⟩).fst - g x := - match x.2.1, x.2.2.1, x.2.2.2 with - | 0, a, b => (a, b) - | Nat.succ n, a, b => (h ⟨x.1, n, a, b⟩, a) - h x => - match x.2.1, x.2.2.1, x.2.2.2 with - | 0, a, b => b - | Nat.succ n, a, b => f ⟨x.1, n, a, b⟩ - ``` - this method produces the following pre definition - ``` - f._mutual x := - PSum.casesOn x - (fun val => - match val.2.1, val.2.2.1, val.2.2.2 with - | 0, a, b => a - | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inl ⟨val.1, n, a, b⟩))).fst - fun val => - PSum.casesOn val - (fun val => - match val.2.1, val.2.2.1, val.2.2.2 with - | 0, a, b => (a, b) - | Nat.succ n, a, b => (f._mutual (PSum.inr (PSum.inr ⟨val.1, n, a, b⟩)), a) - fun val => - match val.2.1, val.2.2.1, val.2.2.2 with - | 0, a, b => b - | Nat.succ n, a, b => - f._mutual (PSum.inl ⟨val.1, n, a, b⟩) - ``` +Creates a single unary function from the given `preDefs`, using the machinery in the `ArgPacker` +module. +-/ +def packMutual (fixedPrefix : Nat) (argsPacker : ArgsPacker) (preDefs : Array PreDefinition) : MetaM PreDefinition := do + let arities := argsPacker.arities + if let #[1] := arities then return preDefs[0]! + let newFn := if argsPacker.numFuncs > 1 then preDefs[0]!.declName ++ `_mutual + else preDefs[0]!.declName ++ `_unary - Remark: `preDefsOriginal` is used for error reporting, it contains the definitions before applying `packDomain`. - -/ -def packMutual (fixedPrefix : Nat) (preDefsOriginal : Array PreDefinition) (preDefs : Array PreDefinition) : MetaM PreDefinition := do - if preDefs.size == 1 then return preDefs[0]! - withFixedPrefix fixedPrefix preDefs fun ys types vals => do - let domains ← types.mapM fun type => do pure (← whnf type).bindingDomain! - let domain ← mkNewDomain domains - withLocalDeclD (← mkFreshUserName `_x) domain fun x => do - let codomain ← mkNewCoDomain preDefsOriginal types x - let type ← mkForallFVars (ys.push x) codomain - let value ← packValues x codomain vals - let newFn := preDefs[0]!.declName ++ `_mutual - let preDefNew := { preDefs[0]! with declName := newFn, type, value } - addAsAxiom preDefNew - let value ← transform value (skipConstInApp := true) (post := post fixedPrefix preDefs domain newFn) - let value ← mkLambdaFVars (ys.push x) value - return { preDefNew with value } + checkCodomainsLevel fixedPrefix argsPacker.arities preDefs + -- Bring the fixed Prefix into scope + forallBoundedTelescope preDefs[0]!.type (some fixedPrefix) fun ys _ => do + let types ← preDefs.mapM (instantiateForall ·.type ys) + let vals ← preDefs.mapM (instantiateLambda ·.value ys) + + let type ← argsPacker.uncurryType types + let packedDomain := type.bindingDomain! + + -- Temporarily add the unary function as an axiom, so that all expressions + -- are still type correct + let type ← mkForallFVars ys type + let preDefNew := { preDefs[0]! with declName := newFn, type } + addAsAxiom preDefNew + + let value ← argsPacker.uncurry vals + let value ← transform value (skipConstInApp := true) + (post := post fixedPrefix argsPacker (preDefs.map (·.declName)) packedDomain newFn) + let value ← mkLambdaFVars ys value + return { preDefNew with value } end Lean.Elab.WF diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index bcccb54951..9fdf612b2b 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -657,6 +657,27 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do else mkAppM ``Iff.of_eq #[h] +/-- +Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`. +If `n = 0` returns a proof of `True`. +If `n = 1` returns the proof of `P₁`. +-/ +def mkAndIntroN : Array Expr → MetaM Expr +| #[] => return mkConst ``True.intro [] +| #[e] => return e +| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back + + +/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/ +def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do + let mut value := e + for _ in [:i] do + value := mkProj ``And 1 value + if i + 1 < n then + value := mkProj ``And 0 value + return value + + builtin_initialize do registerTraceClass `Meta.appBuilder registerTraceClass `Meta.appBuilder.result (inherited := true) diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean new file mode 100644 index 0000000000..61a4c4d555 --- /dev/null +++ b/src/Lean/Meta/ArgsPacker.lean @@ -0,0 +1,572 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude +import Lean.Meta.AppBuilder +import Lean.Meta.ArgsPacker.Basic + +/-! +This module implements the equivalence between the types +``` +(x : a) → (y : b) → r1[x,y], (x : c) → (y : d) → r2[x,y] +``` +(the “curried form”) and +``` +(p : (a ⊗' b) ⊕' (c ⊗' d)) → r'[p] +``` +where +``` +r'[p] = match p with | inl (x,y) => r1[x,y] | inr (x,y) => r2[x,y] +``` +(the “packed form”). + +The `ArgsPacker` data structure (defined in `Lean.Meta.ArgsPacker.Basic` for fewer module +dependencies) contains necessary information to pack and unpack reliably. Care is taken that the +code is not confused even if the user intentionally uses a `PSigma` or `PSum` type, e.g. as the +ast parameter. Additionaly, “good” variable names are stored here. + +It is used in the transation of a possibly mutual, possibly n-ary recursive function to a single +unary function, which can then be made non-recursive using `WellFounded.fix`. Additional users are +the `GuessLex` and `FunInd` modules, which also have to deal with this encoding. + +Ideally, only this module has to know the precise encoding using `PSigma` and `PSigma`; all other +modules should only use the high-level functions at the bottom of this file. At the same time, +this module should be independent of WF-specific data structures (like `EqnInfos`). + +The subnamespaces `Unary` and `Mutual` take care of `PSigma` resp. `PSum` packing, and are +intended to be local to this module. +-/ + +namespace Lean.Meta.ArgsPacker + +open Lean Meta + +namespace Unary + +/-! +Helpers for iterated `PSigma`. +-/ + +/- +Given a telescope of FVars of type `tᵢ`, iterates `PSigma` to produce the type +`t₁ ⊗' t₂ …`. +-/ +def packType (xs : Array Expr) : MetaM Expr := do + let mut d ← inferType xs.back + for x in xs.pop.reverse do + d ← mkAppOptM ``PSigma #[some (← inferType x), some (← mkLambdaFVars #[x] d)] + return d + + +/-- +Create a unary application by packing the given arguments using `PSigma.mk`. +The `type` should be the the expected type of the packed argument, as created with `packType`. +-/ +partial def pack (type : Expr) (args : Array Expr) : Expr := go 0 type +where + go (i : Nat) (type : Expr) : Expr := + if i < args.size - 1 then + let arg := args[i]! + assert! type.isAppOfArity ``PSigma 2 + let us := type.getAppFn.constLevels! + let α := type.appFn!.appArg! + let β := type.appArg! + assert! β.isLambda + let type := β.bindingBody!.instantiate1 arg + let rest := go (i+1) type + mkApp4 (mkConst ``PSigma.mk us) α β arg rest + else + args[i]! + +/-- +Unpacks a unary packed argument created with `Unary.pack`. + +Throws an error if the expression is not of that form. +-/ +def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do + let mut e := e + let mut args := #[] + while args.size + 1 < arity do + if e.isAppOfArity ``PSigma.mk 4 then + args := args.push (e.getArg! 2) + e := e.getArg! 3 + else + throwError "Unexpected expression while unpacking n-ary argument" + args := args.push e + return args + + +/-- + Given a (dependent) tuple `t` (using `PSigma`) of the given arity. + Return an array containing its "elements". + Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`. + -/ +private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do + let mut result := #[] + let mut t := t + for _ in [:arity - 1] do + result := result.push (mkProj ``PSigma 0 t) + t := mkProj ``PSigma 1 t + result.push t + +/-- +Given a type `t` of the form `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z]` +returns the curried type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`. +-/ +def uncurryType (varNames : Array Name) (type : Expr) : MetaM Expr := do + forallBoundedTelescope type varNames.size fun xs _ => do + assert! xs.size = varNames.size + let d ← packType xs + let name := if xs.size == 1 then varNames[0]! else `_x + withLocalDeclD name d fun tuple => do + let elems := mkTupleElems tuple xs.size + let codomain ← instantiateForall type elems + mkForallFVars #[tuple] codomain + +/-- +Iterated `PSigma.casesOn`: +Given `e : a ⊗' b ⊗' …` (where `e` is `FVarId`), a type `codomain[e]` of level `u`, and +`alt : (x : a) → (y : b) → … → codomain`, uses `PSigma.casesOn` to invoke `alt` on `e`. +-/ +private def casesOn (varNames : List Name) (e : Expr) (u : Level) (codomain : Expr) (alt : Expr) : MetaM Expr := do + match varNames with + | [] => return alt + | [_] => return alt.beta #[e] + | n :: m :: ns => do + let t ← inferType e + match_expr t with + | PSigma a b => + let us := t.getAppFn.constLevels! + let motive ← mkLambdaFVars #[e] codomain + let alt ← + withLocalDeclD n a fun x => do + withLocalDeclD m (b.beta #[x]) fun y => do + let codomain' := motive.beta #[mkApp4 (.const ``PSigma.mk us) a b x y] + mkLambdaFVars #[x,y] (← casesOn (m :: ns) y u codomain' (alt.beta #[x])) + return mkApp5 (.const ``PSigma.casesOn (u :: us)) a b motive e alt + | _ => throwError "ArgsPacker.Binary.casesOn: Expected PSigma type, got {t}" + +/-- +Given expression `e` of type `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z]` +returns an expression of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`. +-/ +def uncurry (varNames : Array Name) (e : Expr) : MetaM Expr := do + let type ← inferType e + let resultType ← uncurryType varNames type + forallBoundedTelescope resultType (some 1) fun xs codomain => do + let #[x] := xs | unreachable! + let u ← getLevel codomain + let value ← casesOn varNames.toList x u codomain e + mkLambdaFVars #[x] value + +/-- Given `(A ⊗' B ⊗' … ⊗' D) → R` (non-dependent) `R`, return `A → B → … → D → R` -/ +private def curryType (varNames : Array Name) (type : Expr) : + MetaM Expr := do + let some (domain, codomain) := type.arrow? | + throwError "curryType: Expected arrow type, got {type}" + go codomain varNames.toList domain + where + go (codomain : Expr) : List Name → Expr → MetaM Expr + | [], _ => pure codomain + | [_], domain => mkArrow domain codomain + | n::ns, domain => + match_expr domain with + | PSigma a b => + withLocalDecl n .default a fun x => do + mkForallFVars #[x] (← go codomain ns (b.beta #[x])) + | _ => throwError "curryType: Expected PSigma type, got {domain}" + +/-- +Given expression `e` of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]` +return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]` +-/ +private partial def curry (varNames : Array Name) (e : Expr) : MetaM Expr := do + let type ← whnfForall (← inferType e) + unless type.isForall do + throwError "curryPSigma: expected forall type, got {type}" + let packedDomain := type.bindingDomain! + go packedDomain packedDomain #[] varNames.toList +where + go (packedDomain domain : Expr) args : List Name → MetaM Expr + | [] => do + let packedArg := Unary.pack packedDomain args + return e.beta #[packedArg] + | [n] => do + withLocalDecl n .default domain fun x => do + let dummy := Expr.const ``Unit [] + mkLambdaFVars #[x] (← go packedDomain dummy (args.push x) []) + | n :: ns => + match_expr domain with + | PSigma a b => + withLocalDecl n .default a fun x => do + mkLambdaFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x) ns) + | _ => throwError "curryPSigma: Expected PSigma type, got {domain}" + + +end Unary + +namespace Mutual + +/-! +Helpers for iterated `PSum`. +-/ + +/-- Given types `#[t₁, t₂,…]`, returns the type `t₁ ⊕' t₂ …`. -/ +def packType (ds : Array Expr) : MetaM Expr := do + let mut r := ds.back + for d in ds.pop.reverse do + r ← mkAppM ``PSum #[d, r] + return r + +/-- Given type `A ⊕' B ⊕' … ⊕' D`, return `[A, B, …, D]` -/ +private def unpackType (n : Nat) (type : Expr) : MetaM (List Expr) := + match n with + | 0 => pure [] + | 1 => pure [type] + | n+1 => + match_expr type with + | PSum a b => return a :: (← unpackType n b) + | _ => throwError "Mutual.unpackType: Expected PSum type, got {type}" + +/-- +If `arg` is the argument to the `fidx`th of the `argsPacker.numFuncs` in the recursive group, +then `mk` packs that argument in `PSum.inl` and `PSum.inr` constructors +to create the mutual-packed argument of type `domain`. +-/ +def pack (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr := do + let rec go (i : Nat) (type : Expr) : MetaM Expr := do + if i >= numFuncs - 1 then + return arg + else + (← whnfD type).withApp fun f args => do + assert! args.size == 2 + if i == fidx then + return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg + else + let r ← go (i+1) args[1]! + return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r + termination_by numFuncs - 1 - i + go 0 domain + +/-- +Unpacks a mutually packed argument created with `Mutual.mk` returning the +argument and function index. + +Throws an error if the expression is not of that form. +-/ +def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do + let mut funidx := 0 + let mut e := expr + while funidx + 1 < numFuncs do + if e.isAppOfArity ``PSum.inr 3 then + e := e.getArg! 2 + funidx := funidx + 1 + else if e.isAppOfArity ``PSum.inl 3 then + e := e.getArg! 2 + break + else + throwError "Unexpected expression while unpacking mutual argument:{indentExpr expr}" + return (funidx, e) + + +/-- +Given unary types `(x : Aᵢ) → Rᵢ[x]`, and `(x : A₁ ⊕ A₂ …)`, calculate the packed codomain +``` +match x with | inl x₁ => R₁[x₁] | inr x₂ => R₂[x₂] | … +``` +This function assumes (and does not check) that `Rᵢ` all have the same level. +-/ +def mkCodomain (types : Array Expr) (x : Expr) : MetaM Expr := do + let u ← forallBoundedTelescope types[0]! (some 1) fun _ body => getLevel body + let rec go (x : Expr) (i : Nat) : MetaM Expr := do + if i < types.size - 1 then + let xType ← whnfD (← inferType x) + assert! xType.isAppOfArity ``PSum 2 + let xTypeArgs := xType.getAppArgs + let casesOn := mkConst ``PSum.casesOn (mkLevelSucc u :: xType.getAppFn.constLevels!) + let casesOn := mkAppN casesOn xTypeArgs -- parameters + let casesOn := mkApp casesOn (← mkLambdaFVars #[x] (mkSort u)) -- motive + let casesOn := mkApp casesOn x -- major + let minor1 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[0]! fun x => do + mkLambdaFVars #[x] (types[i]!.bindingBody!.instantiate1 x) + let minor2 ← withLocalDeclD (← mkFreshUserName `_x) xTypeArgs[1]! fun x => do + mkLambdaFVars #[x] (← go x (i+1)) + return mkApp2 casesOn minor1 minor2 + else + return types[i]!.bindingBody!.instantiate1 x + termination_by types.size - 1 - i + go x 0 + +/- +Given types `(x : A) → R₁[x]` and `(z : B) → R₂[z]`, returns the type +``` +(x : A ⊕' B) → (match x with | .inl x => R₁[x] | .inr R₂[z] +``` +if the codomains are dependent, or +``` +(x : A ⊕' B) → R +``` +if they are all the same. + +-/ +def uncurryType (types : Array Expr) : MetaM Expr := do + let types ← types.mapM whnfForall + types.forM fun type => do + unless type.isForall do + throwError "Mutual.uncurryType: Expected forall type, got {type}" + let domain ← packType (types.map (·.bindingDomain!)) + withLocalDeclD `x domain fun x => do + let codomain ← Mutual.mkCodomain types x + mkForallFVars #[x] codomain + +/- +Given types `(x : A) → R` and `(z : B) → R`, returns the type +``` +(x : A ⊕' B) → R +``` +-/ +def uncurryTypeND (types : Array Expr) : MetaM Expr := do + let types ← types.mapM whnfForall + types.forM fun type => + unless type.isArrow do + throwError "Mutual.uncurryTypeND: Expected non-dependent types, got {type}" + let codomains := types.map (·.bindingBody!) + let t' := codomains.back + codomains.pop.forM fun t => + unless ← isDefEq t t' do + throwError "Mutual.uncurryTypeND: Expected equal codomains, but got {t} and {t'}" + let codomain := codomains[0]! + let domain ← packType (types.map (·.bindingDomain!)) + mkArrow domain codomain + +/- +Iterated `PSum.casesOn`: +Given a value `(x : A ⊕ C)` (which must be a FVar) and functions +`alt₁ : (a : A) → codomain[inl a]` and `alt₂ : (b : B) → codomain[inr b]`, +matches on `x` to apply the right `alt` to produce a value of `codomain[x]`. + +Uses the variable name from the lambda in `altᵢ`, if present. +-/ +private def casesOn (x : Expr) (codomain : Expr) (alts : List Expr) : MetaM Expr := do + match alts with + | [] => throwError "Mutual.casesOn: no alternatives" + | [alt] => return alt.beta #[x] + | alt₁ :: alts => do + let t ← inferType x + match_expr t with + | PSum a b => + let u ← getLevel codomain + let us := t.getAppFn.constLevels! + let motive ← mkLambdaFVars #[x] codomain + let alt₂ ← + if let [alt] := alts then pure alt else + withLocalDeclD (← mkFreshUserName `_x) b fun y => do + let codomain' := motive.beta #[mkApp3 (.const ``PSum.inr us) a b y] + mkLambdaFVars #[y] (← casesOn y codomain' alts) + return mkApp6 (.const ``PSum.casesOn (u::us)) a b motive x alt₁ alt₂ + | _ => throwError "Mutual.casesOn: Expected PSum type, got {t}" + +/-- +Given unary expressions `e₁`, `e₂` with types `(x : A) → R₁[x]` +and `(z : C) → R₂[z]`, returns an expression of type +``` +(x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z]) +``` +-/ +def uncurry (es : Array Expr) : MetaM Expr := do + let types ← es.mapM inferType + let resultType ← uncurryType types + forallBoundedTelescope resultType (some 1) fun xs codomain => do + let #[x] := xs | unreachable! + let value ← casesOn x codomain es.toList + mkLambdaFVars #[x] value + +/-- +Given unary expressions `e₁`, `e₂` with types `(x : A) → R` +and `(z : C) → R`, returns an expression of type +``` +(x : A ⊕' C) → R +``` +-/ +def uncurryND (es : Array Expr) : MetaM Expr := do + let types ← es.mapM inferType + let resultType ← uncurryTypeND types + forallBoundedTelescope resultType (some 1) fun xs codomain => do + let #[x] := xs | unreachable! + let value ← casesOn x codomain es.toList + mkLambdaFVars #[x] value + +/- +Given type `(A ⊕' C) → R` (non-depenent), return types +``` +#[A → R, B → R] +``` +-/ +def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do + let some (domain, codomain) := type.arrow? | + throwError "curryType: Expected arrow type, got {type}" + let ds ← unpackType n domain + ds.toArray.mapM (fun d => mkArrow d codomain) + +end Mutual + +-- Now for the main definitions in this moduleo + +/-- The number of functions being packed -/ +def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size + +/-- The arities of the functions being packed -/ +def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size) + +def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr) + : MetaM Expr := do + assert! fidx < argsPacker.numFuncs + assert! args.size == argsPacker.varNamess[fidx]!.size + let types ← Mutual.unpackType argsPacker.numFuncs domain + let type := types[fidx]! + Mutual.pack argsPacker.numFuncs domain fidx (Unary.pack type args) + +/-- +Given the packed argument of a (possibly) mutual and (possibly) nary call, +return the function index that is called and the arguments individually. + +We expect precisely the expressions produced by `pack`, with manifest +`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart +rather than using projectinos. +-/ +def unpack (argsPacker : ArgsPacker) (e : Expr) : MetaM (Nat × Array Expr) := do + let (funidx, e) ← Mutual.unpack argsPacker.numFuncs e + let args ← Unary.unpack argsPacker.varNamess[funidx]!.size e + return (funidx, args) + + +/-- +Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type +``` +(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z] +``` +-/ +def uncurryType (argsPacker : ArgsPacker) (types : Array Expr) : MetaM Expr := do + let unary ← (Array.zipWith argsPacker.varNamess types Unary.uncurryType).mapM id + Mutual.uncurryType unary + +/-- +Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R₁[x,y]` +and `(z : C) → R₂[z]`, returns an expression of type +``` +(x : (A ⊗ B) ⊕ C) → (match x with | .inl (x, y) => R₁[x,y] | .inr R₂[z] +``` +-/ +def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do + let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id + Mutual.uncurry unary + +/-- +Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R` +and `(z : C) → R`, returns an expression of type +``` +(x : (A ⊗ B) ⊕ C) → R +``` +-/ +def uncurryND (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do + let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id + Mutual.uncurryND unary + +/-- +Given expression `e` of type `(x : a₁ ⊗' b₁ ⊕' a₂ ⊗' d₂ …) → e[x]`, uncurries the expression and +projects to the `i`th function of type, +``` +((x : aᵢ) → (y : bᵢ) → e[.inr….inl (x,y)]) +``` +-/ +def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do + let n := argsPacker.numFuncs + let packedDomain := (← inferType e).bindingDomain! + let unaryTypes ← Mutual.unpackType n packedDomain + unless i < unaryTypes.length do + throwError "curryProj: index out of range" + let unaryType := unaryTypes[i]! + -- unary : (x : a ⊗ b) → e[inl x] + let unary ← withLocalDecl `x .default unaryType fun x => do + let packedArg ← Mutual.pack unaryTypes.length packedDomain i x + mkLambdaFVars #[x] (e.beta #[packedArg]) + -- nary : (x : a) → (y : b) → e[inl (x,y)] + Unary.curry argsPacker.varNamess[i]! unary + + +/-- +Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (non-dependent), return types +``` +#[(x: a) → (y : b) → R, (x : c) → (y : d) → R] +``` +-/ +def curryType (argsPacker : ArgsPacker) (t : Expr) : MetaM (Array Expr) := do + let unary ← Mutual.curryType argsPacker.numFuncs t + (Array.zipWith argsPacker.varNamess unary Unary.curryType).mapM id + +/-- +Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression +to produce an expression of the isomorphic type +``` +((x: a) → (y : b) → e[.inl (x,y)]) ∧ ((x : c) → (y : d) → e[.inr (x,y)]) +``` +-/ +def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do + let mut es := #[] + for i in [:argsPacker.numFuncs] do + es := es.push (← argsPacker.curryProj e i) + mkAndIntroN es + +/-- +Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e` +into scope as fresh local declarations and passes their FVars to the continuation `k`. +The `name` is used to form the variable names; uses `name1`, `name2`, … if there are multiple. +-/ +private def withCurriedDecl {α} (argsPacker : ArgsPacker) (name : Name) (type : Expr) + (k : Array Expr → MetaM α) : MetaM α := do + go (← argsPacker.curryType type).toList #[] +where + go : List Expr → Array Expr → MetaM α + | [], acc => k acc + | t::ts, acc => do + let name := if argsPacker.numFuncs = 1 then name else s!"{name}{acc.size+1}" + withLocalDecl name .default t fun x => do + go ts (acc.push x) + +/-- +Given `value : type` where `type` is +``` +(m : a ⊗' b ⊕' c ⊗' d → s) → r[m] +``` +brings `m1 : a → b → s` and `m2 : c → d → s` into scope. The continuation receives + + * FVars for `m1`… + * `e[m]` + * `t[m]` + +where `m : a ⊗' b ⊕' c ⊗' d → s` is the uncurried form of `m1` and `m2`. + +The variable names `m1` and `m2` are taken from the paramter name in `t`, with numbers added +unless `numFuns = 1` +-/ +def curryParam {α} (argsPacker : ArgsPacker) (value : Expr) (type : Expr) + (k : Array Expr → Expr → Expr → MetaM α) : MetaM α := do + unless type.isForall do + throwError "uncurryParam: expected forall, got {type}" + let packedMotiveType := type.bindingDomain! + unless packedMotiveType.isArrow do + throwError "uncurryParam: unexpected packed motive {packedMotiveType}" + -- Bring unpacked motives (motive1 : a → b → Prop and motive2 : c → d → Prop) into scope + withCurriedDecl argsPacker type.bindingName! packedMotiveType fun motives => do + -- Combine them into a packed motive (motive : a ⊗' b ⊕' c ⊗' d → Prop), and use that + let motive ← argsPacker.uncurryND motives + let type ← instantiateForall type #[motive] + let value := mkApp value motive + k motives value type + + + +end Lean.Meta.ArgsPacker diff --git a/src/Lean/Meta/ArgsPacker/Basic.lean b/src/Lean/Meta/ArgsPacker/Basic.lean new file mode 100644 index 0000000000..a3d451525a --- /dev/null +++ b/src/Lean/Meta/ArgsPacker/Basic.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude +import Init.Data.Array.Basic + +/-! +The basic data type and namespace for the `Lean.Meta.ArgsPacker` modules. + +This is separated so that `Lean.Elab.PreDefinition.WF.Eqns` can include the +type in `EqnInfos` without depending on full module with operations. +-/ + +namespace Lean.Meta + +/-- +The metadata required for the operation in the `Lean.Meta.ArgsPacker` module; see +the module docs there for an overview. +-/ +structure ArgsPacker where + /-- + Variable names to use when unpacking a packed argument. + + Crucialy, the size of this arry also indicates the number of functions to pack, and + the length of each array the arity. + -/ + varNamess : Array (Array Name) + deriving Inhabited + +end Lean.Meta diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index 3e21d32e1c..71f2eec234 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -11,8 +11,8 @@ import Lean.Meta.Check import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Subst import Lean.Meta.Injective -- for elimOptParam +import Lean.Meta.ArgsPacker import Lean.Elab.PreDefinition.WF.Eqns -import Lean.Elab.PreDefinition.WF.PackMutual import Lean.Elab.Command /-! @@ -248,26 +248,6 @@ partial def foldCalls (fn : Expr) (oldIH : FVarId) (e : Expr) : MetaM Expr := do throwError m!"collectIHs: cannot eliminate unsaturated call to induction hypothesis" -/-- -Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`. -If `n = 0` returns a proof of `True`. -If `n = 1` returns the proof of `P₁`. --/ -def mkAndIntroN : Array Expr → MetaM Expr -| #[] => return mkConst ``True.intro [] -| #[e] => return e -| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back - -/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/ -def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do - let mut value := e - for _ in [:i] do - value := mkProj ``And 1 value - if i + 1 < n then - value := mkProj ``And 0 value - return value - - -- Non-tail-positions: Collect induction hypotheses -- (TODO: Worth folding with `foldCalls`, like before?) -- (TODO: Accumulated with a left fold) @@ -620,11 +600,6 @@ In the type of `value`, reduces and then wraps `value` in an appropriate type hint. -/ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do - -- TODO: Make arities (or varnames) part of eqnInfo - let arities ← eqnInfo.declNames.mapM fun name => do - let ci ← getConstInfoDefn name - lambdaTelescope ci.value fun xs _body => return xs.size - eqnInfo.fixedPrefixSize - let t ← Meta.transform (← inferType value) (skipConstInApp := true) (pre := fun e => do -- Need to beta-reduce first let e' := e.headBeta @@ -660,7 +635,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do let args := e.getAppArgs if eqnInfo.fixedPrefixSize + 1 ≤ args.size then let packedArg := args.back - let (i, unpackedArgs) ← WF.unpackArg arities packedArg + let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels! let e' := mkAppN e' args.pop let e' := mkAppN e' unpackedArgs @@ -670,163 +645,6 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do return .continue e) mkExpectedTypeHint value t -/-- Given type `A ⊕' B ⊕' … ⊕' D`, return `[A, B, …, D]` -/ -partial def unpackPSum (type : Expr) : List Expr := - if type.isAppOfArity ``PSum 2 then - if let #[a, b] := type.getAppArgs then - a :: unpackPSum b - else unreachable! - else - [type] - -/-- Given `A ⊗' B ⊗' … ⊗' D` and `R`, return `A → B → … → D → R` -/ -partial def uncurryPSumArrow (domain : Expr) (codomain : Expr) : MetaM Expr := do - if domain.isAppOfArity ``PSigma 2 then - let #[a, b] := domain.getAppArgs | unreachable! - withLocalDecl `x .default a fun x => do - mkForallFVars #[x] (← uncurryPSumArrow (b.beta #[x]) codomain) - else - mkArrow domain codomain - -/-- -Given expression `e` with type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]` -return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]` --/ -partial def uncurryPSigma (e : Expr) : MetaM Expr := do - let packedDomain := (← inferType e).bindingDomain! - go packedDomain packedDomain #[] -where - go (packedDomain domain : Expr) args : MetaM Expr := do - if domain.isAppOfArity ``PSigma 2 then - let #[a, b] := domain.getAppArgs | unreachable! - withLocalDecl `x .default a fun x => do - mkLambdaFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x)) - else - withLocalDecl `x .default domain fun x => do - let args := args.push x - let packedArg ← WF.mkUnaryArg packedDomain args - mkLambdaFVars #[x] (e.beta #[packedArg]) - -/-- -Iterated `PSigma.casesOn`: Given `y : a ⊗' b ⊗' …` and a type `codomain`, -and `alt : (x : a) → (y : b) → codomain`, uses `PSigma.casesOn` to invoke `alt` on `y`. - -This very is similar to `Lean.Predefinition.WF.mkPSigmaCasesOn`, but takes a lambda rather than -free variables. --/ -partial def mkPSigmaNCasesOn (y : FVarId) (codomain : Expr) (alt : Expr) : MetaM Expr := do - let mvar ← mkFreshExprSyntheticOpaqueMVar codomain - let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := mvarId.withContext do - if (← inferType (mkFVar y)).isAppOfArity ``PSigma 2 then - let #[s] ← mvarId.cases y | unreachable! - go s.mvarId s.fields[1]!.fvarId! (ys.push s.fields[0]!) - else - let ys := ys.push (mkFVar y) - mvarId.assign (alt.beta ys) - go mvar.mvarId! y #[] - instantiateMVars mvar - -/-- -Given expression `e` with type `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R` -returns an expression of type `(x : A ⊗' B ⊗' … ⊗' D) → R`. --/ -partial def curryPSigma (e : Expr) : MetaM Expr := do - let (d, codomain) ← forallTelescope (← inferType e) fun xs codomain => do - if xs.any (codomain.containsFVar ·.fvarId!) then - throwError "curryPSum: codomain depends on domain variables" - let mut d ← inferType xs.back - for x in xs.pop.reverse do - d ← mkLambdaFVars #[x] d - d ← mkAppOptM ``PSigma #[some (← inferType x), some d] - return (d, codomain) - withLocalDecl `x .default d fun x => do - let value ← mkPSigmaNCasesOn x.fvarId! codomain e - mkLambdaFVars #[x] value - -/-- -Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e` -into scope as fresh local declarations and passes their FVars to the continuation `k`. -The `name` is used to form the variable names; uses `name1`, `name2`, … if there are multiple. --/ -def withCurriedDecl {α} (name : String) (type : Expr) (k : Array Expr → MetaM α) : MetaM α := do - let some (d,c) := type.arrow? | throwError "withCurriedDecl: Expected arrow" - let motiveTypes ← (unpackPSum d).mapM (uncurryPSumArrow · c) - if let [t] := motiveTypes then - -- If a singleton, do not number the names. - withLocalDecl name .default t fun x => do k #[x] - else - go motiveTypes #[] -where - go : List Expr → Array Expr → MetaM α - | [], acc => k acc - | t::ts, acc => do - let name := s!"{name}{acc.size+1}" - withLocalDecl name .default t fun x => do - go ts (acc.push x) - - -/-- -Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression -to produce an expression of the isomorphic type -``` -((x: a) → (y : b) → e[.inl (x,y)]) ∧ ((x : c) → (y : d) → e[.inr (x,y)]) -``` --/ -def deMorganPSumPSigma (e : Expr) : MetaM Expr := do - let packedDomain := (← inferType e).bindingDomain! - let unaryTypes := unpackPSum packedDomain - shareIf (unaryTypes.length > 1) e fun e => do - let mut es := #[] - for unaryType in unaryTypes, i in [:unaryTypes.length] do - -- unary : (x : a ⊗ b) → e[inl x] - let unary ← withLocalDecl `x .default unaryType fun x => do - let packedArg ← WF.mkMutualArg unaryTypes.length packedDomain i x - mkLambdaFVars #[x] (e.beta #[packedArg]) - -- nary : (x : a) → (y : b) → e[inl (x,y)] - let nary ← uncurryPSigma unary - es := es.push nary - mkAndIntroN es - where - shareIf (b : Bool) (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do - if b then - withLetDecl `packed (← inferType e) e fun e => do mkLetFVars #[e] (← k e) - else - k e - - --- Adapted from PackMutual: TODO: Compare and unify -/-- - Combine/pack the values of the different definitions in a single value - `x` is `PSum`, and we use `PSum.casesOn` to select the appropriate `preDefs.value`. - See: `packMutual`. - - Remark: this method does not replace the nested recursive `preDefValues` applications. - This step is performed by `transform` with the following `post` method. - -/ -private def packValues (x : Expr) (codomain : Expr) (preDefValues : Array Expr) : MetaM Expr := do - let varNames := preDefValues.map fun val => - if val.isLambda then val.bindingName! else `x - let mvar ← mkFreshExprSyntheticOpaqueMVar codomain - let rec go (mvarId : MVarId) (x : FVarId) (i : Nat) : MetaM Unit := do - if i < preDefValues.size - 1 then - /- - Names for the `cases` tactics. The names are important to preserve the user provided names (unary functions). - -/ - let givenNames : Array AltVarNames := - if i == preDefValues.size - 2 then - #[{ varNames := [varNames[i]!] }, { varNames := [varNames[i+1]!] }] - else - #[{ varNames := [varNames[i]!] }] - let #[s₁, s₂] ← mvarId.cases x (givenNames := givenNames) | unreachable! - s₁.mvarId.assign (mkApp preDefValues[i]! s₁.fields[0]!).headBeta - go s₂.mvarId s₂.fields[0]!.fvarId! (i+1) - else - mvarId.assign (mkApp preDefValues[i]! (mkFVar x)).headBeta - termination_by preDefValues.size - 1 - i - go mvar.mvarId! x.fvarId! 0 - instantiateMVars mvar - - /-- Takes an induction principle where the motive is a `PSigma`/`PSum` type and unpacks it into a n-ary and (possibly) joint induction principle. @@ -853,23 +671,12 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : Meta pure motivePos let value ← forallBoundedTelescope ci.type motivePos fun params type => do let value := mkAppN value params - -- Next parameter is the motive (motive : a ⊗' b ⊕' c ⊗' d → Prop). - let packedMotiveType := type.bindingDomain! - -- Bring unpacked motives (motive1 : a → b → Prop and motive2 : c → d → Prop) into scope - withCurriedDecl "motive" packedMotiveType fun motives => do - -- Combine them into a packed motive (motive : a ⊗' b ⊕' c ⊗' d → Prop), and use that - let motive ← forallBoundedTelescope packedMotiveType (some 1) fun xs motiveCodomain => do - let #[x] := xs | throwError "packedMotiveType is not a forall: {packedMotiveType}" - let packedMotives ← motives.mapM curryPSigma - let motiveBody ← packValues x motiveCodomain packedMotives - mkLambdaFVars xs motiveBody - let type ← instantiateForall type #[motive] - let value := mkApp value motive + eqnInfo.argsPacker.curryParam value type fun motives value type => -- Bring the rest into scope forallTelescope type fun xs _concl => do let alts := xs.pop let value := mkAppN value alts - let value ← deMorganPSumPSigma value + let value ← eqnInfo.argsPacker.curry value let value ← mkLambdaFVars alts value let value ← mkLambdaFVars motives value let value ← mkLambdaFVars params value diff --git a/tests/lean/guessLex.lean b/tests/lean/guessLex.lean index c836ab72d7..006cb2b696 100644 --- a/tests/lean/guessLex.lean +++ b/tests/lean/guessLex.lean @@ -134,6 +134,11 @@ def shadow2 (some_n : Nat) : Nat → Nat | .succ n => shadow2 (some_n + 1) n decreasing_by decreasing_tactic +-- Tests that the inferred termination argument is shown without extra underscores +def foo : Nat → Nat → Nat → Nat + | _, 0, acc => acc + | k, n+1, acc => foo (k+1) n (acc + k) +decreasing_by decreasing_tactic -- The following test whether `sizeOf` is properly printed, and possibly qualified -- For this we need a type that needs an explicit “sizeOf”. @@ -204,7 +209,7 @@ def bar (o : OddNat3) : Nat := if h : @id Nat o < 41 then foo (41 - @id Nat o) e -- termination_by sizeOf o decreasing_by simp_wf; simp [id] at *; omega end -namespace MutualNotNat2 +end MutualNotNat2 namespace MutualNotNat3 -- A varant of the above, but where the type of the parameter refined to `Nat`. @@ -227,4 +232,4 @@ def bar : OddNat3 → Nat -- termination_by x1 => sizeOf x1 decreasing_by simp_wf; omega end -namespace MutualNotNat3 +end MutualNotNat3 diff --git a/tests/lean/guessLex.lean.expected.out b/tests/lean/guessLex.lean.expected.out index 737e10af6a..674ee9b4ea 100644 --- a/tests/lean/guessLex.lean.expected.out +++ b/tests/lean/guessLex.lean.expected.out @@ -25,9 +25,9 @@ termination_by x1 x2 x3 x4 x5 x6 x7 x8 => (x8, x7, x6, x5, x4, x3, x2, x1) Inferred termination argument: termination_by x1 => sizeOf x1 Inferred termination argument: -termination_by x1 x2 => (x1, sizeOf x2) +termination_by n m => (n, sizeOf m) Inferred termination argument: -termination_by x1 x2 => x1 +termination_by m acc => m Inferred termination argument: termination_by (sizeOf a, 1) Inferred termination argument: @@ -37,6 +37,8 @@ termination_by x2' => x2' Inferred termination argument: termination_by x2 => x2 Inferred termination argument: +termination_by x1 x2 x3 => x2 +Inferred termination argument: termination_by x1 => sizeOf x1 Inferred termination argument: termination_by x2 => SizeOf.sizeOf x2 @@ -52,13 +54,13 @@ Inferred termination argument: termination_by x1 => x1 Inferred termination argument: termination_by sizeOf o -guessLex.lean:217:0-229:3: error: Could not find a decreasing measure. +guessLex.lean:222:0-234:3: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) -Call from MutualNotNat2.MutualNotNat2.MutualNotNat3.foo to MutualNotNat2.MutualNotNat2.MutualNotNat3.bar at 221:23-35: +Call from MutualNotNat3.foo to MutualNotNat3.bar at 226:23-35: x1 x1 < -Call from MutualNotNat2.MutualNotNat2.MutualNotNat3.bar to MutualNotNat2.MutualNotNat2.MutualNotNat3.foo at 226:30-42: +Call from MutualNotNat3.bar to MutualNotNat3.foo at 231:30-42: x1 x1 ? diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index 7ca2512b31..274909f64d 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -38,18 +38,18 @@ well-founded recursion cannot be used, 'noNonFixedArguments' does not take any ( guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) - x1 x2 x3 -1) 29:6-25 = = = -2) 30:6-23 = < _ -3) 31:6-23 < _ _ + n m l +1) 29:6-25 = = = +2) 30:6-23 = < _ +3) 31:6-23 < _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) - x1 x2 x3 x4 -1) 39:6-27 = = _ = -2) 40:6-25 = < _ _ -3) 41:6-25 < _ _ _ + n m h x4 +1) 39:6-27 = = _ = +2) 40:6-25 = < _ _ +3) 41:6-25 < _ _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: @@ -88,20 +88,20 @@ Call from Mutual.g to Mutual.g at 69:8-33: n m H l _ _ _ < Call from Mutual.g to Mutual.h at 70:8-27: - n m H l -x1 _ _ _ ? -x2 _ _ _ ? + n m H l +n _ _ _ ? +m _ _ _ ? Call from Mutual.h to Mutual.f at 75:8-33: - x1 x2 -n _ _ -m _ _ -l _ _ + n m +n _ _ +m _ _ +l _ _ Call from Mutual.h to Mutual.h at 76:8-27: - x1 x2 - _ _ + n m + _ _ Call from Mutual.h to Mutual.h at 77:8-27: - x1 x2 - _ _ + n m + _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:89:19-89:32: error: fail to show termination for @@ -120,8 +120,8 @@ structural recursion cannot be used Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) - x1 x2 -1) 89:19-32 ? ? + n m +1) 89:19-32 ? ? Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:100:0-103:31: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: diff --git a/tests/lean/mutwftypemismatch.lean b/tests/lean/mutwftypemismatch.lean new file mode 100644 index 0000000000..65e0821c30 --- /dev/null +++ b/tests/lean/mutwftypemismatch.lean @@ -0,0 +1,28 @@ +namespace Ex1 +mutual +def foo : Nat → Nat + | 0 => 1 + | n+1 => bar n +termination_by n => n + +def bar : Nat → Nat + | 0 => 1 + | n+1 => foo n +termination_by n => n > 2 +end +end Ex1 + +namespace Ex2 +-- With dependency on fixed parameter +mutual +def foo (fixed : Nat) : Nat → Nat + | 0 => 1 + | n+1 => bar fixed n +termination_by n => n + +def bar (fixed : Nat) : Nat → Nat + | 0 => 1 + | n+1 => foo fixed n +termination_by n => (⟨n, sorry⟩ : Fin fixed) +end +end Ex2 diff --git a/tests/lean/mutwftypemismatch.lean.expected.out b/tests/lean/mutwftypemismatch.lean.expected.out new file mode 100644 index 0000000000..4173f3704e --- /dev/null +++ b/tests/lean/mutwftypemismatch.lean.expected.out @@ -0,0 +1,14 @@ +mutwftypemismatch.lean:11:20-11:25: error: The termination argument types differ for the different functions, or depend on the function's varying parameters. Try using `sizeOf` explicitly: +The termination argument has type + Prop : Type +but is expected to have type + Nat : Type +mutwftypemismatch.lean:5:10-5:15: error: failed to prove termination, possible solutions: + - Use `have`-expressions to prove the remaining goals + - Use `termination_by` to specify a different well-founded relation + - Use `decreasing_by` to specify your own tactic for discharging this kind of goal +n : Nat +⊢ sorryAx Nat true < n + 1 +mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry' +mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry' +mutwftypemismatch.lean:18:4-18:7: warning: declaration uses 'sorry' diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean index 6091baa4f4..8090af4fb5 100644 --- a/tests/lean/run/funind_demo.lean +++ b/tests/lean/run/funind_demo.lean @@ -9,8 +9,8 @@ derive_functional_induction ackermann /-- info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) - (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) - (x : Nat) : ∀ (x_1 : Nat), motive x x_1 + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) : + ∀ (a a_1 : Nat), motive a a_1 -/ #guard_msgs in #check ackermann.induct diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean index 229c26fa42..5efaf51be6 100644 --- a/tests/lean/run/funind_mutual_dep.lean +++ b/tests/lean/run/funind_mutual_dep.lean @@ -48,7 +48,7 @@ end derive_functional_induction Finite.functions /-- -info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type) → Finite → List x → Prop) +info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (α : Type) → Finite → List α → Prop) (case1 : motive1 Finite.unit) (case2 : motive1 Finite.bool) (case3 : ∀ (t1 t2 : Finite), motive1 t1 → motive1 t2 → motive1 (Finite.pair t1 t2)) (case4 : @@ -65,7 +65,7 @@ info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (x : Type) (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → α)), motive2 (Finite.asType (Finite.arr t1 t2) → α) t2 rest) → motive2 α (Finite.arr t1 t2) results) - (x : Type) : ∀ (x_1 : Finite) (x_2 : List x), motive2 x x_1 x_2 + (α : Type) (t : Finite) (results : List α) : motive2 α t results -/ #guard_msgs in #check Finite.functions.induct diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean index cc33203077..028f04f579 100644 --- a/tests/lean/run/funind_proof.lean +++ b/tests/lean/run/funind_proof.lean @@ -31,7 +31,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 (case2 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1)) (case3 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1)) (case4 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) - (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) (x : Term) : motive1 x + (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a -/ #guard_msgs in #check replaceConst.induct diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 1e3cdd5262..fe0f08128c 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -31,8 +31,8 @@ derive_functional_induction ackermann /-- info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0) - (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) - (x : Nat) : ∀ (x_1 : Nat), motive x x_1 + (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) : + ∀ (a a_1 : Nat), motive a a_1 -/ #guard_msgs in #check ackermann.induct @@ -244,7 +244,7 @@ derive_functional_induction with_arg_refining_match1 /-- info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0) (case2 : ∀ (n : Nat), motive 0 (Nat.succ n)) - (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 + (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (i : Nat) : ∀ (a : Nat), motive i a -/ #guard_msgs in #check with_arg_refining_match1.induct @@ -259,8 +259,7 @@ derive_functional_induction with_arg_refining_match2 /-- info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n) (case2 : ∀ (i : Nat), ¬i = 0 → motive i 0) - (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (x : Nat) : - ∀ (x_1 : Nat), motive x x_1 + (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (i n : Nat) : motive i n -/ #guard_msgs in #check with_arg_refining_match2.induct @@ -293,9 +292,9 @@ termination_by n => n derive_functional_induction with_mixed_match_tailrec /-- -info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (c d x : Nat), motive 0 x c d) - (case2 : ∀ (c d a x : Nat), motive a x (c % 2) (d % 2) → motive (Nat.succ a) x c d) (x : Nat) : - ∀ (x_1 x_2 x_3 : Nat), motive x x_1 x_2 x_3 +info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1) + (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive (Nat.succ a_2) x a a_1) : + ∀ (a a_1 a_2 a_3 : Nat), motive a a_1 a_2 a_3 -/ #guard_msgs in #check with_mixed_match_tailrec.induct @@ -313,9 +312,9 @@ derive_functional_induction with_mixed_match_tailrec2 /-- info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop) - (case1 : ∀ (a b c d : Nat), motive 0 a b c d) (case2 : ∀ (c d n x : Nat), motive (Nat.succ n) 0 x c d) - (case3 : ∀ (c d n a x : Nat), motive n a x (c % 2) (d % 2) → motive (Nat.succ n) (Nat.succ a) x c d) (x : Nat) : - ∀ (x_1 x_2 x_3 x_4 : Nat), motive x x_1 x_2 x_3 x_4 + (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive (Nat.succ n) 0 x a a_1) + (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive (Nat.succ n) (Nat.succ a_2) x a a_1) : + ∀ (a a_1 a_2 a_3 a_4 : Nat), motive a a_1 a_2 a_3 a_4 -/ #guard_msgs in #check with_mixed_match_tailrec2.induct @@ -406,7 +405,7 @@ derive_functional_induction binary /-- info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 + (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) : ∀ (a a_1 : Nat), motive a a_1 -/ #guard_msgs in #check binary.induct @@ -621,16 +620,16 @@ derive_functional_induction even /-- info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) - (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) - (x : Nat) : motive1 x + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) : + ∀ (a : Nat), motive1 a -/ #guard_msgs in #check even.induct /-- info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) - (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) - (x : Nat) : motive2 x + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) : + ∀ (a : Nat), motive2 a -/ #guard_msgs in #check odd.induct @@ -654,7 +653,7 @@ derive_functional_induction Tree.map /-- info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) - (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (x : Tree) : motive1 x + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a : Tree), motive1 a -/ #guard_msgs in #check Tree.map.induct @@ -662,7 +661,7 @@ info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive /-- info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) - (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (x : List Tree) : motive2 x + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (ts : List Tree) : motive2 ts -/ #guard_msgs in #check Tree.map_forest.induct @@ -696,7 +695,7 @@ derive_functional_induction foo /-- info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m) - (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (x : Nat) : ∀ (x_1 : Nat), motive x x_1 + (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (n m : Nat) : motive n m -/ #guard_msgs in #check foo.induct @@ -715,15 +714,15 @@ termination_by n => n derive_functional_induction foo /-- -info: Nary.foo.induct (motive : Nat → Nat → (x : Nat) → Fin x → Prop) +info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (case1 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), motive 0 x x_1 x_2) (case2 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), (x = 0 → False) → motive x 0 x_1 x_2) (case3 : ∀ (x x_1 : Nat) (x_2 : Fin 0), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 0 x_2) (case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2) (case5 : ∀ (n m k : Nat) (x : Fin (k + 2)), - motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) - (x : Nat) : ∀ (x_1 x_2 : Nat) (x_3 : Fin x_2), motive x x_1 x_2 x_3 + motive n m (k + 1) { val := 0, isLt := ⋯ } → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) : + ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2 -/ #guard_msgs in #check foo.induct @@ -798,8 +797,8 @@ info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (c /-- info: CommandIdempotence.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0) - (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) - (x : Nat) : motive1 x + (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) : + ∀ (a : Nat), motive1 a -/ #guard_msgs in #check even.induct diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean index 1c1fefa9a1..ff793f9e80 100644 --- a/tests/lean/run/mutwf3.lean +++ b/tests/lean/run/mutwf3.lean @@ -32,7 +32,7 @@ end #print f #print g #print h -#print f._unary._mutual +#print f._mutual end Ex1 namespace Ex2 @@ -53,7 +53,7 @@ mutual termination_by _ _ n => (n, 0) end -#print f._unary._mutual +#print f._mutual end Ex2 @@ -72,6 +72,6 @@ mutual | a, b, n+1 => f n a b end -#print f._unary._mutual +#print f._mutual end Ex3 diff --git a/tests/lean/run/mutwf4.lean b/tests/lean/run/mutwf4.lean index b49943ee22..7881e09a91 100644 --- a/tests/lean/run/mutwf4.lean +++ b/tests/lean/run/mutwf4.lean @@ -15,4 +15,4 @@ end #print f #print g -#print f._unary._mutual +#print f._mutual