nice way to define mutually inductive types

Stream: lean4

[Ryan Lahfa]

I have:

inductive KrivineInstruction
| Access (n: Nat)
| Grab (next: KrivineInstruction)
| Push (next: KrivineInstruction) (continuation: KrivineInstruction)

mutual
inductive KrivineClosure
| term (i: KrivineInstruction) (e: KrivineEnv)

inductive KrivineEnv
| term (closures: List KrivineClosure)
end

The adhoc definition of KrivineXXX.term looks a bit strange, but I'm not sure if it's related to missing features or if I'm not aware of a better way to do this kind of these definitions.

I would just like to have KrivineClosure := KrivineInstruction × KrivineEnv and KrivineEnv := List KrivineClosure if that's possible.

[Mario Carneiro]

I would make one inductive type

inductive KrivineClosure
| term (i: KrivineInstruction) (e: List KrivineClosure)

and then def KrivineEnv := List KrivineClosure. That way KrivineClosure.term has the type KrivineInstruction -> KrivineEnv -> KrivineClosure

[Mario Carneiro]

They can't both be defs because that would be an infinitely large type

[Ryan Lahfa]

Makes sense @Mario Carneiro I have gone with your definition, but that might be a #Program verification question, if I have:

inductive KrivineInstruction
| Access (n: Nat)
| Grab (next: KrivineInstruction)
| Push (next: KrivineInstruction) (continuation: KrivineInstruction)

inductive KrivineClosure
| pair (i: KrivineInstruction) (e: List KrivineClosure)

def KrivineEnv := List KrivineClosure
def KrivineStack := List KrivineClosure

def KrivineEnv.depth: KrivineEnv -> Nat
| [] => 0
| KrivineClosure.pair _ e :: closures => Nat.max (1 + depth e) (depth closures)

I do understand that depth cannot be defined because structural recursion uses the recursive type and do not care about what is really in.
At the same time, I do not have the feeling I can solve this by well-founded recursion, as this is the predicate I would like to use to define wf-recursion for other similar functions.

Also, e looks "smaller" than the argument, as it is syntaxically smaller.

In that case, how are these functions even definable?

[Ryan Lahfa]

Ryan Lahfa said:

Makes sense Mario Carneiro I have gone with your definition, but that might be a #Program verification question, if I have:

inductive KrivineInstruction
| Access (n: Nat)
| Grab (next: KrivineInstruction)
| Push (next: KrivineInstruction) (continuation: KrivineInstruction)

inductive KrivineClosure
| pair (i: KrivineInstruction) (e: List KrivineClosure)

def KrivineEnv := List KrivineClosure
def KrivineStack := List KrivineClosure

def KrivineEnv.depth: KrivineEnv -> Nat
| [] => 0
| KrivineClosure.pair _ e :: closures => Nat.max (1 + depth e) (depth closures)

I do understand that depth cannot be defined because structural recursion uses the recursive type and do not care about what is really in.
At the same time, I do not have the feeling I can solve this by well-founded recursion, as this is the predicate I would like to use to define wf-recursion for other similar functions.

Also, e looks "smaller" than the argument, as it is syntaxically smaller.

In that case, how are these functions even definable?

So I answer myself, it's possible to use rec/induction to define the data:

set_option codegen false in
def KrivineClosure.depth: KrivineClosure -> Nat :=
fun closure => by induction closure with
| pair i env depth_env => exact 1 + depth_env
| nil => exact 0
| cons head tail head_depth tail_depth => exact (Nat.max head_depth tail_depth)

My question are now:

(a) is there an issue related to the lack of codegen for recursors?
(b) is there a better way to do this or a more "proper" way?
(c) where can I read more about recursors and such things?

[Chris B]

I haven't looked closely at how v4 handles the recursors for nested inductives, but if you can use the new generated one to define a Prop-valued less than relation on KrivineEnv you should be able to define recursive functions using Acc.rec. That's how the non-structural recursion in core is defined.
Mario's paper obviously has information on the formation of recursors for regular inductive types. For nested inductives the only source is probably the kernel code.

[Chris B]

False alarm, I just tried it and didn't realize you can't even use the Acc recursor yet. It returns an error about not yet generating code for Acc.rec

[Ryan Lahfa]

Chris B said:

False alarm, I just tried it and didn't realize you can't even use the Acc recursor yet. It returns an error about not yet generating code for Acc.rec

You can do set_option codegen false in … and provide an unsafe definition in fact.

[Ryan Lahfa]

Which is what I have done to define depth and I fled to WF definitions.

[Chris B]

I saw that in your earlier attempts, I thought this might provide an escape hatch since Acc was already implemented and wellFounded.fix is used in core without any annotations.

[Mario Carneiro]

Chris B said:

Mario's paper obviously has information on the formation of recursors for regular inductive types. For nested inductives the only source is probably the kernel code.

Actually my paper borrows heavily from Dybjer, Inductive Families, which was also the official source for the lean implementation. That paper covers nested and mutual inductives as well, although mine doesn't. (However my paper covers universes and large elimination, unlike Dybjer, who was working in a generic dependent type theory without universes.)

[Chris B]

Nice, I didn't know that paper also covered nested inductives.

[Mario Carneiro]

Actually I lied, it covers mutual inductives but not nested inductives. (There are also entire "Omitted." sections in the definition of mutual inductives.) From looking at the kernel terms produced by a nested inductive, it's clearly just doing the same as the analogous mutual inductive where you mutually define all the inductives and nested versions; the only technically interesting thing that happens is that if you have | mk : list T -> T then you don't just get list_T and T defined mutually, you actually get a recursor that talks about list T and list_T is not created. So we are adding new axioms on an existing inductive type which is just slightly questionable. (It can still be modeled by using less nominal types.)