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.

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`

yes this is what am talking about, my question is why does this work, while mutual inductive definitions does not work!

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.

I see, so that means that my proofs fail to work for different reason! Alright I will dig deeper.

that's not clear either

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?

what does that mean ?

`Lemma foo : ... with bar : ...`

or `Lemma foo_mut : (statement1) /\ (statement2).`

sometimes

Alright, I will check how pcuic does it in metacoq.

I also wonder if you could or should assume `⊢ (Γ ∪ Γ').`

as a hypothesis

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.

_in general_ the exact order in which lemmas are proven, what is (mutually) recursive with what, is very subtle

(is/can be)

So parameterize things and avoiding mutual inductive types usually simplifies stuff ?

the problem you're describing seems orthogonal from how the types are defined

I am not if that means related to, or not related to :sweat_smile: .

orthogonal ~= unrelated

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

one can still prove the "right" induction principle, but that's not automated by Coq's standard support

I assume that mutual recurious is better in this case.

Alright. I will have to study pcuic in more details. at least the helper lemma before I proceed with my implementation.

Last updated: Jan 30 2023 at 16:03 UTC