Zulip Chat Archive

Stream: lean4

Topic: nice way to define mutually inductive types


Ryan Lahfa (Apr 30 2021 at 21:36):

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 (Apr 30 2021 at 22:43):

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 (Apr 30 2021 at 22:43):

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

Ryan Lahfa (May 01 2021 at 10:17):

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 (May 05 2021 at 09:57):

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 (May 06 2021 at 10:01):

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 (May 06 2021 at 20:49):

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 (May 06 2021 at 20:51):

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 (May 06 2021 at 20:51):

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

Chris B (May 06 2021 at 20:55):

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 (May 07 2021 at 00:32):

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 (May 07 2021 at 16:25):

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

Mario Carneiro (May 07 2021 at 17:58):

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.)


Last updated: Dec 20 2023 at 11:08 UTC