Zulip Chat Archive

I would be easy to just post my code here again and ask for direct help,but I want to learn how to unstuck myself .... so I will try doing that first for a while.

walker (Oct 08 2022 at 13:04):

Notification Bot (Oct 08 2022 at 13:04):

Paolo Giarrusso (Oct 08 2022 at 13:06):

welcome — but please keep in mind I'm not a metacoq dev/expert, I have more experience in simpler cases

Meven Lennon-Bertrand (Oct 10 2022 at 12:32):

Regarding context well-formation, what MetaCoq uses here is called a _nested_ inductive type: this is a type where the type under definition appears as a parameter of another inductive type in its own definition. The standard example is

Inductive rose_tree (A : Type) :=
| node : list (rose_tree A) -> rose_tree A.

A lot of such nested inductive type can be expressed as mutual ones instead, here for instance we can do

Inductive rose_tree' (A : Type) :=
| node' : rose_forest A -> rose_tree' A
with
rose_forest (A : Type) :=
| nil : rose_forest A
| cons : rose_tree' A -> rose_forest A -> rose_forest A.

But inlining the nested definition (here, that of list) means that each time you need to reprove all theorems on your inlined inductive type (in the second definition, you cannot use lemmas on lists to reason on rose_forest). In a setting such as that of MetaCoq, this is inconvenient, which is why we go the nested way, so that we can share the theory (of All_local_env in your particular case). However, on paper it is often nicer in terms of presentation to go for a more "independent" formulation, which does not depend on another definition, and thus resembles more the mutual definition than the nested one. In the end though this is mostly a formalization question, but should not impact too much the provability of lemmas.

Meven Lennon-Bertrand (Oct 10 2022 at 12:34):

Note, though, that in MetaCoq the "induction principle" we show for typing and use everywhere is not just the "standard" one you would get for a nested inductive type (although even that notion is afaik an open question, at least engineering-wise), but one that is tailored to make subsequent proofs by induction nicer.

Meven Lennon-Bertrand (Oct 10 2022 at 12:36):

Also, I wouldn't call my thesis "the" thesis on MetaCoq: Théo Winterhalter talks about it in his as well, and I only cover a small bit of all there is in the project!

walker (Oct 10 2022 at 12:42):

thanks for the clarification, and I think I was able to prove weakening lemma, and almost completed proving the substitution lemma, but I went with the mutual induction, as it looks more readable to me.

Stream: MetaCoq

Topic: ✔ Why is wf_local is not mutual recursion with `typing`

walker (Oct 08 2022 at 13:02):