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.
This commit is contained in:
Joachim Breitner
GitHub
parent
68eaf33e86
commit
f89ed40618
21 changed files with 863 additions and 705 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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."
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
572
src/Lean/Meta/ArgsPacker.lean
Normal file
572
src/Lean/Meta/ArgsPacker.lean
Normal file
|
|
@ -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
|
||||
33
src/Lean/Meta/ArgsPacker/Basic.lean
Normal file
33
src/Lean/Meta/ArgsPacker/Basic.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 ?
|
||||
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
28
tests/lean/mutwftypemismatch.lean
Normal file
28
tests/lean/mutwftypemismatch.lean
Normal file
|
|
@ -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
|
||||
14
tests/lean/mutwftypemismatch.lean.expected.out
Normal file
14
tests/lean/mutwftypemismatch.lean.expected.out
Normal file
|
|
@ -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'
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -15,4 +15,4 @@ end
|
|||
|
||||
#print f
|
||||
#print g
|
||||
#print f._unary._mutual
|
||||
#print f._mutual
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue