max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve auto generated termination_by a bit

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-19 09:28:19 -07:00
parent 64c5cda612
commit c7cdbf8ff8
2 changed files with 5 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Elab/PreDefinition/WF/Rel.lean
View file

@ -130,12 +130,15 @@ where
generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do
let mut result := #[]
let var ← `(x)
let body ← `(sizeOf x)
let hole ← `(_)
for preDef in preDefs, numArg in numArgs, argIdx in argCombination do
for preDef in preDefs, numArg in numArgs, argIdx in argCombination, i in [:preDefs.size] do
let mut vars := #[var]
for i in [:numArg - argIdx - 1] do
vars := vars.push hole
-- TODO: improve this.
-- The following trick allows a function `f` in a mutual block to invoke `g` appearing before it with the input argument.
-- We should compute the "right" order (if there is one) in the future.
let body ← `((sizeOf x, $(quote i)))
result := result.push {
ref := preDef.ref
declName := preDef.declName

10
tests/lean/run/lex.lean
View file

@ -66,10 +66,6 @@ mutual
| .error _ => return { text := { data := text.reverse }, tok := Tok.num soFar } :: (← lex2 (c::cs)) -- Use `c::cs` here instead of `input` because the default tactic doesn't know they are equal.
| .ok d => lex2number (soFar * 10 + d) (c :: text) cs
end
-- `termination_by` is used to specify a well-founded relation.
termination_by
lex2 input => (input, 0) -- Lean is proving a termination using the instance `WellFoundedRelation (List Char × Nat)` which is just a lex-order. In the future, we should be able to guess this too.
lex2number input => (input, 1)
#eval lex2 (m := Except LexErr) "".data
#eval lex2 (m := Except LexErr) "123".data
@ -131,9 +127,6 @@ mutual
| .error _ => return { text := { data := text.reverse }, tok := Tok.num soFar } :: (← lex4 input)
| .ok d => lex4number (soFar * 10 + d) (c :: text) cs
end
termination_by
lex4 input => (input, 0) -- Lean is proving a termination using the instance `WellFoundedRelation (List Char × Nat)` which is just a lex-order. In the future, we should be able to guess this too.
lex4number input => (input, 1)
-- decreasing_by allows us to specify a tactic for showing the recursive applications are decreasing.
decreasing_by
solve | decreasing_tactic -- get easy cases with the builtin tactic `decreasing_tactic`
@ -210,9 +203,6 @@ mutual
else
return [{ text := text.reverse.asString, tok := Tok.num soFar }]
end
termination_by
lex input => (input, 0)
lexnumber input => (input, 1)
#eval lex (m := Except LexErr) "".iter
#eval lex (m := Except LexErr) "123".iter