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 `ConstraintSet`

s are finite and hence `ConstraintSet.For_all`

poses no problem in quotation, I cannot invert `satisfies0`

to construct a finite list of `valuation`

s 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?

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...

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).

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...)

But as I said that version requires a bunch of extra data that I'm not sure how to generate

It seems like I need some function `ConstraintSet.t -> ContextSet.t`

or `ConstraintSet.t -> LevelSet.t`

? (Do you know of some such function?)

And now I'm running into a similar trouble with `eq_levelalg`

, where even the graph-version doesn't seem to be obviously decidable?

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.

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`

.

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`

I think it often happens that the decider is sound/complete under some additional hypothesis, yes

But these should typically hold if the decider is called in a valid environment

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.

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.

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?

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.

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

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...

I'm not sure I understand what your issue is. But I agree that staying away from intrinsically well-typed syntax sound wise

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.

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)

And then I also want to have `quote_typing : (Σ;;; Γ |- t : T) -> Ast.term`

, and a similar proof about the typing of `quote_typing pf`

.

(This is all so that I can formalize Löb's theorem about Coq)

And what you are saying is that you want the least amount possible of dependencies between those definitions?

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.

Yup, that I agree with

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.

Which would mean you cannot have a well-formed environment (in the sense of MetaCoq) containing either one of them :/

This is really unfortunate :-(

(This does not mean I cannot quote them, though, just that I cannot prove that the quotation is well-typed)

(But this is all the more reason to separate quotation from well-typedness)

Indeed!

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

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 :/

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

I see, then indeed you should be fine. Maybe this will even give someone a strong enough push to tackle these!

Thoughts on replacing `valuation`

functions with association lists, essentially forcing universe assignments to be finite?

I guess you could simply use finite-support functions like mathcomp's finfuns

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)

Jason Gross has marked this topic as resolved.

Last updated: Feb 04 2023 at 03:30 UTC