Skip to content

Commit

Permalink
More strict termination_by
Browse files Browse the repository at this point in the history
implements #3081.
  • Loading branch information
nomeata committed Dec 19, 2023
1 parent fd6a606 commit 943cd8c
Show file tree
Hide file tree
Showing 18 changed files with 292 additions and 80 deletions.
30 changes: 17 additions & 13 deletions src/Lean/Elab/LetRec.lean
Original file line number Diff line number Diff line change
Expand Up @@ -94,19 +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!
termination := view.termination
: 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
Expand Down
6 changes: 4 additions & 2 deletions src/Lean/Elab/MutualDef.lean
Original file line number Diff line number Diff line change
Expand Up @@ -634,11 +634,14 @@ def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
| _ => none
| _ => none


def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr)
(mainHeaders : Array DefViewElabHeader) (mainVals : Array Expr)
: 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 {
Expand All @@ -647,8 +650,7 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr)
declName := header.declName
levelParams := [], -- we set it later
modifiers := header.modifiers
type, value
termination := declValToTerminationHint header.valueStx
type, value, termination
}

def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : MetaM (Array PreDefinition) :=
Expand Down
3 changes: 0 additions & 3 deletions src/Lean/Elab/PreDefinition/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,6 @@ namespace Lean.Elab
open Meta
open Term

/-- All termination hints for a given clique -/
def TerminationHints := Array (TSyntax ``Parser.Termination.suffix)

