I see

```
uGraph.consistent_ext_on_full_ext:
forall {cf : config.checker_flags} [uctx : ContextSet.t] [G : uGraph.universes_graph]
[uctx' : ContextSet.t] [G' : uGraph.universes_graph],
` uctx ->
uGraph.is_graph_of_uctx G' uctx' ->
uGraph.global_uctx_invariants uctx ->
uGraph.global_uctx_invariants uctx' ->
is_true (uGraph.wGraph.is_acyclic G') ->
uGraph.wGraph.subgraph G G' ->
consistent_extension_on uctx (snd uctx') <->
is_true (uGraph.wGraph.IsFullSubgraph.is_full_extension G G')
```

Why do we need `uGraph.wGraph.subgraph G G'`

? (Is it just to establish acyclicity of G?) And is there a way to manufacture `G`

from `uctx`

such that `uGraph.is_graph_of_uctx`

and `uGraph.wGraph.is_acyclic`

?

The subgraph part is used for acyclicity of `G`

but also to be able to use `wGraph.is_full_extension_spec`

. For the second part, I think you should be able to use `uGraph.make_graph uctx`

to obtain `G`

and then you would need to use `uGraph.is_consistent_spec2`

for the acyclicity part

Thanks

For the second part, will the resulting manufactured G and G' satisfy the subgraph hypothesis? (Is there a way to ensure that they do?)

I'm not sure I understand what you are trying to achieve here. I wrote `uGraph.consistent_ext_on_full_ext`

to be able to extend an existing graph of universe constraints with additional ones (which is required when defining a universe-polymorphic constant that adds constraints between pre-existing monomorphic universes)

I'm trying to find / write a boolean decider for `consistent_extension_on`

in full generality.

Here is my series of instrumental goals:

I want:

`gc_consistent_dec : forall ctrs, {@gc_consistent ctrs} + {~@gc_consistent ctrs}`

;`gc_leq0_levelalg_n_dec : forall n ctrs u u', {@gc_leq0_levelalg_n n ctrs u u'} + {~@gc_leq0_levelalg_n n ctrs u u'}`

;`consistent_extension_on_dec : forall cs cstr, {@consistent_extension_on cs cstr} + {~@consistent_extension_on cs cstr}`

; and`valid_constraints_dec : forall cf ϕ cstrs, {@valid_constraints cf ϕ cstrs} + {~@valid_constraints cf ϕ cstrs}`

; so that I can get`consistent_dec : forall ctrs, {@consistent ctrs} + {~@consistent ctrs}`

,`leq0_levelalg_n_dec : forall n ϕ u u', {@leq0_levelalg_n n ϕ u u'} + {~@leq0_levelalg_n n ϕ u u'}`

,`consistent_extension_on_dec`

, and`valid_constraints_dec`

; so that I can get- functions from
`consistent`

,`leq0_levelalg_n`

,`consistent_extension_on`

,`valid_constraints`

, etc; to`Ast.term`

which "quote" ground values

My ultimate goal is writing a function `quote_term : Ast.term -> Ast.term`

and `quote_typing : forall {Σ Γ t T}, Σ ;;; Γ |- t : T -> Ast.term`

such that for any ground term, `quote_term t ≡ <% t %>`

, and we have for `Σ`

with enough declarations and for any `Γ`

with `wf_local Σ Γ`

, that `Σ ;;; Γ |- quote_term t : <% Ast.term %>`

, and for `pf : Σ' ;;; Γ' |- t : T`

we have `Σ ;;; Γ |- quote_typing pf : <% typing %> (quote Σ') (quote Γ') (quote_term t) (quote_term T)`

So indeed using `wGraph.IsFullSubgraph.is_full_extension`

to decide whether the extension is correct and `uGraph.consistent_ext_on_full_ext`

to change representation seems like the right way to go.

`uGraph.make_graph : uGraph.VSet.t * uGraph.GoodConstraintSet.t -> uGraph.wGraph.t`

but I need `ContextSet.t -> uGraph.universes_graph`

I guess `uGraph.universes_graph`

is just `uGraph.wGraph.t`

though

It looks like `wGraph.IsFullSubgraph.is_full_extension`

just doesn't work when both sets are missing lzero?

Yeah, it seems like `uGraph.consistent_ext_on_full_ext`

doesn't actually work for representation changes because `consistent_extension_on`

doesn't require `uGraph.global_uctx_invariants`

and `uGraph.consistent_ext_on_full_ext`

doesn't specify the behavior when `uGraph.global_uctx_invariants`

doesn't hold. Should `consistent_extension_on`

be modified to require that `uGraph.global_uctx_invariants`

?

@Kenji Maillard Could you help me figure out how to finish the proof at https://github.com/JasonGross/metacoq-lob/blob/4222900653a338b2870e933d1b6a5da7a94a2eb7/theories/Template/Decidable/Universes.v#L105-L175 ?

@Matthieu Sozeau this is the one part of deciding universe graphs that I haven't figured out. Any ideas?

Still looking for help on this

Last updated: Oct 12 2024 at 11:01 UTC