Jason Gross (Oct 25 2022 at 08:40): Jason Gross (Oct 25 2022 at 08:40):I'm trying to write a gallina function that quotes typing judgments. (I hope this is not a doomed endeavor.) Right now I'm running into the problem that the type_Const case takes an argument of type consistent_instance_ext which after unfolding consistent_instance_ext, consistent_instance, valid_constraints, valid_constraints0, and satisfies holds an argument of type forall v : valuation, ConstraintSet.For_all (satisfies0 v) Σ -> ConstraintSet.For_all (satisfies0 v) (subst_instance_cstrs u c.2).
This is a problem, because I cannot quote lambdas in general. The valuation type is not finite (it holds string -> positive and nat -> nat), and so I cannot enumerate it. While ConstraintSets are finite and hence ConstraintSet.For_all poses no problem in quotation, I cannot invert satisfies0 to construct a finite list of valuations that satisfy a given universe constraint. Thus, unlike for wf_universe, it's not obvious that valid_constraints is decidable. I see that there's a completeness proof relating valid_constraints to check_constraints, but it seems to require manufacturing a bunch of other information which it's not clear to me is implied by valid_constraints, namely I have to manufacture G : universes_graph and uctx : ContextSet.t such that global_uctx_invariants uctx, consistent uctx.2, is_graph_of_uctx G uctx, global_uctx_invariants (uctx.1, ctrs).
Is there any hope of quoting valid_constraints? If not, could I convince the MetaCoq devs to base the inductive typing judgments on some more model-independent notion of valid constraints, which does not even in theory depend on what sorts of nat -> nat functions can exist beyond the syntactic ones?
Jason Gross (Oct 25 2022 at 08:42):I guess there's only a finite amount of information from the valuation used for any given constraint set, so I should be able to just enumerate that information...
Théo Winterhalter (Oct 25 2022 at 08:47):I'm not sure you will convince us to change it back to graphs. Our goal is to have the specification as natural as possible and mostly implementation independent. That said, you should probably be fine if you can use the fact that the two are equivalent right? I'll let someone who worked on it tell you where to find such proof (assuming it was proven).
Jason Gross (Oct 25 2022 at 08:51):Yes, I'm fine as long as the two are actually equivalent. (I believe check_constraints_spec and check_constraints_complete prove equivalence with a version based on universes_graph, which I guess is a starting place...)
Jason Gross (Oct 25 2022 at 08:54):But as I said that version requires a bunch of extra data that I'm not sure how to generate
Jason Gross (Oct 25 2022 at 09:06):It seems like I need some function ConstraintSet.t -> ContextSet.t or ConstraintSet.t -> LevelSet.t? (Do you know of some such function?)
Jason Gross (Oct 25 2022 at 10:13):And now I'm running into a similar trouble with eq_levelalg, where even the graph-version doesn't seem to be obviously decidable?
Meven Lennon-Bertrand (Oct 26 2022 at 13:24):Indeed, as Theo said, we definitely do not want typing to be obviously decidable, but rather to be as "natural" as possible. I guess we could have an intermediate presentation, that while still presented as a judgement is somehow model-independent as you say (and probably closer to the implementation). This is morally what bidirectional typing does, but internally it still uses the same definitions as typing, for instance for constraints.
Meven Lennon-Bertrand (Oct 26 2022 at 13:26):But since for the type-checker we need to show that everything is decidable, you should have all you need in the development. I would probably try and work from the type-checker to locate the decision procedures corresponding to the judgments you have trouble with, and replace those with the decision procedure outputing true.
Jason Gross (Oct 26 2022 at 13:38):In the typechecker it seems that you only show things are decidable under well-formedness assumptions or something? I'm having trouble finding deciders for consistent / gc_consistent, for valid_constraints (in particular I'm not sure how to satisfy the preconditions of check_constraints_spec / check_constraints_complete), eq_levelalg / gc_eq_levelalg, and leq_levelalg_n / gc_leq_levelalg_n
Meven Lennon-Bertrand (Oct 26 2022 at 13:40):I think it often happens that the decider is sound/complete under some additional hypothesis, yes
Meven Lennon-Bertrand (Oct 26 2022 at 13:40):But these should typically hold if the decider is called in a valid environment
Meven Lennon-Bertrand (Oct 26 2022 at 13:42):I think the place to look at for this is probably again in SafeChecker, where to call these deciders and use the fact that they indeed decide the right thing we must show these preconditions are satisfied.
Jason Gross (Oct 26 2022 at 13:45):The issue is that my work is probably an order of magnitude simpler if I can decide the predicate in all cases, not just under additional assumptions.
Meven Lennon-Bertrand (Oct 26 2022 at 13:48):I know the issue, I faced it too when wanting to write the completeness proof… But I think in the end most statements are some kind of "bundles", and usually the first part of the bundle gives you the precondition for the decider of the second to be correct. Isn't this enough for you?
Jason Gross (Oct 26 2022 at 13:52):It's the other way around for me. If I need to satisfy the preconditions of the checker, then I must map bundles to bundles wholesale, because the second part of my input bundle is required to satisfy the preconditions for using the checker to generate the first part of my output bundle.
Jason Gross (Oct 26 2022 at 13:53):And this makes things more painful, because it means that I can no longer work with untyped syntax at all in my development, but instead have to phrase everything in terms of well-typed syntax
Jason Gross (Oct 26 2022 at 13:57):And there are some things that I want to try out that I don't know how to do when using only syntax that is indexed on its type, so I'm inclined to just write the decider myself rather than bundle...
Meven Lennon-Bertrand (Oct 26 2022 at 14:00):I'm not sure I understand what your issue is. But I agree that staying away from intrinsically well-typed syntax sound wise
Jason Gross (Oct 26 2022 at 14:14):I'm trying to write a Gallina function quote : Ast.term -> Ast.term such that quote x is more-or-less equivalent to <% x %> when x is closed / in the empty context.
Jason Gross (Oct 26 2022 at 14:17):Separately, I want to show that if Σ is rich enough and Γ is well-formed, then Σ;;; Γ |- quote x : <% Ast.term %> in all cases, independent of x (even if x is not sufficiently well-formed, that is)
Jason Gross (Oct 26 2022 at 14:18):And then I also want to have quote_typing : (Σ;;; Γ |- t : T) -> Ast.term, and a similar proof about the typing of quote_typing pf.
Jason Gross (Oct 26 2022 at 14:18):(This is all so that I can formalize Löb's theorem about Coq)
Meven Lennon-Bertrand (Oct 26 2022 at 14:21):And what you are saying is that you want the least amount possible of dependencies between those definitions?
Jason Gross (Oct 26 2022 at 14:22):Yes, I don't want to have to assume (Σ;;; Γ |- t : T) to write quote : Ast.term -> Ast.term. Because my prior experience is that inconsistency about abstraction barriers (in this case, about whether I'm operating on typed or untyped syntax) is begging for pain.
Meven Lennon-Bertrand (Oct 26 2022 at 14:22):Yup, that I agree with
Meven Lennon-Bertrand (Oct 26 2022 at 14:25):I'm not sure about this, but I think that the current positivity criterion is too weak to be able to quote Ast.term or typing. From what I understand, nested inductive types are not supported by it yet, and both term and typing use list of terms/typing judgments in their definitions.
Meven Lennon-Bertrand (Oct 26 2022 at 14:26):Which would mean you cannot have a well-formed environment (in the sense of MetaCoq) containing either one of them :/
Jason Gross (Oct 26 2022 at 14:27):This is really unfortunate :-(
Jason Gross (Oct 26 2022 at 14:27):(This does not mean I cannot quote them, though, just that I cannot prove that the quotation is well-typed)
Jason Gross (Oct 26 2022 at 14:28):(But this is all the more reason to separate quotation from well-typedness)
Meven Lennon-Bertrand (Oct 26 2022 at 14:39):Indeed!
Meven Lennon-Bertrand (Oct 26 2022 at 14:40):Although I do not think this is because of "deep" difficulties, just that inductive types are already extremely technical, and that nested ones are even worse
Meven Lennon-Bertrand (Oct 26 2022 at 14:46):Nasty inductives are a recurring topic of conversation in Nantes, so the addition of nested ones to MetaCoq is bound to happen (especially if we have a good reason to do so) but nobody is working on it just yet. So I don't know how long it will take to have them :/
Jason Gross (Oct 26 2022 at 14:48):I don't think it'll be a blocker for my use-case unless / until I'm ready to write a paper; I'm planning on parameterizing everything over "a global env strong enough to hold quoted versions of Ast.term, etc", until the very very end where I'll instantiate it with some particular global env. In the meantime it's okay if my theorems are technically vacuous because no well-formed global env can hold quoted versions of Ast.term
Meven Lennon-Bertrand (Oct 26 2022 at 14:50):I see, then indeed you should be fine. Maybe this will even give someone a strong enough push to tackle these!
Jason Gross (Nov 02 2022 at 00:55):Thoughts on replacing valuation functions with association lists, essentially forcing universe assignments to be finite?
Matthieu Sozeau (Nov 23 2022 at 12:40):I guess you could simply use finite-support functions like mathcomp's finfuns
Jason Gross (Nov 23 2022 at 13:51):I've managed to bypass this issue using deciders, eg at https://github.com/JasonGross/metacoq-lob/blob/4222900653a338b2870e933d1b6a5da7a94a2eb7/theories/Template/Decidable/Universes.v#L218, there's only one I can't figure out (I'll bump that thread)
Notification Bot (Nov 23 2022 at 13:51):Jason Gross has marked this topic as resolved.
Last updated: May 31 2023 at 04:01 UTC