private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := false) : TermElabM Unit := do
for preDef in preDefs do
trace[Elab.definition] "processing {preDef.declName}"
Expand Down
39 changes: 29 additions & 10 deletions src/Lean/Elab/PreDefinition/WF/GuessLex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -79,9 +79,13 @@ Use user-given parameter names if present; use x1...xn otherwise.
The length of the returned array is also used to determine the arity
of the function, so it should match what `packDomain` does.
The names ought to accessible (no macro scopes) and still fresh wrt to the current environment,
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 variabes).
-/
partial
def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do
Expand All @@ -90,8 +94,11 @@ def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array
let mut ns : Array Name := #[]
for h : i in [:xs.size] do
let n ← (xs[i]'h.2).fvarId!.getUserName
let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
ns := ns.push (← freshen ns n)
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
Expand Down Expand Up @@ -538,19 +545,30 @@ def mkTupleSyntax : Array Term → MetaM Term
Given an array of `MutualMeasures`, creates a `TerminationWF` that specifies the lexicographic
combination of these measures.
-/
def buildTermWF (varNamess : Array (Array Name)) (measures : Array MutualMeasure) :
MetaM TerminationWF := do
def buildTermWF (extraParams : Array Nat) (varNamess : Array (Array Name))
(measures : Array MutualMeasure) : MetaM TerminationWF := do
let mut termByElements := #[]
for h : funIdx in [:varNamess.size] do
let vars := (varNamess[funIdx]'h.2).map mkIdent
let body ← mkTupleSyntax (← measures.mapM fun
| .args varIdxs => do
let v := vars.get! (varIdxs[funIdx]!)
let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
let varIdx := varIdxs[funIdx]!
let v := vars[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, which
-- we detect in a rather ad-hoc way here.
let sizeOfIdent :=
if vars.any (·.getId = `sizeOf) then
mkIdent ``sizeOf -- fully qualified
else
mkIdent (← unresolveNameGlobal ``sizeOf)
`($sizeOfIdent $v)
| .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
)
termByElements := termByElements.push { ref := .missing, vars, body }
let extraVars := vars[vars.size - extraParams[funIdx]! : vars.size]
termByElements := termByElements.push { ref := .missing, vars := extraVars, body }
return termByElements


Expand Down Expand Up @@ -665,6 +683,7 @@ terminates. See the module doc string for a high-level overview.
def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
(fixedPrefixSize : Nat) :
MetaM TerminationWF := do
let extraParamss := preDefs.map (·.termination.extraParams)
let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
let arities := varNamess.map (·.size)
trace[Elab.definition.wf] "varNames is: {varNamess}"
Expand All @@ -678,7 +697,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)

-- If there is only one plausible measure, use that
if let #[solution] := measures then
return ← buildTermWF varNamess #[solution]
return ← buildTermWF extraParamss varNamess #[solution]

-- Collect all recursive calls and extract their context
let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
Expand All @@ -688,7 +707,7 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)

match ← liftMetaM <| solve measures callMatrix with
| .some solution => do
let wf ← buildTermWF varNamess solution
let wf ← buildTermWF extraParamss varNamess solution

if showInferredTerminationBy.get (← getOptions) then
for preDef in preDefs, term in wf do
Expand Down
45 changes: 41 additions & 4 deletions src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,12 @@ structure TerminationBy where

open Parser.Termination in
def TerminationBy.unexpand (wf : TerminationBy) : MetaM Syntax := do
-- TODO: Why can I not use $wf.vars below?
-- TODO: Why can I not just use $wf.vars in the quotation below?
let vars : TSyntaxArray `ident := wf.vars.map (⟨·.raw⟩)
`(terminationBy|termination_by $vars* => $wf.body)
if vars.isEmpty then
`(terminationBy|termination_by $wf.body)
else
`(terminationBy|termination_by $vars* => $wf.body)

/-- A complete set of `termination_by` hints, as applicable to a single clique. -/
abbrev TerminationWF := Array TerminationBy
Expand All @@ -41,9 +44,18 @@ structure TerminationHints where
ref : Syntax
termination_by? : Option TerminationBy
decreasing_by? : Option DecreasingBy
/-- Here we record the number of paramters past the `:`. This is currently
only used by GuessLex when there is no `termination_by` annotation, so that
we can print the guessed order in the right form.
It it set in `TerminationHints.checkVars`, which is the place where we
check that we have the right number of variables when there *is* a user-provided
`termination_by`.
-/
extraParams : Nat
deriving Inhabited

def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none⟩
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
Expand All @@ -56,6 +68,29 @@ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String): Co
| .some _, .some _ =>
logErrorAt hints.ref m!"unused termination hints, function is {reason}"

/--
Checks that `termination_by` binds exactly as many variables are present in the outermost
lambda of `value`, and logs (without failing) appropriate errors.
Also remembers `extraParams`, so that we can later (in GuessLex) produce valid termination hints.
-/
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
if tb.vars.isEmpty then
logErrorAt tb.ref <| m!"The function definition has {extraParams} extra parameters. " ++
"These need to be bound here (`termination_by x1 ... xn =>`)."
else if extraParams = 0 then
logErrorAt tb.ref <| "The function definition has no extra parameters, so `termination_by` " ++
"should not bind any. Variables bound in the function header can be referred directly."
else
logErrorAt tb.ref <| m!"The function definition has {extraParams} extra paramters, " ++
m!"but {tb.vars.size} variables are bound here. Bind exactly {extraParams} variables here!"
return { hints with extraParams := extraParams }


open Parser.Termination

def elabTerminationHints (stx : TSyntax ``suffix) : TerminationHints :=
Expand All @@ -69,10 +104,12 @@ def elabTerminationHints (stx : TSyntax ``suffix) : TerminationHints :=
{ ref := stx
termination_by? := t?.map fun t => match t with
| `(terminationBy|termination_by $vars* => $body) => {ref := t, vars, body}
| `(terminationBy|termination_by $body:term) => {ref := t, vars := #[], body}
| _ => unreachable!
decreasing_by? := d?.map fun t => match t with
| `(decreasingBy|decreasing_by $tactic) => {ref := t, tactic}
| _ => unreachable! }
| _ => unreachable!
extraParams := 0 }
| _ => panic! s!"Unexpected Termination.suffix syntax: {stx} of kind {stx.raw.getKind}"

end Lean.Elab.WF
16 changes: 12 additions & 4 deletions src/Lean/Parser/Term.lean
Original file line number Diff line number Diff line change
Expand Up @@ -106,16 +106,24 @@ letrec we need them here already.
/--
Specify a termination argument for well-founded termination:
```
termination_by a _ b => a - b
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the first and third argument decreases.
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" >> many (ppSpace >> (ident <|> "_")) >>
" => " >> termParser
ppDedent ppLine >>
"termination_by " >>
optional (atomic (many1 (ppSpace >> (ident <|> "_")) >> " => ")) >>
termParser

/--
Manually prove that the termination argument (as specified with `termination_by` or inferred)
Expand Down
8 changes: 4 additions & 4 deletions tests/lean/decreasing_by.lean
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ 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 => (n, m)
termination_by (n, m)
decreasing_by
· simp_wf
apply Prod.Lex.right
Expand Down Expand Up @@ -47,7 +47,7 @@ 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 => (n, m)
termination_by (n, m)
decreasing_by all_goals
simp_wf
first
Expand Down Expand Up @@ -87,7 +87,7 @@ 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 => (n, m)
termination_by (n, m)
decreasing_by apply id -- Error

end Ex6
Expand All @@ -106,7 +106,7 @@ 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 => (n, m)
termination_by (n, m)
decreasing_by -- Error
· simp_wf
apply Prod.Lex.right
Expand Down
1 change: 1 addition & 0 deletions tests/lean/guessLex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ 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
Expand Down
22 changes: 11 additions & 11 deletions tests/lean/guessLex.lean.expected.out
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
Inferred termination argument:
termination_by n m => (sizeOf n, sizeOf m)
termination_by (sizeOf n, sizeOf m)
Inferred termination argument:
termination_by n m => (sizeOf m, sizeOf n)
termination_by (sizeOf m, sizeOf n)
Inferred termination argument:
termination_by n m => (sizeOf n, sizeOf m)
termination_by (sizeOf n, sizeOf m)
Inferred termination argument:
termination_by x1 x2 => (sizeOf x2, sizeOf x1)
Inferred termination argument:
Expand All @@ -17,23 +17,23 @@ termination_by x1 => sizeOf x1
Inferred termination argument:
termination_by x1 => (sizeOf x1, 0)
Inferred termination argument:
termination_by n => (sizeOf n, 1)
termination_by (sizeOf n, 1)
Inferred termination argument:
termination_by n _h m => (sizeOf m, sizeOf n)
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 x1 x2 => (sizeOf x1, sizeOf x2)
Inferred termination argument:
termination_by a => (sizeOf a, 1)
termination_by (sizeOf a, 1)
Inferred termination argument:
termination_by a => (sizeOf a, 0)
termination_by (sizeOf a, 0)
Inferred termination argument:
termination_by x2 x2' => sizeOf x2'
termination_by x2' => sizeOf x2'
Inferred termination argument:
termination_by some_n' x2 => sizeOf x2
termination_by x2 => sizeOf x2
Inferred termination argument:
termination_by sizeOf' x2 => sizeOf x2
termination_by x2 => SizeOf.sizeOf x2
Inferred termination argument:
termination_by m x2 => SizeOf.sizeOf x2
termination_by x2 => SizeOf.sizeOf x2
8 changes: 4 additions & 4 deletions tests/lean/guessLexFailures.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 n m => n
-- termination_by n
decreasing_by decreasing_tactic


Expand All @@ -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 n m => n
termination_by n
decreasing_by decreasing_tactic

-- The GuessLex code at does not like `casesOn` alternative with insufficient lambdas
Expand All @@ -119,15 +119,15 @@ 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 n m => n
-- termination_by n
decreasing_by decreasing_tactic


-- Same test, explicit termination_by
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 n m => n
termination_by n
decreasing_by decreasing_tactic

end TrickyCode
Loading

0 comments on commit 943cd8c

Please sign in to comment.