I am trying to formalize preservation proofs for dependent type lambda calculus in Coq, and I am stuck at the preservation proof, I wanted to know if there is already public resouces (paper/.v files) on how to do deal wit the tricks
I will try to describe where I am stuck
Γ is used to represent global variables declarations (variable & type), while the Ψ is for local variables (I separated between them in my implementation) and Δ is used for global variable definition (variable and content) The reason for the separation is that I have global variables as well and they are represented as strings.
The typing rule (part of it) looks like this
Inductive SyntaticallyTypes: stringmap Term -> gmap nat Term -> Term -> Term -> Prop :=
| SyntaticallyTypes_pi: forall Γ Ψ A B l (L: gset nat),
Γ, Ψ ⊢ A: univ l ->
(forall x, x ∉ L -> Γ, Ψ ∪ {[ x := A ]} ⊢ open B (fvar x) : univ l ) ->
Γ, Ψ ⊢ pi A B : univ l
| SyntaticallyTypes_lam: forall Γ Ψ A y B l (L: gset nat),
Γ, Ψ ⊢ A: univ l ->
(forall x, x ∉ L -> Γ, Ψ ∪ {[ x := A ]} ⊢ open y (fvar x) : open B (fvar x) ) ->
Γ, Ψ ⊢ lam A y : pi A B
| SyntaticallyTypes_appl: forall Γ Ψ A B m n,
Γ, Ψ ⊢ m : pi A B ->
Γ, Ψ ⊢ n : A ->
Γ, Ψ ⊢ appl m n : open B n
where "Γ ',' Ψ '⊢' t : T" := (SyntaticallyTypes Γ Ψ t T).
The main difference is the part where we say Γ, Ψ ⊢ appl m n : open B n
we just don't type function application as return value:
Then there is the stepping rules:
Reserved Notation "Δ '⊢' t '--->' t'" (at level 20).
Inductive Step: stringmap Term -> Term -> Term -> Prop :=
| Step_appl: forall (Δ: stringmap Term) (T y m: Term),
Δ ↛ (lam T y) ->
Δ ↛ m ->
Δ ⊢ (appl (lam T y) m) ---> (open y m)
| Step_appl_left: forall (Δ: stringmap Term) (f f' m: Term),
LC m ->
Δ ⊢ f ---> f' ->
Δ ⊢ (appl f m) ---> (appl f' m)
| Step_appl_right: forall (Δ: stringmap Term) (f m m': Term),
LC m ->
Δ ↛ f ->
Δ ⊢ m ---> m' ->
Δ ⊢ (appl f m) ---> (appl f m')
where "Δ '⊢' t '--->' t'" := (Step Δ t t').
LC is for locally closed terms, and Δ ↛ f
means f is value (or if it is global variable than the data stored in Δ is also a value
Here is where I am stuck
H': Δ ⊢ appl m n ---> t'
------------------------------
Goal: Γ, ∅ ⊢ t' : open B n
I would just invert H'
to get the three cases of application. First case (Γ, ∅ ⊢ open y n : open B n
) is solved by substitution lemma,
Second case is trivial,
The problem is with Step_appl_right
case:
The goal is to solve he following
H7: Δ ⊢ n ---> m'
-----------------------
Γ, ∅ ⊢ appl m m' : open B n
substitution lemma, and transitivity of Typing assumes that m'
and n
are the same, If I don't do so, I end up creating a more complex version of the preservation lemma itself.
I can share additional information as needed, but I wanted to avoid copy pasting the whole implementation here, and thought it might be better to put effort into explaining the problem.
P.S, I think it might be important to mention that I am doing the cofinite quantifications and nameless representations from enginering formal metatheory
paper, this case I am stuck at is one of the core differences between dependent lambda calculus and normal typed lambda calculus.
also I can share the transitivity and substitution lemma (transitivitiy implmented, substitution admitted).
Lemma trans_SyntaticallyTypes: forall Γ Ψ A B a f,
Γ, Ψ ⊢ f : pi A B ->
Γ, Ψ ⊢ a: A ->
Γ, Ψ ⊢ appl f a : open B a.
Lemma substitution_lemma: forall Γ Ψ A B a y,
Γ, Ψ ⊢ lam A y : pi A B ->
Γ, Ψ ⊢ a: A ->
Γ, Ψ ⊢ open y a : open B a.
I think a lot of the stuff from the Engineering Formal Metatheory paper is now maintained here: https://github.com/plclub
Specifically: https://github.com/plclub/metalib
yes, that is true, and I am following their tutorial but without the library, but that is not the current problem, my problem is unfornately with the one thing they don't show how to do :(
I realized that I wrote lots of stuff, so let me summarize, i am stuck trying to prove preservation for f x
where f
is lambda abstraction with arbitrary pi type.
That doesn't seem provable with only that one typing rule for application. You should either weaken the preservation theorem to allow the type to change through reduction, or add that flexibility in typing rules to allow types in typing derivations to differ up to convertibility.
I am listening, does this have a name or is it described somewhere?
most text book formalization only offers one application rule, so I assumed this is the way to go.
I am worried that If I did it the way you described, that will be just just cheating the system.
The second option I mentioned is to add a "conversion rule", for example there's one in this paper (Figure 3, rule E-Conv) https://dl.acm.org/doi/pdf/10.1145/3110275
thank you so much! I will read it and hopefully breakthought his issue.
I don't know the terminology for dependent types, but analogy with subtyping would give standard names to @Li-yao 's suggestions: adding conversion gives a declarative type system, while embedding conversion in the application rule gives an algorithmic type system.
(and I don't know if you need conversion just in application)
I am not sure I understand what that means "adding conversion gives a declarative type system, while embedding conversion in the application rule gives an algorithmic type system."
TAPL explains the distinction for subtyping in chapter 16 or 17, I forget... but TLDR:
rules for STLC are syntax-directed — from the term you know which typing rule could apply
even more strongly, each term constructor has only one typing rule
Therefore, writing a typechecker is pretty mechanic. If this is the case, we call the type system "algorithmic". However, the conversion rule is not like that!
I see, all those details are glossed over in most lecture materials.
It is funny because I thought conversion rule is something deducable :(
anyways thanks a lot for explaination and pointing to the book,
one last question:
if we add or embed the type conversion rule, that is basically saying that type conversion is our denominational equality, right ?
The rule I had in mind looked like something like this as an addition to the typing rules (or embedding it in every rule):
| SyntaticallyTypes_conv: forall Γ Ψ t T T',
Γ, Ψ ⊢ t: T ->
(forall Δ, Δ ⊢ T --->* T') -> (*T can be reduced to T' via zero or more steps *)
Γ, Ψ ⊢ t: T'
also never mind the Δ ⊢
part, that is the global definitions. but you get the idea.
so this rule basically says --->* is our equality, right ?
it seems you're looking at material on simply-typed lambda calculus — extending to dependent types is _not_ an exercise for the reader
It is funny because I thought conversion rule is something deducable :(
conversion _is_ decidable, the question is when to use it. One can rephrase things to "embed" conversion only where needed, that is in elimination rules — in your case, in SyntaticallyTypes_appl
you'd replace Γ, Ψ ⊢ m : pi A B
with Γ, Ψ ⊢ m : T
and T ~= pi A B
s/denominational equality/definitional equality/, but yes
re Δ ⊢ T --->* T'
, I don't think that's enough. You need T
and T'
to be convertible, but that might require reduction in either direction. And in modern formulations of dependent types, convertibility is not restricted to reduction
Even without dependent types, you may need arbitrary equational reasoning (e.g. for Fω that's already the case)
also not an exercise for the reader from STLC — chapters 11 vs 3X in TAPL
yes I admit, I underestimated, how complex it is, and thought it is an exercise to just free style it.
pi types + universes look deceivingly simple, I thought I can do it in a week.
I will look at book description of the language and try to follow it.
I do not know if you are aware of it, but you might want to look at MetaCoq which does this kind of things for a realistic type system (as close as possible to Coq's). Although quite some difficulties come from "advanced" Coq features (patterrn-matching, complicated universes, etc.), even for the "λ-Π-universes" fragment preservation is not trivial. In particular, you need to show what is usually called injectivity of product types with respect to conversion, which requires a non-trivial proof (MetaCoq uses that conversion can be characterized in term of reduction, and that said reduction is confluent). For paper details on this, you can go look at this paper.
Regarding algorithmic vs declarative type system, this is also something we encountered in this project, and we actually have both kinds of systems around. But, again, showing their equivalence is not trivial. For more on this, you might want to give a look at my PhD thesis, which talks quite a lot about these issues :)
aren't there all these (machine-checked) formalizations of "pure type systems" as well? aren't they also close to these kinds of calculi?
Yes, indeed, the fragment we are talking about looks a lot like a PTS (maybe with added constants, but these do not change too much), and most of these questions have been studied in that setting a while ago. I can't give the relevant citations on the top of my head, though…
But imho PTS formulations tend to be oldish, meaning some things are harder than they should be, making it sometimes difficult to distinguish between what is actually a hard question and will only become harder in more complex systems, and what is mostly a presentation issue.
if we believe Larry Paulson, a lot of type theory was basically motivated by presentational issues: https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html
types are syntax, not semantics.
A view from I tend to think of the syntactic rules of type theory as giving a “presentation of an algebraic theory”.
Yes, indeed, and this is precisely my critic of PTS: they got some things right, but I think we now know how to do better presentations (of very similar systems)
@Meven Lennon-Bertrand I think your phd thesis is the thing I was literally looking for, and the idea to check how metacoq do it, thanks a lot!
Hope you have a nice read, then :) Don't hesitate to ask if you have questions!
I have one actually, do you think it is good idea to implement the type system the way you describe it in the phd ? or is there a better approach to tackle this problem ?
I'm not sure I get what you mean: what "implementation" are you talking about?
from above, I think the intended meaning of "implement" is: make a deep embedding of the system in a proof assistant and prove its metatheory correct there
in the PhD thesis, I presume a number of results are already formalized/"implemented" as part of MetaCoq on GitHub
If this is the question, yes indeed, many parts of the PhD are not only formalized in MetaCoq, but needed to complete the proof of completeness of the implemented type-checker that is part of the project. I give an overview of this in the second part.
Yes this partially the qeustion, but then I am interested in useful extraction, that is a problem for another day.
thanks a lot everyone for clarifications. I will use the thesis as my main guide when impelementing the dependent parts of my language.
walker said:
Yes this partially the qeustion, but then I am interested in useful extraction, that is a problem for another day.
The aim of our type-checker is to yield a reasonable program when erased, so in that sense, yes. However, the main point is that I present bidirectional/algorithmic typing as an inductive relation, which it does not make much sense to extract. Only after the fact do we write a type-checker, which is proven correct wrt. the inductive relation (and this is much easier than with respect to the declarative presentation, because even when described as a relation the algorithmic presentation is closer to the implementation).
Is the topic extracting the typechecker or the actual programs? From past discussions with @walker I thought the latter, but I'm not sure
So What I am trying to do is designing an optimizing compiler that incorporates features from dependently typed programming languaes and CSL.
Compiler that people can trust to be type safe
So first I need to prove meta theoritic properties about the type system of that compiler.
Then I apparently need to extract the type system so I can build the rest of the compiler around it.
The type system I was trying to design was not the real langage type system but basically a dependently typed intermediate representation.
That meant it doesn't have to be easy to use, or comes with inference rules or anything fancy, it just have to have all the needed features without necessarily the needed convenience.
That is not to say I assumed the representation used for proofs will be suitable for extraction. I wanted to make sure that the system in question is decidable, thus I can write something that can be extracted and prove that the two implementations are equivalent.
@walker : are you aware of CertiCoq and/or rupicola?
As far as I understand both can't handle all of Gallina and CertiCoq (again afaik) more focusses on completeness while Rupicola focusses on generating very high performance code for a small application domain and making this domain easy to extend. Also both have different backends (CompCert for CertiCoq vs. Bedrock2 for Rupicola (afaik)).
Do I understand your project correctly that you want to design a language similar to Gallina, for which you want to create a complete compiler certified in Coq? What are your plans for the backend?
My plan for the backend was using cranelift.
https://github.com/bytecodealliance/wasmtime/tree/main/cranelift
It is not publically advertised yet, but I know that they have workgroups trying to formally verify that cranelift SSA to assembly preserve semantics.
I would hope that this stage will be complete by the time I need it.
but it is good to know that there is a thing called bedrock2 and the project's goal!
but yes I want to create something like gallina ... only if gallina had side effects and resource managements ... I know this sounds too insane and too ambitious but this is goal, and we will see how much complexity will I get in the way.
and the good thing I don't have to restrict myself to gallina, since I am doing it from scratch. and now that projects like metacoq, certicoq, rupicola exist, I might have to borrow the techniques they used to engineer the proofs.
I wish I could say "I know this is not as easy as it sounds," but then it doesn't sound easy to start with anyways ....
Thanks for sharing the details!
I would not bet on that cranelift has ready to use Coq specs and proofs in some near future. But I guess the backend decisions are quite a bit in the future for you, and there is no need to think too much about it now. You can have a look at things when you are ready. I would just advise to not have a specific backend in mind now.
bedrock2, Rupicola and fiat-crypto are btw included in the extended level of the soon to be released Coq Platform 2022.09. I found these libraries rather hard o build before, because there were no tags and one needed a specific set of commits of all the dependencies to compile it. I hope the inclusion makes it much easier to "play" with these developments.
yeah I didn't really have one in mind, my main focus was was on trying to get a good dependently typed intermedite representation. but the reality is I couldn't even prove preservation for language that contains dependent pi types with book style universes.
but thanks a lot for letting me know about bedrock2, I never heard about it and it sounds like an interesting project
also I honestly never used coq platform before, I build stuff by hand or opam
Well you might be using Coq Platform anyway. The majority of the work behind it is not the scripts or the installers, but to make people create compatible sets of opam packages in a reasonable time frame after a Coq release and test if this actually works. For bedrock2 there likely would not be an opam package without Coq Platform (see https://github.com/coq/platform/issues/178). All the "please create an opam package which works" issues linked in (https://github.com/coq/platform/issues/274) might give you an impression on the impact of Coq Platform on opam.
@walker re "gallina with side effects and resources", I'd mention ATS as related work, and note it uses refinement types (not quite dependent types)
And more recently the introduction of exceptional type theories, as well as the lines of work on dependent call-by-push-value (cf the various papers of Pédrot-Tabareau, Ahman, Vakar)
Dependent types with effects are quite nasty, if you want my opinion.
Basically you have to pick a side between call-by-name and call-by-value, and then you get two wildly different realms that are both annoying, for different reasons.
CBN is the most natural choice for MLTT (it's actually implicitly already the case), but it's a terrible setting for most effects.
CBV is better for effects but then you get into very weird crap due to dependent types, and you essentially have to always defensively turn things into values to be able to depend on them.
I received this as a advice, and I actually checked it once, but will dig deeper into it soon.
@Kenji Maillard @Pierre-Marie Pédrot could you suggest a good reference for the lazy reader? The two remarks by PMP about CBN and CBV look very interesting to me, where can I read about them? (sorry, I don't have the time to do a lot of bibliography myself)
I think that https://hal.inria.fr/hal-02383109 is a good start (albeit a bit dense).
Last updated: Sep 25 2023 at 14:01 UTC