Simulating well founded recursions?

Stream: lean4

[Ryan Lahfa]

I'm trying to formalize the function compile.inv :

inductive LambdaTerm where
| var (val : Nat)
| app (fn: LambdaTerm) (arg: LambdaTerm)
| lambda (body: LambdaTerm)

inductive KrivineInstruction
| Access (n: Nat)
| Grab
| Push (c: List KrivineInstruction)

inductive KrivineEnv
| Item (instrs: List KrivineInstruction) (env: List KrivineEnv)

inductive KrivineStack
| Item (instrs: List KrivineInstruction) (env: List KrivineEnv)

structure KrivineState where
  code: List KrivineInstruction
  env: List KrivineEnv
  stack: List KrivineStack

def compile.inv: List KrivineInstruction -> LambdaTerm
| [] => LambdaTerm.var 0
| KrivineInstruction.Access n :: _ => LambdaTerm.var n
| KrivineInstruction.Push c' :: c => LambdaTerm.app (inv c) (inv c')
| KrivineInstruction.Grab :: c => LambdaTerm.lambda (inv c)

But it looks like Lean 4 is not able to show termination on compile.inv (due to https://github.com/leanprover/lean4/issues/176 I suppose), is there a way forward or tricks to still build this function manually and show stuff on it?

[Daniel Fabian]

does making it partial work for your case?

[Ryan Lahfa]

Daniel Fabian said:

does making it partial work for your case?

I'm getting

failed to compile partial definition 'compile.inv', failed to show that type is inhabited

[Daniel Fabian]

ah, you'll need to add a deriving Inhabited to your type.

[Daniel Fabian]

Probably to LambdaTerm

[Sebastian Ullrich]

You will not be able to prove anything about it then though

[Ryan Lahfa]

Ha, so indeed, deriving Inhabitedfor LambdaTerm and making it partial creates the function, but I still need to prove things on its composition with other functions

[Ryan Lahfa]

Okay, I see, partial makes the function unsafe and uses implementedBy, makes sense why I cannot prove anything on it

[Sebastian Ullrich]

You could try to apply Wellfounded.fixF manually or, probably nicer, define a custom "accessibility" inductive predicate for your datatype and do induction on that one. Not completely sure about that one though, I haven't tried yet.

[Ryan Lahfa]

Sebastian Ullrich said:

You could try to apply Wellfounded.fixF manually or, probably nicer, define a custom "accessibility" inductive predicate for your datatype and do induction on that one. Not completely sure about that one though, I haven't tried yet.

Alright, will give it a try, thanks!

[Sebastian Ullrich]

Well, I guess the predicate merely moves the issue since you still have to show by well-founded recursion that it is inhabited :) . So it might only make sense if you have multiple functions using the same recursion scheme. In other words, it is more or less equivalent to hiding the wf recursion behind a custom recursor.

[Ryan Lahfa]

Sebastian Ullrich said:

Well, I guess the predicate merely moves the issue since you still have to show by well-founded recursion that it is inhabited :) . So it might only make sense if you have multiple functions using the same recursion scheme. In other words, it is more or less equivalent to hiding the wf recursion behind a custom recursor.

This custom recursor can be used then with induction <> using custom_recursor syntax?

[Ryan Lahfa]

So I tried a real quick definition and got to this:

inductive LambdaTerm where
| var (val : Nat)
| app (fn: LambdaTerm) (arg: LambdaTerm)
| lambda (body: LambdaTerm)

inductive KrivineInstruction
| Access (n: Nat)
| Grab
| Push (c: List KrivineInstruction)

inductive KrivineEnv
| Item (instrs: List KrivineInstruction) (env: List KrivineEnv)

inductive KrivineStack
| Item (instrs: List KrivineInstruction) (env: List KrivineEnv)

structure KrivineState where
  code: List KrivineInstruction
  env: List KrivineEnv
  stack: List KrivineStack

def compile.inv_rel: List KrivineInstruction -> List KrivineInstruction -> Prop := sorry
def compile.inv_wf (x: List KrivineInstruction): Acc inv_rel x := sorry

def compile.inv (c: List KrivineInstruction): LambdaTerm :=
WellFounded.fixF (fun code inv => match code with
  | [] => LambdaTerm.var 0
  | KrivineInstruction.Access n :: _ => LambdaTerm.var n
  | KrivineInstruction.Push c' :: c => LambdaTerm.app (inv c (sorry)) (inv c' (sorry))
  | KrivineInstruction.Grab :: c => LambdaTerm.lambda (inv c (sorry))
) c (inv_wf c)

Now, Lean is giving me: (kernel) compiler failed to infer low level type, unknown declaration 'WellFounded.fixF' ; is this expected because I abused of sorry :> ?

[Sebastian Ullrich]

Oops, the compiler does not know how to handle wf recursion. You can turn it off using set_option codegen false. Or, if you want to run this def, do what the elaborator will do when it gains support for wf recursion and define a partial def for the compiler and an @[implementedBy ...] def for proving.

[Ryan Lahfa]

Sebastian Ullrich said:

Oops, the compiler does not know how to handle wf recursion. You can turn it off using set_option codegen false. Or, if you want to run this def, do what the elaborator will do when it gains support for wf recursion and define a partial def for the compiler and an @[implementedBy ...] def for proving.

so I would need to do something like:

partial def compile.inv …

@[implementedBy compile.inv]
def compile.inv_defined_with_wf …

?

[Ryan Lahfa]

oh no, I understood I think now

[Ryan Lahfa]

I tried:

partial def compile.inv: List KrivineInstruction -> LambdaTerm
| [] => LambdaTerm.var 0
| KrivineInstruction.Access n :: _ => LambdaTerm.var n
| KrivineInstruction.Push c' :: c => LambdaTerm.app (inv c) (inv c')
| KrivineInstruction.Grab :: c => LambdaTerm.lambda (inv c)

@[implementedBy compile.inv]
def compile.inv_with_wf (c: List KrivineInstruction): LambdaTerm :=
WellFounded.fixF (fun code inv => match code with
  | [] => LambdaTerm.var 0
  | KrivineInstruction.Access n :: _ => LambdaTerm.var n
  | KrivineInstruction.Push c' :: c => LambdaTerm.app (inv c (sorry)) (inv c' (sorry))
  | KrivineInstruction.Grab :: c => LambdaTerm.lambda (inv c (sorry))
) c (inv_wf c)

without much more luck, do I still need to disable codegen for the wf definition?

[Sebastian Ullrich]

You might, that could be an oversight in implementedBy

[Ryan Lahfa]

Alright, it did the trick I think, thanks!

[Sebastian Ullrich]

Nice!

[Marcus Rossel]

So the whole partial + implementedBy dance is only there to achieve efficient computation, right? That is, the partial def is not necessary if you're only interested in proving things about the definition?

[Sebastian Ullrich]

Yes, see
Sebastian Ullrich said:

You can turn it off using set_option codegen false. Or, if you want to run this def, do what the elaborator will do when it gains support for wf recursion and define a partial def for the compiler and an @[implementedBy ...] def for proving.