Fix universe inconsistency issue in FoldCTree

[ionathanch]

I haven't been able to dune build the entire thing¹ bc my laptop is too pathetic so you should check this yourselves but I've built enough portions that I'm fairly confident this should fix the universe inconsistency issue in FoldCTree.

(Unfortunately for me (but fortunately for y'all) it wasn't an instance where something really needed to be polymorphic but rather that C was applied to X when you have ctree E C X. It would probably help prevent future issues if you changed the definition of ctrees to enforce that the universe level of ctree E C X and of X be exactly the same...)

Footnotes

1. Is there a dune build GH action for PRs? That'd be v handy ↩

[YaZko]

Hey Jon!

Thanks for your message! That's quite the good catch indeed, thanks a bunch.
Unfortunately, we still have deep-rooted universes issues, but it's great to fix one!

W.r.t. compilation, we just fixed at least the execution time --- and I'm fairly confident the ram consumption as well, but I need to double check --- by relying on the new coinduction branch. I only fixed the v0.1 branch against it for now, I do things more properly asap.

Best,
Yannick

[YaZko]

Ah I had overlooked this part of your message:

It would probably help prevent future issues if you changed the definition of ctrees to enforce that the universe level of ctree E C X and of X be exactly the same...

Would you have an intuition about this?

[ionathanch]

Both universe inconsistencies (incl. the one Lef pushed a fix for earlier) were caused by C being applied to X which somehow enforces the universe level of X to be strictly smaller than ctree E C X which then prevents you from using the two at the same level (e.g. ctree E C (ctree E C X)).

Specifically it starts out with a section with context variables (I've added explicit universes for clarity):

Section Lib.
  Universes a b c d e.
  Context {E : Type@{a} -> Type@{b}}
          {C: Type@{c} -> Type@{d}}
          {X : Type@{e}}.

Either the section explicitly applies ctree E C X or when you use something in the section they get instantiated to E, C, X that have been applied to a ctree, so you get constraints like this (u being the level of the ctree):

a < u
c < u
b <= u
d <= u
e <= u

Then C X occurs somewhere; in the Kripke file those were some of the ktrans lemmas, and in SSim that was the spin thing:

  Lemma ktrans_lem: forall (c : C X) (t : ctree E C X) (k : X -> ctree E C X), ...
  Lemma spinny : forall {Y} (c: C X) (c': C Y) (x: X) (y: Y), ...
End Lib.

I'm not entirely sure why, but this seems to add the constraint c = e between C's domain level and X's level, which then means that e < u must hold whenever you use those lemmas, since you're instantiating the E, C, X. I think it might be related to this: coq/coq#17498.

So if in a later file you do use those lemmas:

Require Import Lib.
Section OtherFile.
  Lemma some_lemma : forall {E C X} (t : ctree E C X), ...
  Proof.
    ...
    apply ktrans_lem.
    ...
  Qed.

and then attempt to violate the constraints you've unwittingly imported:

  Fail Lemma inc : forall {E C X} (t : ctree E C (ctree E C X)), ...
End OtherFile.

you'll get an inconsistency saying that u <= e cannot be enforced (level of inner ctree E C X) because e < u. Sometimes these inconsistencies don't show up until my later because you simply haven't attempted something nesty like inc until much later (e.g. Network imports Ctl uses ktrans from Kripke). tbh I'm not sure why the inconsistency shows up in FoldCTree bc I don't actually see any nested ctrees around, but thankfully the culprit was the direct usage of something from SSim. Anyway the fix is simply to generalize over X in those earlier lemmas.

I don't actually really know much about the intended meanings of what ctrees are, but from the use of nested ctrees I gather that the levels of ctrees and result type X really should be the same. I suppose you could simply make sure to never ever ever apply a context C to a context X, but that's really a workaround for Coq being weird about elaborating universe levels, and I don't know how you'd enforce that, so it'd be easier to just say c <= e or even e = u to prevent that from happening.

Of course if you actually do want to apply C to X (what is that, a choice over your result type? do you do that?), then you'll run into the exact same issue, and I think at this point you really do need universe-polymorphic ctrees. In that case, good luck lol

(I know this is getting long but one final addendum: I noticed in Bisim there's a ton of instances of C X or similar, but that doesn't cause issues because C and X are generalized in each lemma and not in a Context. Do you get universe inconsistencies when you apply a specific lemma in Bisim and then go on to state a nested ctree? If not, then I think the issue really is just Coq's elaboration and not something more fundamental, but it also seems unreasonable to ask that people annotate Type on every single type.)

(Also some things behave weird when you have things like ctree E C X + X but I didn't care to look into that and I think you know about the issues with +.)