Recursive Functions and Termination Proofs #170

New Issue

aniva · 2025-02-25T17:07:56-08:00

aniva commented

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

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 0.4.0 milestone 2025-04-14 16:48:56 -07:00

aniva commented

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

Related: https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/detect.20termination.20proof.20obligations.20in.20TacticM/near/513200547

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

Sign in to join this conversation.