feat: per-function termination hints
This change * moves `termination_by` and `decreasing_by` next to the function they apply to * simplify the syntax of `termination_by` * apply the `decreasing_by` goal to all goals at once, for better interactive use. See the section in `RELEASES.md` for more details and migration advise. This is a hard breaking change, requiring developers to touch every `termination_by` in their code base. We decided to still do it as a hard-breaking change, because supporting both old and new syntax at the same time would be non-trivial, and not save that much. Moreover, this requires changes to some metaprograms that developers might have written, and supporting both syntaxes at the same time would make _their_ migration harder.
This commit is contained in:
Joachim Breitner
Sebastian Ullrich
parent
8bc1a9c4ba
commit
b5122b6a7b
98 changed files with 1222 additions and 809 deletions
131
RELEASES.md
131
RELEASES.md
|
|
@ -65,6 +65,133 @@ example : x + foo 2 = 12 + x := by
|
|||
simp_arith
|
||||
```
|
||||
|
||||
* The syntax of the `termination_by` and `decreasing_by` termination hints is overhauled:
|
||||
|
||||
* They are now placed directly after the function they apply to, instead of
|
||||
after the whole `mutual` block.
|
||||
* Therefore, the function name no longer has to be mentioned in the hint.
|
||||
* If the function has a `where` clause, the `termination_by` and
|
||||
`decreasing_by` for that function come before the `where`. The
|
||||
functions in the `where` clause can have their own termination hints, each
|
||||
following the corresponding definition.
|
||||
* The `termination_by` clause can only bind “extra parameters”, that are not
|
||||
already bound by the function header, but are bound in a lambda (`:= fun x
|
||||
y z =>`) or in patterns (`| x, n + 1 => …`). These extra parameters used to
|
||||
be understood as a suffix of the function parameters; now it is a prefix.
|
||||
|
||||
Migration guide: In simple cases just remove the function name, and any
|
||||
variables already bound at the header.
|
||||
```diff
|
||||
def foo : Nat → Nat → Nat := …
|
||||
-termination_by foo a b => a - b
|
||||
+termination_by a b => a - b
|
||||
```
|
||||
or
|
||||
```diff
|
||||
def foo : Nat → Nat → Nat := …
|
||||
-termination_by _ a b => a - b
|
||||
+termination_by a b => a - b
|
||||
```
|
||||
|
||||
If the parameters are bound in the function header (before the `:`), remove them as well:
|
||||
```diff
|
||||
def foo (a b : Nat) : Nat := …
|
||||
-termination_by foo a b => a - b
|
||||
+termination_by a - b
|
||||
```
|
||||
|
||||
Else, if there are multiple extra parameters, make sure to refer to the right
|
||||
ones; the bound variables are interpreted from left to right, no longer from
|
||||
right to left:
|
||||
```diff
|
||||
def foo : Nat → Nat → Nat → Nat
|
||||
| a, b, c => …
|
||||
-termination_by foo b c => b
|
||||
+termination_by a b => b
|
||||
```
|
||||
|
||||
In the case of a `mutual` block, place the termination arguments (without the
|
||||
function name) next to the function definition:
|
||||
```diff
|
||||
-mutual
|
||||
-def foo : Nat → Nat → Nat := …
|
||||
-def bar : Nat → Nat := …
|
||||
-end
|
||||
-termination_by
|
||||
- foo a b => a - b
|
||||
- bar a => a
|
||||
+mutual
|
||||
+def foo : Nat → Nat → Nat := …
|
||||
+termination_by a b => a - b
|
||||
+def bar : Nat → Nat := …
|
||||
+termination_by a => a
|
||||
+end
|
||||
```
|
||||
|
||||
Similarly, if you have (mutual) recursion through `where` or `let rec`, the
|
||||
termination hints are now placed directly after the function they apply to:
|
||||
```diff
|
||||
-def foo (a b : Nat) : Nat := …
|
||||
- where bar (x : Nat) : Nat := …
|
||||
-termination_by
|
||||
- foo a b => a - b
|
||||
- bar x => x
|
||||
+def foo (a b : Nat) : Nat := …
|
||||
+termination_by a - b
|
||||
+ where
|
||||
+ bar (x : Nat) : Nat := …
|
||||
+ termination_by x
|
||||
|
||||
-def foo (a b : Nat) : Nat :=
|
||||
- let rec bar (x : Nat) : Nat := …
|
||||
- …
|
||||
-termination_by
|
||||
- foo a b => a - b
|
||||
- bar x => x
|
||||
+def foo (a b : Nat) : Nat :=
|
||||
+ let rec bar (x : Nat) : Nat := …
|
||||
+ termination_by x
|
||||
+ …
|
||||
+termination_by a - b
|
||||
```
|
||||
|
||||
In cases where a single `decreasing_by` clause applied to multiple mutually
|
||||
recursive functions before, the tactic now has to be duplicated.
|
||||
|
||||
* The semantics of `decreasing_by` changed; the tactic is applied to all
|
||||
termination proof goals together, not individually.
|
||||
|
||||
This helps when writing termination proofs interactively, as one can focus
|
||||
each subgoal individually, for example using `·`. Previously, the given
|
||||
tactic script had to work for _all_ goals, and one had to resort to tactic
|
||||
combinators like `first`:
|
||||
|
||||
```diff
|
||||
def foo (n : Nat) := … foo e1 … foo e2 …
|
||||
-decreasing_by
|
||||
-simp_wf
|
||||
-first | apply something_about_e1; …
|
||||
- | apply something_about_e2; …
|
||||
+decreasing_by
|
||||
+all_goals simp_wf
|
||||
+· apply something_about_e1; …
|
||||
+· apply something_about_e2; …
|
||||
```
|
||||
|
||||
To obtain the old behaviour of applying a tactic to each goal individually,
|
||||
use `all_goals`:
|
||||
```diff
|
||||
def foo (n : Nat) := …
|
||||
-decreasing_by some_tactic
|
||||
+decreasing_by all_goals some_tactic
|
||||
```
|
||||
|
||||
In the case of mutual recursion each `decreasing_by` now applies to just its
|
||||
function. If some functions in a recursive group do not have their own
|
||||
`decreasing_by`, the default `decreasing_tactic` is used. If the same tactic
|
||||
ought to be applied to multiple functions, the `decreasing_by` clause has to
|
||||
be repeated at each of these functions.
|
||||
|
||||
|
||||
v4.5.0
|
||||
---------
|
||||
|
|
@ -88,7 +215,7 @@ v4.5.0
|
|||
Migration guide: Use `termination_by` instead, e.g.:
|
||||
```diff
|
||||
-termination_by' measure (fun ⟨i, _⟩ => as.size - i)
|
||||
+termination_by go i _ => as.size - i
|
||||
+termination_by i _ => as.size - i
|
||||
```
|
||||
|
||||
If the well-founded relation you want to use is not the one that the
|
||||
|
|
@ -96,7 +223,7 @@ v4.5.0
|
|||
you can use `WellFounded.wrap` from the std libarary to explicitly give one:
|
||||
```diff
|
||||
-termination_by' ⟨r, hwf⟩
|
||||
+termination_by _ x => hwf.wrap x
|
||||
+termination_by x => hwf.wrap x
|
||||
```
|
||||
|
||||
* Support snippet edits in LSP `TextEdit`s. See `Lean.Lsp.SnippetString` for more details.
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ theorem List.palindrome_ind (motive : List α → Prop)
|
|||
have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
|
||||
have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
|
||||
this ▸ h₃ _ _ _ ih
|
||||
termination_by _ as => as.length
|
||||
termination_by as.length
|
||||
|
||||
/-!
|
||||
We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
|
|||
import Lean.Elab.Quotation.Precheck
|
||||
import Lean.Elab.Term
|
||||
import Lean.Elab.BindersUtil
|
||||
import Lean.Elab.PreDefinition.WF.TerminationHint
|
||||
|
||||
namespace Lean.Elab.Term
|
||||
open Meta
|
||||
|
|
@ -570,7 +571,8 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
|
|||
-/
|
||||
def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
|
||||
let matchAlts := matchAltsWhereDecls[0]
|
||||
let whereDeclsOpt := matchAltsWhereDecls[1]
|
||||
-- matchAltsWhereDecls[1] is the termination hints, collected elsewhere
|
||||
let whereDeclsOpt := matchAltsWhereDecls[2]
|
||||
let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
|
||||
match i with
|
||||
| 0 => do
|
||||
|
|
|
|||
|
|
@ -187,15 +187,6 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
|
|||
let v ← classInductiveSyntaxToView modifiers stx
|
||||
elabInductiveViews #[v]
|
||||
|
||||
def getTerminationHints (stx : Syntax) : TerminationHints :=
|
||||
let decl := stx[1]
|
||||
let k := decl.getKind
|
||||
if k == ``Parser.Command.def || k == ``Parser.Command.abbrev || k == ``Parser.Command.theorem || k == ``Parser.Command.instance then
|
||||
let args := decl.getArgs
|
||||
{ terminationBy? := args[args.size - 2]!.getOptional?, decreasingBy? := args[args.size - 1]!.getOptional? }
|
||||
else
|
||||
{}
|
||||
|
||||
@[builtin_command_elab declaration]
|
||||
def elabDeclaration : CommandElab := fun stx => do
|
||||
match (← liftMacroM <| expandDeclNamespace? stx) with
|
||||
|
|
@ -219,7 +210,7 @@ def elabDeclaration : CommandElab := fun stx => do
|
|||
let modifiers ← elabModifiers stx[0]
|
||||
elabStructure modifiers decl
|
||||
else if isDefLike decl then
|
||||
elabMutualDef #[stx] (getTerminationHints stx)
|
||||
elabMutualDef #[stx]
|
||||
else
|
||||
throwError "unexpected declaration"
|
||||
|
||||
|
|
@ -332,21 +323,10 @@ def expandMutualPreamble : Macro := fun stx =>
|
|||
|
||||
@[builtin_command_elab «mutual»]
|
||||
def elabMutual : CommandElab := fun stx => do
|
||||
let hints := { terminationBy? := stx[3].getOptional?, decreasingBy? := stx[4].getOptional? }
|
||||
if isMutualInductive stx then
|
||||
if let some bad := hints.terminationBy? then
|
||||
throwErrorAt bad "invalid 'termination_by' in mutually inductive datatype declaration"
|
||||
if let some bad := hints.decreasingBy? then
|
||||
throwErrorAt bad "invalid 'decreasing_by' in mutually inductive datatype declaration"
|
||||
elabMutualInductive stx[1].getArgs
|
||||
else if isMutualDef stx then
|
||||
for arg in stx[1].getArgs do
|
||||
let argHints := getTerminationHints arg
|
||||
if let some bad := argHints.terminationBy? then
|
||||
throwErrorAt bad "invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword"
|
||||
if let some bad := argHints.decreasingBy? then
|
||||
throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
|
||||
elabMutualDef stx[1].getArgs hints
|
||||
elabMutualDef stx[1].getArgs
|
||||
else
|
||||
throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
|
||||
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
|
|||
| some val => pure val
|
||||
| none =>
|
||||
let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
|
||||
pure <| mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
|
||||
`(Parser.Command.declValSimple| := $val)
|
||||
return {
|
||||
ref := stx, kind := DefKind.opaque, modifiers := modifiers,
|
||||
declId := stx[1], binders := binders, type? := some type, value := val
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ structure LetRecDeclView where
|
|||
type : Expr
|
||||
mvar : Expr -- auxiliary metavariable used to lift the 'let rec'
|
||||
valStx : Syntax
|
||||
termination : WF.TerminationHints
|
||||
|
||||
structure LetRecView where
|
||||
decls : Array LetRecDeclView
|
||||
|
|
@ -59,7 +60,9 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
|
|||
pure decl[4]
|
||||
else
|
||||
liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
|
||||
pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx : LetRecDeclView }
|
||||
let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
|
||||
pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
|
||||
termination : LetRecDeclView }
|
||||
else
|
||||
throwUnsupportedSyntax
|
||||
return { decls, body := letRec[3] }
|
||||
|
|
@ -91,18 +94,23 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
|
|||
throwError "'{view.declName}' has already been declared"
|
||||
let lctx ← getLCtx
|
||||
let localInstances ← getLocalInstances
|
||||
let toLift := views.mapIdx fun i view => {
|
||||
ref := view.ref
|
||||
fvarId := fvars[i]!.fvarId!
|
||||
attrs := view.attrs
|
||||
shortDeclName := view.shortDeclName
|
||||
declName := view.declName
|
||||
lctx
|
||||
localInstances
|
||||
type := view.type
|
||||
val := values[i]!
|
||||
mvarId := view.mvar.mvarId!
|
||||
: LetRecToLift }
|
||||
|
||||
let toLift ← views.mapIdxM fun i view => do
|
||||
let value := values[i]!
|
||||
let termination ← view.termination.checkVars view.binderIds.size value
|
||||
pure {
|
||||
ref := view.ref
|
||||
fvarId := fvars[i]!.fvarId!
|
||||
attrs := view.attrs
|
||||
shortDeclName := view.shortDeclName
|
||||
declName := view.declName
|
||||
lctx
|
||||
localInstances
|
||||
type := view.type
|
||||
val := value
|
||||
mvarId := view.mvar.mvarId!
|
||||
termination := termination
|
||||
: LetRecToLift }
|
||||
modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
|
||||
|
||||
@[builtin_term_elab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@ import Lean.Elab.Match
|
|||
import Lean.Elab.DefView
|
||||
import Lean.Elab.Deriving.Basic
|
||||
import Lean.Elab.PreDefinition.Main
|
||||
import Lean.Elab.PreDefinition.WF.TerminationHint
|
||||
import Lean.Elab.DeclarationRange
|
||||
|
||||
namespace Lean.Elab
|
||||
|
|
@ -221,14 +222,16 @@ private def expandWhereStructInst : Macro
|
|||
/-
|
||||
Recall that
|
||||
```
|
||||
def declValSimple := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
|
||||
def declValSimple := leading_parser " :=\n" >> termParser >> Termination.suffix >> optional Term.whereDecls
|
||||
def declValEqns := leading_parser Term.matchAltsWhereDecls
|
||||
def declVal := declValSimple <|> declValEqns <|> Term.whereDecls
|
||||
```
|
||||
|
||||
The `Termination.suffix` is ignored here, and extracted in `declValToTerminationHint`.
|
||||
-/
|
||||
private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal do
|
||||
if declVal.isOfKind ``Parser.Command.declValSimple then
|
||||
expandWhereDeclsOpt declVal[2] declVal[1]
|
||||
expandWhereDeclsOpt declVal[3] declVal[1]
|
||||
else if declVal.isOfKind ``Parser.Command.declValEqns then
|
||||
expandMatchAltsWhereDecls declVal[0]
|
||||
else if declVal.isOfKind ``Parser.Command.whereStructInst then
|
||||
|
|
@ -238,6 +241,15 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
|
|||
else
|
||||
Macro.throwErrorAt declVal "unexpected declaration body"
|
||||
|
||||
/-- Elaborates the termination hints in a `declVal` syntax. -/
|
||||
private def declValToTerminationHint (declVal : Syntax) : TermElabM WF.TerminationHints :=
|
||||
if declVal.isOfKind ``Parser.Command.declValSimple then
|
||||
WF.elabTerminationHints ⟨declVal[2]⟩
|
||||
else if declVal.isOfKind ``Parser.Command.declValEqns then
|
||||
WF.elabTerminationHints ⟨declVal[0][1]⟩
|
||||
else
|
||||
return .none
|
||||
|
||||
private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
|
||||
headers.mapM fun header => withDeclName header.declName <| withLevelNames header.levelNames do
|
||||
let valStx ← liftMacroM <| declValToTerm header.valueStx
|
||||
|
|
@ -629,6 +641,8 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
|
|||
: TermElabM (Array PreDefinition) :=
|
||||
mainHeaders.size.foldM (init := preDefs) fun i preDefs => do
|
||||
let header := mainHeaders[i]!
|
||||
let termination ← declValToTerminationHint header.valueStx
|
||||
let termination ← termination.checkVars header.numParams mainVals[i]!
|
||||
let value ← mkLambdaFVars sectionVars mainVals[i]!
|
||||
let type ← mkForallFVars sectionVars header.type
|
||||
return preDefs.push {
|
||||
|
|
@ -637,7 +651,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
|
|||
declName := header.declName
|
||||
levelParams := [], -- we set it later
|
||||
modifiers := header.modifiers
|
||||
type, value
|
||||
type, value, termination
|
||||
}
|
||||
|
||||
def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : MetaM (Array PreDefinition) :=
|
||||
|
|
@ -655,7 +669,8 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
|
|||
declName := c.toLift.declName
|
||||
levelParams := [] -- we set it later
|
||||
modifiers := { modifiers with attrs := c.toLift.attrs }
|
||||
kind, type, value
|
||||
kind, type, value,
|
||||
termination := c.toLift.termination
|
||||
}
|
||||
|
||||
def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
|
||||
|
|
@ -766,7 +781,7 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
|
|||
for preDef in preDefs do
|
||||
checkPreDef preDef
|
||||
|
||||
def elabMutualDef (vars : Array Expr) (views : Array DefView) (hints : TerminationHints) : TermElabM Unit :=
|
||||
def elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit :=
|
||||
if isExample views then
|
||||
withoutModifyingEnv do
|
||||
-- save correct environment in info tree
|
||||
|
|
@ -805,7 +820,7 @@ where
|
|||
for preDef in preDefs do
|
||||
trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}"
|
||||
checkForHiddenUnivLevels allUserLevelNames preDefs
|
||||
addPreDefinitions preDefs hints
|
||||
addPreDefinitions preDefs
|
||||
processDeriving headers
|
||||
|
||||
processDeriving (headers : Array DefViewElabHeader) := do
|
||||
|
|
@ -820,13 +835,13 @@ where
|
|||
end Term
|
||||
namespace Command
|
||||
|
||||
def elabMutualDef (ds : Array Syntax) (hints : TerminationHints) : CommandElabM Unit := do
|
||||
def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
|
||||
let views ← ds.mapM fun d => do
|
||||
let modifiers ← elabModifiers d[0]
|
||||
if ds.size > 1 && modifiers.isNonrec then
|
||||
throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
|
||||
mkDefView modifiers d[1]
|
||||
runTermElabM fun vars => Term.elabMutualDef vars views hints
|
||||
runTermElabM fun vars => Term.elabMutualDef vars views
|
||||
|
||||
end Command
|
||||
end Lean.Elab
|
||||
|
|
|
|||
|
|
@ -8,11 +8,13 @@ import Lean.Util.CollectLevelParams
|
|||
import Lean.Meta.AbstractNestedProofs
|
||||
import Lean.Elab.RecAppSyntax
|
||||
import Lean.Elab.DefView
|
||||
import Lean.Elab.PreDefinition.WF.TerminationHint
|
||||
|
||||
namespace Lean.Elab
|
||||
open Meta
|
||||
open Term
|
||||
|
||||
|
||||
/--
|
||||
A (potentially recursive) definition.
|
||||
The elaborator converts it into Kernel definitions using many different strategies.
|
||||
|
|
@ -25,6 +27,7 @@ structure PreDefinition where
|
|||
declName : Name
|
||||
type : Expr
|
||||
value : Expr
|
||||
termination : WF.TerminationHints
|
||||
deriving Inhabited
|
||||
|
||||
def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
|
||||
|
|
|
|||
|
|
@ -13,11 +13,6 @@ namespace Lean.Elab
|
|||
open Meta
|
||||
open Term
|
||||
|
||||
structure TerminationHints where
|
||||
terminationBy? : Option Syntax := none
|
||||
decreasingBy? : Option Syntax := none
|
||||
deriving Inhabited
|
||||
|
||||
private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := false) : TermElabM Unit := do
|
||||
for preDef in preDefs do
|
||||
trace[Elab.definition] "processing {preDef.declName}"
|
||||
|
|
@ -94,15 +89,12 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
|
|||
applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
|
||||
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
|
||||
|
||||
def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints) : TermElabM Unit := withLCtx {} {} do
|
||||
def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
|
||||
for preDef in preDefs do
|
||||
trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
|
||||
let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
|
||||
let preDefs ← betaReduceLetRecApps preDefs
|
||||
let cliques := partitionPreDefs preDefs
|
||||
let mut terminationBy ← liftMacroM <| WF.expandTerminationBy? hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
|
||||
let mut decreasingBy ← liftMacroM <| WF.expandDecreasingBy? hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
|
||||
let mut hasErrors := false
|
||||
for preDefs in cliques do
|
||||
trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
|
||||
if preDefs.size == 1 && isNonRecursive preDefs[0]! then
|
||||
|
|
@ -116,35 +108,31 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
|
|||
addNonRec preDef
|
||||
else
|
||||
addAndCompileNonRec preDef
|
||||
preDef.termination.ensureNone "not recursive"
|
||||
else if preDefs.any (·.modifiers.isUnsafe) then
|
||||
addAndCompileUnsafe preDefs
|
||||
preDefs.forM (·.termination.ensureNone "unsafe")
|
||||
else if preDefs.any (·.modifiers.isPartial) then
|
||||
for preDef in preDefs do
|
||||
if preDef.modifiers.isPartial && !(← whnfD preDef.type).isForall then
|
||||
withRef preDef.ref <| throwError "invalid use of 'partial', '{preDef.declName}' is not a function{indentExpr preDef.type}"
|
||||
addAndCompilePartial preDefs
|
||||
preDefs.forM (·.termination.ensureNone "partial")
|
||||
else
|
||||
try
|
||||
let mut wf? := none
|
||||
let mut decrTactic? := none
|
||||
if let some wf := terminationBy.find? (preDefs.map (·.declName)) then
|
||||
wf? := some wf
|
||||
terminationBy := terminationBy.markAsUsed (preDefs.map (·.declName))
|
||||
if let some { ref, value := decrTactic } := decreasingBy.find? (preDefs.map (·.declName)) then
|
||||
decrTactic? := some (← withRef ref `(by $(⟨decrTactic⟩)))
|
||||
decreasingBy := decreasingBy.markAsUsed (preDefs.map (·.declName))
|
||||
if wf?.isSome || decrTactic?.isSome then
|
||||
wfRecursion preDefs wf? decrTactic?
|
||||
let hasHints := preDefs.any fun preDef =>
|
||||
preDef.termination.decreasing_by?.isSome || preDef.termination.termination_by?.isSome
|
||||
if hasHints then
|
||||
wfRecursion preDefs
|
||||
else
|
||||
withRef (preDefs[0]!.ref) <| mapError
|
||||
(orelseMergeErrors
|
||||
(structuralRecursion preDefs)
|
||||
(wfRecursion preDefs none none))
|
||||
(wfRecursion preDefs))
|
||||
(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}")
|
||||
catch ex =>
|
||||
hasErrors := true
|
||||
logException ex
|
||||
let s ← saveState
|
||||
try
|
||||
|
|
@ -159,9 +147,6 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
|
|||
else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
|
||||
addAsAxioms preDefs
|
||||
catch _ => s.restore
|
||||
unless hasErrors do
|
||||
liftMacroM <| terminationBy.ensureAllUsed
|
||||
liftMacroM <| decreasingBy.ensureAllUsed
|
||||
|
||||
builtin_initialize
|
||||
registerTraceClass `Elab.definition.body
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@ 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
|
||||
|
|
@ -186,22 +187,48 @@ def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
|
|||
return (false, true)
|
||||
return (true, true)
|
||||
|
||||
def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
|
||||
/--
|
||||
The subgoals, created by `mkDecreasingProof`, are of the form `[data _recApp: rel arg param]`, where
|
||||
`param` is the `PackMutual`'ed parameter of the current function, and thus we can peek at that to
|
||||
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
|
||||
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
|
||||
r := r.modify funidx (·.push goal)
|
||||
return r
|
||||
|
||||
def solveDecreasingGoals (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
|
||||
let goals ← getMVarsNoDelayed value
|
||||
let goals ← assignSubsumed goals
|
||||
goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
|
||||
let goalss ← groupGoalsByFunction decrTactics.size goals
|
||||
for goals in goalss, decrTactic? in decrTactics do
|
||||
Lean.Elab.Term.TermElabM.run' do
|
||||
match decrTactic? with
|
||||
| none => do
|
||||
let some ref := getRecAppSyntax? (← goal.getType)
|
||||
| throwError "MVar does not look like like a recursive call"
|
||||
for goal in goals do
|
||||
let some ref := getRecAppSyntax? (← goal.getType)
|
||||
| throwError "MVar does not look like like a recursive call"
|
||||
withRef ref <| applyDefaultDecrTactic goal
|
||||
| some decrTactic => do
|
||||
-- make info from `runTactic` available
|
||||
pushInfoTree (.hole goal)
|
||||
Term.runTactic goal decrTactic
|
||||
| some decrTactic => withRef decrTactic.ref do
|
||||
unless goals.isEmpty do -- unlikely to be empty
|
||||
-- make info from `runTactic` available
|
||||
goals.forM fun goal => pushInfoTree (.hole goal)
|
||||
let remainingGoals ← Tactic.run goals[0]! do
|
||||
Tactic.setGoals goals.toList
|
||||
Tactic.withTacticInfoContext decrTactic.ref do
|
||||
Tactic.evalTactic decrTactic.tactic
|
||||
unless remainingGoals.isEmpty do
|
||||
Term.reportUnsolvedGoals remainingGoals
|
||||
instantiateMVars value
|
||||
|
||||
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
|
||||
def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (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]!
|
||||
|
|
@ -224,7 +251,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (dec
|
|||
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 decrTactic? val
|
||||
let val ← solveDecreasingGoals decrTactics val
|
||||
mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
|
||||
|
||||
end Lean.Elab.WF
|
||||
|
|
|
|||
|
|
@ -72,27 +72,42 @@ register_builtin_option showInferredTerminationBy : Bool := {
|
|||
descr := "In recursive definitions, show the inferred `termination_by` measure."
|
||||
}
|
||||
|
||||
|
||||
/--
|
||||
Given a predefinition, find good variable names for its parameters.
|
||||
Use user-given parameter names if present; use x1...xn otherwise.
|
||||
Given a predefinition, return the variabe names in the outermost lambdas.
|
||||
Includes the “fixed prefix”.
|
||||
|
||||
The length of the returned array is also used to determine the arity
|
||||
of the function, so it should match what `packDomain` does.
|
||||
-/
|
||||
def originalVarNames (preDef : PreDefinition) : MetaM (Array Name) := do
|
||||
lambdaTelescope preDef.value fun xs _ => xs.mapM (·.fvarId!.getUserName)
|
||||
|
||||
The names ought to accessible (no macro scopes) and still fresh wrt to the current environment,
|
||||
/--
|
||||
Given the original paramter names from `originalVarNames`, remove the fixed prefix and 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,
|
||||
so that with `showInferredTerminationBy` we can print them to the user reliably.
|
||||
We do that by appending `'` as needed.
|
||||
|
||||
It is possible (but unlikely without malice) that some of the user-given names
|
||||
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) (preDef : PreDefinition) : MetaM (Array Name):= do
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
let xs := xs.extract fixedPrefixSize xs.size
|
||||
let mut ns : Array Name := #[]
|
||||
for h : i in [:xs.size] do
|
||||
let n ← xs[i].fvarId!.getUserName
|
||||
let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
|
||||
ns := ns.push (← freshen ns n)
|
||||
return ns
|
||||
def naryVarNames (fixedPrefixSize : Nat) (xs : Array Name) : MetaM (Array Name) := do
|
||||
let xs := xs.extract fixedPrefixSize xs.size
|
||||
let mut ns : Array Name := #[]
|
||||
for h : i in [:xs.size] do
|
||||
let n := xs[i]
|
||||
let n ← if n.hasMacroScopes then
|
||||
freshen ns (.mkSimple s!"x{i+1}")
|
||||
else
|
||||
pure n
|
||||
ns := ns.push n
|
||||
return ns
|
||||
where
|
||||
freshen (ns : Array Name) (n : Name): MetaM Name := do
|
||||
if !(ns.elem n) && (← resolveGlobalName n).isEmpty then
|
||||
|
|
@ -274,7 +289,6 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
|
|||
unless xs.size == fixedPrefixSize + 1 do
|
||||
-- Maybe cleaner to have lambdaBoundedTelescope?
|
||||
throwError "Unexpected number of lambdas in unary pre-definition"
|
||||
-- trace[Elab.definition.wf] "collectRecCalls: {xs} {body}"
|
||||
let param := xs[fixedPrefixSize]!
|
||||
withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
|
||||
unless args.size ≥ fixedPrefixSize + 1 do
|
||||
|
|
@ -318,7 +332,7 @@ def mkSizeOf (e : Expr) : MetaM Expr := do
|
|||
For a given recursive call, and a choice of parameter and argument index,
|
||||
try to prove equality, < or ≤.
|
||||
-/
|
||||
def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
|
||||
def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext) (paramIdx argIdx : Nat) :
|
||||
MetaM GuessLexRel := do
|
||||
rcc.ctxt.run do
|
||||
let param := rcc.params[paramIdx]!
|
||||
|
|
@ -334,25 +348,20 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramI
|
|||
let mvar ← mkFreshExprSyntheticOpaqueMVar goalExpr
|
||||
let mvarId := mvar.mvarId!
|
||||
let mvarId ← mvarId.cleanup
|
||||
-- logInfo m!"Remaining goals: {goalsToMessageData [mvarId]}"
|
||||
try
|
||||
if rel = .eq then
|
||||
MVarId.refl mvarId
|
||||
else do
|
||||
Lean.Elab.Term.TermElabM.run' do
|
||||
match decrTactic? with
|
||||
| none =>
|
||||
let remainingGoals ← Tactic.run mvarId do
|
||||
Tactic.evalTactic (← `(tactic| decreasing_tactic))
|
||||
remainingGoals.forM fun mvarId => Term.reportUnsolvedGoals [mvarId]
|
||||
-- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}"
|
||||
pure ()
|
||||
| some decrTactic => Term.withoutErrToSorry do
|
||||
-- make info from `runTactic` available
|
||||
pushInfoTree (.hole mvarId)
|
||||
Term.runTactic mvarId decrTactic
|
||||
-- trace[Elab.definition.wf] "Found {rel} proof: {← instantiateMVars mvar}"
|
||||
pure ()
|
||||
Lean.Elab.Term.TermElabM.run' do Term.withoutErrToSorry do
|
||||
let remainingGoals ← Tactic.run mvarId do Tactic.withoutRecover do
|
||||
let tacticStx : Syntax ←
|
||||
match decrTactic? with
|
||||
| none => pure (← `(tactic| decreasing_tactic)).raw
|
||||
| some decrTactic =>
|
||||
trace[Elab.definition.wf] "Using tactic {decrTactic.tactic.raw}"
|
||||
pure decrTactic.tactic.raw
|
||||
Tactic.evalTactic tacticStx
|
||||
remainingGoals.forM fun _ => throwError "goal not solved"
|
||||
trace[Elab.definition.wf] "inspectRecCall: success!"
|
||||
return rel
|
||||
catch _e =>
|
||||
|
|
@ -362,13 +371,15 @@ def evalRecCall (decrTactic? : Option Syntax) (rcc : RecCallWithContext) (paramI
|
|||
|
||||
/- A cache for `evalRecCall` -/
|
||||
structure RecCallCache where mk'' ::
|
||||
decrTactic? : Option Syntax
|
||||
decrTactic? : Option DecreasingBy
|
||||
rcc : RecCallWithContext
|
||||
cache : IO.Ref (Array (Array (Option GuessLexRel)))
|
||||
|
||||
/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
|
||||
def RecCallCache.mk (decrTactic? : Option Syntax) (rcc : RecCallWithContext) :
|
||||
def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
|
||||
(rcc : RecCallWithContext) :
|
||||
BaseIO RecCallCache := do
|
||||
let decrTactic? := decrTactics[rcc.caller]!
|
||||
let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
|
||||
return { decrTactic?, rcc, cache }
|
||||
|
||||
|
|
@ -536,29 +547,46 @@ def mkTupleSyntax : Array Term → MetaM Term
|
|||
|
||||
/--
|
||||
Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
|
||||
combination of these measures.
|
||||
combination of these measures. The parameters are
|
||||
|
||||
* `originalVarNamess`: For each function in the clique, the original parameter names, _including_
|
||||
the fixed prefix. Used to determine if we need to fully qualify `sizeOf`.
|
||||
* `varNamess`: For each function in the clique, the parameter names to be used in the
|
||||
termination relation. Excludes the fixed prefix. Includes names like `x1` for unnamed parameters.
|
||||
* `measures`: The measures to be used.
|
||||
-/
|
||||
def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
|
||||
(measures : Array MutualMeasure) : MetaM TerminationWF := do
|
||||
let mut termByElements := #[]
|
||||
for h : funIdx in [:varNamess.size] do
|
||||
let vars := varNamess[funIdx].map mkIdent
|
||||
let body ← mkTupleSyntax (← measures.mapM fun
|
||||
def buildTermWF (originalVarNamess : Array (Array Name)) (varNamess : Array (Array Name))
|
||||
(measures : Array MutualMeasure) : MetaM TerminationWF := do
|
||||
varNamess.mapIdxM fun funIdx varNames => do
|
||||
let idents := varNames.map mkIdent
|
||||
let measureStxs ← measures.mapM fun
|
||||
| .args varIdxs => do
|
||||
let v := vars.get! varIdxs[funIdx]!
|
||||
let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
|
||||
let varIdx := varIdxs[funIdx]!
|
||||
let v := idents[varIdx]!
|
||||
-- Print `sizeOf` as such, unless it is shadowed.
|
||||
-- Shadowing by a `def` in the current namespace is handled by `unresolveNameGlobal`.
|
||||
-- But it could also be shadowed by an earlier parameter (including the fixed prefix),
|
||||
-- so look for unqualified (single tick) occurrences in `originalVarNames`
|
||||
let sizeOfIdent :=
|
||||
if originalVarNamess[funIdx]!.any (· = `sizeOf) then
|
||||
mkIdent ``sizeOf -- fully qualified
|
||||
else
|
||||
mkIdent (← unresolveNameGlobal ``sizeOf)
|
||||
`($sizeOfIdent $v)
|
||||
| .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
|
||||
)
|
||||
let declName := declNames[funIdx]!
|
||||
|
||||
termByElements := termByElements.push
|
||||
{ ref := .missing
|
||||
declName, vars, body,
|
||||
implicit := true
|
||||
}
|
||||
return termByElements
|
||||
let body ← mkTupleSyntax measureStxs
|
||||
return { ref := .missing, vars := idents, body }
|
||||
|
||||
/--
|
||||
The TerminationWF produced by GuessLex may mention more variables than allowed in the surface
|
||||
syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid
|
||||
syntax with more information, or valid syntax with (possibly) unresolved variable names?
|
||||
The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so
|
||||
we do that.
|
||||
-/
|
||||
def trimTermWF (extraParams : Array Nat) (elems : TerminationWF) : TerminationWF :=
|
||||
elems.mapIdx fun funIdx elem =>
|
||||
{ elem with vars := elem.vars[elem.vars.size - extraParams[funIdx]! : elem.vars.size] }
|
||||
|
||||
/--
|
||||
Given a matrix (row-major) of strings, arranges them in tabular form.
|
||||
|
|
@ -668,10 +696,12 @@ Main entry point of this module:
|
|||
Try to find a lexicographic ordering of the arguments for which the recursive definition
|
||||
terminates. See the module doc string for a high-level overview.
|
||||
-/
|
||||
def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
|
||||
(fixedPrefixSize : Nat) (decrTactic? : Option Syntax) :
|
||||
def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
|
||||
(fixedPrefixSize : Nat) :
|
||||
MetaM TerminationWF := do
|
||||
let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
|
||||
let extraParamss := preDefs.map (·.termination.extraParams)
|
||||
let originalVarNamess ← preDefs.mapM originalVarNames
|
||||
let varNamess ← originalVarNamess.mapM (naryVarNames fixedPrefixSize ·)
|
||||
let arities := varNamess.map (·.size)
|
||||
trace[Elab.definition.wf] "varNames is: {varNamess}"
|
||||
|
||||
|
|
@ -684,24 +714,22 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
|
|||
|
||||
-- If there is only one plausible measure, use that
|
||||
if let #[solution] := measures then
|
||||
return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
|
||||
return ← buildTermWF originalVarNamess varNamess #[solution]
|
||||
|
||||
-- Collect all recursive calls and extract their context
|
||||
let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
|
||||
let recCalls := filterSubsumed recCalls
|
||||
let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
|
||||
let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasing_by?)) ·)
|
||||
let callMatrix := rcs.map (inspectCall ·)
|
||||
|
||||
match ← liftMetaM <| solve measures callMatrix with
|
||||
| .some solution => do
|
||||
let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
|
||||
|
||||
let wfStx ← withoutModifyingState do
|
||||
preDefs.forM (addAsAxiom ·)
|
||||
wf.unexpand
|
||||
let wf ← buildTermWF originalVarNamess varNamess solution
|
||||
|
||||
if showInferredTerminationBy.get (← getOptions) then
|
||||
logInfo m!"Inferred termination argument:{wfStx}"
|
||||
let wf' := trimTermWF extraParamss wf
|
||||
for preDef in preDefs, term in wf' do
|
||||
logInfoAt preDef.ref m!"Inferred termination argument: {← term.unexpand}"
|
||||
|
||||
return wf
|
||||
| .none =>
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize :
|
|||
else
|
||||
return false
|
||||
|
||||
def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (decrTactic? : Option Syntax) : TermElabM Unit := do
|
||||
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
|
||||
for preDef in preDefs do
|
||||
|
|
@ -91,20 +91,29 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
|
|||
let unaryPreDefs ← packDomain fixedPrefixSize preDefsDIte
|
||||
return (← packMutual fixedPrefixSize preDefs unaryPreDefs, fixedPrefixSize)
|
||||
|
||||
let wf ←
|
||||
if let .some wf := wf? then
|
||||
pure wf
|
||||
let extraParamss := preDefs.map (·.termination.extraParams)
|
||||
let wf ← do
|
||||
let (preDefsWith, preDefsWithout) := preDefs.partition (·.termination.termination_by?.isSome)
|
||||
if preDefsWith.isEmpty then
|
||||
-- No termination_by anywhere, so guess one
|
||||
guessLex preDefs unaryPreDef fixedPrefixSize
|
||||
else if preDefsWithout.isEmpty then
|
||||
pure <| preDefsWith.map (·.termination.termination_by?.get!)
|
||||
else
|
||||
guessLex preDefs unaryPreDef fixedPrefixSize decrTactic?
|
||||
-- Some have, some do not, so report errors
|
||||
preDefsWithout.forM fun preDef => do
|
||||
logErrorAt preDef.ref (m!"Missing `termination_by`; this function is mutually " ++
|
||||
m!"recursive with {preDefsWith[0]!.declName}, which has a `termination_by` clause.")
|
||||
return
|
||||
|
||||
let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
|
||||
let type ← whnfForall type
|
||||
let packedArgType := type.bindingDomain!
|
||||
elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf fun wfRel => do
|
||||
elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType extraParamss wf fun wfRel => do
|
||||
trace[Elab.definition.wf] "wfRel: {wfRel}"
|
||||
let (value, envNew) ← withoutModifyingEnv' do
|
||||
addAsAxiom unaryPreDef
|
||||
let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
|
||||
let value ← mkFix unaryPreDef prefixArgs wfRel (preDefs.map (·.termination.decreasing_by?))
|
||||
eraseRecAppSyntaxExpr value
|
||||
/- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
|
||||
let value ← unfoldDeclsFrom envNew value
|
||||
|
|
|
|||
|
|
@ -14,12 +14,6 @@ namespace Lean.Elab.WF
|
|||
open Meta
|
||||
open Term
|
||||
|
||||
private def getRefFromElems (elems : Array TerminationByElement) : Syntax := Id.run do
|
||||
for elem in elems do
|
||||
if !elem.implicit then
|
||||
return elem.ref
|
||||
return elems[0]!.ref
|
||||
|
||||
private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarId) (fvarId : FVarId) : TermElabM (Array (FVarId × MVarId)) := do
|
||||
let rec go (i : Nat) (mvarId : MVarId) (fvarId : FVarId) (result : Array (FVarId × MVarId)) : TermElabM (Array (FVarId × MVarId)) := do
|
||||
if i < preDefs.size - 1 then
|
||||
|
|
@ -29,7 +23,13 @@ private partial def unpackMutual (preDefs : Array PreDefinition) (mvarId : MVarI
|
|||
return result.push (fvarId, mvarId)
|
||||
go 0 mvarId fvarId #[]
|
||||
|
||||
private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId) (fvarId : FVarId) (element : TerminationByElement) : TermElabM MVarId := do
|
||||
private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mvarId : MVarId)
|
||||
(fvarId : FVarId) (extraParams : Nat) (element : TerminationBy) : TermElabM MVarId := do
|
||||
-- If elements.vars is ≤ extraParams, this is user-provided, and should be interpreted
|
||||
-- as left to right. Else it is provided by GuessLex, and may rename non-extra paramters as well.
|
||||
-- (Not pretty, but it works for now)
|
||||
let implicit_underscores :=
|
||||
if element.vars.size < extraParams then extraParams - element.vars.size else 0
|
||||
let varNames ← lambdaTelescope preDef.value fun xs _ => do
|
||||
let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
|
||||
if element.vars.size > varNames.size then
|
||||
|
|
@ -37,7 +37,8 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
|
|||
for h : i in [:element.vars.size] do
|
||||
let varStx := element.vars[i]
|
||||
if let `($ident:ident) := varStx then
|
||||
varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
|
||||
let j := varNames.size - implicit_underscores - element.vars.size + i
|
||||
varNames := varNames.set! j ident.getId
|
||||
return varNames
|
||||
let mut mvarId := mvarId
|
||||
for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
|
||||
|
|
@ -54,19 +55,19 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
|
|||
go 0 mvarId fvarId
|
||||
|
||||
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat)
|
||||
(argType : Expr) (wf : TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
|
||||
(argType : Expr) (extraParamss : Array Nat) (wf : TerminationWF) (k : Expr → TermElabM α) :
|
||||
TermElabM α := do
|
||||
let α := argType
|
||||
let u ← getLevel α
|
||||
let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
|
||||
trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
|
||||
withDeclName unaryPreDefName do
|
||||
withRef (getRefFromElems wf) do
|
||||
let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
|
||||
let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
|
||||
let (d, fMVarId) ← fMVarId.intro1
|
||||
let subgoals ← unpackMutual preDefs fMVarId d
|
||||
for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
|
||||
let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
|
||||
for (d, mvarId) in subgoals, extraParams in extraParamss, element in wf, preDef in preDefs do
|
||||
let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d extraParams element
|
||||
mvarId.withContext do
|
||||
let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
|
||||
mvarId.assign value
|
||||
|
|
|
|||
|
|
@ -1,213 +1,113 @@
|
|||
/-
|
||||
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
Authors: Leonardo de Moura, Joachim Breitner
|
||||
-/
|
||||
import Lean.Parser.Command
|
||||
import Lean.Parser.Term
|
||||
|
||||
set_option autoImplicit false
|
||||
|
||||
namespace Lean.Elab.WF
|
||||
|
||||
/-! # Support for `decreasing_by` -/
|
||||
|
||||
structure DecreasingByTactic where
|
||||
ref : Syntax
|
||||
value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
|
||||
deriving Inhabited
|
||||
|
||||
inductive DecreasingBy where
|
||||
| none
|
||||
| one (val : DecreasingByTactic)
|
||||
| many (map : NameMap DecreasingByTactic)
|
||||
deriving Inhabited
|
||||
|
||||
open Parser.Command in
|
||||
/--
|
||||
This function takes a user-specified `decreasing_by` clause (as `Sytnax`).
|
||||
If it is a `decreasingByMany` (a set of clauses guarded by the function name) then
|
||||
* checks that all mentioned names exist in the current declaration
|
||||
* check that at most one function from each clique is mentioned
|
||||
and sort the entries by function name.
|
||||
-/
|
||||
def expandDecreasingBy? (decreasingBy? : Option Syntax) (cliques : Array (Array Name)) : MacroM DecreasingBy := do
|
||||
let some decreasingBy := decreasingBy? | return DecreasingBy.none
|
||||
let ref := decreasingBy
|
||||
match decreasingBy with
|
||||
| `(decreasingBy|decreasing_by $hint1:tacticSeq) =>
|
||||
return DecreasingBy.one { ref, value := hint1 }
|
||||
| `(decreasingBy|decreasing_by $hints:decreasingByMany) => do
|
||||
let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => do
|
||||
let arg : TSyntax `decreasingByElement := ⟨arg⟩ -- cannot use syntax pattern match with lookahead
|
||||
let `(decreasingByElement| $declId:ident => $tac:tacticSeq) := arg | Macro.throwUnsupported
|
||||
let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
|
||||
if declId.getId.isSuffixOf declName then some declName else none
|
||||
match declName? with
|
||||
| none => Macro.throwErrorAt declId s!"function '{declId.getId}' not found in current declaration"
|
||||
| some declName => return m.insert declName { ref := arg, value := tac }
|
||||
for clique in cliques do
|
||||
let mut found? := Option.none
|
||||
for declName in clique do
|
||||
if let some { ref, .. } := m.find? declName then
|
||||
if let some found := found? then
|
||||
Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
|
||||
found? := some declName
|
||||
return DecreasingBy.many m
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
|
||||
match t with
|
||||
| DecreasingBy.none => DecreasingBy.none
|
||||
| DecreasingBy.one .. => DecreasingBy.none
|
||||
| DecreasingBy.many m => Id.run do
|
||||
for declName in clique do
|
||||
if m.contains declName then
|
||||
let m := m.erase declName
|
||||
if m.isEmpty then
|
||||
return DecreasingBy.none
|
||||
else
|
||||
return DecreasingBy.many m
|
||||
return t
|
||||
|
||||
def DecreasingBy.find? (t : DecreasingBy) (clique : Array Name) : Option DecreasingByTactic :=
|
||||
match t with
|
||||
| DecreasingBy.none => Option.none
|
||||
| DecreasingBy.one v => some v
|
||||
| DecreasingBy.many m => clique.findSome? m.find?
|
||||
|
||||
def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
|
||||
match t with
|
||||
| DecreasingBy.one v => Macro.throwErrorAt v.ref "unused termination hint element"
|
||||
| DecreasingBy.many m => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
|
||||
| _ => pure ()
|
||||
|
||||
/-! # Support for `termination_by` notation -/
|
||||
|
||||
/-- A single `termination_by` clause -/
|
||||
structure TerminationByElement where
|
||||
structure TerminationBy where
|
||||
ref : Syntax
|
||||
declName : Name
|
||||
vars : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
|
||||
body : Term
|
||||
implicit : Bool
|
||||
deriving Inhabited
|
||||
|
||||
/-- `termination_by` clauses, grouped by clique -/
|
||||
structure TerminationByClique where
|
||||
elements : Array TerminationByElement
|
||||
used : Bool := false
|
||||
open Parser.Termination in
|
||||
def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
|
||||
-- TODO: Why can I not just use $wf.vars in the quotation below?
|
||||
let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
|
||||
if vars.isEmpty then
|
||||
`(terminationBy|termination_by $wf.body)
|
||||
else
|
||||
`(terminationBy|termination_by $vars* => $wf.body)
|
||||
|
||||
/--
|
||||
A `termination_by` hint, as specified by the user
|
||||
-/
|
||||
structure TerminationBy where
|
||||
cliques : Array TerminationByClique
|
||||
/-- A complete set of `termination_by` hints, as applicable to a single clique. -/
|
||||
abbrev TerminationWF := Array TerminationBy
|
||||
|
||||
/-- A single `decreasing_by` clause -/
|
||||
structure DecreasingBy where
|
||||
ref : Syntax
|
||||
tactic : TSyntax ``Lean.Parser.Tactic.tacticSeq
|
||||
deriving Inhabited
|
||||
|
||||
/-- The termination annotations for a single function.
|
||||
For `decreasing_by`, we store the whole `decreasing_by tacticSeq` expression, as this
|
||||
is what `Term.runTactic` expects.
|
||||
-/
|
||||
structure TerminationHints where
|
||||
ref : Syntax
|
||||
termination_by? : Option TerminationBy
|
||||
decreasing_by? : Option DecreasingBy
|
||||
/-- Here we record the number of parameters past the `:`. This is
|
||||
* `GuessLex` when there is no `termination_by` annotation, so that
|
||||
we can print the guessed order in the right form.
|
||||
* If there are fewer variables in the `termination_by` annotation than there are extra
|
||||
parameters, we know which parameters they should apply to.
|
||||
|
||||
It it set in `TerminationHints.checkVars`, which is the place where we also check that the user
|
||||
does not bind more extra parameters than present in the predefinition.
|
||||
-/
|
||||
extraParams : Nat
|
||||
deriving Inhabited
|
||||
|
||||
def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, 0⟩
|
||||
|
||||
/-- Logs warnings when the `TerminationHints` are present. -/
|
||||
def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): CoreM Unit := do
|
||||
match hints.termination_by?, hints.decreasing_by? with
|
||||
| .none, .none => pure ()
|
||||
| .none, .some dec_by =>
|
||||
logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
|
||||
| .some term_by, .none =>
|
||||
logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
|
||||
| .some _, .some _ =>
|
||||
logErrorAt hints.ref m!"unused termination hints, function is {reason}"
|
||||
|
||||
/--
|
||||
A `termination_by` hint, as applicable to a single clique
|
||||
Checks that `termination_by` binds at most as many variables are present in the outermost
|
||||
lambda of `value`, and logs (without failing) appropriate errors.
|
||||
|
||||
Also remembers `extraParams` for later use.
|
||||
-/
|
||||
abbrev TerminationWF := Array TerminationByElement
|
||||
def TerminationHints.checkVars (headerParams : Nat) (hints : TerminationHints) (value : Expr) :
|
||||
MetaM TerminationHints := do
|
||||
let extraParams := value.getNumHeadLambdas - headerParams
|
||||
if let .some tb := hints.termination_by? then
|
||||
if tb.vars.size > extraParams then
|
||||
logErrorAt tb.ref <| m!"Too many extra parameters bound; the function definition only " ++
|
||||
m!"has {extraParams} extra parameters."
|
||||
return { hints with extraParams := extraParams }
|
||||
|
||||
open Parser.Command in
|
||||
/--
|
||||
Expands the syntax for a `termination_by` clause, checking that
|
||||
* each function is mentioned once
|
||||
* each function mentioned actually occurs in the current declaration
|
||||
* if anything is specified, then all functions have a clause
|
||||
* the else-case (`_`) occurs only once, and only when needed
|
||||
open Parser.Termination
|
||||
|
||||
NB:
|
||||
```
|
||||
def terminationByElement := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
|
||||
def terminationBy := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
|
||||
```
|
||||
-/
|
||||
def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name)) :
|
||||
MacroM TerminationBy := do
|
||||
let some hint := hint? | return { cliques := #[] }
|
||||
let `(terminationBy|termination_by $elementStxs*) := hint | Macro.throwUnsupported
|
||||
let mut alreadyFound : NameSet := {}
|
||||
let mut elseElemStx? := none
|
||||
for elementStx in elementStxs do
|
||||
match elementStx with
|
||||
| `(terminationByElement|$ident:ident $_* => $_) =>
|
||||
let declSuffix := ident.getId
|
||||
if alreadyFound.contains declSuffix then
|
||||
withRef elementStx <| Macro.throwError s!"invalid `termination_by` syntax, `{declSuffix}` case has already been provided"
|
||||
alreadyFound := alreadyFound.insert declSuffix
|
||||
if cliques.all fun clique => clique.all fun declName => !declSuffix.isSuffixOf declName then
|
||||
withRef elementStx <| Macro.throwError s!"function '{declSuffix}' not found in current declaration"
|
||||
| `(terminationByElement|_ $_vars* => $_term) =>
|
||||
if elseElemStx?.isSome then
|
||||
withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified"
|
||||
else
|
||||
elseElemStx? := some elementStx
|
||||
| _ => Macro.throwUnsupported
|
||||
let toElement (declName : Name) (elementStx : TSyntax ``terminationByElement) : TerminationByElement :=
|
||||
match elementStx with
|
||||
| `(terminationByElement|$ioh $vars* => $body:term) =>
|
||||
let implicit := !ioh.raw.isIdent
|
||||
{ ref := elementStx, declName, vars, implicit, body }
|
||||
| _ => unreachable!
|
||||
let elementAppliesTo (declName : Name) : TSyntax ``terminationByElement → Bool
|
||||
| `(terminationByElement|$ident:ident $_* => $_) => ident.getId.isSuffixOf declName
|
||||
| _ => false
|
||||
let mut result := #[]
|
||||
let mut usedElse := false
|
||||
for clique in cliques do
|
||||
let mut elements := #[]
|
||||
for declName in clique do
|
||||
if let some elementStx := elementStxs.find? (elementAppliesTo declName) then
|
||||
elements := elements.push (toElement declName elementStx)
|
||||
else if let some elseElemStx := elseElemStx? then
|
||||
elements := elements.push (toElement declName elseElemStx)
|
||||
usedElse := true
|
||||
unless elements.isEmpty do
|
||||
if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then
|
||||
withRef elements[0]!.ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'"
|
||||
result := result.push { elements }
|
||||
if !usedElse && elseElemStx?.isSome then
|
||||
withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
|
||||
return ⟨result⟩
|
||||
|
||||
open Parser.Command in
|
||||
def TerminationWF.unexpand (elements : TerminationWF) : MetaM Syntax := do
|
||||
let elementStxs ← elements.mapM fun element => do
|
||||
let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
|
||||
`(terminationByElement|$fn $element.vars* => $element.body)
|
||||
`(terminationBy|termination_by $elementStxs*)
|
||||
|
||||
def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
|
||||
.mk <| t.cliques.map fun clique =>
|
||||
if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
|
||||
{ clique with used := true }
|
||||
else
|
||||
clique
|
||||
|
||||
def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF :=
|
||||
t.cliques.findSome? fun clique =>
|
||||
if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
|
||||
some <| clique.elements
|
||||
else
|
||||
none
|
||||
|
||||
def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
|
||||
c.elements.all fun elem => elem.implicit
|
||||
|
||||
def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
|
||||
c.elements.find? (!·.implicit)
|
||||
|
||||
def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := do
|
||||
let hasUsedAllImplicit := t.cliques.any fun c => c.allImplicit && c.used
|
||||
let mut reportedAllImplicit := true
|
||||
for clique in t.cliques do
|
||||
unless clique.used do
|
||||
if let some explicitElem := clique.getExplicitElement? then
|
||||
Macro.throwErrorAt explicitElem.ref "unused termination hint element"
|
||||
else if !hasUsedAllImplicit then
|
||||
unless reportedAllImplicit do
|
||||
reportedAllImplicit := true
|
||||
Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
|
||||
/-- Takes apart a `Termination.suffix` syntax object -/
|
||||
def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) : m TerminationHints := do
|
||||
-- Fail gracefully upon partial parses
|
||||
if let .missing := stx.raw then
|
||||
return { TerminationHints.none with ref := stx }
|
||||
-- This can be removed after the next stage0 bump
|
||||
if stx.raw.matchesNull 0 then
|
||||
return { TerminationHints.none with ref := stx }
|
||||
match stx with
|
||||
| `(suffix| $[$t?:terminationBy]? $[$d?:decreasingBy]? ) => do
|
||||
let termination_by? ← t?.mapM fun t => match t with
|
||||
| `(terminationBy|termination_by $vars* => $body) =>
|
||||
if vars.isEmpty then
|
||||
throwErrorAt t "no extra parameters bounds, please omit the `=>`"
|
||||
else
|
||||
pure {ref := t, vars, body}
|
||||
| `(terminationBy|termination_by $body:term) => pure {ref := t, vars := #[], body}
|
||||
| _ => throwErrorAt t "unexpected `termination_by` syntax"
|
||||
let decreasing_by? ← d?.mapM fun d => match d with
|
||||
| `(decreasingBy|decreasing_by $tactic) => pure {ref := d, tactic}
|
||||
| _ => throwErrorAt d "unexpected `decreasing_by` syntax"
|
||||
return { ref := stx, termination_by?, decreasing_by?, extraParams := 0 }
|
||||
| _ => throwErrorAt stx s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"
|
||||
|
||||
end Lean.Elab.WF
|
||||
|
|
|
|||
|
|
@ -291,9 +291,10 @@ mutual
|
|||
|
||||
/--
|
||||
Try to synthesize a term `val` using the tactic code `tacticCode`, and then assign `mvarId := val`.
|
||||
|
||||
The `tacticCode` syntax comprises the whole `by ...` expression.
|
||||
-/
|
||||
partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := withoutAutoBoundImplicit do
|
||||
/- Recall, `tacticCode` is the whole `by ...` expression. -/
|
||||
let code := tacticCode[1]
|
||||
instantiateMVarDeclMVars mvarId
|
||||
/-
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ import Lean.Linter.Deprecated
|
|||
import Lean.Elab.Config
|
||||
import Lean.Elab.Level
|
||||
import Lean.Elab.DeclModifiers
|
||||
import Lean.Elab.PreDefinition.WF.TerminationHint
|
||||
|
||||
namespace Lean.Elab
|
||||
|
||||
|
|
@ -95,6 +96,7 @@ structure LetRecToLift where
|
|||
type : Expr
|
||||
val : Expr
|
||||
mvarId : MVarId
|
||||
termination : WF.TerminationHints
|
||||
deriving Inhabited
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -28,27 +28,6 @@ match against a quotation in a command kind's elaborator). -/
|
|||
@[builtin_term_parser low] def quot := leading_parser
|
||||
"`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
|
||||
|
||||
/--
|
||||
A decreasing_by clause can either be a single tactic (for all functions), or
|
||||
a list of tactics labeled with the function they apply to.
|
||||
-/
|
||||
def decreasingByElement := leading_parser
|
||||
ppLine >> ppIndent (ident >> " => " >> Tactic.tacticSeq >> patternIgnore (optional ";"))
|
||||
def decreasingByMany := leading_parser
|
||||
atomic (lookahead (ident >> " => ")) >> many1Indent decreasingByElement
|
||||
def decreasingBy1 := leading_parser Tactic.tacticSeq
|
||||
|
||||
def decreasingBy := leading_parser
|
||||
ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
|
||||
|
||||
def terminationByElement := leading_parser
|
||||
ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
|
||||
" => " >> termParser >> patternIgnore (optional ";")
|
||||
def terminationBy := leading_parser
|
||||
ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
|
||||
|
||||
def terminationSuffix :=
|
||||
optional terminationBy >> optional decreasingBy
|
||||
|
||||
@[builtin_command_parser]
|
||||
def moduleDoc := leading_parser ppDedent <|
|
||||
|
|
@ -96,7 +75,7 @@ def declSig := leading_parser
|
|||
def optDeclSig := leading_parser
|
||||
many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
|
||||
def declValSimple := leading_parser
|
||||
" :=" >> ppHardLineUnlessUngrouped >> termParser >> optional Term.whereDecls
|
||||
" :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
|
||||
def declValEqns := leading_parser
|
||||
Term.matchAltsWhereDecls
|
||||
def whereStructField := leading_parser
|
||||
|
|
@ -116,20 +95,20 @@ def declVal :=
|
|||
withAntiquot (mkAntiquot "declVal" `Lean.Parser.Command.declVal (isPseudoKind := true)) <|
|
||||
declValSimple <|> declValEqns <|> whereStructInst
|
||||
def «abbrev» := leading_parser
|
||||
"abbrev " >> declId >> ppIndent optDeclSig >> declVal >> terminationSuffix
|
||||
"abbrev " >> declId >> ppIndent optDeclSig >> declVal
|
||||
def optDefDeriving :=
|
||||
optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
|
||||
def «def» := leading_parser
|
||||
"def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
|
||||
"def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving
|
||||
def «theorem» := leading_parser
|
||||
"theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
|
||||
"theorem " >> declId >> ppIndent declSig >> declVal
|
||||
def «opaque» := leading_parser
|
||||
"opaque " >> declId >> ppIndent declSig >> optional declValSimple
|
||||
/- As `declSig` starts with a space, "instance" does not need a trailing space
|
||||
if we put `ppSpace` in the optional fragments. -/
|
||||
def «instance» := leading_parser
|
||||
Term.attrKind >> "instance" >> optNamedPrio >>
|
||||
optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
|
||||
optional (ppSpace >> declId) >> ppIndent declSig >> declVal
|
||||
def «axiom» := leading_parser
|
||||
"axiom " >> declId >> ppIndent declSig
|
||||
/- As `declSig` starts with a space, "example" does not need a trailing space. -/
|
||||
|
|
@ -269,7 +248,7 @@ def openDecl :=
|
|||
|
||||
@[builtin_command_parser] def «mutual» := leading_parser
|
||||
"mutual" >> many1 (ppLine >> notSymbol "end" >> commandParser) >>
|
||||
ppDedent (ppLine >> "end") >> terminationSuffix
|
||||
ppDedent (ppLine >> "end")
|
||||
def initializeKeyword := leading_parser
|
||||
"initialize " <|> "builtin_initialize "
|
||||
@[builtin_command_parser] def «initialize» := leading_parser
|
||||
|
|
|
|||
|
|
@ -96,6 +96,52 @@ end Tactic
|
|||
def darrow : Parser := " => "
|
||||
def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
|
||||
|
||||
namespace Termination
|
||||
|
||||
/-
|
||||
Termination suffix parsers, typically thought of as part of a command, but due to
|
||||
letrec we need them here already.
|
||||
-/
|
||||
|
||||
/--
|
||||
Specify a termination argument for well-founded termination:
|
||||
```
|
||||
termination_by a - b
|
||||
```
|
||||
indicates that termination of the currently defined recursive function follows
|
||||
because the difference between the the arguments `a` and `b`.
|
||||
|
||||
If the fuction takes further argument after the colon, you can name them as follows:
|
||||
```
|
||||
def example (a : Nat) : Nat → Nat → Nat :=
|
||||
termination_by b c => a - b
|
||||
```
|
||||
|
||||
If omitted, a termination argument will be inferred.
|
||||
-/
|
||||
def terminationBy := leading_parser
|
||||
ppDedent ppLine >>
|
||||
"termination_by " >>
|
||||
optional (atomic (many (ppSpace >> (ident <|> "_")) >> " => ")) >>
|
||||
termParser
|
||||
|
||||
/--
|
||||
Manually prove that the termination argument (as specified with `termination_by` or inferred)
|
||||
decreases at each recursive call.
|
||||
|
||||
By default, the tactic `decreasing_tactic` is used.
|
||||
-/
|
||||
def decreasingBy := leading_parser
|
||||
ppDedent ppLine >> "decreasing_by " >> Tactic.tacticSeqIndentGt
|
||||
|
||||
/--
|
||||
Termination hints are `termination_by` and `decreasing_by`, in that order.
|
||||
-/
|
||||
def suffix := leading_parser
|
||||
optional terminationBy >> optional decreasingBy
|
||||
|
||||
end Termination
|
||||
|
||||
namespace Term
|
||||
|
||||
/-! # Built-in parsers -/
|
||||
|
|
@ -533,7 +579,7 @@ def attributes := leading_parser
|
|||
/-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
|
||||
a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/
|
||||
def letRecDecl := leading_parser
|
||||
optional Command.docComment >> optional «attributes» >> letDecl
|
||||
optional Command.docComment >> optional «attributes» >> letDecl >> Termination.suffix
|
||||
/-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`). -/
|
||||
def letRecDecls := leading_parser
|
||||
sepBy1 letRecDecl ", "
|
||||
|
|
@ -548,7 +594,7 @@ def whereDecls := leading_parser
|
|||
|
||||
@[run_builtin_parser_attribute_hooks]
|
||||
def matchAltsWhereDecls := leading_parser
|
||||
matchAlts >> optional whereDecls
|
||||
matchAlts >> Termination.suffix >> optional whereDecls
|
||||
|
||||
@[builtin_term_parser] def noindex := leading_parser
|
||||
"no_index " >> termParser maxPrec
|
||||
|
|
|
|||
|
|
@ -86,15 +86,15 @@ def mkConfigDecl (name? : Option Name)
|
|||
| `(structDeclSig| $id:ident) =>
|
||||
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty :=
|
||||
{name := $(quote id.getId)})
|
||||
| `(structDeclSig| $id:ident where $fs;* $[$wds?]?) => do
|
||||
| `(structDeclSig| $id:ident where $fs;* $[$wds?:whereDecls]?) => do
|
||||
let fields ← fs.getElems.mapM expandDeclField
|
||||
let defn ← `({ name := $(quote id.getId), $fields,* })
|
||||
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
|
||||
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
|
||||
| `(structDeclSig| $id:ident $[: $ty?]? :=%$defTk $defn $[$wds?]?) => do
|
||||
let notice ← withRef defTk `(#eval IO.eprintln s!" warning: {__dir__}: `:=` syntax for configurations has been deprecated")
|
||||
`($notice $[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
|
||||
| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
|
||||
| `(structDeclSig| $id:ident { $[$fs $[,]?]* } $[$wds?:whereDecls]?) => do
|
||||
let fields ← fs.mapM expandDeclField
|
||||
let defn ← `({ name := $(quote id.getId), $fields,* })
|
||||
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?]?)
|
||||
`($[$doc?]? @[$attrs,*] abbrev $(fixName id name?) : $ty := $defn $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed configuration syntax"
|
||||
|
|
|
|||
|
|
@ -65,12 +65,12 @@ optional(docComment) optional(Term.attributes)
|
|||
"post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command
|
||||
|
||||
macro_rules
|
||||
| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?]?) =>
|
||||
`($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?]?)
|
||||
| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?]?) => do
|
||||
| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?:whereDecls]?) =>
|
||||
`($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?)
|
||||
| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => do
|
||||
let pkg ← expandOptSimpleBinder pkg?
|
||||
let pkgName := mkIdentFrom pkg `_package.name
|
||||
let attr ← withRef kw `(Term.attrInstance| «post_update»)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
`($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl :=
|
||||
{pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?]?)
|
||||
{pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?)
|
||||
|
|
|
|||
|
|
@ -37,10 +37,10 @@ scoped syntax (name := scriptDecl)
|
|||
|
||||
@[macro scriptDecl]
|
||||
def expandScriptDecl : Macro
|
||||
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?]?) => do
|
||||
`($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?]?)
|
||||
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?]?) => do
|
||||
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? do $seq $[$wds?:whereDecls]?) => do
|
||||
`($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := do $seq $[$wds?:whereDecls]?)
|
||||
| `($[$doc?]? $[$attrs?]? script $id:ident $[$args?]? := $defn $[$wds?:whereDecls]?) => do
|
||||
let args ← expandOptSimpleBinder args?
|
||||
let attrs := #[← `(Term.attrInstance| «script»)] ++ expandAttrs attrs?
|
||||
`($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?]?)
|
||||
`($[$doc?]? @[$attrs,*] def $id : ScriptFn := fun $args => $defn $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed script declaration"
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ scoped macro (name := moduleFacetDecl)
|
|||
doc?:optional(docComment) attrs?:optional(Term.attributes)
|
||||
kw:"module_facet " sig:buildDeclSig : command => do
|
||||
match sig with
|
||||
| `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?]?) =>
|
||||
| `(buildDeclSig| $id:ident $[$mod?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| module_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
|
|
@ -45,7 +45,7 @@ kw:"module_facet " sig:buildDeclSig : command => do
|
|||
name := $name
|
||||
config := Lake.mkFacetJobConfig
|
||||
fun $mod => ($defn : IndexBuildM (BuildJob $ty))
|
||||
} $[$wds?]?)
|
||||
} $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
|
||||
|
||||
/--
|
||||
|
|
@ -62,7 +62,7 @@ scoped macro (name := packageFacetDecl)
|
|||
doc?:optional(docComment) attrs?:optional(Term.attributes)
|
||||
kw:"package_facet " sig:buildDeclSig : command => do
|
||||
match sig with
|
||||
| `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
|
||||
| `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| package_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
|
|
@ -73,7 +73,7 @@ kw:"package_facet " sig:buildDeclSig : command => do
|
|||
name := $name
|
||||
config := Lake.mkFacetJobConfig
|
||||
fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
|
||||
} $[$wds?]?)
|
||||
} $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
|
||||
|
||||
/--
|
||||
|
|
@ -90,7 +90,7 @@ scoped macro (name := libraryFacetDecl)
|
|||
doc?:optional(docComment) attrs?:optional(Term.attributes)
|
||||
kw:"library_facet " sig:buildDeclSig : command => do
|
||||
match sig with
|
||||
| `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?]?) =>
|
||||
| `(buildDeclSig| $id:ident $[$lib?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| library_facet)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
|
|
@ -101,7 +101,7 @@ kw:"library_facet " sig:buildDeclSig : command => do
|
|||
name := $name
|
||||
config := Lake.mkFacetJobConfig
|
||||
fun $lib => ($defn : IndexBuildM (BuildJob $ty))
|
||||
} $[$wds?]?)
|
||||
} $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -124,7 +124,7 @@ scoped macro (name := targetDecl)
|
|||
doc?:optional(docComment) attrs?:optional(Term.attributes)
|
||||
kw:"target " sig:buildDeclSig : command => do
|
||||
match sig with
|
||||
| `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?]?) =>
|
||||
| `(buildDeclSig| $id:ident $[$pkg?]? : $ty := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| target)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let name := Name.quoteFrom id id.getId
|
||||
|
|
@ -136,7 +136,7 @@ kw:"target " sig:buildDeclSig : command => do
|
|||
name := $name
|
||||
config := Lake.mkTargetJobConfig
|
||||
fun $pkg => ($defn : IndexBuildM (BuildJob $ty))
|
||||
} $[$wds?]?)
|
||||
} $[$wds?:whereDecls]?)
|
||||
| stx => Macro.throwErrorAt stx "ill-formed target declaration"
|
||||
|
||||
|
||||
|
|
@ -208,13 +208,13 @@ scoped macro (name := externLibDecl)
|
|||
doc?:optional(docComment) attrs?:optional(Term.attributes)
|
||||
"extern_lib " spec:externLibDeclSpec : command => do
|
||||
match spec with
|
||||
| `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?]?) =>
|
||||
| `(externLibDeclSpec| $id:ident $[$pkg?]? := $defn $[$wds?:whereDecls]?) =>
|
||||
let attr ← `(Term.attrInstance| extern_lib)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let pkgName := mkIdentFrom id `_package.name
|
||||
let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
|
||||
let name := Name.quoteFrom id id.getId
|
||||
`(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?]?
|
||||
`(target $targetId $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
|
||||
$[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := {
|
||||
pkg := $pkgName
|
||||
name := $name
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ options get_default_options() {
|
|||
// switch to `true` for ABI-breaking changes affecting meta code
|
||||
opts = opts.update({"interpreter", "prefer_native"}, false);
|
||||
// switch to `true` for changing built-in parsers used in quotations
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
|
||||
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
|
||||
// with custom precheck hooks were affected
|
||||
opts = opts.update({"quotPrecheck"}, true);
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ def foo (n : Nat) : Nat :=
|
|||
let x := n - 1
|
||||
have := match () with | _ => trivial
|
||||
foo x
|
||||
termination_by _ n => n
|
||||
termination_by n
|
||||
decreasing_by sorry
|
||||
|
||||
theorem ex : foo 0 = 0 := by
|
||||
|
|
|
|||
|
|
@ -7,15 +7,15 @@ namespace Foo
|
|||
mutual
|
||||
def bar : {as bs: Type u} → Foo.{u} as bs → bs :=
|
||||
bar_aux
|
||||
termination_by _ _ => 0
|
||||
decreasing_by sorry
|
||||
|
||||
def bar_aux: {as bs: Type u} → Foo.{u} as bs → bs
|
||||
| as, bs, foo _ x => x.bar
|
||||
termination_by _ _ _ => 0
|
||||
decreasing_by sorry
|
||||
|
||||
end
|
||||
termination_by
|
||||
bar => 0
|
||||
bar_aux => 0
|
||||
decreasing_by sorry
|
||||
end Foo
|
||||
|
||||
|
||||
|
|
@ -23,15 +23,15 @@ namespace Foo
|
|||
mutual
|
||||
def bar1 : {as bs: Type u} → Foo.{u} as bs → bs
|
||||
| as, bs, x => bar_aux1 x
|
||||
termination_by _ _ _ => 0
|
||||
decreasing_by sorry
|
||||
|
||||
def bar_aux1 : {as bs: Type u} → Foo.{u} as bs → bs
|
||||
| as, bs, foo _ x => x.bar1
|
||||
termination_by _ _ _ => 0
|
||||
decreasing_by sorry
|
||||
|
||||
end
|
||||
termination_by
|
||||
bar1 => 0
|
||||
bar_aux1 => 0
|
||||
decreasing_by sorry
|
||||
end Foo
|
||||
|
||||
|
||||
|
|
@ -39,12 +39,11 @@ namespace Foo
|
|||
mutual
|
||||
def bar2 : Foo as bs → bs
|
||||
| x => bar_aux2 x
|
||||
termination_by x => (sizeOf x, 1)
|
||||
|
||||
def bar_aux2 : Foo as bs → bs
|
||||
| foo _ x => x.bar2
|
||||
termination_by x => (sizeOf x, 0)
|
||||
|
||||
end
|
||||
termination_by
|
||||
bar2 x => (sizeOf x, 1)
|
||||
bar_aux2 x => (sizeOf x, 0)
|
||||
end Foo
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
1050.lean:7:2-18:21: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
|
||||
1050.lean:7:2-18:5: error: invalid mutual definition, result types must be in the same universe level, resulting type for `Foo.bar` is
|
||||
Foo as bs → bs : Type (u + 1)
|
||||
and for `Foo.bar_aux` is
|
||||
bs : Type u
|
||||
|
|
|
|||
|
|
@ -10,13 +10,13 @@ def f : Nat → Nat
|
|||
def g : Nat → Nat
|
||||
| 0 => 0
|
||||
| n + 1 => g n
|
||||
termination_by g x => x
|
||||
termination_by x => x
|
||||
|
||||
@[macro_inline] -- Error
|
||||
def h : Nat → Nat → Nat
|
||||
| 0, _ => 0
|
||||
| n + 1, m => h n m
|
||||
termination_by h x y => x
|
||||
termination_by x y => x
|
||||
|
||||
@[macro_inline] -- Error
|
||||
partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ def natPrintAux (n : Nat) (sink : List Char) : List Char :=
|
|||
if h0 : n < 10
|
||||
then (n.digitChar :: sink)
|
||||
else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink)
|
||||
termination_by _ n => n
|
||||
termination_by n
|
||||
decreasing_by sorry
|
||||
|
||||
set_option maxRecDepth 100 -- default takes ages in debug mode and triggers stack space threshold
|
||||
|
|
|
|||
|
|
@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term
|
|||
"(«term_+_» (num \"1\") \"+\" (num \"1\"))"
|
||||
StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
|
||||
"(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))"
|
||||
"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))"
|
||||
"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") [])\n []\n []\n []))]"
|
||||
"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))"
|
||||
"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))]"
|
||||
"`Nat.one._@.UnhygienicMain._hyg.1"
|
||||
"`Nat.one._@.UnhygienicMain._hyg.1"
|
||||
"(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
|
||||
|
|
@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
|
|||
"(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
|
||||
"(«term_+_» (num \"2\") \"+\" (num \"1\"))"
|
||||
"(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))"
|
||||
"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))"
|
||||
"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") [])\n []\n []\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") [])\n []\n []\n []))]"
|
||||
"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))"
|
||||
"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))]"
|
||||
"0"
|
||||
0
|
||||
1
|
||||
|
|
|
|||
|
|
@ -1,41 +1,138 @@
|
|||
mutual
|
||||
inductive Even : Nat → Prop
|
||||
| base : Even 0
|
||||
| step : Odd n → Even (n+1)
|
||||
inductive Odd : Nat → Prop
|
||||
| step : Even n → Odd (n+1)
|
||||
end
|
||||
decreasing_by assumption
|
||||
/-!
|
||||
Various tests about `decreasing_by`.
|
||||
-/
|
||||
|
||||
mutual
|
||||
def f (n : Nat) :=
|
||||
if n == 0 then 0 else f (n / 2) + 1
|
||||
decreasing_by assumption
|
||||
end
|
||||
-- For concise recursive definition that need well-founded recursion
|
||||
-- and `decreasing_by` tactics that would fail if run on the subgoal
|
||||
opaque dec1 : Nat → Nat
|
||||
axiom dec1_lt (n : Nat) : dec1 n < n
|
||||
opaque dec2 : Nat → Nat
|
||||
axiom dec2_lt (n : Nat) : dec2 n < n
|
||||
|
||||
def g' (n : Nat) :=
|
||||
match n with
|
||||
| 0 => 1
|
||||
| n+1 => g' n * 3
|
||||
|
||||
def simple (n : Nat) := n + simple (dec1 n)
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
namespace Ex1
|
||||
|
||||
-- Multiple goals, explicit termination_By
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
|
||||
termination_by (n, m)
|
||||
decreasing_by
|
||||
h => assumption
|
||||
· simp_wf
|
||||
apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
· simp_wf
|
||||
apply Prod.Lex.left
|
||||
apply dec1_lt
|
||||
|
||||
namespace Test
|
||||
mutual
|
||||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n+1, a, b => g n a b |>.1
|
||||
end Ex1
|
||||
|
||||
def g : Nat → α → α → (α × α)
|
||||
| 0, a, b => (a, b)
|
||||
| n+1, a, b => (h n a b, a)
|
||||
namespace Ex2
|
||||
|
||||
def h : Nat → α → α → α
|
||||
| 0, a, b => b
|
||||
| n+1, a, b => f n a b
|
||||
end
|
||||
-- Multiple goals, no termination_By
|
||||
-- This does *not* work, because GuessLex does not pass multiple goals to the tactic.
|
||||
-- so this tactic script fails.
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
|
||||
decreasing_by
|
||||
f => assumption
|
||||
g => assumption
|
||||
· simp_wf
|
||||
apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
· simp_wf
|
||||
apply Prod.Lex.left
|
||||
apply dec1_lt
|
||||
|
||||
end Test
|
||||
end Ex2
|
||||
|
||||
namespace Ex3
|
||||
-- Using `all_goals`, explicit termination_By
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
|
||||
termination_by (n, m)
|
||||
decreasing_by all_goals
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
| apply Prod.Lex.left
|
||||
apply dec1_lt
|
||||
|
||||
end Ex3
|
||||
|
||||
namespace Ex4
|
||||
|
||||
-- Multiple goals, no termination_By
|
||||
-- This does work, because the tactic is flexible enough
|
||||
-- (Not a recommended way; complex `decrasing_by` should go along with `termination_by`.)
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
|
||||
decreasing_by all_goals
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
| apply Prod.Lex.left
|
||||
apply dec1_lt
|
||||
|
||||
end Ex4
|
||||
|
||||
namespace Ex5
|
||||
-- Empty proof. Produces parse error and unsolved goals.
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
|
||||
termination_by n m => (n, m)
|
||||
decreasing_by -- Error
|
||||
|
||||
end Ex5
|
||||
|
||||
namespace Ex6
|
||||
|
||||
-- Incomplete tactic
|
||||
-- Unsolved goals reported
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
|
||||
termination_by (n, m)
|
||||
decreasing_by apply id -- Error
|
||||
|
||||
end Ex6
|
||||
|
||||
namespace Ex7
|
||||
|
||||
-- Incomplete tactic, no termination_by
|
||||
-- Shows guess-lex matrix
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
|
||||
decreasing_by apply id
|
||||
|
||||
end Ex7
|
||||
|
||||
namespace Ex8
|
||||
|
||||
-- tactic solving just one goal
|
||||
-- unsolved goals
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100
|
||||
termination_by (n, m)
|
||||
decreasing_by -- Error
|
||||
· simp_wf
|
||||
apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
|
||||
end Ex8
|
||||
|
||||
namespace Ex9
|
||||
|
||||
-- Incomplete tactic, no termination_by
|
||||
-- Shows guess-lex matrix
|
||||
def foo (n m : Nat) : Nat := foo n (dec2 m) + foo (dec1 n) 100 -- Error
|
||||
decreasing_by
|
||||
· simp_wf
|
||||
apply Prod.Lex.right
|
||||
apply dec2_lt
|
||||
|
||||
end Ex9
|
||||
|
||||
namespace Ex10
|
||||
|
||||
-- This checks that guess-lex does not run tactics in “recover” mode.
|
||||
-- (If it would it would produce the wrong termination order and then we should see errors)
|
||||
def foo (n m : Nat) : Nat := foo (n - 1) (dec2 m)
|
||||
decreasing_by all_goals
|
||||
· simp_wf
|
||||
apply dec2_lt
|
||||
|
||||
end Ex10
|
||||
|
|
|
|||
|
|
@ -1,4 +1,50 @@
|
|||
decreasing_by.lean:8:0-8:24: error: invalid 'decreasing_by' in mutually inductive datatype declaration
|
||||
decreasing_by.lean:13:1-13:25: error: invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword
|
||||
decreasing_by.lean:21:2-21:3: error: function 'h' not found in current declaration
|
||||
decreasing_by.lean:39:2-39:17: error: invalid termination hint element, 'Test.g' and 'Test.f' are in the same clique
|
||||
decreasing_by.lean:36:0-43:17: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
n m
|
||||
1) 36:29-43 = ?
|
||||
2) 36:46-62 ? _
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
decreasing_by.lean:66:0-73:19: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
n m
|
||||
1) 66:29-43 = ?
|
||||
2) 66:46-62 ? _
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic
|
||||
decreasing_by.lean:81:0-81:13: error: unsolved goals
|
||||
n m : Nat
|
||||
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
||||
{ fst := n, snd := dec2 m } { fst := n, snd := m }
|
||||
|
||||
n m : Nat
|
||||
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
||||
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
||||
decreasing_by.lean:91:0-91:22: error: unsolved goals
|
||||
case a
|
||||
n m : Nat
|
||||
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
||||
{ fst := n, snd := dec2 m } { fst := n, snd := m }
|
||||
|
||||
n m : Nat
|
||||
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
||||
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
||||
decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
n m
|
||||
1) 99:29-43 = ?
|
||||
2) 99:46-62 ? _
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
decreasing_by.lean:110:0-113:17: error: unsolved goals
|
||||
n m : Nat
|
||||
⊢ (invImage (fun a => PSigma.casesOn a fun n snd => (n, snd)) Prod.instWellFoundedRelationProd).1
|
||||
{ fst := dec1 n, snd := 100 } { fst := n, snd := m }
|
||||
decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
n m
|
||||
1) 121:29-43 = ?
|
||||
2) 121:46-62 ? _
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
|
|
|
|||
|
|
@ -120,18 +120,27 @@ def shadow1 (x2 : Nat) : Nat → Nat
|
|||
decreasing_by decreasing_tactic
|
||||
|
||||
|
||||
-- This test is a bit moot since #3081, but lets keep it
|
||||
def some_n : Nat := 1
|
||||
def shadow2 (some_n : Nat) : Nat → Nat
|
||||
| 0 => 0
|
||||
| .succ n => shadow2 (some_n + 1) n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
def shadow3 (sizeOf : Nat) : Nat → Nat
|
||||
-- Shadowing `sizeOf`, as a varying paramter
|
||||
def shadowSizeOf1 (sizeOf : Nat) : Nat → Nat
|
||||
| 0 => 0
|
||||
| .succ n => shadow3 (sizeOf + 1) n
|
||||
| .succ n => shadowSizeOf1 (sizeOf + 1) n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
def sizeOf : Nat := 2 -- should cause sizeOf to be qualfied below
|
||||
-- Shadowing `sizeOf`, as a fixed paramter
|
||||
def shadowSizeOf2 (sizeOf : Nat) : Nat → Nat → Nat
|
||||
| 0, m => m
|
||||
| .succ n, m => shadowSizeOf2 sizeOf n m
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
-- Shadowing `sizeOf`, as something in the environment
|
||||
def sizeOf : Nat := 2
|
||||
|
||||
def qualifiedSizeOf (m : Nat) : Nat → Nat
|
||||
| 0 => 0
|
||||
|
|
|
|||
|
|
@ -1,50 +1,41 @@
|
|||
Inferred termination argument:
|
||||
termination_by
|
||||
ackermann n m => (sizeOf n, sizeOf m)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
ackermann2 n m => (sizeOf m, sizeOf n)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
ackermannList n m => (sizeOf n, sizeOf m)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
foo2 x1 x2 => (sizeOf x2, sizeOf x1)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
even x1 => sizeOf x1
|
||||
odd x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
evenWithFixed x1 => sizeOf x1
|
||||
oddWithFixed x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
ping.pong x1 => (sizeOf x1, 0)
|
||||
ping n => (sizeOf n, 1)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
hasForbiddenArg n _h m => (sizeOf m, sizeOf n)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
blowup x1 x2 x3 x4 x5 x6 x7 x8 =>
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf n, sizeOf m)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf m, sizeOf n)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf n, sizeOf m)
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 => (sizeOf x2, sizeOf x1)
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => (sizeOf x1, 0)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf n, 1)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf m, sizeOf n)
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 x3 x4 x5 x6 x7 x8 =>
|
||||
(sizeOf x8, sizeOf x7, sizeOf x6, sizeOf x5, sizeOf x4, sizeOf x3, sizeOf x2, sizeOf x1)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
dependent x1 x2 => (sizeOf x1, sizeOf x2)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
eval a => (sizeOf a, 1)
|
||||
eval_add a => (sizeOf a, 0)
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
shadow1 x2 x2' => sizeOf x2'
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
shadow2 some_n' x2 => sizeOf x2
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
shadow3 sizeOf' x2 => sizeOf x2
|
||||
Inferred termination argument:
|
||||
termination_by
|
||||
qualifiedSizeOf m x2 => SizeOf.sizeOf x2
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 => (sizeOf x1, sizeOf x2)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf a, 1)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf a, 0)
|
||||
Inferred termination argument:
|
||||
termination_by x2' => sizeOf x2'
|
||||
Inferred termination argument:
|
||||
termination_by x2 => sizeOf x2
|
||||
Inferred termination argument:
|
||||
termination_by x2 => SizeOf.sizeOf x2
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 => SizeOf.sizeOf x1
|
||||
Inferred termination argument:
|
||||
termination_by x2 => SizeOf.sizeOf x2
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ namespace TrickyCode
|
|||
def FinPlus1 n := Fin (n + 1)
|
||||
def badCasesOn (n m : Nat) : Fin (n + 1) :=
|
||||
Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n (.succ m)))
|
||||
-- termination_by badCasesOn n m => n
|
||||
-- termination_by n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
|
||||
|
|
@ -109,7 +109,7 @@ decreasing_by decreasing_tactic
|
|||
-- https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Going.20under.20exactly.20one.20lambda/near/404278529
|
||||
def badCasesOn2 (n m : Nat) : Fin (n + 1) :=
|
||||
Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn2 n (.succ m)))
|
||||
termination_by badCasesOn2 n m => n
|
||||
termination_by n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
-- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
|
||||
|
|
@ -119,7 +119,7 @@ def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) :=
|
|||
def badCasesOn3 (n m : Nat) : Fin (n + 1) :=
|
||||
Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
|
||||
(Fin_succ_comp (fun n => badCasesOn3 n (.succ m)))
|
||||
-- termination_by badCasesOn3 n m => n
|
||||
-- termination_by n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
|
||||
|
|
@ -127,7 +127,7 @@ decreasing_by decreasing_tactic
|
|||
def badCasesOn4 (n m : Nat) : Fin (n + 1) :=
|
||||
Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩)
|
||||
(Fin_succ_comp (fun n => badCasesOn4 n (.succ m)))
|
||||
termination_by badCasesOn4 n m => n
|
||||
termination_by n
|
||||
decreasing_by decreasing_tactic
|
||||
|
||||
end TrickyCode
|
||||
|
|
|
|||
|
|
@ -39,15 +39,32 @@ macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
|
|||
mutual
|
||||
def prod (x y z : Nat) : Nat :=
|
||||
if y % 2 = 0 then eprod x y z else oprod x y z
|
||||
decreasing_by
|
||||
-- TODO: Why does it not work to wrap it all in `all_goals`?
|
||||
all_goals simp_wf
|
||||
· search_lex solve
|
||||
| decreasing_trivial
|
||||
| apply Nat.bitwise_rec_lemma; assumption
|
||||
· search_lex solve
|
||||
| decreasing_trivial
|
||||
| apply Nat.bitwise_rec_lemma; assumption
|
||||
|
||||
def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
|
||||
def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
|
||||
end
|
||||
-- termination_by
|
||||
-- prod x y z => (y, 2)
|
||||
-- oprod x y z => (y, 1)
|
||||
-- eprod x y z => (y, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
search_lex solve
|
||||
| decreasing_trivial
|
||||
| apply Nat.bitwise_rec_lemma; assumption
|
||||
|
||||
def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
|
||||
decreasing_by
|
||||
simp_wf
|
||||
search_lex solve
|
||||
| decreasing_trivial
|
||||
| apply Nat.bitwise_rec_lemma; assumption
|
||||
|
||||
end
|
||||
-- termination_by
|
||||
-- prod x y z => (y, 2)
|
||||
-- oprod x y z => (y, 1)
|
||||
-- eprod x y z => (y, 0)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
Inferred termination argument:
|
||||
termination_by
|
||||
prod x y z => (sizeOf y, 1, 0)
|
||||
oprod x y z => (sizeOf y, 0, 1)
|
||||
eprod x y z => (sizeOf y, 0, 0)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf y, 1, 0)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf y, 0, 1)
|
||||
Inferred termination argument:
|
||||
termination_by (sizeOf y, 0, 0)
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
Inferred termination argument:
|
||||
termination_by
|
||||
pedal x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
|
||||
coast x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 0)
|
||||
Inferred termination argument:
|
||||
termination_by x1 x2 x3 => (sizeOf x1, sizeOf x2, 1)
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
|
|||
rw [a.size_swap i j]; sorry
|
||||
let ⟨a₂, h₂⟩ := heapifyDown lt a' j'
|
||||
⟨a₂, h₂.trans (a.size_swap i j)⟩
|
||||
termination_by _ => a.size - i
|
||||
termination_by a.size - i
|
||||
decreasing_by assumption
|
||||
|
||||
@[simp] theorem size_heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
|
||||
|
|
@ -65,7 +65,7 @@ if i0 : i.1 = 0 then ⟨a, rfl⟩ else
|
|||
let ⟨a₂, h₂⟩ := heapifyUp lt a' ⟨j.1, by rw [a.size_swap i j]; exact j.2⟩
|
||||
⟨a₂, h₂.trans (a.size_swap i j)⟩
|
||||
else ⟨a, rfl⟩
|
||||
termination_by _ => i.1
|
||||
termination_by i.1
|
||||
decreasing_by assumption
|
||||
|
||||
@[simp] theorem size_heapifyUp (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
|
||||
|
|
@ -168,9 +168,9 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
|
|||
have : a.popMax.size < a.size := by
|
||||
simp; exact Nat.sub_lt (BinaryHeap.size_pos_of_max e) Nat.zero_lt_one
|
||||
loop a.popMax (out.push x)
|
||||
termination_by a.size
|
||||
decreasing_by assumption
|
||||
loop (a.toBinaryHeap gt) #[]
|
||||
termination_by _ => a.size
|
||||
decreasing_by assumption
|
||||
|
||||
attribute [simp] Array.heapSort.loop
|
||||
#check Array.heapSort.loop._eq_1
|
||||
|
|
|
|||
|
|
@ -188,7 +188,7 @@ example : Nat → Nat → Nat := by
|
|||
--^ textDocument/hover
|
||||
|
||||
def g (n : Nat) : Nat := g 0
|
||||
termination_by g n => n
|
||||
termination_by n => n
|
||||
decreasing_by have n' := n; admit
|
||||
--^ textDocument/hover
|
||||
|
||||
|
|
|
|||
|
|
@ -4,5 +4,5 @@ def sum (as : Array Nat) : Nat :=
|
|||
go (i+2) (s + as.get ⟨i, h⟩) -- Error
|
||||
else
|
||||
s
|
||||
termination_by as.size - i
|
||||
go 0 0
|
||||
termination_by go i _ => as.size - i
|
||||
|
|
|
|||
|
|
@ -4,24 +4,24 @@ mutual
|
|||
| n, true => 2 * f n false
|
||||
| 0, false => 1
|
||||
| n, false => n + g n
|
||||
termination_by n b => (n, if b then 2 else 1)
|
||||
decreasing_by
|
||||
all_goals simp_wf
|
||||
· apply Prod.Lex.right; decide
|
||||
· apply Prod.Lex.right; decide
|
||||
|
||||
def g (n : Nat) : Nat :=
|
||||
if h : n ≠ 0 then
|
||||
f (n-1) true
|
||||
else
|
||||
n
|
||||
end
|
||||
termination_by
|
||||
f n b => (n, if b then 2 else 1)
|
||||
g n => (n, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.left
|
||||
apply Nat.pred_lt
|
||||
| apply Prod.Lex.right
|
||||
decide
|
||||
termination_by (n, 0)
|
||||
decreasing_by
|
||||
all_goals simp_wf
|
||||
apply Prod.Lex.left
|
||||
apply Nat.pred_lt
|
||||
done -- should fail
|
||||
end
|
||||
end Ex1
|
||||
|
||||
|
||||
|
|
@ -31,14 +31,13 @@ mutual
|
|||
| n, true => 2 * f n false
|
||||
| 0, false => 1
|
||||
| n, false => n + g (n+1) -- Error
|
||||
termination_by n b => (n, if b then 2 else 1)
|
||||
|
||||
def g (n : Nat) : Nat :=
|
||||
if h : n ≠ 0 then
|
||||
f (n-1) true
|
||||
else
|
||||
n
|
||||
termination_by (n, 0)
|
||||
end
|
||||
termination_by
|
||||
f n b => (n, if b then 2 else 1)
|
||||
g n => (n, 0)
|
||||
end Ex2
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
mutwf1.lean:24:2-24:6: error: unsolved goals
|
||||
mutwf1.lean:23:2-23:6: error: unsolved goals
|
||||
case h.a
|
||||
n : Nat
|
||||
h : n ≠ 0
|
||||
|
|
|
|||
|
|
@ -50,6 +50,6 @@ def mwe [Stream ρ τ] (acc : α) : {l : ρ // isFinite l} → α
|
|||
| some (x,xs) =>
|
||||
have h_next : hasNext l xs := by exists x
|
||||
mwe acc ⟨xs, by sorry⟩
|
||||
termination_by _ l => l
|
||||
termination_by l => l
|
||||
|
||||
end Stream
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ def Nat.hasDecEq: (a: Nat) → (b: Nat) → Decidable (Eq a b)
|
|||
match h:hasDecEq n m with -- it works without `h:`
|
||||
| isTrue heq => isTrue (heq ▸ rfl)
|
||||
| isFalse hne => isFalse (Nat.noConfusion · (λ heq => absurd heq hne))
|
||||
termination_by _ a b => (a, b)
|
||||
termination_by a b => (a, b)
|
||||
|
||||
set_option pp.proofs true
|
||||
#print Nat.hasDecEq
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ namespace Foo
|
|||
cases h₂ : n; sorry
|
||||
have: Bar s' := sorry
|
||||
exact ex₁ this
|
||||
termination_by _ => sizeOf s
|
||||
termination_by sizeOf s
|
||||
|
||||
theorem ex₂
|
||||
{s: Foo n}
|
||||
|
|
@ -22,7 +22,7 @@ namespace Foo
|
|||
have: Bar s' := sorry
|
||||
have hterm: sizeOf s' < sizeOf s := by simp_all_arith
|
||||
exact ex₂ this
|
||||
termination_by _ => sizeOf s
|
||||
termination_by sizeOf s
|
||||
|
||||
theorem ex₃ {s: Foo n} (H: s.Bar): True := by
|
||||
cases h₁ : s
|
||||
|
|
@ -32,7 +32,7 @@ namespace Foo
|
|||
| _ =>
|
||||
have: Bar s' := sorry
|
||||
exact ex₃ this
|
||||
termination_by _ => sizeOf s
|
||||
termination_by sizeOf s
|
||||
|
||||
-- it works
|
||||
theorem ex₄ {s: Foo n} (H: s.Bar): True := by
|
||||
|
|
@ -43,4 +43,4 @@ namespace Foo
|
|||
| _ =>
|
||||
have: Bar s' := sorry
|
||||
exact ex₄ this
|
||||
termination_by _ => sizeOf s
|
||||
termination_by sizeOf s
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
abbrev f : Nat → Nat
|
||||
| 0 => 0
|
||||
| n + 1 => f n
|
||||
termination_by _ n => n
|
||||
termination_by n => n
|
||||
|
||||
mutual
|
||||
abbrev f1 : Nat → Nat
|
||||
| 0 => 0
|
||||
| n + 1 => f1 n
|
||||
termination_by n => n
|
||||
end
|
||||
termination_by _ n => n
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ def f3 (n : Nat) : Nat :=
|
|||
match n with
|
||||
| 0 => 0
|
||||
| n + 1 => (f3) n
|
||||
termination_by f3 n => n
|
||||
termination_by n
|
||||
|
||||
-- Same with rewrite
|
||||
|
||||
|
|
|
|||
|
|
@ -13,17 +13,19 @@ private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
|
|||
· apply Nat.zero_lt_succ
|
||||
|
||||
def pack (n: Nat) : List Nat :=
|
||||
let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
|
||||
let next (n: Nat) := n / 2;
|
||||
match n with
|
||||
| Nat.zero => List.cons acc accs
|
||||
| n+1 => match evenq n with
|
||||
| true => loop (next n) 0 (List.cons acc accs)
|
||||
| false => loop (next n) (acc+1) accs
|
||||
let rec
|
||||
loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
|
||||
let next (n: Nat) := n / 2;
|
||||
match n with
|
||||
| Nat.zero => List.cons acc accs
|
||||
| n+1 => match evenq n with
|
||||
| true => loop (next n) 0 (List.cons acc accs)
|
||||
| false => loop (next n) (acc+1) accs
|
||||
termination_by n
|
||||
decreasing_by all_goals
|
||||
simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
|
||||
apply pack_loop_terminates
|
||||
|
||||
loop n 0 []
|
||||
termination_by _ n _ _ => n
|
||||
decreasing_by
|
||||
simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
|
||||
apply pack_loop_terminates
|
||||
|
||||
#eval pack 27
|
||||
|
|
|
|||
|
|
@ -1,17 +1,4 @@
|
|||
variable (a : Nat)
|
||||
|
||||
def foo1 (b c : Nat) := if h : b = 0 then a + c else foo1 (b - 1) c
|
||||
termination_by _ => b
|
||||
|
||||
def foo2 (b c : Nat) := if h : b = 0 then a + c else foo2 (b - 1) c
|
||||
termination_by
|
||||
foo2 x y z => y
|
||||
|
||||
def foo3 (b c : Nat) := if h : b = 0 then a + c else foo3 (b - 1) c
|
||||
termination_by
|
||||
_ x y z => y
|
||||
|
||||
def foo4 (b c : Nat) := if h : b = 0 then a + c else foo4 (b - 1) c
|
||||
termination_by
|
||||
-- We can rename from right to left
|
||||
foo4 y _ => y
|
||||
termination_by b
|
||||
|
|
|
|||
|
|
@ -3,11 +3,15 @@ mutual
|
|||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
termination_by n =>
|
||||
match n with
|
||||
| _ => n
|
||||
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
termination_by n =>
|
||||
match n with
|
||||
| _ => n
|
||||
end
|
||||
termination_by _ n =>
|
||||
match n with
|
||||
| _ => n
|
||||
end Ex2
|
||||
|
|
|
|||
|
|
@ -2,4 +2,4 @@ def ack : Nat → Nat → Nat
|
|||
| 0, y => y+1
|
||||
| x+1, 0 => ack x 1
|
||||
| x+1, y+1 => ack x (ack (x+1) y)
|
||||
termination_by _ a b => (a, b)
|
||||
termination_by a b => (a, b)
|
||||
|
|
|
|||
|
|
@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
|
|||
let rest := Expr.forallE name newType newBody data
|
||||
some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
|
||||
| _ => none
|
||||
decreasing_by exact Nat.le_trans (by simp_arith) h
|
||||
decreasing_by all_goals exact Nat.le_trans (by simp_arith) h
|
||||
|
|
|
|||
|
|
@ -44,8 +44,8 @@ def Nat.binrec
|
|||
bit_div_even h₂ ▸ ind false (n / 2) (fun _ => binrec motive base ind (n / 2))
|
||||
else
|
||||
bit_div_odd h₂ ▸ ind true (n / 2) (fun _ => binrec motive base ind (n / 2))
|
||||
termination_by _ n => n
|
||||
decreasing_by exact Nat.div2_lt h₁
|
||||
termination_by n
|
||||
decreasing_by all_goals exact Nat.div2_lt h₁
|
||||
|
||||
theorem Nat.binind
|
||||
(motive : Nat → Prop)
|
||||
|
|
|
|||
|
|
@ -11,4 +11,4 @@ def List.bubblesort [LT α] [DecidableRel (· < · : α → α → Prop)] (l : L
|
|||
⟨y :: zs, by simp[h, ← he]⟩
|
||||
else
|
||||
⟨x :: y :: ys, by simp[h]⟩
|
||||
termination_by _ => l.length
|
||||
termination_by l.length
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
|
|||
| ForInStep.done b => pure b
|
||||
| ForInStep.yield b => have := Nat.Up.next h; loop f arr off _end (i+1) b
|
||||
else pure b
|
||||
termination_by _ => _end - i
|
||||
termination_by _end - i
|
||||
|
||||
attribute [simp] ByteSlice.forIn.loop
|
||||
#check @ByteSlice.forIn.loop._eq_1
|
||||
|
|
|
|||
|
|
@ -397,7 +397,7 @@ def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.leng
|
|||
match σ₂.find? x with
|
||||
| some w => if v = w then (x, v) :: join σ₁' σ₂ else join σ₁' σ₂
|
||||
| none => join σ₁' σ₂
|
||||
termination_by _ σ₁ _ => σ₁.length
|
||||
termination_by σ₁.length
|
||||
|
||||
local notation "⊥" => []
|
||||
|
||||
|
|
@ -468,7 +468,7 @@ theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ :=
|
|||
next => apply cons_le_cons; apply le_trans ih (erase_le _)
|
||||
next => apply le_trans ih (erase_le_cons (le_refl _))
|
||||
next h => apply le_trans ih (erase_le_cons (le_refl _))
|
||||
termination_by _ σ₁ _ => σ₁.length
|
||||
termination_by σ₁.length
|
||||
|
||||
theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ :=
|
||||
le_trans (join_le_left σ₁ σ₃) h
|
||||
|
|
@ -485,7 +485,7 @@ theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ :
|
|||
split <;> simp [*]
|
||||
next => apply cons_le_of_eq ih h
|
||||
next h => assumption
|
||||
termination_by _ σ₁ _ => σ₁.length
|
||||
termination_by σ₁.length
|
||||
|
||||
theorem State.join_le_right_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₃.join σ₁ ≼ σ₂ :=
|
||||
le_trans (join_le_right σ₃ σ₁) h
|
||||
|
|
|
|||
|
|
@ -21,4 +21,4 @@ def f (x : Nat) : Nat :=
|
|||
1
|
||||
else
|
||||
f (g x (x > 0)) + 2
|
||||
termination_by f x => x
|
||||
termination_by x
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@
|
|||
| x+1, 0 => succ_zero x (go x 0)
|
||||
| 0, y+1 => zero_succ y (go 0 y)
|
||||
| x+1, y+1 => succ_succ x y (go x y)
|
||||
termination_by x y => (x, y)
|
||||
go x y
|
||||
termination_by go x y => (x, y)
|
||||
|
||||
def f (x y : Nat) :=
|
||||
match x, y with
|
||||
|
|
@ -18,7 +18,7 @@ def f (x y : Nat) :=
|
|||
| x+1, 0 => f x 0
|
||||
| 0, y+1 => f 0 y
|
||||
| x+1, y+1 => f x y
|
||||
termination_by f x y => (x, y)
|
||||
termination_by (x, y)
|
||||
|
||||
example (x y : Nat) : f x y > 0 := by
|
||||
induction x, y with
|
||||
|
|
|
|||
|
|
@ -2,13 +2,17 @@ mutual
|
|||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
end
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
|
||||
theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
|
||||
induction x with
|
||||
|
|
|
|||
|
|
@ -2,11 +2,13 @@ mutual
|
|||
@[simp] def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
|
||||
@[simp] def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
end
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
|
||||
theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
|
||||
induction x with
|
||||
|
|
|
|||
|
|
@ -5,5 +5,5 @@ inductive Vector (α : Type u) : Nat → Type u
|
|||
def test [Monad m] (xs : Vector α a) : m Unit :=
|
||||
match xs with
|
||||
| Vector.nil => return ()
|
||||
| Vector.cons x xs => test xs
|
||||
termination_by test xs => sizeOf xs
|
||||
| Vector.cons _ xs => test xs
|
||||
termination_by sizeOf xs
|
||||
|
|
|
|||
|
|
@ -8,12 +8,13 @@ mutual
|
|||
def foo : Nat → Nat
|
||||
| .zero => 0
|
||||
| .succ n => (id bar) n
|
||||
decreasing_by sorry
|
||||
|
||||
def bar : Nat → Nat
|
||||
| .zero => 0
|
||||
| .succ n => foo n
|
||||
end
|
||||
termination_by foo n => n; bar n => n
|
||||
decreasing_by sorry
|
||||
end
|
||||
|
||||
end Ex1
|
||||
|
||||
|
|
@ -28,12 +29,15 @@ def foo : Nat → Nat → Nat
|
|||
| .zero, _m => 0
|
||||
| .succ n, .zero => (id' (bar n)) .zero
|
||||
| .succ n, m => (id' bar) n m
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
|
||||
def bar : Nat → Nat → Nat
|
||||
| .zero, _m => 0
|
||||
| .succ n, m => foo n m
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by foo n m => (n,m); bar n m => (n,m)
|
||||
decreasing_by sorry
|
||||
|
||||
end Ex2
|
||||
|
||||
|
|
@ -44,12 +48,12 @@ mutual
|
|||
def foo : Nat → Nat → Nat
|
||||
| .zero => fun _ => 0
|
||||
| .succ n => fun m => (id bar) n m
|
||||
decreasing_by all_goals sorry
|
||||
def bar : Nat → Nat → Nat
|
||||
| .zero => fun _ => 0
|
||||
| .succ n => fun m => foo n m
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by foo n => n; bar n => n
|
||||
decreasing_by sorry
|
||||
|
||||
end Ex3
|
||||
|
||||
|
|
@ -62,12 +66,14 @@ def foo : Nat → Nat → Nat → Nat
|
|||
| .zero, _m => fun _ => 0
|
||||
| .succ n, .zero => fun k => (id' (bar n)) .zero k
|
||||
| .succ n, m => fun k => (id' bar) n m k
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
def bar : Nat → Nat → Nat → Nat
|
||||
| .zero, _m => fun _ => 0
|
||||
| .succ n, m => fun k => foo n m k
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by foo n m => (n,m); bar n m => (n,m)
|
||||
decreasing_by sorry
|
||||
|
||||
end Ex4
|
||||
|
||||
|
|
@ -80,12 +86,12 @@ mutual
|
|||
def foo : FunType
|
||||
| .zero => 0
|
||||
| .succ n => (id bar) n
|
||||
decreasing_by all_goals sorry
|
||||
def bar : Nat → Nat
|
||||
| .zero => 0
|
||||
| .succ n => foo n
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by foo n => n; bar n => n
|
||||
decreasing_by sorry
|
||||
|
||||
end Ex5
|
||||
|
||||
|
|
@ -98,11 +104,13 @@ def foo : Nat → Nat → Nat → Nat
|
|||
| .zero, _m => fun _ => 0
|
||||
| .succ n, .zero => fun k => (id' (bar n)) .zero k
|
||||
| .succ n, m => fun k => (id' bar) n m k
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
def bar : Nat → Fun3Type
|
||||
| .zero, _m => fun _ => 0
|
||||
| .succ n, m => fun k => foo n m k
|
||||
termination_by n m => (n,m)
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by foo n m => (n,m); bar n m => (n,m)
|
||||
decreasing_by sorry
|
||||
|
||||
end Ex6
|
||||
|
|
|
|||
|
|
@ -15,11 +15,10 @@ end
|
|||
mutual
|
||||
def foo : B → Prop
|
||||
| .fromA a => bar a 0
|
||||
termination_by x => sizeOf x
|
||||
|
||||
def bar : A → Nat → Prop
|
||||
| .baseA => (fun _ => True)
|
||||
| .fromB b => (fun (c : Nat) => ∃ (t : Nat), foo b)
|
||||
termination_by x => sizeOf x
|
||||
end
|
||||
termination_by
|
||||
foo x => sizeOf x
|
||||
bar x => sizeOf x
|
||||
|
|
|
|||
|
|
@ -5,11 +5,13 @@ mutual
|
|||
def foo : FunType
|
||||
| .zero => 0
|
||||
| .succ n => bar n
|
||||
termination_by n => n
|
||||
def bar : Nat → Nat
|
||||
| .zero => 0
|
||||
| .succ n => baz n 0
|
||||
termination_by n => n
|
||||
def baz : Fun2Type
|
||||
| .zero, m => 0
|
||||
| .succ n, m => foo n
|
||||
termination_by n _ => n
|
||||
end
|
||||
termination_by foo n => n; bar n => n; baz n _ => n
|
||||
|
|
|
|||
|
|
@ -16,7 +16,10 @@ def Tree.size : Tree α → Nat
|
|||
apply Nat.lt_succ_self
|
||||
sizeList l
|
||||
| Tree.leaf _ => 1
|
||||
where sizeList : TreeList α → Nat
|
||||
-- use automatically synthesized size function, which is not quite the number of leaves
|
||||
termination_by t => sizeOf t
|
||||
where
|
||||
sizeList : TreeList α → Nat
|
||||
| TreeList.nil => 0
|
||||
| TreeList.cons t l =>
|
||||
have : sizeOf t < 1 + sizeOf t + sizeOf l := by
|
||||
|
|
@ -28,7 +31,4 @@ where sizeList : TreeList α → Nat
|
|||
apply Nat.lt_succ_of_le
|
||||
apply Nat.le_add_left
|
||||
t.size + sizeList l
|
||||
-- use automatically synthesized size function, which is not quite the number of leaves
|
||||
termination_by
|
||||
size t => sizeOf t
|
||||
sizeList l => sizeOf l
|
||||
termination_by l => sizeOf l
|
||||
|
|
|
|||
|
|
@ -47,4 +47,4 @@ def List.mergeSort (p : α → α → Bool) (as : List α) : List α :=
|
|||
merge p (mergeSort p as') (mergeSort p bs')
|
||||
else
|
||||
as
|
||||
termination_by _ as => as.length
|
||||
termination_by as.length
|
||||
|
|
|
|||
|
|
@ -19,6 +19,8 @@ def Tree.size : Tree α → Nat
|
|||
apply Nat.lt_succ_self
|
||||
sizeList l
|
||||
| Tree.leaf _ => 1
|
||||
-- use automatically synthesized size function, which is not quite the number of leaves
|
||||
termination_by t => sizeOf t
|
||||
|
||||
def Tree.sizeList : TreeList α → Nat
|
||||
| TreeList.nil => 0
|
||||
|
|
@ -32,11 +34,8 @@ def Tree.sizeList : TreeList α → Nat
|
|||
apply Nat.lt_succ_of_le
|
||||
apply Nat.le_add_left
|
||||
t.size + sizeList l
|
||||
termination_by l => sizeOf l
|
||||
end
|
||||
-- use automatically synthesized size function, which is not quite the number of leaves
|
||||
termination_by
|
||||
size t => sizeOf t
|
||||
sizeList l => sizeOf l
|
||||
|
||||
end Mutual
|
||||
|
||||
|
|
@ -54,6 +53,7 @@ def Tree.size : Tree α → Nat
|
|||
apply Nat.lt_succ_self
|
||||
sizeList l
|
||||
| Tree.leaf _ => 1
|
||||
termination_by t => sizeOf t
|
||||
|
||||
def Tree.sizeList : List (Tree α) → Nat
|
||||
| [] => 0
|
||||
|
|
@ -67,9 +67,7 @@ def Tree.sizeList : List (Tree α) → Nat
|
|||
apply Nat.lt_succ_of_le
|
||||
apply Nat.le_add_left
|
||||
t.size + sizeList l
|
||||
termination_by l => sizeOf l
|
||||
end
|
||||
termination_by
|
||||
size t => sizeOf t
|
||||
sizeList l => sizeOf l
|
||||
|
||||
end Nested
|
||||
|
|
|
|||
|
|
@ -3,19 +3,18 @@ mutual
|
|||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n, a, b => g a n b |>.1
|
||||
termination_by n _ _ => (n, 2)
|
||||
|
||||
def g : α → Nat → α → (α × α)
|
||||
| a, 0, b => (a, b)
|
||||
| a, n, b => (h a b n, a)
|
||||
termination_by _ n _ => (n, 1)
|
||||
|
||||
def h : α → α → Nat → α
|
||||
| a, b, 0 => b
|
||||
| a, b, n+1 => f n a b
|
||||
termination_by _ _ n => (n, 0)
|
||||
end
|
||||
termination_by
|
||||
f n _ _ => (n, 2)
|
||||
g _ n _ => (n, 1)
|
||||
h _ _ n => (n, 0)
|
||||
|
||||
#print f
|
||||
#print g
|
||||
|
|
|
|||
|
|
@ -3,11 +3,12 @@ mutual
|
|||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
termination_by n => n
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
termination_by n => n
|
||||
end
|
||||
termination_by _ n => n
|
||||
|
||||
#print isEven
|
||||
#print isOdd
|
||||
|
|
|
|||
|
|
@ -3,26 +3,30 @@ mutual
|
|||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n, a, b => g a n b |>.1
|
||||
termination_by n _ _ => (n, 2)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.right
|
||||
decide
|
||||
|
||||
def g : α → Nat → α → (α × α)
|
||||
| a, 0, b => (a, b)
|
||||
| a, n, b => (h a b n, a)
|
||||
termination_by _ n _ => (n, 1)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.right
|
||||
decide
|
||||
|
||||
def h : α → α → Nat → α
|
||||
| _a, b, 0 => b
|
||||
| a, b, n+1 => f n a b
|
||||
end
|
||||
termination_by
|
||||
f n _ _ => (n, 2)
|
||||
g _ n _ => (n, 1)
|
||||
h _ _ n => (n, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.left
|
||||
termination_by _ _ n => (n, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.left
|
||||
apply Nat.lt_succ_self
|
||||
| apply Prod.Lex.right
|
||||
decide
|
||||
end
|
||||
|
||||
#eval f 5 'a' 'b'
|
||||
#print f
|
||||
|
|
@ -36,19 +40,18 @@ mutual
|
|||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n, a, b => g a n b |>.1
|
||||
termination_by n _ _ => (n, 2)
|
||||
|
||||
def g : α → Nat → α → (α × α)
|
||||
| a, 0, b => (a, b)
|
||||
| a, n, b => (h a b n, a)
|
||||
termination_by _ n _ => (n, 1)
|
||||
|
||||
def h : α → α → Nat → α
|
||||
| a, b, 0 => b
|
||||
| a, b, n+1 => f n a b
|
||||
termination_by _ _ n => (n, 0)
|
||||
end
|
||||
termination_by
|
||||
f n _ _ => (n, 2)
|
||||
g _ n _ => (n, 1)
|
||||
h _ _ n => (n, 0)
|
||||
|
||||
#print f._unary._mutual
|
||||
|
||||
|
|
|
|||
|
|
@ -1,19 +1,17 @@
|
|||
set_option trace.Elab.definition.wf true in
|
||||
mutual
|
||||
def f : Nat → Bool → Nat
|
||||
| n, true => 2 * f n false
|
||||
| 0, false => 1
|
||||
| n, false => n + g n
|
||||
termination_by n b => (n, if b then 2 else 1)
|
||||
|
||||
def g (n : Nat) : Nat :=
|
||||
if h : n ≠ 0 then
|
||||
f (n-1) true
|
||||
else
|
||||
n
|
||||
termination_by (n, 0)
|
||||
end
|
||||
termination_by
|
||||
f n b => (n, if b then 2 else 1)
|
||||
g n => (n, 0)
|
||||
|
||||
#print f
|
||||
#print g
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ def g (t : Nat) : Nat := match t with
|
|||
| 0 => 0
|
||||
| m + 1 => g n
|
||||
| 0 => 0
|
||||
decreasing_by sorry
|
||||
decreasing_by all_goals sorry
|
||||
|
||||
attribute [simp] g
|
||||
|
||||
|
|
|
|||
|
|
@ -4,6 +4,9 @@ mutual
|
|||
def h (c : Nat) (x : Nat) := match g c x c c with
|
||||
| 0 => 1
|
||||
| r => r + 2
|
||||
termination_by 0
|
||||
decreasing_by all_goals sorry
|
||||
|
||||
def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
|
||||
| (n+1) => match g c n a b with
|
||||
| 0 => 0
|
||||
|
|
@ -11,15 +14,15 @@ def g (c : Nat) (t : Nat) (a b : Nat) : Nat := match t with
|
|||
| 0 => 0
|
||||
| m + 1 => g c m a b
|
||||
| 0 => f c 0
|
||||
termination_by 0
|
||||
decreasing_by all_goals sorry
|
||||
|
||||
def f (c : Nat) (x : Nat) := match h c x with
|
||||
| 0 => 1
|
||||
| r => f c r
|
||||
termination_by 0
|
||||
decreasing_by all_goals sorry
|
||||
end
|
||||
termination_by
|
||||
g x a b => 0
|
||||
f c x => 0
|
||||
h c x => 0
|
||||
decreasing_by sorry
|
||||
|
||||
attribute [simp] g
|
||||
attribute [simp] h
|
||||
|
|
@ -43,7 +46,7 @@ def g (t : Nat) : Nat := match t with
|
|||
| 0 => 0
|
||||
| m + 1 => g n
|
||||
| 0 => 0
|
||||
decreasing_by sorry
|
||||
decreasing_by all_goals sorry
|
||||
|
||||
theorem ex1 : g 0 = 0 := by
|
||||
rw [g]
|
||||
|
|
|
|||
|
|
@ -10,14 +10,13 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
|
|||
· have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
|
||||
subst heq
|
||||
exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
|
||||
termination_by _ => a.size - i
|
||||
termination_by _ _ _ => a.size - i
|
||||
|
||||
@[simp] def f (x y : Nat) : Nat → Nat :=
|
||||
if h : x > 0 then
|
||||
fun z => f (x - 1) (y + 1) z + 1
|
||||
else
|
||||
(· + y)
|
||||
termination_by
|
||||
f x y => x
|
||||
termination_by x
|
||||
|
||||
#check f._eq_1
|
||||
|
|
|
|||
|
|
@ -4,13 +4,12 @@ def fn (f : α → α) (a : α) (n : Nat) : α :=
|
|||
match n with
|
||||
| 0 => a
|
||||
| n+1 => gn f (f (f a)) (f a) n
|
||||
termination_by n
|
||||
|
||||
def gn (f : α → α) (a b : α) (n : Nat) : α :=
|
||||
match n with
|
||||
| 0 => b
|
||||
| n+1 => fn f (f b) n
|
||||
termination_by n
|
||||
|
||||
end
|
||||
termination_by
|
||||
fn n => n
|
||||
gn n => n
|
||||
|
|
|
|||
|
|
@ -1,6 +0,0 @@
|
|||
def f (as : Array Nat) (hsz : as.size > 0) (i : Nat) : Nat :=
|
||||
if h : i < as.size then
|
||||
as.get ⟨i, h⟩ + f as hsz (i + 1)
|
||||
else
|
||||
0
|
||||
termination_by f a h i => a.size - i
|
||||
|
|
@ -41,11 +41,10 @@ def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
|
|||
| .Var i, .Var j =>
|
||||
if i = j then ⟨ some id, sorry ⟩
|
||||
else ⟨ some λ n => if n = i then j else n, sorry ⟩
|
||||
termination_by _ u v => (u, v)
|
||||
termination_by (u, v)
|
||||
decreasing_by
|
||||
first
|
||||
| apply decr_left _ _ _ _
|
||||
| apply decr_right _ _ _ _ _
|
||||
· apply decr_left _ _ _ _
|
||||
· apply decr_right _ _ _ _ _
|
||||
|
||||
attribute [simp] robinson
|
||||
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ where
|
|||
iter n next
|
||||
else
|
||||
guess
|
||||
termination_by iter guess => guess
|
||||
termination_by guess
|
||||
|
||||
end Std.Data.Nat.Basic
|
||||
|
||||
|
|
|
|||
|
|
@ -14,8 +14,9 @@ def len : List α → Nat
|
|||
| l =>
|
||||
match splitList l with
|
||||
| ListSplit.split fst snd => len fst + len snd
|
||||
termination_by _ l => l.length
|
||||
termination_by l => l.length
|
||||
decreasing_by
|
||||
all_goals
|
||||
simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf] <;>
|
||||
first
|
||||
| apply Nat.lt_add_right
|
||||
|
|
|
|||
|
|
@ -32,7 +32,7 @@ def len : List α → Nat
|
|||
have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
|
||||
have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
|
||||
len fst + len snd
|
||||
termination_by _ xs => xs.length
|
||||
termination_by xs => xs.length
|
||||
|
||||
theorem len_nil : len ([] : List α) = 0 := by
|
||||
simp [len]
|
||||
|
|
@ -76,12 +76,13 @@ def len : List α → Nat
|
|||
match h₂ : l, h₃ : splitList l with
|
||||
| _, ListSplit.split fst snd =>
|
||||
len fst + len snd
|
||||
termination_by _ xs => xs.length
|
||||
termination_by xs => xs.length
|
||||
decreasing_by
|
||||
simp_wf
|
||||
have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
|
||||
subst h₂
|
||||
simp_arith [eq_of_heq h₃] at this |- ; simp [this]
|
||||
all_goals
|
||||
simp_wf
|
||||
have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
|
||||
subst h₂
|
||||
simp_arith [eq_of_heq h₃] at this |- ; simp [this]
|
||||
|
||||
theorem len_nil : len ([] : List α) = 0 := by
|
||||
simp [len]
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ def List.unfoldr' {α β : Type u} [w : WellFoundedRelation β] (f : (b : β)
|
|||
match f b with
|
||||
| none => []
|
||||
| some (a, ⟨b', h⟩) => a :: unfoldr' f b'
|
||||
termination_by unfoldr' b => b
|
||||
termination_by b
|
||||
|
||||
-- We need the `master` branch to test the following example
|
||||
|
||||
|
|
|
|||
|
|
@ -9,13 +9,17 @@ mutual
|
|||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
end
|
||||
decreasing_by
|
||||
simp [measure, invImage, InvImage, Nat.lt_wfRel]
|
||||
apply Nat.lt_succ_self
|
||||
|
||||
#print isEven
|
||||
|
||||
|
|
|
|||
|
|
@ -11,21 +11,24 @@ def g (i j : Nat) : Nat :=
|
|||
match j with
|
||||
| Nat.zero => 1
|
||||
| Nat.succ j => h i j
|
||||
termination_by (i + j, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
· apply Prod.Lex.left
|
||||
apply Nat.lt_succ_self
|
||||
|
||||
def h (i j : Nat) : Nat :=
|
||||
match j with
|
||||
| 0 => g i 0
|
||||
| Nat.succ j => g i j
|
||||
end
|
||||
termination_by
|
||||
g i j => (i + j, 0)
|
||||
h i j => (i + j, 1)
|
||||
termination_by (i + j, 1)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.left
|
||||
apply Nat.lt_succ_self
|
||||
| apply Prod.Lex.right
|
||||
all_goals simp_wf
|
||||
· apply Prod.Lex.right
|
||||
decide
|
||||
· apply Prod.Lex.left
|
||||
apply Nat.lt_succ_self
|
||||
end
|
||||
|
||||
#eval tst ``g
|
||||
#check g._eq_1
|
||||
|
|
|
|||
|
|
@ -9,26 +9,30 @@ mutual
|
|||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n, a, b => g a n b |>.1
|
||||
termination_by n _ _ => (n, 2)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.right
|
||||
decide
|
||||
|
||||
def g : α → Nat → α → (α × α)
|
||||
| a, 0, b => (a, b)
|
||||
| a, n, b => (h a b n, a)
|
||||
termination_by _ n _ => (n, 1)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.right
|
||||
decide
|
||||
|
||||
def h : α → α → Nat → α
|
||||
| a, b, 0 => b
|
||||
| a, b, n+1 => f n a b
|
||||
end
|
||||
termination_by
|
||||
f n _ _ => (n, 2)
|
||||
g _ n _ => (n, 1)
|
||||
h _ _ n => (n, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
first
|
||||
| apply Prod.Lex.left
|
||||
termination_by _ _ n => (n, 0)
|
||||
decreasing_by
|
||||
simp_wf
|
||||
apply Prod.Lex.left
|
||||
apply Nat.lt_succ_self
|
||||
| apply Prod.Lex.right
|
||||
decide
|
||||
end
|
||||
|
||||
#eval f 5 'a' 'b'
|
||||
|
||||
|
|
|
|||
|
|
@ -84,4 +84,4 @@ def Stmt.mapCtx (f : HList Γ' → HList Γ) : Stmt m ω Γ Δ b c β → Stmt m
|
|||
| sfor e body => sfor (e ∘ f) (body.mapCtx (fun | HList.cons a as => HList.cons a (f as)))
|
||||
| sbreak => sbreak
|
||||
| scont => scont
|
||||
termination_by mapCtx _ s => sizeOf s
|
||||
termination_by s => sizeOf s
|
||||
|
|
|
|||
|
|
@ -3,4 +3,4 @@ def foo : Nat → Nat → Nat
|
|||
| s+1, 0 => foo s 0 + 1
|
||||
| 0, b+1 => foo 0 b + 1
|
||||
| s+1, b+1 => foo (s+1) b + foo s (b+1)
|
||||
termination_by foo b s => (b, s)
|
||||
termination_by b s => (b, s)
|
||||
|
|
|
|||
|
|
@ -8,5 +8,5 @@ theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h
|
|||
next he => subst a; apply sizeOf_get_lt
|
||||
next => have ih := aux (j+1) h; assumption
|
||||
· contradiction
|
||||
termination_by as.size - j
|
||||
apply aux 0 h
|
||||
termination_by aux j => as.size - j
|
||||
|
|
|
|||
|
|
@ -6,4 +6,4 @@ where
|
|||
go (i+1) (s + as.get ⟨i, h⟩)
|
||||
else
|
||||
s
|
||||
termination_by _ i s => as.size - i
|
||||
termination_by as.size - i
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ namespace Ex3
|
|||
def heapifyDown (a : Array α) (i : Fin a.size) : Array α :=
|
||||
have : i < i := sorry
|
||||
heapifyDown a ⟨i.1, a.size_swap i i ▸ i.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
|
||||
termination_by _ i => i.1
|
||||
termination_by i.1
|
||||
decreasing_by assumption
|
||||
end Ex3
|
||||
|
||||
|
|
@ -34,6 +34,6 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : Arra
|
|||
heapifyDown lt a' ⟨j.1.1, a.size_swap i j ▸ j.1.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
|
||||
else
|
||||
a
|
||||
termination_by _ a i => a.size - i.1
|
||||
termination_by a.size - i.1
|
||||
decreasing_by assumption
|
||||
end Ex4
|
||||
|
|
|
|||
|
|
@ -1,105 +1,85 @@
|
|||
mutual
|
||||
inductive Even : Nat → Prop
|
||||
| base : Even 0
|
||||
| step : Odd n → Even (n+1)
|
||||
inductive Odd : Nat → Prop
|
||||
| step : Even n → Odd (n+1)
|
||||
end
|
||||
termination_by _ n => n -- Error
|
||||
/-!
|
||||
This module tests various mis-uses of termination_by and decreasing_by:
|
||||
* use in non-recursive functions
|
||||
* that all or none of a recursive group have termination_by.
|
||||
-/
|
||||
|
||||
def nonRecursive1 (n : Nat) : Nat := n
|
||||
termination_by n -- Error
|
||||
|
||||
def nonRecursive2 (n : Nat) : Nat := n
|
||||
decreasing_by sorry -- Error
|
||||
|
||||
def nonRecursive3 (n : Nat) : Nat := n
|
||||
termination_by n -- Error
|
||||
decreasing_by sorry
|
||||
|
||||
partial def partial1 (n : Nat) : Nat := partial1 n
|
||||
termination_by n -- Error
|
||||
|
||||
partial def partial2 (n : Nat) : Nat := partial2 n
|
||||
decreasing_by sorry -- Error
|
||||
|
||||
partial def partial3 (n : Nat) : Nat := partial3 n
|
||||
termination_by n -- Error
|
||||
decreasing_by sorry
|
||||
|
||||
unsafe def unsafe1 (n : Nat) : Nat := unsafe1 n
|
||||
termination_by n -- Error
|
||||
|
||||
unsafe def unsafe2 (n : Nat) : Nat := unsafe2 n
|
||||
decreasing_by sorry -- Error
|
||||
|
||||
unsafe def unsafe3 (n : Nat) : Nat := unsafe3 n
|
||||
termination_by x -- Error
|
||||
decreasing_by sorry
|
||||
|
||||
unsafe def withWhere (n : Nat) : Nat := foo n
|
||||
where foo (n : Nat) := n
|
||||
termination_by n -- Error
|
||||
|
||||
unsafe def withLetRec (n : Nat) : Nat :=
|
||||
let rec foo (n : Nat) := n
|
||||
termination_by n -- Error
|
||||
foo n
|
||||
|
||||
mutual
|
||||
def f (n : Nat) :=
|
||||
if n == 0 then 0 else f (n / 2) + 1
|
||||
termination_by _ => n -- Error
|
||||
def rec : Nat → Nat
|
||||
| 0 => 0
|
||||
| n+1 => rec n + notrec n
|
||||
termination_by x => x
|
||||
|
||||
def notrec (n : Nat) : Nat := n
|
||||
termination_by n -- Error
|
||||
end
|
||||
|
||||
mutual
|
||||
def f (n : Nat) :=
|
||||
if n == 0 then 0 else f (n / 2) + 1
|
||||
end
|
||||
termination_by n => n -- Error
|
||||
|
||||
|
||||
def g' (n : Nat) :=
|
||||
match n with
|
||||
| 0 => 1
|
||||
| n+1 => g' n * 3
|
||||
termination_by
|
||||
h' n => n -- Error
|
||||
|
||||
def g' (n : Nat) :=
|
||||
match n with
|
||||
| 0 => 1
|
||||
| n+1 => g' n * 3
|
||||
termination_by
|
||||
g' n => n
|
||||
_ n => n -- Error
|
||||
|
||||
mutual
|
||||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
def isOdd : Nat → Bool
|
||||
termination_by x => x
|
||||
|
||||
def isOdd : Nat → Bool -- Error
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
end
|
||||
termination_by
|
||||
isEven x => x -- Error
|
||||
|
||||
mutual
|
||||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
end
|
||||
termination_by
|
||||
isEven x => x
|
||||
isOd x => x -- Error
|
||||
|
||||
mutual
|
||||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
end
|
||||
termination_by
|
||||
isEven x => x
|
||||
isEven y => y -- Error
|
||||
|
||||
mutual
|
||||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
end
|
||||
termination_by
|
||||
isEven x => x
|
||||
_ x => x
|
||||
_ x => x + 1 -- Error
|
||||
|
||||
|
||||
namespace Test
|
||||
mutual
|
||||
def f : Nat → α → α → α
|
||||
| 0, a, b => a
|
||||
| n+1, a, b => g n a b |>.1
|
||||
termination_by n _ _ => n
|
||||
|
||||
def g : Nat → α → α → (α × α)
|
||||
| 0, a, b => (a, b)
|
||||
| n+1, a, b => (h n a b, a)
|
||||
termination_by n _ _ => n
|
||||
|
||||
def h : Nat → α → α → α
|
||||
def h : Nat → α → α → α -- Error
|
||||
| 0, a, b => b
|
||||
| n+1, a, b => f n a b
|
||||
end
|
||||
termination_by
|
||||
f n => n -- Error
|
||||
g n => n
|
||||
|
||||
end Test
|
||||
|
|
|
|||
|
|
@ -1,10 +1,14 @@
|
|||
termination_by.lean:8:0-8:23: error: invalid 'termination_by' in mutually inductive datatype declaration
|
||||
termination_by.lean:13:1-13:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
|
||||
termination_by.lean:20:15-20:21: error: function 'n' not found in current declaration
|
||||
termination_by.lean:28:2-28:11: error: function 'h'' not found in current declaration
|
||||
termination_by.lean:36:2-36:10: error: invalid `termination_by` syntax, unnecessary else-case
|
||||
termination_by.lean:47:3-47:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
|
||||
termination_by.lean:59:3-59:14: error: function 'isOd' not found in current declaration
|
||||
termination_by.lean:71:3-71:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
|
||||
termination_by.lean:84:3-84:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
|
||||
termination_by.lean:102:2-102:10: error: invalid `termination_by` syntax, missing case for function 'Test.h'
|
||||
termination_by.lean:8:2-8:18: error: unused `termination_by`, function is not recursive
|
||||
termination_by.lean:11:2-11:21: error: unused `decreasing_by`, function is not recursive
|
||||
termination_by.lean:14:2-15:21: error: unused termination hints, function is not recursive
|
||||
termination_by.lean:18:2-18:18: error: unused `termination_by`, function is partial
|
||||
termination_by.lean:21:2-21:21: error: unused `decreasing_by`, function is partial
|
||||
termination_by.lean:24:2-25:21: error: unused termination hints, function is partial
|
||||
termination_by.lean:28:0-28:16: error: unused `termination_by`, function is unsafe
|
||||
termination_by.lean:31:2-31:21: error: unused `decreasing_by`, function is unsafe
|
||||
termination_by.lean:34:2-35:21: error: unused termination hints, function is unsafe
|
||||
termination_by.lean:39:4-39:20: error: unused `termination_by`, function is not recursive
|
||||
termination_by.lean:43:4-43:20: error: unused `termination_by`, function is not recursive
|
||||
termination_by.lean:53:2-53:18: error: unused `termination_by`, function is not recursive
|
||||
termination_by.lean:63:6-63:11: error: Missing `termination_by`; this function is mutually recursive with isEven, which has a `termination_by` clause.
|
||||
termination_by.lean:80:6-80:7: error: Missing `termination_by`; this function is mutually recursive with Test.f, which has a `termination_by` clause.
|
||||
|
|
|
|||
119
tests/lean/termination_by_vars.lean
Normal file
119
tests/lean/termination_by_vars.lean
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
/-!
|
||||
Here we test that lean correctly complains if `termination_by` has too many variables,
|
||||
and that it does the right thing if it has fewer variables.
|
||||
-/
|
||||
|
||||
opaque dec1 : Nat → Nat
|
||||
axiom dec1_lt (n : Nat) : dec1 n < n
|
||||
opaque dec2 : Nat → Nat
|
||||
axiom dec2_lt (n : Nat) : dec2 n < n
|
||||
|
||||
namespace Basic
|
||||
|
||||
def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n)
|
||||
termination_by x => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n)
|
||||
termination_by n
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
|
||||
def blankArrow (n : Nat) : Nat := blankArrow (dec1 n)
|
||||
termination_by => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b => fewerVariables1 (dec2 n) a (dec1 b)
|
||||
termination_by n -- Not an error
|
||||
decreasing_by apply dec2_lt
|
||||
|
||||
def fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => fewerVariables2 n (dec1 a) (dec2 b)
|
||||
termination_by a => a
|
||||
decreasing_by apply dec1_lt -- NB: dec2_lt would no work
|
||||
|
||||
def okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => okVariables2 n (dec1 a) (dec2 b)
|
||||
termination_by a b => b
|
||||
decreasing_by apply dec2_lt
|
||||
|
||||
def tooManyVariables2 (n : Nat) : Nat → Nat → Nat := fun a b => tooManyVariables2 n (dec1 a) (dec2 b)
|
||||
termination_by a b c => b
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
end Basic
|
||||
|
||||
namespace WithVariable
|
||||
|
||||
variable (v : Nat)
|
||||
|
||||
def tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n) + v
|
||||
termination_by x => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n) + v
|
||||
termination_by n
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
|
||||
def blankArrow (n : Nat) : Nat := blankArrow (dec1 n) + v
|
||||
termination_by => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
fewerVariables1 (dec2 n) a (dec1 b) + v
|
||||
termination_by n
|
||||
decreasing_by apply dec2_lt
|
||||
|
||||
def fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
fewerVariables2 n (dec1 a) (dec2 b) + v
|
||||
termination_by a => a
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
okVariables2 n a (dec1 b) + v
|
||||
termination_by a b => b
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
end WithVariable
|
||||
|
||||
namespace InLetRec
|
||||
|
||||
def foo1 (v : Nat) := 5
|
||||
where
|
||||
tooManyVars (n : Nat) : Nat := tooManyVars (dec1 n) + v
|
||||
termination_by x => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def foo2 (v : Nat) := 5
|
||||
where
|
||||
okVariables1 (n : Nat) : Nat := okVariables1 (dec1 n) + v
|
||||
termination_by n
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def foo3 (v : Nat) := 5
|
||||
where
|
||||
blankArrow (n : Nat) : Nat := blankArrow (dec1 n) + v
|
||||
termination_by => x -- Error
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def foo4 (v : Nat) := 5
|
||||
where
|
||||
fewerVariables1 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
fewerVariables1 (dec2 n) a (dec1 b) + v
|
||||
termination_by n
|
||||
decreasing_by apply dec2_lt
|
||||
|
||||
def foo5 (v : Nat) := 5
|
||||
where
|
||||
fewerVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
fewerVariables2 n (dec1 a) (dec2 b) + v
|
||||
termination_by a => a
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
def foo6 (v : Nat) := 5
|
||||
where
|
||||
okVariables2 (n : Nat) : Nat → Nat → Nat := fun a b =>
|
||||
okVariables2 n a (dec1 b) + v
|
||||
termination_by a b => b
|
||||
decreasing_by apply dec1_lt
|
||||
|
||||
end InLetRec
|
||||
7
tests/lean/termination_by_vars.lean.expected.out
Normal file
7
tests/lean/termination_by_vars.lean.expected.out
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
termination_by_vars.lean:14:2-14:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
|
||||
termination_by_vars.lean:23:2-23:21: error: no extra parameters bounds, please omit the `=>`
|
||||
termination_by_vars.lean:39:2-39:27: error: Too many extra parameters bound; the function definition only has 2 extra parameters.
|
||||
termination_by_vars.lean:49:2-49:23: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
|
||||
termination_by_vars.lean:58:2-58:21: error: no extra parameters bounds, please omit the `=>`
|
||||
termination_by_vars.lean:83:4-83:25: error: Too many extra parameters bound; the function definition only has 0 extra parameters.
|
||||
termination_by_vars.lean:95:4-95:23: error: no extra parameters bounds, please omit the `=>`
|
||||
16
tests/lean/termination_by_where.lean
Normal file
16
tests/lean/termination_by_where.lean
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
/-!
|
||||
This module systematically tests the relative placement of `decreasing_by` and `where`.
|
||||
-/
|
||||
|
||||
-- For concise recursive definition that need well-founded recursion
|
||||
-- and `decreasing_by` tactics that would fail if run on the wrong function
|
||||
opaque dec1 : Nat → Nat
|
||||
axiom dec1_lt (n : Nat) : dec1 n < n
|
||||
opaque dec2 : Nat → Nat
|
||||
axiom dec2_lt (n : Nat) : dec2 n < n
|
||||
|
||||
def foo (n : Nat) := foo (dec1 n) + bar n
|
||||
decreasing_by apply dec1_lt
|
||||
where
|
||||
bar (m : Nat) : Nat := bar (dec2 m)
|
||||
decreasing_by apply dec2_lt
|
||||
0
tests/lean/termination_by_where.lean.expected.out
Normal file
0
tests/lean/termination_by_where.lean.expected.out
Normal file
|
|
@ -6,4 +6,4 @@ open TreeNode in def treeToList (t : TreeNode) : List String :=
|
|||
match t with
|
||||
| mkLeaf name => [name]
|
||||
| mkNode name children => name :: List.join (children.map treeToList)
|
||||
termination_by _ t => t
|
||||
termination_by t
|
||||
|
|
|
|||
|
|
@ -2,11 +2,12 @@ mutual
|
|||
def isEven : Nat → Bool
|
||||
| 0 => true
|
||||
| n+1 => isOdd n
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
def isOdd : Nat → Bool
|
||||
| 0 => false
|
||||
| n+1 => isEven n
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
end
|
||||
decreasing_by apply Nat.lt_succ_self
|
||||
|
||||
theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
|
||||
induction x with
|
||||
|
|
|
|||
|
|
@ -3,4 +3,4 @@ def g (x : Nat) (y : Nat) : Nat :=
|
|||
2 * g (x-1) y -- Error here
|
||||
else
|
||||
0
|
||||
termination_by g x y => x
|
||||
termination_by x
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue