Stream: MetaCoq

Topic: uGraph.consistent_ext_on_full_ext

Jason Gross (Nov 03 2022 at 16:37):

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?

Kenji Maillard (Nov 04 2022 at 13:04):

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

Jason Gross (Nov 04 2022 at 13:07):

Thanks

Jason Gross (Nov 04 2022 at 13:09):

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

Kenji Maillard (Nov 04 2022 at 13:56):

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)

Jason Gross (Nov 04 2022 at 14:53):

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:

1. 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
2. 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
3. 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)

Kenji Maillard (Nov 04 2022 at 15:50):

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.

Jason Gross (Nov 04 2022 at 16:07):

uGraph.make_graph : uGraph.VSet.t * uGraph.GoodConstraintSet.t -> uGraph.wGraph.t but I need ContextSet.t -> uGraph.universes_graph

Jason Gross (Nov 04 2022 at 16:08):

I guess uGraph.universes_graph is just uGraph.wGraph.t though

Jason Gross (Nov 04 2022 at 16:36):

It looks like wGraph.IsFullSubgraph.is_full_extension just doesn't work when both sets are missing lzero?

Jason Gross (Nov 04 2022 at 21:36):

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?

Jason Gross (Nov 05 2022 at 18:47):

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

Jason Gross (Nov 23 2022 at 13:55):

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

Jason Gross (Dec 09 2022 at 12:38):

Still looking for help on this

Last updated: Oct 12 2024 at 11:01 UTC