Methodology for coming up with lemmas · Miscellaneous

So I was finally able to prove the substitution lemma after lots of guess work / trial and error,

I am going to explain the guess work, brainstorming I went through and then my question is : is there a pragmatic way to define good lemmas that are general enough so proofs go through?

Lemma substitution_lemma: forall Γ1 Γ2 Γ A B f n x,
    ([(x, A)] ++ Γ) ⊢ f : B ->
    Γ ⊢ n : A ->
    (Γ ##  Γ2) ->
    ⊢ (Γ2 ++ Γ) ->
    (Γ2 ++ Γ)  ⊢ subst f x n : subst B x n.

Now the important detail here is that most literature uses (([(x, A)] ++ Γ)) to signify x of type A and the rest of Γ may depend on x.
In my situation I do it the other way around (I assume that would lead to faster insertions, removals).

So back to the story, When I did induction on [(x, A)] ++ Γ) ⊢ f : B, things were completely mesed up for the pi and lambda abstraction cases.

Lemma substitution_lemma: forall Γ1 Γ2 Γ A B f n x,
    (Γ1 ++ [(x, A)] ++ Γ2) ⊢ f : B ->
    Γ ⊢ n : A ->
    (Γ ## ((subst' x n) <$> Γ1) ++ Γ2) ->
    ⊢ ((subst' x n <$> Γ1) ++ Γ2 ++ Γ) ->
    ((subst' x n <$> Γ1) ++ Γ2 ++ Γ)  ⊢ subst f x n : subst B x n.

Nota that we generalized the location of [(x, A)] to be somewhere in the middle. Then there was another problem (that also existed in the first substitution lemma):

Lemma WF_FV: forall Γ x T, ⊢ ((x, T)::Γ) -> x ∉ fv T.

Which says if x of type T plus other variables with their types form a well-formed context, then x cannot appear in T`.

This was pain to prove .... to say the least, Induction gives cases that does not make sense, and at some point I started to believe that maybe my model is incorrect.

but my model is correct, and after literally doing nothing but staring for days:

I did the following:
A- Assuming ⊢ ((x, T)::Γ) what can we deduce from that, and I came up with two lemmas
one that deduce that x ∉ dom Γ and the other says that exists l, Γ ⊢ t: univ l (I hope that readers have an intuition for what those do..
dom as in get domain of associated array)
B- I tried moving away from the ⊢ ((x, T)::Γ) form, so I tried proving

Lemma typing_fv: forall Γ t T y, Γ ⊢ t: T -> y∉ dom Γ -> y ∉ fv t.

But that also failed and I kept thinking of ways to generalize, until I finally found the form that is provable, that can prove the lemma at B which can prove the lemma that says: forall Γ x T, ⊢ ((x, T)::Γ) -> x ∉ fv T which can solve the remaining goal in my substitution lemma.

forall Γ t T, Γ ⊢ t: T -> fv t ⊆ dom Γ.

Note that this look abolutely nothing like anything I would expect to come up with in normal circumstances.

So my question is is there thinking process to come up with the key lemmas like this awkward looking one without wasting a full week wondering if mayb my type system is completely broken.

mind you that in Meven's thesis he mentions the following about the substitution lemma:

I am not sure if my approach qualifies for being called direct proof by induction (note that he mentions that other lemmas are not easy to prove and I am not touching those in the near future until I learn an efficient way to tackle proofs).

I deliberately wanted to come up with the proof myself to see if maybe I learn something during the process, but it was mostly random unstructured attempts. so now that the proof is complete, I want to learn it from you guys!

Matthieu Sozeau (Oct 13 2022 at 16:28):

I think the particular lemma you are looking at WF_FV has to come up during the proof, whatever the representation you use. In case of de Bruijn indices this is related to the lifting operation. Probably the locally nameless paper has attached examples where they come up with the same path as yours

walker (Oct 13 2022 at 18:30):

The problem was even this lemma was not directly provably and what I want to figure out, is how to develop an instinct to identify the right lemma to prove.

Paolo Giarrusso (Oct 14 2022 at 13:07):

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

I think this is one reason why careful pen-and-paper proofs in type theory report the statements they prove.

Paolo Giarrusso (Oct 14 2022 at 13:11):

and the statements are reused across type systems as far as possible.
The problem you run into for substitution_lemma applies even to STLC, tho it manifests in a different way; on paper, TAPL for STLC solves that by using a _permutation_ lemma to permute bindings, but that doesn't work for dependent types; your solution is a common one.

Paolo Giarrusso (Oct 14 2022 at 13:14):

for the second, I've never seen typing_fv (my ignorance!), but forall Γ t T, Γ ⊢ t: T -> fv t ⊆ dom Γ. seems a natural statement (tho I'd struggle to think of that from WF_FV)

walker (Oct 14 2022 at 14:59):

I see, so these lemmas (or some of them) are well known already ... unfortunately, I didn't know any of them, and maybe that is why it took long to come up with them.

Paolo Giarrusso (Oct 14 2022 at 22:14):

Either they're "well-known" (to type system people), or inventing them is part of your research, or you've already worked through many other type systems so you have more experience and examples

Paolo Giarrusso (Oct 14 2022 at 22:15):

I don't know if there's a better answer than "how do you learn a mathematical theory", but at least there are textbooks and papers

Paolo Giarrusso (Oct 14 2022 at 22:16):

You probably want to use autosubst 2, but its easier to start from the docs for 1

Stream: Miscellaneous

Topic: Methodology for coming up with lemmas

walker (Oct 13 2022 at 15:48):

Matthieu Sozeau (Oct 13 2022 at 16:28):

walker (Oct 13 2022 at 18:30):

Paolo Giarrusso (Oct 14 2022 at 13:07):

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

Paolo Giarrusso (Oct 14 2022 at 13:11):

Paolo Giarrusso (Oct 14 2022 at 13:14):

walker (Oct 14 2022 at 14:59):

Paolo Giarrusso (Oct 14 2022 at 22:14):

Paolo Giarrusso (Oct 14 2022 at 22:15):

Paolo Giarrusso (Oct 14 2022 at 22:16):

Paolo Giarrusso (Oct 14 2022 at 22:16):

Paolo Giarrusso (Oct 14 2022 at 22:16):