Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: partial_fixpoint: partial functions with equations #6355

Merged
merged 168 commits into from
Jan 21, 2025
Merged
Changes from 1 commit
Commits
Show all changes
168 commits
Select commit Hold shift + click to select a range
f7d7391
Stash
nomeata Nov 25, 2024
366a43f
Use type classes, fun_order
nomeata Nov 25, 2024
5815cc9
Stash
nomeata Nov 25, 2024
f48bcfb
ok
nomeata Nov 25, 2024
8b9e1f5
Non-dependent API
nomeata Nov 26, 2024
1eec1f7
Imports
nomeata Nov 26, 2024
de8c13e
First definitions
nomeata Nov 26, 2024
9e73376
Progress
nomeata Nov 26, 2024
e4712e2
Does this help?
nomeata Nov 26, 2024
25080d8
Improve errormessage
nomeata Nov 26, 2024
ef876e5
Use nonempty
nomeata Nov 27, 2024
96a32a3
Try to make it dependent
nomeata Nov 27, 2024
9c38a1c
Try to make it dependent, take 2
nomeata Nov 27, 2024
2f66cca
Limited dependent types support works
nomeata Nov 27, 2024
672707a
Success with mono_psum_casesOn!
nomeata Nov 27, 2024
28ba271
Handle let properly
nomeata Nov 27, 2024
4ed1667
Debug some issues with splitting
nomeata Nov 27, 2024
2c63aec
Making mono_psigma_casesOn solves it
nomeata Nov 27, 2024
da21569
Handle ite manually
nomeata Nov 27, 2024
bdc486d
Use mkInhabitantFor instead of type class inference
nomeata Nov 27, 2024
ff7cb25
Improve error messages
nomeata Nov 28, 2024
7af569e
Add constants to environment for error message
nomeata Nov 28, 2024
8df67e7
Cleanup
nomeata Nov 28, 2024
a85d91e
Half-way through per-function monotonicity proofs. The paramter names…
nomeata Nov 28, 2024
b4b0a56
Seems to work suddenly?
nomeata Nov 28, 2024
3b8126b
Cleanup
nomeata Nov 28, 2024
860f78d
Remove now unused code for PSum/PSigma
nomeata Nov 28, 2024
7ffc36f
Better error message
nomeata Dec 2, 2024
78c8852
Rename keyword to nontermination_tailrecursive
nomeata Dec 2, 2024
183e5e7
Handle letFun
nomeata Dec 2, 2024
5f72bd1
Preserve variable name in letFun
nomeata Dec 2, 2024
4634b84
Generalize lemmas
nomeata Dec 2, 2024
c057d55
Avoid “mono” abbreviation
nomeata Dec 2, 2024
29ccde2
Elaborate to fix
nomeata Dec 2, 2024
17efc71
Simplify
nomeata Dec 2, 2024
52d89dd
Introduce MonoBind
nomeata Dec 4, 2024
7d450e8
Shuffle things around
nomeata Dec 4, 2024
f82c320
Try to change syntax
nomeata Dec 4, 2024
2c12af1
evert "Try to change syntax"
nomeata Dec 4, 2024
0b3fc25
Use extends
nomeata Dec 4, 2024
ecd3f71
Pick up user-provided CCPO instance, use `fix` directly.
nomeata Dec 4, 2024
cdc626e
Handle bind
nomeata Dec 4, 2024
84d88b5
Shuffle sections
nomeata Dec 5, 2024
077923f
More lemmas
nomeata Dec 5, 2024
70ff22d
Test update
nomeata Dec 5, 2024
7ac5525
Try to use Tailrec.monotone_apply_of_monotone_fun, but doomed
nomeata Dec 5, 2024
c50a45d
Revert "Try to use Tailrec.monotone_apply_of_monotone_fun, but doomed"
nomeata Dec 5, 2024
06f08e7
Introduce monotone_fun to simplify name preservation
nomeata Dec 5, 2024
9057ab6
monotone_mapM
nomeata Dec 5, 2024
c21f5e7
Handle mapM
nomeata Dec 5, 2024
9884da6
Introduce forall_arg
nomeata Dec 5, 2024
d288ee1
Merge remote-tracking branch 'origin/nightly-with-mathlib' into joach…
nomeata Dec 9, 2024
3ef7c75
Fix monotone_mapFinIdxM
nomeata Dec 9, 2024
6c2559a
instantiateMVars!
nomeata Dec 9, 2024
aeac365
Use applyConst where possible
nomeata Dec 9, 2024
a7952d9
Try synthAssignedInstances := false
nomeata Dec 9, 2024
fd1c424
More applyConst!
nomeata Dec 9, 2024
d451ad0
Even more applyConst! (but worse error message)
nomeata Dec 9, 2024
e5dad0a
Cosmetics
nomeata Dec 9, 2024
895812f
Abstract out findMonoThms
nomeata Dec 9, 2024
211c8cf
Recursive coin-toss example
nomeata Dec 9, 2024
f745633
Make it work
nomeata Dec 9, 2024
025bba1
Guard msg
nomeata Dec 9, 2024
82f52e0
More proofs about geom
nomeata Dec 10, 2024
99f32a1
Move tactic to its own file
nomeata Dec 10, 2024
fdae35c
extract _step
nomeata Dec 10, 2024
9cff0e8
Explicit tactic does one step only
nomeata Dec 10, 2024
d620965
Add attribute
nomeata Dec 10, 2024
23b9b9e
Test comments
nomeata Dec 10, 2024
a6d07ec
More applyConst
nomeata Dec 10, 2024
e4c4853
Undo some premature refactoringin WF code
nomeata Dec 10, 2024
9170fe1
Mutual recursion with different orders
nomeata Dec 11, 2024
9b2ad13
Big rename, partial_fixpoint, Lean.Init.Order, etc.
nomeata Dec 11, 2024
e22f7f8
s/Lean.Internal.Order/Lean.Order/g
nomeata Dec 11, 2024
24a16a4
Coinductive Predicates
nomeata Dec 11, 2024
530bd52
Code golf, just to show off
nomeata Dec 11, 2024
b24c1b5
ofConstName
nomeata Dec 11, 2024
1301bce
Scope monotone attribute syntax
nomeata Dec 11, 2024
7e804bd
Revert "Scope monotone attribute syntax"
nomeata Dec 11, 2024
130b8d0
s/partial_monotone/partial_fixpoint_monotone/g
nomeata Dec 11, 2024
408193d
Merge branch 'nightly-with-mathlib' of github.com:leanprover/lean4 in…
nomeata Dec 11, 2024
a905da3
Typo
nomeata Dec 11, 2024
f9b44aa
Completey ArgsPacker.Unary for the nullary case
nomeata Dec 11, 2024
5382395
Beta-reduce, to not confuse delta?
nomeata Dec 11, 2024
1f8d1b6
Scope notatin
nomeata Dec 11, 2024
9b01a0b
Did I do this?
nomeata Dec 11, 2024
5768144
Update test output
nomeata Dec 11, 2024
d5af308
Expand coinduction example
nomeata Dec 11, 2024
e94a190
prod_order
nomeata Dec 12, 2024
e8b3f54
s/Order/PartialOrder
nomeata Dec 12, 2024
6749029
Stash big refactor to product encoding. Equations still missing
nomeata Dec 14, 2024
4172ddd
No need for argspacker
nomeata Dec 14, 2024
11a0290
Handle equations again
nomeata Dec 14, 2024
b681437
Simplify equation proofs
nomeata Dec 14, 2024
823eacf
More test
nomeata Dec 14, 2024
1800ce4
Even more test
nomeata Dec 14, 2024
95b9a1d
Use withoutModifyingEnv
nomeata Dec 14, 2024
25956de
Introduce Lean.Elab.PreDefinition.Mutual for the common code
nomeata Dec 14, 2024
56b0374
Update simpDiag numbers
nomeata Dec 16, 2024
5eca0d6
No forall_arg, Sort not Type, better handling of letFun
nomeata Dec 16, 2024
777e82a
More defensive curryProj
nomeata Dec 16, 2024
fec1c33
Remove unused lemmas
nomeata Dec 17, 2024
5e2b3de
Prove fix_induct
nomeata Dec 17, 2024
182f361
admissible_or
nomeata Dec 17, 2024
775ef64
admissible_eq_some
nomeata Dec 17, 2024
17bf981
Experiment with admissible
nomeata Dec 17, 2024
30e1126
Beginning of .fixpoing_induct for mutual functions
nomeata Dec 17, 2024
ce61874
Refine text
nomeata Dec 17, 2024
f4e20e4
fixpoint_induct finished, even for mutual inductives, it seems
nomeata Dec 18, 2024
d34f48e
Only pass relevant induction hypotheses
nomeata Dec 18, 2024
665e2f6
Tweak the test
nomeata Dec 18, 2024
e8df162
Partial correctness theorems for option-valued fixpoints
nomeata Dec 18, 2024
c771220
Docstrings
nomeata Dec 19, 2024
611c9c8
Exclude empty chains from admissible, as in Isabelle
nomeata Dec 19, 2024
ce5a8b2
Revert "Exclude empty chains from admissible, as in Isabelle"
nomeata Dec 19, 2024
05532dc
Code cleanup
nomeata Dec 20, 2024
c298964
Move stripPProdProjs
nomeata Dec 20, 2024
2263816
More refactor
nomeata Dec 20, 2024
c62f24a
Introduce PProdN.genMk
nomeata Dec 20, 2024
c747aef
Introduce PProdN.projs
nomeata Dec 20, 2024
d8f4198
Introduce CCPOProdProjs
nomeata Dec 20, 2024
b47fc08
Polish
nomeata Dec 20, 2024
266504c
Trace message
nomeata Dec 26, 2024
f0116c5
More comment wordsmithing
nomeata Dec 26, 2024
2310905
Syntax for monotonicity proofs
nomeata Dec 28, 2024
9fa8f97
Check for metavariables
nomeata Dec 28, 2024
6311d39
mvar pretty printing
nomeata Dec 28, 2024
577a854
Merge remote-tracking branch 'origin/nightly-with-mathlib' into joach…
nomeata Dec 30, 2024
3a5f0e6
feat: partial_fixpoint: theory
nomeata Dec 30, 2024
38280d2
Merge branch 'joachim/partial_fixpoint_theory' into joachim/tailrec
nomeata Dec 30, 2024
43573b8
More theory cleanup
nomeata Dec 30, 2024
4c63d19
Merge branch 'joachim/partial_fixpoint_theory' into joachim/tailrec
nomeata Dec 30, 2024
3f5b911
post-merge
nomeata Dec 30, 2024
aa04710
Use Term.logUnassignedUsingErrorInfos
nomeata Dec 30, 2024
64a7d1d
Merge remote-tracking branch 'origin/master' into joachim/partial_fix…
nomeata Jan 2, 2025
e9b80c6
Merge branch 'joachim/partial_fixpoint_theory' into joachim/tailrec
nomeata Jan 2, 2025
ed2e741
feat: partial_fixpoint: monotonicity tactic
nomeata Jan 2, 2025
e2f2a9b
Polish
nomeata Jan 2, 2025
b01d4d7
Merge commit 'ed2e7417ef1cc41046195cb41dd8c0d6563bacd3' into joachim/…
nomeata Jan 2, 2025
1313cd7
Merge branch 'joachim/partial_fixpoint_tactic' into joachim/tailrec
nomeata Jan 2, 2025
45d02ad
More monotonicity lemmas
nomeata Jan 2, 2025
aea35bc
Some more monotone list lemmas
nomeata Jan 2, 2025
1fc5d44
Monotonicity for List.forIn
nomeata Jan 2, 2025
d178fea
Fix some tests
nomeata Jan 2, 2025
0c2b838
Merge branch 'master' of github.com:leanprover/lean4 into joachim/par…
nomeata Jan 2, 2025
6bb7d9f
Merge branch 'joachim/partial_fixpoint_tactic' into joachim/tailrec
nomeata Jan 2, 2025
4e3a675
Move attributes to core
nomeata Jan 2, 2025
5eba8b1
Complex do-notation example
nomeata Jan 2, 2025
cec6ab2
Array lemmas
nomeata Jan 3, 2025
a674d97
infinite_chain coinduction
nomeata Jan 3, 2025
45b92d7
if if
nomeata Jan 3, 2025
c7318ec
Fix test
nomeata Jan 3, 2025
ee7b1c1
Partial metaprogram to list all higher-order monadic functions
nomeata Jan 6, 2025
1532e42
Revert "Partial metaprogram to list all higher-order monadic functions"
nomeata Jan 6, 2025
893eb28
Add test cases from aeneas
nomeata Jan 7, 2025
c90ea19
More aeneas examples
nomeata Jan 10, 2025
4022113
Lean together demo file
nomeata Jan 13, 2025
a0d13b4
partial_correctness: beta-reduce theorem type
nomeata Jan 13, 2025
62ff401
Don’t leave failing test here
nomeata Jan 13, 2025
bc17f7c
Zeta-reduce lets that may contain recursive calls
nomeata Jan 13, 2025
17cbd41
Remove demo file
nomeata Jan 14, 2025
e1e199b
Add monotone_map
nomeata Jan 16, 2025
1bdefd1
Include example from the manual
nomeata Jan 16, 2025
6df12f0
Add monotone_seq
nomeata Jan 16, 2025
87265ee
Rename a bunch of lemmas
nomeata Jan 21, 2025
54214bf
Merge branch 'master' of github.com:leanprover/lean4 into joachim/tai…
nomeata Jan 21, 2025
6c488b1
Post-merge fixes
nomeata Jan 21, 2025
2455a15
Adjust to mapFinIdxM
nomeata Jan 21, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Progress
nomeata committed Nov 26, 2024
commit 9e733764946c59a5845d223f9f3d7f1bcb1b9016
22 changes: 15 additions & 7 deletions src/Init/Tailrec.lean
Original file line number Diff line number Diff line change
@@ -288,22 +288,30 @@ variable [Inhabited β]
def mono (F : (α → β) → β) :=
monotone (α := ∀ _, FlatOrder default) (β := FlatOrder default) F

theorem mono_const (c : β) : mono (fun (_ : α → β) => c) :=
theorem mono_const (c : β) : mono fun (_ : α → β) => c :=
monotone_const _

theorem mono_apply (x : α) : mono (β := β) (fun f => f x) :=
theorem mono_apply (x : α) : mono (β := β) fun f => f x :=
monotone_apply (β := fun _ => FlatOrder _) x

theorem mono_psigma_casesOn {γ : Sort uu} {δ : γ → Sort vv} (x : PSigma δ)
(k : (α → β) → (a : γ) → (b : δ a) → β )
(hmono : ∀ a b, mono (β := β) fun f => k f a b) :
mono (β := β) fun f => PSigma.casesOn x (k f) := by
cases x; apply hmono

set_option linter.unusedVariables false in
noncomputable
def tailrec_fix (F : (α → β) → (α → β)) (hmono : ∀ (x : α), mono (fun f => F f x)) : (α → β) :=
@fix (∀ _, FlatOrder default) _ _ F

theorem tailrec_fix_eq (F : (α → β) → (α → β))
(hmono : ∀ (x : α), mono (fun f => F f x)) :
tailrec_fix F hmono = F (tailrec_fix F hmono) :=
@fix_eq (∀ _, FlatOrder _) _ _ F
(monotone_of_monotone_apply (β := fun _ => FlatOrder _) (γ := ∀ _, FlatOrder _) F hmono)
(hmono : ∀ (x : α), mono (fun f => F f x)) (x : α) :
tailrec_fix F hmono x = F (tailrec_fix F hmono) x :=
congrFun
(@fix_eq (∀ _, FlatOrder _) _ _ F
(monotone_of_monotone_apply (β := fun _ => FlatOrder _) (γ := ∀ _, FlatOrder _) F hmono)
) x

end tailrec

@@ -322,7 +330,7 @@ noncomputable def find P := tailrec_fix (findF P) <| by
· apply mono_const
· apply mono_apply

theorem find_eq : find P = findF P (find P) := tailrec_fix_eq ..
theorem find_eq : find P x = findF P (find P) x := tailrec_fix_eq ..

end Example

50 changes: 34 additions & 16 deletions src/Lean/Elab/PreDefinition/Tailrec.lean
Original file line number Diff line number Diff line change
@@ -11,32 +11,51 @@ namespace Lean.Elab
open WF
open Meta

partial def solveMono (goal : MVarId) : MetaM Unit :=
goal.withContext do
let type ← goal.getType
let_expr Tailrec.mono _α _β _inst f := type |
throwError "Unexpected goal:{goal}"
partial def solveMono (goal : MVarId) : MetaM Unit := goal.withContext do
let type ← goal.getType
if type.isForall then
let (_, goal) ← goal.intro1P
solveMono goal
return

if f.isLambda && !f.bindingBody!.hasLooseBVars then
let_expr Tailrec.mono α β inst f := type |
throwError "Unexpected goal:{goal}"
if f.isLambda then
-- No recursive calls left
if !f.bindingBody!.hasLooseBVars then
let new_goals ← goal.applyConst ``Tailrec.mono_const
unless new_goals.isEmpty do
throwError "Left over goals"
return

if f.isLambda && f.bindingBody!.isApp && f.bindingBody!.appFn! == .bvar 0 then
-- A recursive call here
if f.bindingBody!.isApp && f.bindingBody!.appFn! == .bvar 0 then
let new_goals ← goal.applyConst ``Tailrec.mono_apply
unless new_goals.isEmpty do
throwError "Left over goals"
return

-- Manually handle PSigma.casesOn, as split doesn't
match_expr f.bindingBody! with
| PSigma.casesOn γ δ _motive x k =>
if f.bindingBody!.appFn!.hasLooseBVars then
throwError "Recursive calls in non-tail position:{indentExpr type}"
let us := type.getAppFn.constLevels! ++ f.bindingBody!.getAppFn.constLevels!.tail
let k' := f.updateLambdaE! f.bindingDomain! k
let p := mkApp7 (.const ``Tailrec.mono_psigma_casesOn us) α β inst γ δ x k'
let new_goals ← goal.apply p
new_goals.forM solveMono
return
| _ => pure

-- We could be more careful here and only split a match or ite that
-- is right under the lambda, and maybe use `apply_ite`-style lemmas to avoid the more
-- expesive splitter machinery. For now using `splitTarget` works fine.
if let some mvarIds ← splitTarget? goal (splitIte := true) then
mvarIds.forM solveMono
return

throwError "Recursive calls in non-tail position:{indentExpr type}"
throwError "Recursive calls in non-tail position:{indentExpr type}"

private def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (F : Expr) (e : Expr) : Expr :=
e.replace fun e =>
@@ -51,11 +70,13 @@ def derecursifyTailrec (fixedPrefixSize : Nat) (preDef : PreDefinition) :
let type ← whnfForall type
unless type.isForall do
throwError "expected unary function type: {type}"
-- TODO: Check these properties on the original function types
let some (α, β) := type.arrow?
| throwError "function has dependent type {type}"
| throwError "Termination by tailrecursion cannot handle dependent type:{indentExpr type}"
let u ← getDecLevel α
let v ← getDecLevel β
let inst ← synthInstance (mkApp (.const ``Inhabited [v.succ]) β)
let inst ← mapError (f := (m!"Termination by tailrecursion needs an inhabited codomain:{indentD ·}")) do
synthInstance (mkApp (.const ``Inhabited [v.succ]) β)
let value := mkApp3 (mkConst ``Lean.Tailrec.tailrec_fix [u, v]) α β inst

let F ← withoutModifyingEnv do
@@ -72,19 +93,16 @@ def derecursifyTailrec (fixedPrefixSize : Nat) (preDef : PreDefinition) :
-- Now try to prove the monotonicity
let monoGoal := (← inferType value).bindingDomain!
let mono ← mkFreshExprSyntheticOpaqueMVar monoGoal
let goal := mono.mvarId!
let (_, goal) ← goal.intro1
mapError (f := (m!"Could not prove function to be tail-recursive:{indentD ·}")) do
solveMono goal
mapError (f := (m!"Could not prove function to be tailrecursive:{indentD ·}")) do
solveMono mono.mvarId!
let value := .app value (← instantiateMVars mono)

let value ← mkLambdaFVars prefixArgs value
return { preDef with value }

def tailRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
let (fixedPrefixSize, argsPacker, unaryPreDef) ← mkUnaryPreDef preDefs

let preDefNonRec : PreDefinition ← derecursifyTailrec fixedPrefixSize unaryPreDef
addPreDefsFromUnary preDefs fixedPrefixSize argsPacker preDefNonRec
addPreDefsFromUnary preDefs fixedPrefixSize argsPacker preDefNonRec (hasInduct := false)

