aniva/Pantograph

Fork 0

🖇️ Recursive Functions and Termination Proofs #170

New issue

Open

opened 2025-02-25 17:07:56 -08:00 by aniva · 3 comments

aniva commented

2025-02-25 17:07:56 -08:00

Owner

This will require some filtering on the local context. We need to expose the self declaration (currently an implementationDetail). Each invocation to self would be accompanied by a termination and well-foundedness proof.

This will require some filtering on the local context. We need to expose the self declaration (currently an `implementationDetail`). Each invocation to self would be accompanied by a termination and well-foundedness proof.

aniva added the

part/Goal

category

feature

labels

2025-02-25 17:07:56 -08:00

aniva self-assigned this

2025-02-25 17:07:56 -08:00

aniva added the

priority

low

label

2025-03-08 20:44:27 -08:00

aniva added this to the v0.4.0 milestone

2025-04-14 16:48:56 -07:00

aniva commented

2025-05-06 07:40:40 -07:00

Author

Owner

This detects recursive references

import Lean.Elab.Tactic

open Lean Meta Elab Tactic

elab "ban_termination" t:tactic : tactic => do
  let goals ← getUnsolvedGoals
  evalTactic t
  for goal in goals do
    let some expr ← getExprMVarAssignment? goal | continue
    let expr ← instantiateMVars expr
    goal.withContext do
      let recFVars : FVarIdSet := (← getLCtx).foldl
        (fun set decl => if decl.isAuxDecl then set.insert decl.fvarId else set) ∅
      if expr.hasAnyFVar recFVars.contains then
        Meta.throwTacticEx `ban_termination goal "tactic used recursion"

theorem testing : 3 = 3 := by
  ban_termination exact testing -- error: tactic 'ban_termination' failed, tactic used recursion

Related: https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/detect.20termination.20proof.20obligations.20in.20TacticM/near/513200547 This detects recursive references ```lean import Lean.Elab.Tactic open Lean Meta Elab Tactic elab "ban_termination" t:tactic : tactic => do let goals ← getUnsolvedGoals evalTactic t for goal in goals do let some expr ← getExprMVarAssignment? goal | continue let expr ← instantiateMVars expr goal.withContext do let recFVars : FVarIdSet := (← getLCtx).foldl (fun set decl => if decl.isAuxDecl then set.insert decl.fvarId else set) ∅ if expr.hasAnyFVar recFVars.contains then Meta.throwTacticEx `ban_termination goal "tactic used recursion" theorem testing : 3 = 3 := by ban_termination exact testing -- error: tactic 'ban_termination' failed, tactic used recursion ```

aniva changed title from ~~Allow generation of recursive functions~~ to Recursive Functions and Termination Proofs

2025-05-06 07:47:48 -07:00

aniva changed title from ~~Recursive Functions and Termination Proofs~~ to 🖇️ Recursive Functions and Termination Proofs

2025-06-25 10:45:27 -07:00

aniva removed the

priority

low

label

2025-06-25 21:19:42 -07:00

aniva commented

2025-07-14 15:44:13 -07:00

Author

Owner

There are ~~two~~ three solutions:

Prohibit the generation of recursive calls via tactics. If a prover agent wishes to generate recursive calls, it has to announce it up-front. This is easy to implement.
Add a surrogate free variable representing a call to self. For example, if we are generating a function A -> B, the recursive surrogate would have type (a' : A) -> a' < a -> B where the argument a' < a proves a decreasing measure. After the proof finishes, some other process would then need to convert it back into a proper recursive call.
Combine the two solutions. The recursive reference would only be available if the agent announces the intention to generate recursion via a special tactic. Then it would be free to access a recursive copy of the function in question. Notably, the tactic can run in the middle of a proof, and this would generate an auxiliary declaration. From a search perspective (and especially Project No. 3) this requires a strong CCIS unit.

There are ~~two~~ three solutions: 1. Prohibit the generation of recursive calls via tactics. If a prover agent wishes to generate recursive calls, it has to announce it up-front. This is easy to implement. 2. Add a surrogate free variable representing a call to self. For example, if we are generating a function `A -> B`, the recursive surrogate would have type `(a' : A) -> a' < a -> B` where the argument `a' < a` proves a decreasing measure. After the proof finishes, some other process would then need to convert it back into a proper recursive call. 3. Combine the two solutions. The recursive reference would only be available if the agent announces the intention to generate recursion via a special tactic. Then it would be free to access a recursive copy of the function in question. Notably, the tactic can run in the middle of a proof, and this would generate an auxiliary declaration. From a search perspective (and especially Project No. 3) this requires a strong CCIS unit.

aniva commented

2025-07-16 17:47:53 -07:00

Author

Owner

Regarding computability, Batteries has a temporary solution: 82fd0cf6aa/Batteries/WF.lean (L117-L121)

Regarding computability, `Batteries` has a temporary solution: https://github.com/leanprover-community/batteries/blob/82fd0cf6aaa1e2580aa17b3b1e5b9140e6e6a5e5/Batteries/WF.lean#L117-L121

aniva added a new dependency

2025-08-27 14:54:31 -07:00

aniva/Trillium#169 - Could not atomize Nat.log2_le_self