So this is follow up on my struggle in this thread:https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Progress.20and.20preservation.20proofs.20for.20dependent.20types
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?
Guess work starts here:
So substitution lemma:
So my lemma looked like this at the beginning:
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
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
lambda abstraction cases.
So after staring, I realized that I need to change the lemma to be:
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):
I had a case that can be proven directly If I can prove the following 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:
⊢ ((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.
That lemma says the following:
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!
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
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.
Kudos on succeeding, that's some determination!
I think this is one reason why careful pen-and-paper proofs in type theory report the statements they prove.
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.
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
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.
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
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
BTW, I liked a lot autosubst 1 docs: https://www.ps.uni-saarland.de/autosubst/
You probably want to use autosubst 2, but its easier to start from the docs for 1
They also come with formalized proofs for many calculi.
Last updated: Dec 05 2023 at 06:01 UTC