feat: infer mutual structural recursion (#4718)
the support for mutual structural recursion (new since #4575) is extended so that Lean tries to infer it even without annotations. * The error message when termination checking fails looks quite different now. Maybe a bit better, maybe with more room for improvements. * If there are too many combinations (with an arbitrary cut-off) for a given argument type, it will just give up and ask the user to use `termination_by structural`. * It is now legal to specify `termination_by structural` on not necessarily all functions of a clique; this simply restricts the combinations of arguments that Lean considers. --------- Co-authored-by: Tobias Grosser <tobias@grosser.es>
This commit is contained in:
Joachim Breitner
GitHub
parent
f99427bd1a
commit
3ab2c714ec
15 changed files with 417 additions and 247 deletions
|
|
@ -111,7 +111,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
|
|||
preDefWith.termination.terminationBy? matches some {structural := true, ..}
|
||||
for preDef in preDefs do
|
||||
if let .some termBy := preDef.termination.terminationBy? then
|
||||
if !preDefsWithout.isEmpty then
|
||||
if !structural && !preDefsWithout.isEmpty then
|
||||
let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
|
||||
let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
|
||||
logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
|
||||
|
|
@ -135,13 +135,12 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
|
|||
/--
|
||||
Elaborates the `TerminationHint` in the clique to `TerminationArguments`
|
||||
-/
|
||||
def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Option TerminationArguments) := do
|
||||
let tas ← preDefs.mapM fun preDef => do
|
||||
def elabTerminationByHints (preDefs : Array PreDefinition) : TermElabM (Array (Option TerminationArgument)) := do
|
||||
preDefs.mapM fun preDef => do
|
||||
let arity ← lambdaTelescope preDef.value fun xs _ => pure xs.size
|
||||
let hints := preDef.termination
|
||||
hints.terminationBy?.mapM
|
||||
(TerminationArgument.elab preDef.declName preDef.type arity hints.extraParams ·)
|
||||
return tas.sequenceMap id -- only return something if every function has a hint
|
||||
|
||||
def shouldUseStructural (preDefs : Array PreDefinition) : Bool :=
|
||||
preDefs.any fun preDef =>
|
||||
|
|
@ -188,16 +187,16 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
|
|||
try
|
||||
checkCodomainsLevel preDefs
|
||||
checkTerminationByHints preDefs
|
||||
let termArgs ← elabTerminationByHints preDefs
|
||||
let termArg?s ← elabTerminationByHints preDefs
|
||||
if shouldUseStructural preDefs then
|
||||
structuralRecursion preDefs termArgs
|
||||
structuralRecursion preDefs termArg?s
|
||||
else if shouldUseWF preDefs then
|
||||
wfRecursion preDefs termArgs
|
||||
wfRecursion preDefs termArg?s
|
||||
else
|
||||
withRef (preDefs[0]!.ref) <| mapError
|
||||
(orelseMergeErrors
|
||||
(structuralRecursion preDefs termArgs)
|
||||
(wfRecursion preDefs termArgs))
|
||||
(structuralRecursion preDefs termArg?s)
|
||||
(wfRecursion preDefs termArg?s))
|
||||
(fun msg =>
|
||||
let preDefMsgs := preDefs.toList.map (MessageData.ofExpr $ mkConst ·.declName)
|
||||
m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
|
||||
|
|
|
|||
|
|
@ -4,12 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura, Joachim Breitner
|
||||
-/
|
||||
prelude
|
||||
import Lean.Elab.PreDefinition.TerminationArgument
|
||||
import Lean.Elab.PreDefinition.Structural.Basic
|
||||
import Lean.Elab.PreDefinition.Structural.RecArgInfo
|
||||
|
||||
namespace Lean.Elab.Structural
|
||||
open Meta
|
||||
|
||||
def prettyParam (xs : Array Expr) (i : Nat) : MetaM MessageData := do
|
||||
let x := xs[i]!
|
||||
let n ← x.fvarId!.getUserName
|
||||
addMessageContextFull <| if n.hasMacroScopes then m!"#{i+1}" else m!"{x}"
|
||||
|
||||
def prettyRecArg (xs : Array Expr) (value : Expr) (recArgInfo : RecArgInfo) : MetaM MessageData := do
|
||||
lambdaTelescope value fun ys _ => prettyParam (xs ++ ys) recArgInfo.recArgPos
|
||||
|
||||
def prettyParameterSet (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
|
||||
(recArgInfos : Array RecArgInfo) : MetaM MessageData := do
|
||||
if fnNames.size = 1 then
|
||||
return m!"parameter " ++ (← prettyRecArg xs values[0]! recArgInfos[0]!)
|
||||
else
|
||||
let mut l := #[]
|
||||
for fnName in fnNames, value in values, recArgInfo in recArgInfos do
|
||||
l := l.push m!"{(← prettyRecArg xs value recArgInfo)} of {fnName}"
|
||||
return m!"parameters " ++ .andList l.toList
|
||||
|
||||
private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run do
|
||||
let mut minPos := xs.size
|
||||
for index in indices do
|
||||
|
|
@ -92,47 +111,139 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
|
|||
throwError "the index #{i+1} exceeds {xs.size}, the number of parameters"
|
||||
|
||||
/--
|
||||
Runs `k` on all argument indices, until it succeeds.
|
||||
We use this argument to justify termination using the auxiliary `brecOn` construction.
|
||||
Collects the `RecArgInfos` for one function, and returns a report for why the others were not
|
||||
considered.
|
||||
|
||||
We give preference for arguments that are *not* indices of inductive types of other arguments.
|
||||
See issue #837 for an example where we can show termination using the index of an inductive family, but
|
||||
we don't get the desired definitional equalities.
|
||||
The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.
|
||||
|
||||
`value` is the function value (including fixed parameters)
|
||||
Takes the optional user annotations into account (`termArg?`). If this is given and the argument
|
||||
is unsuitable, throw an error.
|
||||
-/
|
||||
partial def tryAllArgs (value : Expr) (k : Nat → M α) : M α := do
|
||||
-- It's improtant to keep the call to `k` outside the scope of `lambdaTelescope`:
|
||||
-- The tactics in the IndPred construction search the full local context, so we must not have
|
||||
-- extra FVars there
|
||||
let (indices, nonIndices) ← lambdaTelescope value fun xs _ => do
|
||||
let indicesRef : IO.Ref (Array Nat) ← IO.mkRef {}
|
||||
for x in xs do
|
||||
let xType ← inferType x
|
||||
/- Traverse all sub-expressions in the type of `x` -/
|
||||
forEachExpr xType fun e =>
|
||||
/- If `e` is an inductive family, we store in `indicesRef` all variables in `xs` that occur in "index positions". -/
|
||||
matchConstInduct e.getAppFn (fun _ => pure ()) fun info _ => do
|
||||
if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then
|
||||
for arg in e.getAppArgs[info.numParams:] do
|
||||
forEachExpr arg fun e => do
|
||||
if let .some idx := xs.getIdx? e then
|
||||
indicesRef.modify (·.push idx)
|
||||
let indices ← indicesRef.get
|
||||
let nonIndices := (Array.range xs.size).filter (fun i => !(indices.contains i))
|
||||
return (indices, nonIndices)
|
||||
def getRecArgInfos (fnName : Name) (xs : Array Expr) (value : Expr)
|
||||
(termArg? : Option TerminationArgument) : MetaM (Array RecArgInfo × MessageData) := do
|
||||
lambdaTelescope value fun ys _ => do
|
||||
if let .some termArg := termArg? then
|
||||
-- User explictly asked to use a certain argument, so throw errors eagerly
|
||||
let recArgInfo ← withRef termArg.ref do
|
||||
mapError (f := (m!"cannot use specified parameter for structural recursion:{indentD ·}")) do
|
||||
getRecArgInfo fnName xs.size (xs ++ ys) (← termArg.structuralArg)
|
||||
return (#[recArgInfo], m!"")
|
||||
else
|
||||
let mut recArgInfos := #[]
|
||||
let mut report : MessageData := m!""
|
||||
-- No `termination_by`, so try all, and remember the errors
|
||||
for idx in [:xs.size + ys.size] do
|
||||
try
|
||||
let recArgInfo ← getRecArgInfo fnName xs.size (xs ++ ys) idx
|
||||
recArgInfos := recArgInfos.push recArgInfo
|
||||
catch e =>
|
||||
report := report ++ (m!"Not considering parameter {← prettyParam (xs ++ ys) idx} of {fnName}:" ++
|
||||
indentD e.toMessageData) ++ "\n"
|
||||
trace[Elab.definition.structural] "getRecArgInfos report: {report}"
|
||||
return (recArgInfos, report)
|
||||
|
||||
let mut errors : Array MessageData := Array.mkArray (indices.size + nonIndices.size) m!""
|
||||
let saveState ← get -- backtrack the state for each argument
|
||||
for i in id (nonIndices ++ indices) do
|
||||
trace[Elab.definition.structural] "findRecArg i: {i}"
|
||||
try
|
||||
set saveState
|
||||
return (← k i)
|
||||
catch e => errors := errors.set! i e.toMessageData
|
||||
throwError
|
||||
errors.foldl
|
||||
(init := m!"structural recursion cannot be used:")
|
||||
(f := (· ++ Format.line ++ Format.line ++ .))
|
||||
|
||||
/--
|
||||
Reorders the `RecArgInfos` of one function to put arguments that are indices of other arguments
|
||||
last.
|
||||
See issue #837 for an example where we can show termination using the index of an inductive family, but
|
||||
we don't get the desired definitional equalities.
|
||||
-/
|
||||
def nonIndicesFirst (recArgInfos : Array RecArgInfo) : Array RecArgInfo := Id.run do
|
||||
let mut indicesPos : HashSet Nat := {}
|
||||
for recArgInfo in recArgInfos do
|
||||
for pos in recArgInfo.indicesPos do
|
||||
indicesPos := indicesPos.insert pos
|
||||
let (indices,nonIndices) := recArgInfos.partition (indicesPos.contains ·.recArgPos)
|
||||
return nonIndices ++ indices
|
||||
|
||||
private def dedup [Monad m] (eq : α → α → m Bool) (xs : Array α) : m (Array α) := do
|
||||
let mut ret := #[]
|
||||
for x in xs do
|
||||
unless (← ret.anyM (eq · x)) do
|
||||
ret := ret.push x
|
||||
return ret
|
||||
|
||||
/--
|
||||
Given the `RecArgInfo`s of all the recursive functions, find the inductive groups to consider.
|
||||
-/
|
||||
def inductiveGroups (recArgInfos : Array RecArgInfo) : MetaM (Array IndGroupInst) :=
|
||||
dedup IndGroupInst.isDefEq (recArgInfos.map (·.indGroupInst))
|
||||
|
||||
/--
|
||||
Filters the `recArgInfos` by those that describe an argument that's part of the recursive inductive
|
||||
group `group`.
|
||||
|
||||
|
||||
Anticipating support for nested inductives this function has the ability to change the `recArgInfo`.
|
||||
Consider
|
||||
```
|
||||
inductive Tree where | node : List Tree → Tree
|
||||
```
|
||||
then when we look for arguments whose type is part of the group `Tree`, we want to also consider
|
||||
the argument of type `List Tree`, even though that argument’s `RecArgInfo` refers to initially to
|
||||
`List`.
|
||||
-/
|
||||
def argsInGroup (group : IndGroupInst) (_xs : Array Expr) (_value : Expr)
|
||||
(recArgInfos : Array RecArgInfo) : MetaM (Array RecArgInfo) := do
|
||||
recArgInfos.filterM (group.isDefEq ·.indGroupInst)
|
||||
|
||||
def maxCombinationSize : Nat := 10
|
||||
|
||||
def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
|
||||
if xss.foldl (· * ·.size) 1 > maxCombinationSize then
|
||||
none
|
||||
else
|
||||
let rec go i acc : Array (Array α):=
|
||||
if h : i < xss.size then
|
||||
xss[i].concatMap fun x => go (i + 1) (acc.push x)
|
||||
else
|
||||
#[acc]
|
||||
some (go 0 #[])
|
||||
|
||||
|
||||
def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
|
||||
(termArg?s : Array (Option TerminationArgument)) (k : Array RecArgInfo → M α) : M α := do
|
||||
let mut report := m!""
|
||||
-- Gather information on all possible recursive arguments
|
||||
let mut recArgInfoss := #[]
|
||||
for fnName in fnNames, value in values, termArg? in termArg?s do
|
||||
let (recArgInfos, thisReport) ← getRecArgInfos fnName xs value termArg?
|
||||
report := report ++ thisReport
|
||||
recArgInfoss := recArgInfoss.push recArgInfos
|
||||
-- Put non-indices first
|
||||
recArgInfoss := recArgInfoss.map nonIndicesFirst
|
||||
trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
|
||||
-- Inductive groups to consider
|
||||
let groups ← inductiveGroups recArgInfoss.flatten
|
||||
trace[Elab.definition.structural] "inductive groups: {groups}"
|
||||
if groups.isEmpty then
|
||||
report := report ++ "no parameters suitable for structural recursion"
|
||||
-- Consider each group
|
||||
for group in groups do
|
||||
-- Select those RecArgInfos that are compatible with this inductive group
|
||||
let mut recArgInfoss' := #[]
|
||||
for value in values, recArgInfos in recArgInfoss do
|
||||
recArgInfoss' := recArgInfoss'.push (← argsInGroup group xs value recArgInfos)
|
||||
if let some idx := recArgInfoss'.findIdx? (·.isEmpty) then
|
||||
report := report ++ m!"Skipping arguments of type {group}, as {fnNames[idx]!} has no compatible argument.\n"
|
||||
continue
|
||||
if let some combs := allCombinations recArgInfoss' then
|
||||
for comb in combs do
|
||||
try
|
||||
-- TODO: Here we used to save and restore the state. But should the `try`-`catch`
|
||||
-- not suffice?
|
||||
let r ← k comb
|
||||
trace[Elab.definition.structural] "tryTellArgs report:\n{report}"
|
||||
return r
|
||||
catch e =>
|
||||
let m ← prettyParameterSet fnNames xs values comb
|
||||
report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
|
||||
else
|
||||
report := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
|
||||
m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
|
||||
report := m!"failed to infer structural recursion:\n" ++ report
|
||||
trace[Elab.definition.structural] "tryTellArgs:\n{report}"
|
||||
throwError report
|
||||
|
||||
end Lean.Elab.Structural
|
||||
|
|
|
|||
|
|
@ -89,98 +89,68 @@ def getMutualFixedPrefix (preDefs : Array PreDefinition) : M Nat :=
|
|||
return true
|
||||
resultRef.get
|
||||
|
||||
/-- Checks that all parameter types are mutually inductive -/
|
||||
private def checkAllFromSameClique (recArgInfos : Array RecArgInfo) : MetaM Unit := do
|
||||
for recArgInfo in recArgInfos do
|
||||
unless recArgInfos[0]!.indGroupInst.all.contains recArgInfo.indName! do
|
||||
throwError m!"Cannot use structural mutual recursion: The recursive argument of " ++
|
||||
m!"{recArgInfos[0]!.fnName} is of type {recArgInfos[0]!.indName!}, " ++
|
||||
m!"the recursive argument of {recArgInfo.fnName} is of type " ++
|
||||
m!"{recArgInfo.indName!}, and these are not mutually recursive."
|
||||
private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr)
|
||||
(recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
|
||||
let values ← preDefs.mapM (instantiateLambda ·.value xs)
|
||||
let indInfo ← getConstInfoInduct recArgInfos[0]!.indName!
|
||||
if ← isInductivePredicate indInfo.name then
|
||||
-- Here we branch off to the IndPred construction, but only for non-mutual functions
|
||||
unless preDefs.size = 1 do
|
||||
throwError "structural mutual recursion over inductive predicates is not supported"
|
||||
trace[Elab.definition.structural] "Using mkIndPred construction"
|
||||
let preDef := preDefs[0]!
|
||||
let recArgInfo := recArgInfos[0]!
|
||||
let value := values[0]!
|
||||
let valueNew ← mkIndPredBRecOn recArgInfo value
|
||||
let valueNew ← mkLambdaFVars xs valueNew
|
||||
trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
|
||||
check valueNew
|
||||
return #[{ preDef with value := valueNew }]
|
||||
|
||||
private def elimMutualRecursion (preDefs : Array PreDefinition) (recArgPoss : Array Nat) : M (Array PreDefinition) := do
|
||||
-- Sort the (indices of the) definitions by their position in indInfo.all
|
||||
let positions : Positions := .groupAndSort (·.indName!) recArgInfos indInfo.all.toArray
|
||||
|
||||
-- Construct the common `.brecOn` arguments
|
||||
let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
|
||||
let brecOnConst ← mkBRecOnConst recArgInfos positions motives
|
||||
let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
|
||||
let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
|
||||
mkBRecOnF recArgInfos positions r v t
|
||||
-- Assemble the individual `.brecOn` applications
|
||||
let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
|
||||
mkBrecOnApp positions i brecOnConst FArgs r v
|
||||
-- Abstract over the fixed prefixed
|
||||
let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
|
||||
return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
|
||||
|
||||
private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
|
||||
M (Array Nat × Array PreDefinition) := do
|
||||
withoutModifyingEnv do
|
||||
preDefs.forM (addAsAxiom ·)
|
||||
let names := preDefs.map (·.declName)
|
||||
let fnNames := preDefs.map (·.declName)
|
||||
let preDefs ← preDefs.mapM fun preDef =>
|
||||
return { preDef with value := (← preprocess preDef.value names) }
|
||||
return { preDef with value := (← preprocess preDef.value fnNames) }
|
||||
|
||||
-- The syntactically fixed arguments
|
||||
let maxNumFixed ← getMutualFixedPrefix preDefs
|
||||
|
||||
-- We do two passes to get the RecArgInfo values.
|
||||
-- From the first pass, we only keep the mininum of the `numFixed` reported.
|
||||
let numFixed ← lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
|
||||
lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
|
||||
assert! xs.size = maxNumFixed
|
||||
let values ← preDefs.mapM (instantiateLambda ·.value xs)
|
||||
|
||||
let recArgInfos ← preDefs.mapIdxM fun i preDef => do
|
||||
let recArgPos := recArgPoss[i]!
|
||||
let value := values[i]!
|
||||
lambdaTelescope value fun ys _value => do
|
||||
getRecArgInfo preDef.declName maxNumFixed (xs ++ ys) recArgPos
|
||||
|
||||
checkAllFromSameClique recArgInfos
|
||||
|
||||
-- Check that the inductive parameters agree. This also ensures that they only depend on the
|
||||
-- trimmed prefix (minimum of all `.numFixed`).
|
||||
for recArgInfo in recArgInfos[1:] do
|
||||
let ok ← IndGroupInst.isDefEq recArgInfo.indGroupInst recArgInfos[0]!.indGroupInst
|
||||
unless ok do
|
||||
throwError m!"The inductive type of the recursive parameter of {recArgInfos[0]!.fnName} " ++
|
||||
m!"and {recArgInfo.fnName} have different parameters:" ++
|
||||
indentD m!"{recArgInfos[0]!.indGroupInst.params}" ++
|
||||
indentD m!"{recArgInfo.indGroupInst.params}"
|
||||
|
||||
return (recArgInfos.map (·.numFixed)).foldl Nat.min maxNumFixed
|
||||
|
||||
if numFixed < maxNumFixed then
|
||||
trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
|
||||
|
||||
-- Now we bring exactly that `numFixed` parameter into scope.
|
||||
lambdaBoundedTelescope preDefs[0]!.value numFixed fun xs _ => do
|
||||
assert! xs.size = numFixed
|
||||
let values ← preDefs.mapM (instantiateLambda ·.value xs)
|
||||
|
||||
let recArgInfos ← preDefs.mapIdxM fun i preDef => do
|
||||
let recArgPos := recArgPoss[i]!
|
||||
let value := values[i]!
|
||||
lambdaTelescope value fun ys _value => do
|
||||
getRecArgInfo preDef.declName numFixed (xs ++ ys) recArgPos
|
||||
|
||||
-- Two passes should suffice
|
||||
assert! recArgInfos.all (·.numFixed = numFixed)
|
||||
|
||||
let indInfo ← getConstInfoInduct recArgInfos[0]!.indName!
|
||||
if ← isInductivePredicate indInfo.name then
|
||||
-- Here we branch off to the IndPred construction, but only for non-mutual functions
|
||||
unless preDefs.size = 1 do
|
||||
throwError "structural mutual recursion over inductive predicates is not supported"
|
||||
trace[Elab.definition.structural] "Using mkIndPred construction"
|
||||
let preDef := preDefs[0]!
|
||||
let recArgInfo := recArgInfos[0]!
|
||||
let value := values[0]!
|
||||
let valueNew ← mkIndPredBRecOn recArgInfo value
|
||||
let valueNew ← mkLambdaFVars xs valueNew
|
||||
trace[Elab.definition.structural] "Nonrecursive value:{indentExpr valueNew}"
|
||||
check valueNew
|
||||
return #[{ preDef with value := valueNew }]
|
||||
|
||||
-- Sort the (indices of the) definitions by their position in indInfo.all
|
||||
let positions : Positions := .groupAndSort (·.indName!) recArgInfos indInfo.all.toArray
|
||||
|
||||
-- Construct the common `.brecOn` arguments
|
||||
let motives ← (Array.zip recArgInfos values).mapM fun (r, v) => mkBRecOnMotive r v
|
||||
let brecOnConst ← mkBRecOnConst recArgInfos positions motives
|
||||
let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
|
||||
let FArgs ← (recArgInfos.zip (values.zip FTypes)).mapM fun (r, (v, t)) =>
|
||||
mkBRecOnF recArgInfos positions r v t
|
||||
-- Assemble the individual `.brecOn` applications
|
||||
let valuesNew ← (Array.zip recArgInfos values).mapIdxM fun i (r, v) =>
|
||||
mkBrecOnApp positions i brecOnConst FArgs r v
|
||||
-- Abstract over the fixed prefixed
|
||||
let valuesNew ← valuesNew.mapM (mkLambdaFVars xs ·)
|
||||
return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
|
||||
tryAllArgs fnNames xs values termArg?s fun recArgInfos => do
|
||||
let recArgPoss := recArgInfos.map (·.recArgPos)
|
||||
trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
|
||||
let numFixed := recArgInfos.foldl (·.min ·.numFixed) maxNumFixed
|
||||
if numFixed < maxNumFixed then
|
||||
trace[Elab.definition.structural] "Reduced numFixed from {maxNumFixed} to {numFixed}"
|
||||
-- We may have decreased the number of arguments we consider fixed, so update
|
||||
-- the recArgInfos, remove the extra arguments from local environment, and recalculate value
|
||||
let recArgInfos := recArgInfos.map ({· with numFixed := numFixed })
|
||||
withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do
|
||||
let xs := xs[:numFixed]
|
||||
let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
|
||||
return (recArgPoss, preDefs')
|
||||
|
||||
def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
|
||||
if let some ref := preDef.termination.terminationBy?? then
|
||||
|
|
@ -190,34 +160,20 @@ def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
|
|||
let stx ← termArg.delab arity (extraParams := preDef.termination.extraParams)
|
||||
Tactic.TryThis.addSuggestion ref stx
|
||||
|
||||
private def inferRecArgPos (preDefs : Array PreDefinition)
|
||||
(termArgs? : Option TerminationArguments) : M (Array Nat × Array PreDefinition) := do
|
||||
withoutModifyingEnv do
|
||||
if let some termArgs := termArgs? then
|
||||
let recArgPoss ← termArgs.mapM (·.structuralArg)
|
||||
let preDefsNew ← elimMutualRecursion preDefs recArgPoss
|
||||
return (recArgPoss, preDefsNew)
|
||||
else
|
||||
let #[preDef] := preDefs
|
||||
| throwError "mutual structural recursion requires explicit `termination_by` clauses"
|
||||
-- Use termination_by annotation to find argument to recurse on, or just try all
|
||||
tryAllArgs preDef.value fun i =>
|
||||
mapError (f := fun msg => m!"argument #{i+1} cannot be used for structural recursion{indentD msg}") do
|
||||
let preDefsNew ← elimMutualRecursion #[preDef] #[i]
|
||||
return (#[i], preDefsNew)
|
||||
|
||||
def structuralRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
|
||||
let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArgs?
|
||||
def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
|
||||
let names := preDefs.map (·.declName)
|
||||
let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArg?s
|
||||
for recArgPos in recArgPoss, preDef in preDefs do
|
||||
reportTermArg preDef recArgPos
|
||||
state.addMatchers.forM liftM
|
||||
preDefsNonRec.forM fun preDefNonRec => do
|
||||
let preDefNonRec ← eraseRecAppSyntax preDefNonRec
|
||||
-- state.addMatchers.forM liftM
|
||||
mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg =>
|
||||
m!"structural recursion failed, produced type incorrect term{indentD msg}"
|
||||
-- We create the `_unsafe_rec` before we abstract nested proofs.
|
||||
-- Reason: the nested proofs may be referring to the _unsafe_rec.
|
||||
mapError (f := (m!"structural recursion failed, produced type incorrect term{indentD ·}")) do
|
||||
-- We create the `_unsafe_rec` before we abstract nested proofs.
|
||||
-- Reason: the nested proofs may be referring to the _unsafe_rec.
|
||||
addNonRec preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
|
||||
let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
|
||||
addAndCompilePartialRec preDefs
|
||||
for preDef in preDefs, recArgPos in recArgPoss do
|
||||
|
|
|
|||
|
|
@ -86,7 +86,8 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
|
|||
let xs : Array Expr := xs[fixedPrefixSize:]
|
||||
xs.mapM (·.fvarId!.getUserName)
|
||||
|
||||
def wfRecursion (preDefs : Array PreDefinition) (termArgs? : Option TerminationArguments) : TermElabM Unit := do
|
||||
def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
|
||||
let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
|
||||
let preDefs ← preDefs.mapM fun preDef =>
|
||||
return { preDef with value := (← preprocess preDef.value) }
|
||||
let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do
|
||||
|
|
|
|||
|
|
@ -1,12 +1,11 @@
|
|||
1673.lean:1:4-1:9: error: fail to show termination for
|
||||
foo.a
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Not considering parameter n of foo.a:
|
||||
it is unchanged in the recursive calls
|
||||
|
||||
argument #2 cannot be used for structural recursion
|
||||
Not considering parameter nope of foo.a:
|
||||
it is unchanged in the recursive calls
|
||||
no parameters suitable for structural recursion
|
||||
|
||||
well-founded recursion cannot be used, 'foo.a' does not take any (non-fixed) arguments
|
||||
|
|
|
|||
|
|
@ -35,6 +35,7 @@ mutual
|
|||
def even : Nat → Bool
|
||||
| 0 => true
|
||||
| .succ n => not (odd n)
|
||||
decreasing_by decreasing_tactic
|
||||
def odd : Nat → Bool
|
||||
| 0 => false
|
||||
| .succ n => not (even n)
|
||||
|
|
@ -44,6 +45,7 @@ mutual
|
|||
def evenWithFixed (m : String) : Nat → Bool
|
||||
| 0 => true
|
||||
| .succ n => not (oddWithFixed m n)
|
||||
decreasing_by decreasing_tactic
|
||||
def oddWithFixed (m : String) : Nat → Bool
|
||||
| 0 => false
|
||||
| .succ n => not (evenWithFixed m n)
|
||||
|
|
@ -81,6 +83,7 @@ def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat
|
|||
def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat
|
||||
| 0, _p => 0
|
||||
| .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x, .succ y⟩
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat
|
||||
| ⟨_,0⟩ => 0
|
||||
|
|
|
|||
|
|
@ -23,6 +23,8 @@ termination_by (m, n)
|
|||
Inferred termination argument:
|
||||
termination_by x1 x2 x3 x4 x5 x6 x7 x8 => (x8, x7, x6, x5, x4, x3, x2, x1)
|
||||
Inferred termination argument:
|
||||
termination_by x1 => x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by n m => (n, sizeOf m)
|
||||
|
|
|
|||
|
|
@ -13,15 +13,14 @@ termination_by (xs.size - i, i)
|
|||
guessLexDiff.lean:84:4-84:11: error: fail to show termination for
|
||||
failure
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Not considering parameter xs of failure:
|
||||
it is unchanged in the recursive calls
|
||||
|
||||
argument #2 cannot be used for structural recursion
|
||||
Cannot use parameter i:
|
||||
failed to eliminate recursive application
|
||||
_root_.failure xs i
|
||||
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
|
|
@ -44,7 +43,15 @@ guessLexDiff.lean:102:4-102:18: error: fail to show termination for
|
|||
mutual_failure
|
||||
mutual_failure2
|
||||
with errors
|
||||
mutual structural recursion requires explicit `termination_by` clauses
|
||||
failed to infer structural recursion:
|
||||
Not considering parameter xs of mutual_failure:
|
||||
it is unchanged in the recursive calls
|
||||
Not considering parameter xs of mutual_failure2:
|
||||
it is unchanged in the recursive calls
|
||||
Cannot use parameters i of mutual_failure and i of mutual_failure2:
|
||||
failed to eliminate recursive application
|
||||
mutual_failure2 xs i
|
||||
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
|
|||
|
|
@ -1,15 +1,14 @@
|
|||
guessLexFailures.lean:9:4-9:18: error: fail to show termination for
|
||||
nonTerminating
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Cannot use parameter #1:
|
||||
failed to eliminate recursive application
|
||||
nonTerminating n.succ m.succ
|
||||
Cannot use parameter #2:
|
||||
failed to eliminate recursive application
|
||||
nonTerminating n.succ m.succ
|
||||
|
||||
argument #2 cannot be used for structural recursion
|
||||
failed to eliminate recursive application
|
||||
nonTerminating n.succ m.succ
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
@ -26,16 +25,17 @@ Please use `termination_by` to specify a decreasing measure.
|
|||
guessLexFailures.lean:20:4-20:15: error: fail to show termination for
|
||||
noArguments
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
failed to infer structural recursion:
|
||||
no parameters suitable for structural recursion
|
||||
|
||||
well-founded recursion cannot be used, 'noArguments' does not take any (non-fixed) arguments
|
||||
guessLexFailures.lean:22:4-22:23: error: fail to show termination for
|
||||
noNonFixedArguments
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Not considering parameter n of noNonFixedArguments:
|
||||
it is unchanged in the recursive calls
|
||||
no parameters suitable for structural recursion
|
||||
|
||||
well-founded recursion cannot be used, 'noNonFixedArguments' does not take any (non-fixed) arguments
|
||||
guessLexFailures.lean:27:0-33:31: error: Could not find a decreasing measure.
|
||||
|
|
@ -67,7 +67,17 @@ guessLexFailures.lean:59:6-59:7: error: fail to show termination for
|
|||
Mutual.g
|
||||
Mutual.h
|
||||
with errors
|
||||
mutual structural recursion requires explicit `termination_by` clauses
|
||||
failed to infer structural recursion:
|
||||
Not considering parameter fixed of Mutual.f:
|
||||
it is unchanged in the recursive calls
|
||||
Not considering parameter fixed of Mutual.g:
|
||||
it is unchanged in the recursive calls
|
||||
Not considering parameter H of Mutual.g:
|
||||
its type True does not have a recursor
|
||||
Not considering parameter fixed of Mutual.h:
|
||||
it is unchanged in the recursive calls
|
||||
Too many possible combinations of parameters of type Nat (or please indicate the recursive argument explicitly using `termination_by structural`).
|
||||
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
@ -109,15 +119,14 @@ Please use `termination_by` to specify a decreasing measure.
|
|||
guessLexFailures.lean:87:4-87:5: error: fail to show termination for
|
||||
DuplicatedCall.f
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Cannot use parameter #1:
|
||||
failed to eliminate recursive application
|
||||
DuplicatedCall.f (n + 2) (m + 1)
|
||||
Cannot use parameter #2:
|
||||
failed to eliminate recursive application
|
||||
DuplicatedCall.f (n + 2) (m + 1)
|
||||
|
||||
argument #2 cannot be used for structural recursion
|
||||
failed to eliminate recursive application
|
||||
DuplicatedCall.f (n + 2) (m + 1)
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
|
|||
|
|
@ -5,13 +5,14 @@ inductive A (n : Nat) : Type
|
|||
| b : A n → A n
|
||||
|
||||
/--
|
||||
error: its type is an inductive datatype
|
||||
A n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type is an inductive datatype
|
||||
A n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
-/
|
||||
#guard_msgs in
|
||||
def A.size (acc n : Nat) : A n → Nat
|
||||
|
|
@ -27,13 +28,14 @@ inductive Xn (e : Sigma.{0} (· → Type)) (α : Type) : Nat → Type where
|
|||
| mk2 {n} (s : e.1) (p : e.2 s → Xn e α n) : Xn e α n
|
||||
|
||||
/--
|
||||
error: its type is an inductive datatype
|
||||
Xn e (Xn e α n) m
|
||||
and the datatype parameter
|
||||
Xn e α n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type is an inductive datatype
|
||||
Xn e (Xn e α n) m
|
||||
and the datatype parameter
|
||||
Xn e α n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
-/
|
||||
#guard_msgs in
|
||||
def Xn.zip {e α m n} : Xn e (Xn e α n) m → Xn e α (n+m+1)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,13 @@
|
|||
import Lean.Elab.Command
|
||||
|
||||
/-!
|
||||
Mutual structural recursion.
|
||||
|
||||
In this file, we often attach a `termination_by structural` annotation to at least
|
||||
one of the functions to force structural recursion. We don't want lean to resort to
|
||||
well-founded recursion if structural recursion fails somehow.
|
||||
-/
|
||||
|
||||
mutual
|
||||
inductive A
|
||||
| self : A → A
|
||||
|
|
@ -19,11 +27,11 @@ def A.size : A → Nat
|
|||
| .other b => b.size + 1
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
|
||||
def B.size : B → Nat
|
||||
| .self b => b.size + 1
|
||||
| .other a => a.size + 1
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -87,7 +95,6 @@ def B.subs : (b : B) → (Fin b.size → A ⊕ B)
|
|||
| .self b => Fin.lastCases (.inr b) (b.subs)
|
||||
| .other a => Fin.lastCases (.inl a) (a.subs)
|
||||
| .empty => Fin.elim0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -103,7 +110,6 @@ def B.hasNoBEmpty : B → Prop
|
|||
| .self b => b.hasNoBEmpty
|
||||
| .other a => a.hasNoBEmpty
|
||||
| .empty => False
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
-- Mixing Prop and Nat.
|
||||
|
|
@ -122,7 +128,6 @@ def B.oddCount : B → Nat
|
|||
| .self b => b.oddCount + 1
|
||||
| .other a => if a.hasNoAEmpty then 0 else 1
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
-- Higher levels, but the same level `Type u`
|
||||
|
|
@ -138,7 +143,6 @@ def B.type.{u} : B → Type u
|
|||
| .self b => PUnit × b.type
|
||||
| .other a => PUnit × a.type
|
||||
| .empty => PUnit
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -162,7 +166,6 @@ def B.odderCount : B → Nat
|
|||
| .self b => b.odderCount + 1
|
||||
| .other a => if Nonempty a.strangeType then 0 else 1
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -191,7 +194,6 @@ def B.size (m n : Nat): B m n → Nat
|
|||
| .self b => b.size + m
|
||||
| .other a => a.size + m
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
mutual
|
||||
|
|
@ -204,7 +206,6 @@ theorem B.size_eq_index (m n : Nat) : (b : B m n) → b.size = n
|
|||
| .self b => by dsimp [B.size]; rw [B.size_eq_index]
|
||||
| .other a => by dsimp [B.size]; rw [A.size_eq_index]
|
||||
| .empty => rfl
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
end Index
|
||||
|
|
@ -223,7 +224,6 @@ mutual
|
|||
def Odd : Nat → Prop
|
||||
| 0 => False
|
||||
| n+1 => ¬ Even n
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
mutual
|
||||
|
|
@ -235,7 +235,6 @@ mutual
|
|||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => ! isEven n
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
theorem isEven_eq_2 (n : Nat) : isEven (n+1) = ! isOdd n := rfl
|
||||
|
|
@ -301,12 +300,10 @@ def A.weird_size2 : A → Nat
|
|||
| .self a => a.weird_size3 + 1
|
||||
| .other _ => 0
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
def A.weird_size3 : A → Nat
|
||||
| .self a => a.weird_size1 + 1
|
||||
| .other _ => 0
|
||||
| .empty => 0
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
-- We have equality
|
||||
|
|
@ -329,7 +326,10 @@ inductive Tree where
|
|||
|
||||
-- Nested recursion does not work (yet)
|
||||
|
||||
/-- error: its type NestedWithTuple.Tree is a nested inductive, which is not yet supported -/
|
||||
/--
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type NestedWithTuple.Tree is a nested inductive, which is not yet supported
|
||||
-/
|
||||
#guard_msgs in
|
||||
def Tree.size : Tree → Nat
|
||||
| leaf => 0
|
||||
|
|
@ -348,7 +348,9 @@ inductive A
|
|||
| empty
|
||||
|
||||
/--
|
||||
error: Cannot use structural mutual recursion: The recursive argument of DifferentTypes.A.with_nat is of type DifferentTypes.A, the recursive argument of DifferentTypes.Nat.foo is of type Nat, and these are not mutually recursive.
|
||||
error: failed to infer structural recursion:
|
||||
Skipping arguments of type A, as DifferentTypes.Nat.foo has no compatible argument.
|
||||
Skipping arguments of type Nat, as DifferentTypes.A.with_nat has no compatible argument.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
|
|
@ -359,7 +361,6 @@ termination_by structural x => x
|
|||
def Nat.foo : Nat → Nat
|
||||
| n+1 => Nat.foo n
|
||||
| 0 => A.empty.with_nat
|
||||
termination_by structural x => x
|
||||
end
|
||||
|
||||
end DifferentTypes
|
||||
|
|
@ -387,7 +388,6 @@ termination_by structural t => t
|
|||
def T.size2 (n : Nat) (start : Nat) : T n → Nat
|
||||
| .a => 0
|
||||
| .b t => 1 + T.size1 n start t
|
||||
termination_by structural t => t
|
||||
end
|
||||
|
||||
end Mutual
|
||||
|
|
@ -414,7 +414,6 @@ termination_by structural t => t
|
|||
|
||||
def B.size (n : Nat) (start : Nat) : B → Nat
|
||||
| .a a => 1 + A.size n start (a n)
|
||||
termination_by structural t => t
|
||||
end
|
||||
|
||||
end Mutual2
|
||||
|
|
@ -430,13 +429,14 @@ inductive B (n : Nat) : Type
|
|||
end
|
||||
|
||||
/--
|
||||
error: its type is an inductive datatype
|
||||
A n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type is an inductive datatype
|
||||
A n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
-/
|
||||
#guard_msgs in
|
||||
set_option linter.constructorNameAsVariable false in
|
||||
|
|
@ -448,14 +448,14 @@ termination_by structural t => t
|
|||
|
||||
def B.size (n : Nat) (m : Nat) : B m → Nat
|
||||
| .a a => 1 + A.size m n a
|
||||
termination_by structural t => t
|
||||
end
|
||||
|
||||
end Mutual3
|
||||
|
||||
/--
|
||||
error: its type FixedIndex.T is an inductive family and indices are not variables
|
||||
T 37
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type FixedIndex.T is an inductive family and indices are not variables
|
||||
T 37
|
||||
-/
|
||||
#guard_msgs in
|
||||
def T.size2 : T 37 → Nat
|
||||
|
|
@ -474,13 +474,14 @@ inductive T (n : Nat) : Nat → Type where
|
|||
| n : T n n → T n n
|
||||
|
||||
/--
|
||||
error: its type is an inductive datatype
|
||||
T n n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type is an inductive datatype
|
||||
T n n
|
||||
and the datatype parameter
|
||||
n
|
||||
depends on the function parameter
|
||||
n
|
||||
which does not come before the varying parameters and before the indices of the recursion parameter.
|
||||
-/
|
||||
#guard_msgs in
|
||||
def T.a (n : Nat) : T n n → Nat
|
||||
|
|
@ -502,9 +503,9 @@ inductive T (n : Nat) : Type where
|
|||
| n : T n → T n
|
||||
|
||||
/--
|
||||
error: The inductive type of the recursive parameter of DifferentParameters.T.a and DifferentParameters.T.b have different parameters:
|
||||
[23]
|
||||
[42]
|
||||
error: failed to infer structural recursion:
|
||||
Skipping arguments of type T 23, as DifferentParameters.T.b has no compatible argument.
|
||||
Skipping arguments of type T 42, as DifferentParameters.T.a has no compatible argument.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
|
|
@ -515,11 +516,79 @@ termination_by structural t => t
|
|||
def T.b : T 42 → Nat
|
||||
| .z => 0
|
||||
| .n t => t.b + 1 + T.a .z
|
||||
termination_by structural t => t
|
||||
end
|
||||
|
||||
end DifferentParameters
|
||||
|
||||
namespace ManyCombinations
|
||||
-- A datatype with no size function, to avoid well-founded recursion
|
||||
|
||||
inductive Nattish
|
||||
| zero
|
||||
| cons : (Nat → Nattish) → Nattish
|
||||
|
||||
/--
|
||||
error: fail to show termination for
|
||||
ManyCombinations.f
|
||||
ManyCombinations.g
|
||||
with errors
|
||||
failed to infer structural recursion:
|
||||
Too many possible combinations of parameters of type Nattish (or please indicate the recursive argument explicitly using `termination_by structural`).
|
||||
|
||||
|
||||
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 ManyCombinations.f to ManyCombinations.g at 571:15-29:
|
||||
#1 #2 #3 #4
|
||||
#5 ? ? ? ?
|
||||
#6 ? = ? ?
|
||||
#7 ? ? = ?
|
||||
#8 ? ? ? =
|
||||
Call from ManyCombinations.g to ManyCombinations.f at 574:15-29:
|
||||
#5 #6 #7 #8
|
||||
#1 _ _ _ _
|
||||
#2 _ = _ _
|
||||
#3 _ _ = _
|
||||
#4 _ _ _ =
|
||||
|
||||
|
||||
#1: sizeOf a
|
||||
#2: sizeOf b
|
||||
#3: sizeOf c
|
||||
#4: sizeOf d
|
||||
#5: sizeOf a
|
||||
#6: sizeOf b
|
||||
#7: sizeOf c
|
||||
#8: sizeOf d
|
||||
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
-/
|
||||
#guard_msgs in
|
||||
mutual
|
||||
def f (a b c d : Nattish) : Nat := match a with
|
||||
| .zero => 0
|
||||
| .cons n => g (n 23) b c d
|
||||
def g (a b c d : Nattish) : Nat := match a with
|
||||
| .zero => 0
|
||||
| .cons n => f (n 42) b c d
|
||||
end
|
||||
|
||||
-- specifying one `termination_by structural` helps
|
||||
|
||||
#guard_msgs in
|
||||
mutual
|
||||
def f' (a b c d : Nattish) : Nat := match a with
|
||||
| .zero => 0
|
||||
| .cons n => g' (n 23) b c d
|
||||
termination_by structural a
|
||||
def g' (a b c d : Nattish) : Nat := match a with
|
||||
| .zero => 0
|
||||
| .cons n => f' (n 42) b c d
|
||||
end
|
||||
|
||||
end ManyCombinations
|
||||
|
||||
namespace FunIndTests
|
||||
|
||||
-- FunInd does not handle mutual structural recursion yet, so make sure we error
|
||||
|
|
|
|||
|
|
@ -18,14 +18,18 @@ termination_by «structural»
|
|||
namespace Errors
|
||||
-- A few error conditions
|
||||
|
||||
/-- error: it is unchanged in the recursive calls -/
|
||||
/--
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
it is unchanged in the recursive calls
|
||||
-/
|
||||
#guard_msgs in
|
||||
def foo1 (n : Nat) : Nat := foo1 n
|
||||
termination_by structural n
|
||||
|
||||
/--
|
||||
error: its type Nat.le is an inductive family and indices are not variables
|
||||
n.succ.le 100
|
||||
error: cannot use specified parameter for structural recursion:
|
||||
its type Nat.le is an inductive family and indices are not variables
|
||||
n.succ.le 100
|
||||
-/
|
||||
#guard_msgs in
|
||||
def foo2 (n : Nat) (h : n < 100) : Nat := match n with
|
||||
|
|
@ -43,8 +47,10 @@ def foo3 (n : Nat) : Nat → Nat := match n with
|
|||
termination_by structural m => m
|
||||
|
||||
/--
|
||||
error: failed to eliminate recursive application
|
||||
ackermann (n + 1) m
|
||||
error: failed to infer structural recursion:
|
||||
Cannot use parameter n:
|
||||
failed to eliminate recursive application
|
||||
ackermann (n + 1) m
|
||||
-/
|
||||
#guard_msgs in
|
||||
def ackermann (n m : Nat) := match n, m with
|
||||
|
|
@ -54,8 +60,10 @@ def ackermann (n m : Nat) := match n, m with
|
|||
termination_by structural n
|
||||
|
||||
/--
|
||||
error: failed to eliminate recursive application
|
||||
ackermann2 n 1
|
||||
error: failed to infer structural recursion:
|
||||
Cannot use parameter m:
|
||||
failed to eliminate recursive application
|
||||
ackermann2 n 1
|
||||
-/
|
||||
#guard_msgs in
|
||||
def ackermann2 (n m : Nat) := match n, m with
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
sanitychecks.lean:1:8-1:15: error: fail to show termination for
|
||||
unsound
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
failed to infer structural recursion:
|
||||
no parameters suitable for structural recursion
|
||||
|
||||
well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments
|
||||
sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
|
||||
|
|
|
|||
|
|
@ -2,7 +2,11 @@ terminationFailure.lean:7:2-7:3: error: fail to show termination for
|
|||
f.g
|
||||
f
|
||||
with errors
|
||||
mutual structural recursion requires explicit `termination_by` clauses
|
||||
failed to infer structural recursion:
|
||||
Cannot use parameters #1 of f.g and x of f:
|
||||
failed to eliminate recursive application
|
||||
_root_.f x
|
||||
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
@ -22,12 +26,12 @@ f.g : Nat → Nat
|
|||
terminationFailure.lean:20:4-20:5: error: fail to show termination for
|
||||
h
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Cannot use parameter x:
|
||||
failed to eliminate recursive application
|
||||
h x
|
||||
|
||||
|
||||
failed to prove termination, possible solutions:
|
||||
- Use `have`-expressions to prove the remaining goals
|
||||
- Use `termination_by` to specify a different well-founded relation
|
||||
|
|
|
|||
|
|
@ -1,16 +1,15 @@
|
|||
wf1.lean:1:4-1:5: error: fail to show termination for
|
||||
g
|
||||
with errors
|
||||
structural recursion cannot be used:
|
||||
|
||||
argument #1 cannot be used for structural recursion
|
||||
failed to infer structural recursion:
|
||||
Cannot use parameter x:
|
||||
failed to eliminate recursive application
|
||||
g (x - 1)
|
||||
|
||||
argument #2 cannot be used for structural recursion
|
||||
Cannot use parameter y:
|
||||
insufficient number of parameters at recursive application
|
||||
g (x - 1)
|
||||
|
||||
|
||||
Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue