walker (Oct 03 2022 at 15:55): walker (Oct 03 2022 at 15:55):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.
walker (Oct 03 2022 at 15:57):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.
walker (Oct 03 2022 at 15:57):also I can share the transitivity and substitution lemma (transitivitiy implmented, substitution admitted).
walker (Oct 03 2022 at 15:58):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
walker (Oct 03 2022 at 16:07):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 :(
walker (Oct 03 2022 at 16:24):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.
Li-yao (Oct 03 2022 at 16:31):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.
walker (Oct 03 2022 at 16:34):I am listening, does this have a name or is it described somewhere?
walker (Oct 03 2022 at 16:35):most text book formalization only offers one application rule, so I assumed this is the way to go.
walker (Oct 03 2022 at 16:37):I am worried that If I did it the way you described, that will be just just cheating the system.
Li-yao (Oct 03 2022 at 16:37):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
walker (Oct 03 2022 at 16:38):thank you so much! I will read it and hopefully breakthought his issue.
Paolo Giarrusso (Oct 03 2022 at 19:41):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.
Paolo Giarrusso (Oct 03 2022 at 19:42):(and I don't know if you need conversion just in application)
walker (Oct 03 2022 at 19:48):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."
Paolo Giarrusso (Oct 03 2022 at 19:49):TAPL explains the distinction for subtyping in chapter 16 or 17, I forget... but TLDR:
Paolo Giarrusso (Oct 03 2022 at 19:50):rules for STLC are syntax-directed — from the term you know which typing rule could apply
Paolo Giarrusso (Oct 03 2022 at 19:50):even more strongly, each term constructor has only one typing rule
Paolo Giarrusso (Oct 03 2022 at 19:52):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!
walker (Oct 03 2022 at 19:53):I see, all those details are glossed over in most lecture materials.
walker (Oct 03 2022 at 19:54):It is funny because I thought conversion rule is something deducable :(
walker (Oct 03 2022 at 19:54):anyways thanks a lot for explaination and pointing to the book,
walker (Oct 03 2022 at 19:57):one last question:
if we add or embed the type conversion rule, that is basically saying that type conversion is our denominational equality, right ?
walker (Oct 03 2022 at 19:58):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.
walker (Oct 03 2022 at 20:00):so this rule basically says --->* is our equality, right ?
Paolo Giarrusso (Oct 03 2022 at 21:33):it seems you're looking at material on simply-typed lambda calculus — extending to dependent types is _not_ an exercise for the reader
Paolo Giarrusso (Oct 03 2022 at 21:35):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
Paolo Giarrusso (Oct 03 2022 at 21:36):s/denominational equality/definitional equality/, but yes
Paolo Giarrusso (Oct 03 2022 at 21:37):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
Pierre-Marie Pédrot (Oct 03 2022 at 21:40):Even without dependent types, you may need arbitrary equational reasoning (e.g. for Fω that's already the case)
Paolo Giarrusso (Oct 03 2022 at 21:40):also not an exercise for the reader from STLC — chapters 11 vs 3X in TAPL
walker (Oct 03 2022 at 22:05):yes I admit, I underestimated, how complex it is, and thought it is an exercise to just free style it.
walker (Oct 03 2022 at 22:06):pi types + universes look deceivingly simple, I thought I can do it in a week.
walker (Oct 03 2022 at 22:07):I will look at book description of the language and try to follow it.
Meven Lennon-Bertrand (Oct 04 2022 at 12:33):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.
Meven Lennon-Bertrand (Oct 04 2022 at 12:35):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 :)
Karl Palmskog (Oct 04 2022 at 13:10):aren't there all these (machine-checked) formalizations of "pure type systems" as well? aren't they also close to these kinds of calculi?
Meven Lennon-Bertrand (Oct 04 2022 at 13:14):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…
Meven Lennon-Bertrand (Oct 04 2022 at 13:17):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.
Karl Palmskog (Oct 04 2022 at 13:20):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”.
Meven Lennon-Bertrand (Oct 04 2022 at 13:27):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)
walker (Oct 04 2022 at 14:49):@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!
Meven Lennon-Bertrand (Oct 04 2022 at 14:49):Hope you have a nice read, then :) Don't hesitate to ask if you have questions!
walker (Oct 04 2022 at 14:52):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 ?
Meven Lennon-Bertrand (Oct 04 2022 at 15:01):I'm not sure I get what you mean: what "implementation" are you talking about?
Karl Palmskog (Oct 04 2022 at 15:14):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
Karl Palmskog (Oct 04 2022 at 15:15):in the PhD thesis, I presume a number of results are already formalized/"implemented" as part of MetaCoq on GitHub
Meven Lennon-Bertrand (Oct 04 2022 at 15:17):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.
walker (Oct 04 2022 at 17:51):Yes this partially the qeustion, but then I am interested in useful extraction, that is a problem for another day.
walker (Oct 04 2022 at 17:52):thanks a lot everyone for clarifications. I will use the thesis as my main guide when impelementing the dependent parts of my language.
Meven Lennon-Bertrand (Oct 05 2022 at 08:30):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).
Paolo Giarrusso (Oct 05 2022 at 10:10):Is the topic extracting the typechecker or the actual programs? From past discussions with @walker I thought the latter, but I'm not sure
walker (Oct 05 2022 at 11:15):So What I am trying to do is designing an optimizing compiler that incorporates features from dependently typed programming languaes and CSL.
walker (Oct 05 2022 at 11:15):Compiler that people can trust to be type safe
walker (Oct 05 2022 at 11:15):So first I need to prove meta theoritic properties about the type system of that compiler.
walker (Oct 05 2022 at 11:16):Then I apparently need to extract the type system so I can build the rest of the compiler around it.
walker (Oct 05 2022 at 11:17):The type system I was trying to design was not the real langage type system but basically a dependently typed intermediate representation.
walker (Oct 05 2022 at 11:18):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.
walker (Oct 05 2022 at 12:06):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.
Michael Soegtrop (Oct 05 2022 at 12:43):@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?
walker (Oct 05 2022 at 13:17):My plan for the backend was using cranelift.
walker (Oct 05 2022 at 13:18):https://github.com/bytecodealliance/wasmtime/tree/main/cranelift
walker (Oct 05 2022 at 13:19):It is not publically advertised yet, but I know that they have workgroups trying to formally verify that cranelift SSA to assembly preserve semantics.
walker (Oct 05 2022 at 13:19):I would hope that this stage will be complete by the time I need it.
walker (Oct 05 2022 at 13:21):but it is good to know that there is a thing called bedrock2 and the project's goal!
walker (Oct 05 2022 at 13:22):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.
walker (Oct 05 2022 at 13:24):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.
walker (Oct 05 2022 at 13:25):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 ....
Michael Soegtrop (Oct 05 2022 at 13:52):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.
walker (Oct 05 2022 at 13:54):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.
walker (Oct 05 2022 at 13:55):but thanks a lot for letting me know about bedrock2, I never heard about it and it sounds like an interesting project
walker (Oct 05 2022 at 14:02):also I honestly never used coq platform before, I build stuff by hand or opam
Michael Soegtrop (Oct 05 2022 at 14:38):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.
Paolo Giarrusso (Oct 05 2022 at 16:10):@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)
Kenji Maillard (Oct 05 2022 at 16:18):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)
Pierre-Marie Pédrot (Oct 05 2022 at 16:28):Dependent types with effects are quite nasty, if you want my opinion.
Pierre-Marie Pédrot (Oct 05 2022 at 16:29):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.
Pierre-Marie Pédrot (Oct 05 2022 at 16:30):CBN is the most natural choice for MLTT (it's actually implicitly already the case), but it's a terrible setting for most effects.
Pierre-Marie Pédrot (Oct 05 2022 at 16:30):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.
walker (Oct 05 2022 at 16:49):I received this as a advice, and I actually checked it once, but will dig deeper into it soon.
Enrico Tassi (Oct 05 2022 at 20:34):@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)
Pierre-Marie Pédrot (Oct 06 2022 at 05:00):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