end Lean.Elab
16 changes: 13 additions & 3 deletions src/Lean/Elab/PreDefinition/WF/Eqns.lean
Original file line number Diff line number Diff line change
@@ -10,6 +10,7 @@ import Lean.Elab.PreDefinition.Basic
import Lean.Elab.PreDefinition.Eqns
import Lean.Meta.ArgsPacker.Basic
import Init.Data.Array.Basic
import Init.Tailrec

namespace Lean.Elab.WF
open Meta
@@ -20,20 +21,29 @@ structure EqnInfo extends EqnInfoCore where
declNameNonRec : Name
fixedPrefixSize : Nat
argsPacker : ArgsPacker
hasInduct : Bool
deriving Inhabited

private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
let target ← mvarId.getType'
let some (_, lhs, _) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
if lhs.isAppOf ``WellFounded.fix then
return mvarId
else if lhs.isAppOf ``Tailrec.tailrec_fix then
return mvarId
else
deltaLHSUntilFix (← deltaLHS mvarId)

private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
let target ← mvarId.getType'
let some (_, lhs, rhs) := target.eq? | unreachable!
let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
let h ←
if lhs.isAppOf ``WellFounded.fix then
pure <| mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
else if lhs.isAppOf ``Tailrec.tailrec_fix then
pure <| mkAppN (mkConst ``Tailrec.tailrec_fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
else
throwTacticEx `rwFixEq mvarId "expected fixed-point application"
let some (_, _, lhsNew) := (← inferType h).eq? | unreachable!
let targetNew ← mkEq lhsNew rhs
let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew
@@ -101,7 +111,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension

def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
(argsPacker : ArgsPacker) : MetaM Unit := do
(argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do
preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
/-
See issue #2327.
@@ -114,7 +124,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
modifyEnv fun env =>
preDefs.foldl (init := env) fun env preDef =>
eqnInfoExt.insert env preDef.declName { preDef with
declNames, declNameNonRec, fixedPrefixSize, argsPacker }
declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct }

def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
if let some info := eqnInfoExt.find? (← getEnv) declName then
2 changes: 1 addition & 1 deletion src/Lean/Elab/PreDefinition/WF/Main.lean
Original file line number Diff line number Diff line change
@@ -51,7 +51,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi

let preDefNonRec ← derecursifyUnary preDefs fixedPrefixSize argsPacker unaryPreDef wf
trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
addPreDefsFromUnary preDefs fixedPrefixSize argsPacker preDefNonRec
addPreDefsFromUnary preDefs fixedPrefixSize argsPacker preDefNonRec (hasInduct := true)

builtin_initialize registerTraceClass `Elab.definition.wf

15 changes: 5 additions & 10 deletions src/Lean/Elab/PreDefinition/WF/PackMutual.lean
Original file line number Diff line number Diff line change
@@ -157,14 +157,8 @@ private partial def addNonRecPreDefs (fixedPrefixSize : Nat) (argsPacker : ArgsP
trace[Elab.definition.wf] "{preDef.declName} := {value}"
addNonRec { preDef with value } (applyAttrAfterCompilation := false) (all := all)

private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) (fixedPrefixSize : Nat) : MetaM Bool := do
if preDefs.size == 1 then
lambdaTelescope preDefs[0]!.value fun xs _ => return xs.size == fixedPrefixSize + 1
else
return false

def addPreDefsFromUnary (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
(argsPacker : ArgsPacker) (preDefNonRec : PreDefinition) : TermElabM Unit := do
(argsPacker : ArgsPacker) (preDefNonRec : PreDefinition) (hasInduct : Bool) : TermElabM Unit := do
/-
We must remove `implemented_by` attributes from the auxiliary application because
this attribute is only relevant for code that is compiled. Moreover, the `[implemented_by <decl>]`
@@ -173,21 +167,22 @@ def addPreDefsFromUnary (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
-/
let preDefNonRec := preDefNonRec.filterAttrs fun attr => attr.name != `implemented_by

let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
-- Do not complain if the user sets @[semireducible], which usually is a noop,
-- we recognize that below and then do not set @[irreducible]
withOptions (allowUnsafeReducibility.set · true) do
if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
if argsPacker.onlyOneUnary then
addNonRec preDefNonRec (applyAttrAfterCompilation := false)
else
withEnableInfoTree false do
addNonRec preDefNonRec (applyAttrAfterCompilation := false)
addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec

-- We create the `_unsafe_rec` before we abstract nested proofs.
-- Reason: the nested proofs may be referring to the _unsafe_rec.
addAndCompilePartialRec preDefs
let preDefs ← preDefs.mapM (eraseRecAppSyntax ·)
let preDefs ← preDefs.mapM (abstractNestedProofs ·)
registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker hasInduct
for preDef in preDefs do
markAsRecursive preDef.declName
generateEagerEqns preDef.declName
4 changes: 4 additions & 0 deletions src/Lean/Meta/ArgsPacker.lean
Original file line number Diff line number Diff line change
@@ -422,6 +422,10 @@ def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
/-- The arities of the functions being packed -/
def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size)

def onlyOneUnary (argsPacker : ArgsPacker) :=
argsPacker.varNamess.size = 1 &&
argsPacker.varNamess[0]!.size = 1

def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr)
: MetaM Expr := do
assert! fidx < argsPacker.numFuncs
7 changes: 6 additions & 1 deletion src/Lean/Meta/Tactic/FunInd.lean
Original file line number Diff line number Diff line change
@@ -1114,11 +1114,16 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
let .str p s := name | return false
match s with
| "induct" =>
if (WF.eqnInfoExt.find? env p).isSome then return true
if let some eqnInfo := WF.eqnInfoExt.find? env p then
unless eqnInfo.hasInduct do
return false
return true
if (Structural.eqnInfoExt.find? env p).isSome then return true
return false
| "mutual_induct" =>
if let some eqnInfo := WF.eqnInfoExt.find? env p then
unless eqnInfo.hasInduct do
return false
if h : eqnInfo.declNames.size > 1 then
return eqnInfo.declNames[0] = p
if let some eqnInfo := Structural.eqnInfoExt.find? env p then
79 changes: 75 additions & 4 deletions tests/lean/run/tailrec.lean
Original file line number Diff line number Diff line change
@@ -1,19 +1,90 @@
def loop (x : Nat) : Unit := loop (x + 1)
termination_by tailrecursion

/--
info: equations:
theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
-/
#guard_msgs in
#print equations loop

/-- error: unknown constant 'loop.induct' -/
#guard_msgs in
#check loop.induct

def find (P : Nat → Bool) (x : Nat) : Option Nat :=
if P x then
some x
else
find P (x +1)
termination_by tailrecursion

/--
info: equations:
theorem find.eq_1 : ∀ (P : Nat → Bool) (x : Nat), find P x = if P x = true then some x else find P (x + 1)
-/
#guard_msgs in
#print equations find


/--
error: failed to synthesize
Inhabited (Fin n)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: Termination by tailrecursion needs an inhabited codomain:
failed to synthesize
Inhabited (Fin n)
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
def notinhabited (n m : Nat) : Fin n :=
notinhabited n (m+1)
termination_by tailrecursion

def fib (n : Nat) := go 0 0 1
where
go i fip fi :=
if i = n then
fi
else
go (i + 1) fi (fi + fip)
termination_by tailrecursion

/--
error: fail to show termination for
mutual1
mutual2
with errors
failed to infer structural recursion:
Cannot use parameters n of mutual1 and n of mutual2:
failed to eliminate recursive application
mutual2 (m + 1) n
Cannot use parameters n of mutual1 and m of mutual2:
failed to eliminate recursive application
mutual2 (m + 1) n
Cannot use parameters m of mutual1 and n of mutual2:
failed to eliminate recursive application
mutual2 (m + 1) n
Cannot use parameters m of mutual1 and m of mutual2:
failed to eliminate recursive application
mutual2 (m + 1) n


Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
Call from mutual1 to mutual2 at 88:34-51:
n m
n ? ?
m = ?
Call from mutual2 to mutual1 at 89:34-51:
n m
n _ ?
m _ _

Please use `termination_by` to specify a decreasing measure.

Termination by tailrecursion cannot handle dependent type:
(x : (_ : Nat) ×' Nat ⊕' (_ : Nat) ×' Nat) → PSum.casesOn x (fun _x => Unit) fun _x => Unit
-/
#guard_msgs in
mutual
def mutual1 (n m : Nat) : Unit := mutual2 (m + 1) n
def mutual2 (n m : Nat) : Unit := mutual1 (m + 1) n
end