walker (Oct 08 2022 at 12:23): walker (Oct 08 2022 at 12:23):I was reading the thesis on metacoq 3.2. Functional Core: CCω and I noticed that well formed context is defined in terms of the typing judgement.
So the natural implementation from my perspective was mutual recursion between the typing judgement and the well foundeness of contexts.
But I got stuck during proofs (weakening lemma which is basically the first proof I attempted)
My weakening lemma looked like follows:
Γ ⊢ t: T -> Γ ##ₘ Γ' -> ⊢ Γ -> (Γ ∪ Γ' ) ⊢ t : T.
the ##ₘ means they share no free variables ... (the definition is slightly different from thesis one's.
But to prove it I needed to show the following:
⊢ Γ -> ⊢ Γ' -> Γ ##ₘ Γ' -> ⊢ (Γ ∪ Γ').
Which says if two contexts are well formed and have no common free variables, then their uniion is also well formed.
But then this required proving the weakening lemma.
I saw in metacoq that defined things in a way that avoid the mutually inductive typing as described by the the thesis.
My question here is I don't have good understanding of why mutual induction is problem.
Paolo Giarrusso (Oct 08 2022 at 12:42):you're talking of https://github.com/MetaCoq/metacoq/blob/v1.1-8.16/template-coq/theories/Typing.v#L741-L863 I guess? Seems like they're lifting typing to wf_local using a generic construction All_local_env
walker (Oct 08 2022 at 12:46):yes this is what am talking about, my question is why does this work, while mutual inductive definitions does not work!
Paolo Giarrusso (Oct 08 2022 at 12:47):that sounds unlikely; if you're asking "why do they avoid mutual recursion", one reason is probably that All_local_env and its theory is reusable across lots of judgments.
walker (Oct 08 2022 at 12:48):I see, so that means that my proofs fail to work for different reason! Alright I will dig deeper.
Paolo Giarrusso (Oct 08 2022 at 12:48):that's not clear either
Paolo Giarrusso (Oct 08 2022 at 12:49):all your message shows is that one proof strategy runs into trouble, but maybe weakening and well-formedness need to be proven in mutual recursion?
walker (Oct 08 2022 at 12:49):what does that mean ?
Paolo Giarrusso (Oct 08 2022 at 12:50):Lemma foo : ... with bar : ...
Paolo Giarrusso (Oct 08 2022 at 12:50):or Lemma foo_mut : (statement1) /\ (statement2). sometimes
walker (Oct 08 2022 at 12:52):Alright, I will check how pcuic does it in metacoq.
Paolo Giarrusso (Oct 08 2022 at 12:52):I also wonder if you could or should assume ⊢ (Γ ∪ Γ'). as a hypothesis
walker (Oct 08 2022 at 12:52):Paolo Giarrusso said:
I also wonder if you could or should assume
⊢ (Γ ∪ Γ').as a hypothesis
I was trying to stick to the paper formalization as close as possible.
Paolo Giarrusso (Oct 08 2022 at 12:53):_in general_ the exact order in which lemmas are proven, what is (mutually) recursive with what, is very subtle
Paolo Giarrusso (Oct 08 2022 at 12:53):(is/can be)
walker (Oct 08 2022 at 12:54):So parameterize things and avoiding mutual inductive types usually simplifies stuff ?
Paolo Giarrusso (Oct 08 2022 at 12:55):the problem you're describing seems orthogonal from how the types are defined
walker (Oct 08 2022 at 12:57):I am not if that means related to, or not related to :sweat_smile: .
Paolo Giarrusso (Oct 08 2022 at 12:57):orthogonal ~= unrelated
Paolo Giarrusso (Oct 08 2022 at 12:59):mathematically, I think reusing All_local_env vs "inlining it" into a mutually recursive type should not affect what is provable, but the way theorems are formalized differs... _in particular_, avoiding mutual recursion makes the generated induction principle strictly weaker
Paolo Giarrusso (Oct 08 2022 at 12:59):one can still prove the "right" induction principle, but that's not automated by Coq's standard support
walker (Oct 08 2022 at 13:00):I assume that mutual recurious is better in this case.
walker (Oct 08 2022 at 13:01):Alright. I will have to study pcuic in more details. at least the helper lemma before I proceed with my implementation.
walker (Oct 08 2022 at 13:02):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):once again thanks a lot for all the pointers @Paolo Giarrusso
Notification Bot (Oct 08 2022 at 13:04):walker has marked this topic as resolved.
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.
Gaëtan Gilbert (Oct 10 2022 at 13:34):The standard example is
what's A for?
Meven Lennon-Bertrand (Oct 10 2022 at 13:41):Gaëtan Gilbert said:
what's A for?
Right, there is no need for a parameter
Last updated: Jun 10 2023 at 06:31 UTC