Library MetaCoq.Template.common.uGraph

Require Import ssreflect ssrbool OrderedTypeAlt MSetAVL MSetFacts MSetProperties MSetDecide Morphisms.
From MetaCoq.Template Require Import utils config Universes wGraph.
From Equations.Prop Require Import DepElim.
From Equations Require Import Equations.
Import ConstraintType.

Import MCMonadNotation.

Arguments Z.add : simpl nomatch.
Arguments Nat.leb : simpl nomatch.
Arguments Nat.eqb : simpl nomatch.

Definition Z_of_bool (b : bool) : Z :=
  match b with
  | true ⇒ 1
  | false ⇒ 0
  end.
Notation "⎩ b ⎭" := (Z_of_bool b).

Module VariableLevel.
  Inductive t_ := Level (_ : string) | Var (_ : nat).
  Definition t := t_.

  Declare Scope var_level.
  Delimit Scope var_level with var_level.

  Definition lt : t → t → Prop :=
    fun x y ⇒ match x, y with
            | Level _, Var _ ⇒ True
            | Level s, Level s' ⇒ StringOT.lt s s'
            | Var n, Var n' ⇒ n < n'
            | Var _, Level _ ⇒ False
            end.
  Global Instance lt_strorder : StrictOrder lt.
    split.
    - intros [s|n] H; cbn in H.
      now eapply irreflexivity in H.
      lia.
    - intros [s1|n1] [s2|n2] [s3|n3]; cbn; intuition.
      eapply transitivity; eassumption.
  Qed.
  Definition lt_trans : Transitive lt := _.

  Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
    intros x y [] z t []; reflexivity.
  Qed.
  Definition compare : t → t → comparison :=
    fun x y ⇒ match x, y with
            | Level _, Var _ ⇒ Datatypes.Lt
            | Level s, Level s' ⇒ string_compare s s'
            | Var n, Var n' ⇒ Nat.compare n n'
            | Var _, Level _ ⇒ Datatypes.Gt
            end.
  Infix "?=" := compare : var_level.
  Definition compare_spec :
    ∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
    intros [s|n] [s'|n']; cbn; try now constructor.
    - eapply CompareSpec_Proper. 2-4: reflexivity.
      2: apply CompareSpec_string.
      split; congruence.
    - eapply CompareSpec_Proper. 2-4: reflexivity.
      2: apply PeanoNat.Nat.compare_spec.
      split; congruence.
  Qed.
  Lemma compare_refl (x : t) : compare x x = Datatypes.Eq.
  Proof.
    destruct x ⇒ /= //.
    rewrite string_compare_eq //.
    now rewrite Nat.compare_refl.
  Qed.

  Definition eq_dec : ∀ x y : t, {x = y} + {x ≠ y}.
    intros [s|n] [s'|n']; try now constructor.
    destruct (Classes.eq_dec s s'); [left|right]; congruence.
    destruct (PeanoNat.Nat.eq_dec n n'); [left|right]; congruence.
  Defined.

  Lemma compare_eq : ∀ x y : t, compare x y = Datatypes.Eq → x = y.
  Proof.
    intros x y. destruct (compare_spec x y) ⇒ //.
  Qed.

  Lemma compare_sym : ∀ x y : t, (compare y x) = CompOpp (compare x y).
  Proof.
    induction x; destruct y; simpl; auto.
    apply StringOT.compare_sym.
    apply PeanoNat.Nat.compare_antisym.
  Qed.

  Lemma compare_trans :
    ∀ c (x y z : t), (x?=y)%var_level = c → (y?=z)%var_level = c → (x?=z)%var_level = c.
  Proof.
    intros c x y z.
    destruct (compare_spec x y) ⇒ <-; subst.
    destruct (compare_spec y z); auto.
    destruct (compare_spec y z); auto; try congruence.
    destruct (compare_spec x z); auto; try congruence.
    subst. elimtype False. eapply irreflexivity. etransitivity; [exact H|exact H0].
    elimtype False. eapply irreflexivity. etransitivity; [exact H|].
    eapply transitivity; [exact H0|exact H1].
    destruct (compare_spec y z); auto; try congruence.
    destruct (compare_spec x z); auto; try congruence.
    subst. elimtype False. eapply irreflexivity. etransitivity; [exact H|exact H0].
    elimtype False. eapply irreflexivity. etransitivity; [exact H|].
    eapply transitivity; [exact H1|exact H0].
  Qed.

  Definition to_noprop (l : t) : Level.t :=
    match l with
    | Level s ⇒ Level.Level s
    | Var n ⇒ Level.Var n
    end.

  Definition to_level (l : t) : Level.t := to_noprop l.

  Global Instance Evaluable : Evaluable t
    := fun v l ⇒ match l with
               | Level s ⇒ Pos.to_nat (v.(valuation_mono) s)
               | Var x ⇒ (v.(valuation_poly) x)
               end.
End VariableLevel.

Module VariableLevelOT := OrderedType_from_Alt VariableLevel.

Coercion VariableLevel.to_noprop : VariableLevel.t >-> Level.t.

Module GoodConstraint.
  Inductive t_ :=
  
  | gc_le : VariableLevel.t → Z → VariableLevel.t → t_
  
  | gc_lt_set_level : nat → string → t_
  
  | gc_le_set_var : nat → nat → t_
  
  | gc_le_level_set : string → nat → t_
  
  | gc_le_var_set : nat → nat → t_.
  Derive NoConfusion for t_.
  Definition t : Set := t_.
  Definition eq : t → t → Prop := Logic.eq.
  Definition eq_refl := @eq_refl t.
  Definition eq_sym := @eq_sym t.
  Definition eq_trans := @eq_trans t.

  Definition eq_equiv : RelationClasses.Equivalence eq := _.
  Definition eq_dec : ∀ x y : t, {eq x y} + {¬ eq x y}.
    unfold eq.
    decide equality. all: try apply VariableLevel.eq_dec.
    apply Z.eq_dec. all:apply Classes.eq_dec || apply Peano_dec.eq_nat_dec.
  Defined.

  Reserved Notation "x <c y" (at level 60).

  Definition compare (x : t) (y : t) : comparison :=
    match x, y with
    | gc_le u n v, gc_le u' n' v' ⇒
      compare_cont (VariableLevel.compare u u') (compare_cont (Z.compare n n') (VariableLevel.compare v v'))
    | _, gc_le _ _ _ ⇒ Datatypes.Lt
    | gc_le _ _ _, _ ⇒ Gt
    | gc_lt_set_level n s, gc_lt_set_level n' s' ⇒
      compare_cont (Nat.compare n n') (string_compare s s')
    | _, gc_lt_set_level _ _ ⇒ Datatypes.Lt
    | gc_lt_set_level _ _, _ ⇒ Gt
    | gc_le_set_var n s, gc_le_set_var n' s' ⇒
      compare_cont (Nat.compare n n') (Nat.compare s s')
    | _, gc_le_set_var _ _ ⇒ Datatypes.Lt
    | gc_le_set_var _ _, _ ⇒ Datatypes.Gt
    | gc_le_level_set s n, gc_le_level_set s' n' ⇒
      compare_cont (Nat.compare n n') (string_compare s s')
    | _, gc_le_level_set _ _ ⇒ Datatypes.Lt
    | gc_le_level_set _ _, _ ⇒ Datatypes.Gt
    | gc_le_var_set n k, gc_le_var_set n' k' ⇒
      compare_cont (Nat.compare n n') (Nat.compare k k')
    end.
  Infix "?=" := compare.

  Lemma compare_sym (a b : t):
    compare b a = CompOpp (compare a b).
  Proof.
    revert b. destruct a, b; try easy; cbn;
      rewrite !compare_cont_CompOpp -?VariableLevel.compare_sym ?Zcompare_antisym -?PeanoNat.Nat.compare_antisym
      -?StringOT.compare_sym //.
  Qed.


  Lemma nat_compare_trans : ∀ c (x y z : nat), (x?=y)%nat = c → (y?=z)%nat = c → (x?=z)%nat = c.
  Proof.
    intros c x y z.
    destruct (Nat.compare_spec x y); subst ⇒ // <-;
    destruct (Nat.compare_spec y z); subst ⇒ //;
    destruct (Nat.compare_spec x z); subst ⇒ //; try lia.
  Qed.

  Lemma Z_compare_trans : ∀ c (x y z : Z), (x?=y)%Z = c → (y?=z)%Z = c → (x?=z)%Z = c.
  Proof.
    intros c x y z.
    destruct (Z.compare_spec x y); subst ⇒ // <-;
    destruct (Z.compare_spec y z); subst ⇒ //;
    destruct (Z.compare_spec x z); subst ⇒ //; try lia.
  Qed.

  Lemma nat_compare_eq : ∀ (x y : nat), (x?=y)%nat = Datatypes.Eq → x = y.
  Proof.
    intros x y.
    destruct (Nat.compare_spec x y) ⇒ //.
  Qed.

  Lemma compare_trans : ∀ c (x y z : t), (x?=y) = c → (y?=z) = c → (x?=z) = c.
  Proof.
    intros c x y z.
    destruct x, y, z; cbn; try repeat apply compare_cont_trans; eauto using VariableLevel.compare_trans, VariableLevel.compare_eq;
      try congruence.
    all:eauto using StringOT.compare_trans, nat_compare_trans, nat_compare_eq.
    intros. eapply compare_cont_trans; tea;
      eauto using VariableLevel.compare_trans, VariableLevel.compare_eq, Z.compare_eq, Z_compare_trans.
  Qed.

  Lemma compare_eq (x y : t) : x ?= y = Datatypes.Eq → x = y.
  Proof.
    destruct x, y; cbn ⇒ //.
    destruct (VariableLevel.compare t0 t2) eqn:e ⇒ /= //.
    apply VariableLevel.compare_eq in e. subst. cbn.
    destruct (Z.compare z z0) eqn:e' ⇒ /= //.
    apply Z.compare_eq in e'; subst.
    intros H; apply VariableLevel.compare_eq in H; subst. reflexivity.
    destruct (Nat.compare_spec n n0) ⇒ /= //; subst.
    rewrite StringOT.compare_eq ⇒ → //.
    destruct (Nat.compare_spec n n1) ⇒ /= //; subst.
    destruct (Nat.compare_spec n0 n2) ⇒ /= //; subst ⇒ //.
    destruct (Nat.compare_spec n n0) ⇒ /= //; subst.
    rewrite (StringOT.compare_eq) ⇒ → //.
    destruct (Nat.compare_spec n n1) ⇒ /= //; subst.
    destruct (Nat.compare_spec n0 n2) ⇒ /= //; subst ⇒ //.
  Qed.

  Lemma compare_refl (x : t) : x ?= x = Datatypes.Eq.
  Proof.
    destruct x ⇒ /= //;
    rewrite ?VariableLevel.compare_refl /= ?Z.compare_refl /= ?Nat.compare_refl ?string_compare_eq //.
  Qed.

  Definition lt (x y : t) := (x ?= y = Datatypes.Lt).
  Lemma lt_trans (x y z : t) : lt x y → lt y z → lt x z.
  Proof. apply compare_trans. Qed.
  Lemma lt_not_eq (x y : t) : lt x y → ¬ eq x y.
  Proof.
    intros lt eq. red in eq. subst x.
    red in lt. rewrite compare_refl in lt ⇒ //.
  Qed.

  Lemma lt_strorder : StrictOrder lt.
  Proof.
    split.
    - intros x hlt. apply lt_not_eq in hlt. now apply hlt.
    - red. eapply lt_trans.
  Qed.
  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof.
    intros x y ? ? ? ?. now rewrite H H0.
  Qed.

  Lemma compare_spec : ∀ x y : t, CompSpec eq lt x y (compare x y).
  Proof.
    intros x y.
    destruct (x ?= y) eqn:e; constructor.
    - now eapply compare_eq in e.
    - now red.
    - red. rewrite compare_sym e //.
  Qed.

  Definition satisfies v (gc : GoodConstraint.t) : bool :=
  match gc with
  | gc_le l z l' ⇒ (Z.of_nat (val v l) <=? Z.of_nat (val v l') - z)%Z
  | gc_lt_set_level k l ⇒ k <? Pos.to_nat (v.(valuation_mono) l)
  | gc_le_set_var k l ⇒ k <=? v.(valuation_poly) l
  | gc_le_level_set l k ⇒ Pos.to_nat (v.(valuation_mono) l) <=? k
  | gc_le_var_set l k ⇒ v.(valuation_poly) l <=? k
  end.

End GoodConstraint.

Notation gc_satisfies0 := GoodConstraint.satisfies.

Module GoodConstraintSet := Make GoodConstraint.
Module GoodConstraintSetFact := WFactsOn GoodConstraint GoodConstraintSet.
Module GoodConstraintSetProp := WPropertiesOn GoodConstraint GoodConstraintSet.
Module GoodConstraintSetDecide := WDecide (GoodConstraintSet).
Module GCS := GoodConstraintSet.
Ltac gcsets := GoodConstraintSetDecide.fsetdec.

Definition gcs_equal x y : Prop :=
  LevelSet.Equal x.1 y.1 ∧ GoodConstraintSet.Equal x.2 y.2.

Infix "=_gcs" := gcs_equal (at level 200).
Notation "(=_gcs)" := gcs_equal (at level 0).

Global Instance proper_pair_levels_gcs : Proper ((=_lset) ==> GoodConstraintSet.Equal ==> (=_gcs)) (@pair LevelSet.t GoodConstraintSet.t).
Proof.
  intros l l' eq gcs gcs' eq'.
  split; cbn; auto.
Qed.

Global Instance GCS_For_all_Proper f : Proper (GCS.eq ==> iff) (GCS.For_all f).
Proof.
  move⇒ s s' eq; split; move⇒ h x hx; apply h; by rewrite eq + rewrite <- eq.
Qed.

Definition GoodConstraintSet_pair x y
  := GoodConstraintSet.add y (GoodConstraintSet.singleton x).

Lemma GoodConstraintSet_pair_In x y z
  : GoodConstraintSet.In x (GoodConstraintSet_pair y z)
    → x = y ∨ x = z.
Proof.
  intro H. apply GoodConstraintSetFact.add_iff in H.
  destruct H; [intuition|].
  apply GoodConstraintSetFact.singleton_1 in H. intuition.
Qed.

Lemma GCS_pair_spec x y z :
  GCS.In x (GoodConstraintSet_pair y z) ↔ x = y ∨ x = z.
Proof.
  split; first apply: GoodConstraintSet_pair_In.
  move⇒ [->|->]; apply/GCS.add_spec; by [right; apply/GCS.singleton_spec| left].
Qed.

Definition gc_satisfies v : GoodConstraintSet.t → bool :=
  GoodConstraintSet.for_all (gc_satisfies0 v).

Arguments GoodConstraintSet.for_all : simpl never.

Definition gc_consistent ctrs : Prop := ∃ v, gc_satisfies v ctrs.

Lemma gc_satisfies_pair v gc1 gc2 :
  (gc_satisfies0 v gc1 ∧ gc_satisfies0 v gc2) ↔
  gc_satisfies v (GoodConstraintSet_pair gc1 gc2).
Proof.
  unfold gc_satisfies, GoodConstraintSet_pair.
  rewrite [is_true (GoodConstraintSet.for_all _ _)]GoodConstraintSet.for_all_spec.
  split.
  - intros [sat1 sat2] x.
    rewrite GoodConstraintSet.add_spec. move⇒ [->|] //.
    rewrite GoodConstraintSet.singleton_spec ⇒ → //.
  - intros ha. split; apply ha;
    rewrite GoodConstraintSet.add_spec;
    rewrite GoodConstraintSet.singleton_spec; auto.
Qed.

Section GcOfConstraint.
  Import VariableLevel GoodConstraint.

  Definition gc_of_constraint `{checker_flags} (uc : UnivConstraint.t)
  : option GoodConstraintSet.t
  := let empty := Some GoodConstraintSet.empty in
     let singleton := fun x ⇒ Some (GoodConstraintSet.singleton x) in
     let pair := fun x y ⇒ Some (GoodConstraintSet_pair x y) in
     match uc with
     
     | (Level.lzero, Le z, r) ⇒
      match Z.compare z 0 with
      | Datatypes.Eq ⇒ empty
      | Datatypes.Lt ⇒ empty
      | Datatypes.Gt ⇒
        match r with
        | Level.lzero ⇒ None
        | Level.Level s ⇒ singleton (gc_lt_set_level (Z.to_nat (z - 1)) s)
        | Level.Var n ⇒ singleton (gc_le_set_var (Z.to_nat z) n)
        end
      end
     | (Level.lzero, Eq, Level.lzero) ⇒ empty
     | (Level.lzero, Eq, Level.Level _) ⇒ None
     | (Level.lzero, Eq, Level.Var n) ⇒ singleton (gc_le_var_set n 0%nat)

     
     | (Level.Level l, Le z, Level.lzero) ⇒
       
        if (z <=? 0)%Z then singleton (gc_le_level_set l (Z.to_nat (Z.abs z)))
        else None
     
     | (Level.Level l, Le z, Level.Level l')
       ⇒ singleton (gc_le (Level l) z (Level l'))
     | (Level.Level l, Le z, Level.Var n) ⇒ singleton (gc_le (Level l) z (Var n))
     | (Level.Level _, Eq, Level.lzero) ⇒ None
     | (Level.Level l, Eq, Level.Level l')
       ⇒ pair (gc_le (Level l) 0 (Level l')) (gc_le (Level l') 0 (Level l))
     | (Level.Level l, Eq, Level.Var n)
       ⇒ pair (gc_le (Level l) 0 (Var n)) (gc_le (Var n) 0 (Level l))

     
     | (Level.Var n, Le z, Level.lzero) ⇒
      
      if (z <=? 0)%Z then singleton (gc_le_var_set n (Z.to_nat (Z.abs z)))
      else None

     | (Level.Var n, Le z, Level.Level l) ⇒ singleton (gc_le (Var n) z (Level l))
     | (Level.Var n, Le z, Level.Var n') ⇒ singleton (gc_le (Var n) z (Var n'))
     | (Level.Var n, Eq, Level.lzero) ⇒ singleton (gc_le_var_set n 0)
     | (Level.Var n, Eq, Level.Level l)
       ⇒ pair (gc_le (Var n) 0%Z (Level l)) (gc_le (Level l) 0%Z (Var n))

     | (Level.Var n, Eq, Level.Var n')
       ⇒ pair (gc_le (Var n) 0 (Var n')) (gc_le (Var n') 0 (Var n))
     end.
End GcOfConstraint.

Section GC.

Context `{cf : checker_flags}.

Lemma gc_satisfies_singleton v c :
  gc_satisfies0 v c ↔
  gc_satisfies v (GoodConstraintSet.singleton c).
Proof using Type.
  split.
  - intros H; unfold gc_satisfies.
    eapply GoodConstraintSet.for_all_spec; auto. proper.
    intros x xin. eapply GoodConstraintSet.singleton_spec in xin.
    now subst.
  - unfold gc_satisfies.
    intros gc.
    eapply GoodConstraintSet.for_all_spec in gc; auto. 2:proper.
    specialize (gc c).
    rewrite → GoodConstraintSet.singleton_spec in gc.
    now apply gc.
Qed.

Lemma gc_of_constraint_spec v uc :
  satisfies0 v uc ↔ on_Some (gc_satisfies v) (gc_of_constraint uc).
Proof using Type.
  split.
  - destruct 1; destruct l, l'; try constructor.
    all:unfold gc_of_constraint.
    all: cbn -[GoodConstraintSet_pair] in ×.
    all: cbn -[GoodConstraintSet_pair]; try reflexivity.
    all: rewrite ?if_true_false; repeat toProp ; try lia.
    all: try solve [destruct (Z.compare_spec z 0); simpl; try constructor; lia].
    destruct (Z.compare_spec z 0); simpl; try constructor; try lia.
    apply gc_satisfies_singleton.
    simpl. apply Nat.ltb_lt. lia.
    all:try (destruct (Z.compare_spec z 0); simpl; try constructor; try lia;
    apply gc_satisfies_singleton; simpl; try (apply Nat.ltb_lt||apply Nat.leb_le); lia).
    all:try (destruct (Z.leb_spec z 0); simpl; try constructor; try lia;
      apply gc_satisfies_singleton; simpl; apply Nat.leb_le; lia).
    all: try (apply gc_satisfies_pair; split; cbn; toProp; try lia).
    all: (apply gc_satisfies_singleton; cbn; toProp; lia).
  - destruct uc as [[[] []] []]; intro H; constructor.
    all: cbn -[GoodConstraintSet_pair] in *; try contradiction.
    all: rewrite → ?if_true_false in *; cbn -[GoodConstraintSet_pair] in *;
      try contradiction; repeat toProp; try lia.
    all:try (destruct (Z.compare_spec z 0); simpl in H; auto; try lia;
      apply gc_satisfies_singleton in H; simpl in H;
      (apply Nat.ltb_lt in H || apply Nat.leb_le in H);
      try lia).
    all:try (destruct (Z.leb_spec z 0); simpl in H; auto; try lia;
      apply gc_satisfies_singleton in H; simpl in H;
      (apply Nat.ltb_lt in H || apply Nat.leb_le in H);
      try lia).
    all:(try apply gc_satisfies_singleton in H; cbn in H; try toProp H); try lia.
    all: apply gc_satisfies_pair in H; destruct H as [H1 H2]; cbn in *;
      repeat toProp; try lia.
Qed.

Definition add_gc_of_constraint uc (S : option GoodConstraintSet.t)
  := S1 <- S ;;
     S2 <- gc_of_constraint uc ;;
     ret (GoodConstraintSet.union S1 S2).

Definition gc_of_constraints (ctrs : ConstraintSet.t) : option GoodConstraintSet.t
  := ConstraintSet.fold add_gc_of_constraint
                        ctrs (Some GoodConstraintSet.empty).

Lemma gc_of_constraints_spec v ctrs :
  satisfies v ctrs ↔ on_Some (gc_satisfies v) (gc_of_constraints ctrs).
Proof using Type.
  unfold gc_satisfies, satisfies, ConstraintSet.For_all, gc_of_constraints.
  set (S := GoodConstraintSet.empty).
  rewrite ConstraintSet.fold_spec.
  etransitivity. eapply iff_forall.
  intro; eapply imp_iff_compat_r. eapply ConstraintSetFact.elements_iff.
  set (l := ConstraintSet.elements ctrs). simpl.
  transitivity ((∀ uc, InA Logic.eq uc l → satisfies0 v uc) ∧
                (∀ gc, GoodConstraintSet.In gc S → gc_satisfies0 v gc)). {
    intuition. inversion H0. }
  clearbody S; revert S; induction l; intro S; cbn.
  - split.
    + intro. apply GoodConstraintSetFact.for_all_1.
      intros x y []; reflexivity.
      intro; apply H.
    + intros HS. split. intros ux H; inversion H.
      apply GoodConstraintSetFact.for_all_2.
      intros x y []; reflexivity.
      assumption.
  - split.
    + intros [H1 H2].
      assert (HH : on_Some (gc_satisfies v) (gc_of_constraint a)). {
        apply gc_of_constraint_spec, H1. now constructor. }
      case_eq (gc_of_constraint a); [|intro e; rewrite e in HH; contradiction].
      intros X HX; rewrite HX in HH; cbn in HH.
      apply IHl. split.
      × intros uc H0. apply H1. now apply InA_cons_tl.
      × intros gc H0. apply GoodConstraintSetFact.union_1 in H0.
        induction H0. intuition.
        apply GoodConstraintSetFact.for_all_2 in HH.
        apply HH. assumption.
        intros x y []; reflexivity.
    + intros HH.
      case_eq (gc_of_constraint a).
      × intros X HX; rewrite HX in HH; cbn in HH.
        destruct (proj2 (IHl _) HH) as [IH1 IH2]. clear IHl HH.
        split. intuition. apply InA_cons in H. induction H.
        subst. apply gc_of_constraint_spec. rewrite HX.
        cbn. apply GoodConstraintSetFact.for_all_1.
        intros x y []; reflexivity.
        intros gc Hgc. apply IH2.
        now apply GoodConstraintSetFact.union_3.
        firstorder.
        intros gc Hgc. apply IH2.
        now apply GoodConstraintSetFact.union_2.
      × intro HX; rewrite HX in HH. apply False_rect. revert HH; clear.
        induction l. inversion 1.
        assumption.
Qed.

Lemma gc_consistent_iff ctrs :
  consistent ctrs ↔ on_Some gc_consistent (gc_of_constraints ctrs).
Proof using Type.
  split.
  - intros [v H]. apply gc_of_constraints_spec in H.
    destruct (gc_of_constraints ctrs); cbn in ×.
    ∃ v. assumption. contradiction.
  - case_eq (gc_of_constraints ctrs); cbn; [|contradiction].
    intros ctrs' e HC. destruct HC as [v Hv].
    ∃ v. apply gc_of_constraints_spec. now rewrite e; cbn.
Qed.

Local Open Scope univ_scope.

Definition gc_leq0_levelalg_n n ctrs (u u' : LevelAlgExpr.t) :=
  ∀ v, gc_satisfies v ctrs → (Z.of_nat (val v u) ≤ Z.of_nat (val v u') - n)%Z.

Definition gc_leq_levelalg_n n ctrs (u u' : LevelAlgExpr.t) :=
  if check_univs then gc_leq0_levelalg_n n ctrs u u' else True.

Definition gc_eq0_levelalg φ (u u' : LevelAlgExpr.t) :=
  ∀ v, gc_satisfies v φ → val v u = val v u'.

Definition gc_eq_levelalg φ (u u' : LevelAlgExpr.t) :=
  if check_univs then gc_eq0_levelalg φ u u' else True.

Definition gc_leq0_levelalg := gc_leq0_levelalg_n 0.
Definition gc_lt0_levelalg := gc_leq0_levelalg_n 1.
Definition gc_leq_levelalg := gc_leq_levelalg_n 0.
Definition gc_lt_levelalg := gc_leq_levelalg_n 1.

Ltac unfold_univ_rel0 :=
  unfold eq0_levelalg, leq0_levelalg_n,
  gc_eq0_levelalg, gc_leq0_levelalg, gc_lt0_levelalg, gc_leq0_levelalg_n in *;
  intros v Hv; cbnr.

Ltac unfold_univ_rel :=
  unfold eq_levelalg, leq_levelalg, lt_levelalg, leq_levelalg_n,
  gc_eq_levelalg, gc_leq_levelalg, gc_lt_levelalg, gc_leq_levelalg_n in *;
  destruct check_univs; [| trivial].

Lemma gc_leq0_levelalg_n_iff (n: Z) ctrs u u' :
  leq0_levelalg_n n ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_leq0_levelalg_n n ctrs u u')
                    (gc_of_constraints ctrs).
Proof.
  split.
  - intro H. case_eq (gc_of_constraints ctrs).
    + intros ctrs' e. cbn.
      unfold_univ_rel0.
      apply H. apply gc_of_constraints_spec.
      rewrite e. assumption.
    + intro; exact I.
  - case_eq (gc_of_constraints ctrs); cbn.
    + intros ctrs' e H.
      unfold_univ_rel0. apply H.
      apply gc_of_constraints_spec in Hv.
      rewrite e in Hv; assumption.
    + intros e _. unfold_univ_rel0.
      apply gc_of_constraints_spec in Hv.
      rewrite e in Hv; contradiction.
Defined.

Lemma gc_leq0_levelalg_iff ctrs u u':
  leq0_levelalg_n 0 ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_leq0_levelalg_n 0 ctrs u u')
                      (gc_of_constraints ctrs).
Proof using Type.
  apply gc_leq0_levelalg_n_iff.
Qed.

Lemma gc_eq0_levelalg_iff ctrs u u' :
  eq0_levelalg ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_eq0_levelalg ctrs u u')
                      (gc_of_constraints ctrs).
Proof.
  split.
  - intro H. case_eq (gc_of_constraints ctrs).
    + intros ctrs' e. cbn.
      unfold_univ_rel0. apply H. apply gc_of_constraints_spec.
      rewrite e. assumption.
    + intro; exact I.
  - case_eq (gc_of_constraints ctrs); cbn.
    + intros ctrs' e H.
      unfold_univ_rel0. apply H.
      apply gc_of_constraints_spec in Hv.
      rewrite e in Hv; assumption.
    + intros e _. unfold_univ_rel0.
      apply gc_of_constraints_spec in Hv.
      rewrite e in Hv; contradiction.
Defined.

Lemma gc_leq_levelalg_n_iff n ctrs u u' :
  leq_levelalg_n n ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_leq_levelalg_n n ctrs u u')
                    (gc_of_constraints ctrs).
Proof using Type.
  unfold_univ_rel.
  apply gc_leq0_levelalg_n_iff.
  destruct (gc_of_constraints ctrs); reflexivity.
Qed.

Lemma gc_leq_levelalg_iff ctrs u u' :
  leq_levelalg ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_leq_levelalg ctrs u u')
                    (gc_of_constraints ctrs).
Proof using Type.
  unfold_univ_rel.
  apply gc_leq0_levelalg_iff.
  destruct (gc_of_constraints ctrs); reflexivity.
Qed.

Lemma gc_eq_levelalg_iff ctrs u u' :
  eq_levelalg ctrs u u'
  ↔ on_Some_or_None (fun ctrs ⇒ gc_eq_levelalg ctrs u u')
                    (gc_of_constraints ctrs).
Proof using Type.
  unfold_univ_rel.
  apply gc_eq0_levelalg_iff.
  destruct (gc_of_constraints ctrs); reflexivity.
Qed.

End GC.

Module Import wGraph := WeightedGraph Level LevelSet.
Module VSet := LevelSet.
Local Notation lzero := Level.lzero.
Local Notation vtn := VariableLevel.to_noprop.

Definition universes_graph := t.
Definition init_graph : universes_graph
  := (VSet.singleton lzero, EdgeSet.empty, lzero).

Lemma init_graph_invariants : invariants init_graph.
Proof.
  repeat split; cbn in ×.
  1-2: inversion H. sets.
  apply VSet.singleton_spec in H. subst.
  ∃ (pathOf_refl _ _). simpl. sq. lia.
Defined.

Definition declared : Level.t → LevelSet.t → Prop := LevelSet.In.

Definition uctx_invariants (uctx : ContextSet.t)
  := ConstraintSet.For_all (declared_cstr_levels uctx.1) uctx.2.

Definition global_uctx_invariants (uctx : ContextSet.t)
  := LevelSet.In Level.lzero uctx.1 ∧ uctx_invariants uctx.

Definition global_gc_uctx_invariants (uctx : VSet.t × GoodConstraintSet.t)
  := VSet.In lzero uctx.1 ∧ GoodConstraintSet.For_all (fun gc ⇒ match gc with
                 | GoodConstraint.gc_le l z l' ⇒ VSet.In (vtn l) uctx.1
                                 ∧ VSet.In (vtn l') uctx.1
                 | GoodConstraint.gc_lt_set_level _ n
                 | GoodConstraint.gc_le_level_set n _ ⇒ VSet.In (Level.Level n) uctx.1
                 | GoodConstraint.gc_le_var_set n _
                 | GoodConstraint.gc_le_set_var _ n ⇒ VSet.In (Level.Var n) uctx.1
                 end) uctx.2.

Definition gc_of_uctx `{checker_flags} (uctx : ContextSet.t)
  : option (VSet.t × GoodConstraintSet.t)
  := ctrs <- gc_of_constraints uctx.2 ;;
     ret (uctx.1, ctrs).

Lemma gc_of_uctx_of_constraints `{checker_flags} uctx gctx :
  gc_of_uctx uctx = Some gctx →
  gc_of_constraints uctx.2 = Some gctx.2.
Proof.
  rewrite/gc_of_uctx; case: (gc_of_constraints _)=> //= ? [=] <- //.
Qed.

Lemma gc_of_constraints_of_uctx `{checker_flags} uctx gcstrs :
  gc_of_constraints uctx.2 = Some gcstrs →
  gc_of_uctx uctx = Some (uctx.1, gcstrs).
Proof. rewrite /gc_of_uctx⇒ → //=. Qed.

Lemma gc_of_constraint_iff `{cf:checker_flags} ctrs0 ctrs gc
      (HH : gc_of_constraints ctrs0 = Some ctrs)
: GoodConstraintSet.In gc ctrs
  ↔ ConstraintSet.Exists
      (fun e ⇒ on_Some (GoodConstraintSet.In gc) (gc_of_constraint e)) ctrs0.
Proof.
  unfold gc_of_constraints in HH. rewrite ConstraintSet.fold_spec in HH.
  transitivity ((∃ ctr, In ctr (ConstraintSet.elements ctrs0) ∧
                        on_Some (GoodConstraintSet.In gc) (gc_of_constraint ctr))
                ∨ GoodConstraintSet.In gc GoodConstraintSet.empty).
  2:{ split.
      - intros [[ctr [H1 H2]]|H]. ∃ ctr. split.
        apply ConstraintSetFact.elements_iff, InA_In_eq; tas. tas.
        now apply GoodConstraintSetFact.empty_iff in H.
      - intros [ctr H]. left. ∃ ctr. split.
        apply InA_In_eq, ConstraintSetFact.elements_1, H. apply H. }
  revert HH; generalize GoodConstraintSet.empty.
  induction (ConstraintSet.elements ctrs0).
  - cbn. intros X HH. apply some_inj in HH; subst.
    firstorder.
  - intros X HH. simpl in HH. unfold add_gc_of_constraint at 2 in HH.
    simpl in HH. case_eq (gc_of_constraint a).
    + intros Y HY. rewrite HY in HH.
      apply IHl in HH.
      etransitivity. exact HH. etransitivity.
      apply or_iff_compat_l. apply GoodConstraintSet.union_spec.
      split.
      × intros [[ctr H]|[H|H]]. left. ∃ ctr. intuition. intuition.
        left. ∃ a. intuition. rewrite HY; tas.
      × intros [[ctr [[H1|H1] H2]]|H]. subst a. right. right.
        rewrite HY in H2; tas.
        left. ∃ ctr. intuition.
        right. left; tas.
    + intro eq; rewrite eq in HH; simpl in HH.
      apply False_rect. clear -HH. induction l.
      × discriminate HH.
      × simpl in HH. apply IHl.
        apply HH.
Qed.

Lemma gc_of_uctx_invariants `{cf:checker_flags} uctx uctx'
      (H : gc_of_uctx uctx = Some uctx')
  : global_uctx_invariants uctx → global_gc_uctx_invariants uctx'.
Proof.
  intros [Hi0 Hi].
  unfold gc_of_uctx in H.
  case_eq (gc_of_constraints uctx.2); [|intro eq; rewrite eq in H; discriminate].
  intros ctrs eq; rewrite eq in H; apply some_inj in H. subst uctx'.
  split; simpl.
  - apply Hi0.
  - red in Hi.
    destruct uctx as [levels ctrs0]; cbn in ×.
    intros gc Hgc.
    eapply gc_of_constraint_iff in Hgc; tea.
    destruct Hgc as [e [He HH]].
    specialize (Hi e He); cbn in Hi.
    clear -Hi HH.
    destruct e as [[l ct] l']; simpl in Hi.
    destruct l, ct, l'; cbn in HH; destruct prop_sub_type; cbn in HH.
    change VSet.In with LevelSet.In.
    all:repeat match goal with
         | HH : context [ (?z ?= 0)%Z ] |- _ ⇒
          destruct (Z.compare_spec z 0); simpl in HH; auto
          | HH : context [ (?z <=? 0)%Z ] |- _ ⇒
          destruct (Z.leb_spec z 0); simpl in HH; auto
         | HH : False |- _ ⇒ contradiction HH
         | HH : GoodConstraintSet.In ?A GoodConstraintSet.empty |- _
           ⇒ apply GoodConstraintSetFact.empty_iff in HH; contradiction HH
         | HH : GoodConstraintSet.In ?A (GoodConstraintSet.singleton ?B) |- _
           ⇒ apply GoodConstraintSetFact.singleton_1 in HH; subst gc
         | HH : GoodConstraintSet.In ?A (GoodConstraintSet_pair ?B _) |- _
           ⇒ apply GoodConstraintSet_pair_In in HH; destruct HH as [HH|HH]; subst gc
         end.
    all: try split; try apply Hi;
      try apply Hi.
Qed.

Definition edge_of_level (l : VariableLevel.t) : EdgeSet.elt :=
  match l with
  | VariableLevel.Level l ⇒ (lzero, 1%Z, Level.Level l)
  | VariableLevel.Var n ⇒ (lzero, 0%Z, Level.Var n)
  end.

Definition EdgeSet_pair x y
  := EdgeSet.add y (EdgeSet.singleton x).
Definition EdgeSet_triple x y z
  := EdgeSet.add z (EdgeSet_pair x y).

Definition edge_of_constraint (gc : GoodConstraint.t) : EdgeSet.elt :=
  match gc with
  | GoodConstraint.gc_le l z l' ⇒ (vtn l, z, vtn l')
  | GoodConstraint.gc_lt_set_level k s ⇒ (lzero, Z.of_nat (S k), vtn (VariableLevel.Level s))
  | GoodConstraint.gc_le_set_var k n ⇒ (lzero, Z.of_nat k, vtn (VariableLevel.Var n))
  | GoodConstraint.gc_le_level_set s k ⇒ (vtn (VariableLevel.Level s), (- Z.of_nat k)%Z, lzero)
  | GoodConstraint.gc_le_var_set n k ⇒ (vtn (VariableLevel.Var n), (- Z.of_nat k)%Z, lzero)
  end.

Lemma source_edge_of_level g : (edge_of_level g)..s = lzero.
Proof.
  destruct g; reflexivity.
Qed.

Lemma target_edge_of_level g : (edge_of_level g)..t = vtn g.
Proof.
  destruct g; reflexivity.
Qed.

Definition variable_of_level (l : Level.t) : option VariableLevel.t
  := match l with
      | Level.lzero ⇒ None
      | Level.Level s ⇒ Some (VariableLevel.Level s)
      | Level.Var n ⇒ Some (VariableLevel.Var n)
      end.

Definition option_edge_of_level l : option EdgeSet.elt :=
  match variable_of_level l with
  | None ⇒ None
  | Some ll ⇒ Some (edge_of_level ll)
  end.

Definition add_level_edges :=
  VSet.fold
  (fun l E ⇒
      match variable_of_level l with
      | None ⇒ E
      | Some ll ⇒ EdgeSet.add (edge_of_level ll) E
      end).

Definition add_cstrs ctrs :=
  GoodConstraintSet.fold (fun ctr ⇒ EdgeSet.add (edge_of_constraint ctr)) ctrs.

Lemma add_cstrs_spec e x g :
  EdgeSet.In e (add_cstrs x g) ↔
  (∃ c, edge_of_constraint c = e ∧ GoodConstraintSet.In c x) ∨ EdgeSet.In e g.
Proof.
  rewrite /add_cstrs GoodConstraintSet.fold_spec.
  transitivity
    ((∃ c, edge_of_constraint c = e ∧ In c (GoodConstraintSet.elements x)) ∨ EdgeSet.In e g).
  - induction (GoodConstraintSet.elements x) in g |- *; simpl.
    intuition auto. now destruct H0 as [c [_ F]].
    rewrite IHl.
    rewrite EdgeSet.add_spec.
    split.
    × intros [[c [eq inl]]|?].
      subst e. firstorder auto.
      destruct H as [->|ing]; [left|right]; auto.
      ∃ a; firstorder auto.
    × intros [[c [eq [->|inl]]]|?]; auto.
      left; ∃ c; auto.
  - setoid_rewrite (GoodConstraintSetFact.elements_iff x).
    now setoid_rewrite InA_In_eq.
Qed.

#[global] Instance add_cstrs_proper : Proper (Logic.eq ==> EdgeSet.Equal ==> EdgeSet.Equal)%signature add_cstrs.
Proof.
  intros s s' eq x y H.
  intros e.
  rewrite /add_cstrs.
  rewrite !GoodConstraintSet.fold_spec. subst s'.
  induction (GoodConstraintSet.elements s) in x, y, H, e |- *; cbn; auto.
  apply IHl. now rewrite H.
Qed.

#[global] Instance add_cstrs_proper' : Proper (GoodConstraintSet.Equal ==> EdgeSet.Equal ==> EdgeSet.Equal)%signature add_cstrs.
Proof.
  intros s s' eq x y H.
  red in H. intros e.
  rewrite !add_cstrs_spec.
  rewrite H. firstorder auto.
Qed.

Definition make_graph (uctx : VSet.t × GoodConstraintSet.t) : t :=
  let init_edges := add_level_edges uctx.1 EdgeSet.empty in
  let edges := add_cstrs uctx.2 init_edges in
  (uctx.1, edges, lzero).

Lemma make_graph_E uctx e
  : EdgeSet.In e (wGraph.E (make_graph uctx))
    ↔ (∃ l, VSet.In (vtn l) uctx.1 ∧ e = edge_of_level l)
      ∨ (GoodConstraintSet.Exists (fun gc ⇒ e = edge_of_constraint gc) uctx.2).
Proof.
  unfold make_graph. unfold wGraph.E.
  simpl.
  assert (XX: ∀ E, EdgeSet.In e (GoodConstraintSet.fold
                           (fun ctr ⇒ EdgeSet.add (edge_of_constraint ctr)) uctx.2 E)
          ↔ (∃ gc, In gc (GoodConstraintSet.elements uctx.2) ∧ e = edge_of_constraint gc)
             ∨ EdgeSet.In e E). {
    intro E. rewrite GoodConstraintSet.fold_spec.
    induction (GoodConstraintSet.elements uctx.2) in E |- ×.
    - cbn. firstorder.
    - simpl. etransitivity. apply IHl. clear IHl. split.
      + intros [[gc H]|H]. left. ∃ gc. intuition.
        apply EdgeSet.add_spec in H. destruct H as [H|H].
        left. ∃ a. intuition. right; tas.
      + intros [[gc [[H1|H1] H2]]|H].
        right. apply EdgeSet.add_spec. left; now subst.
        left. ∃ gc. split; tas.
        right. apply EdgeSet.add_spec. right; tas. }
  etransitivity. apply XX. clear XX.
  etransitivity. apply or_comm.
  etransitivity. apply or_iff_compat_l.
  2: apply or_iff_compat_r.
  - apply iff_ex; intro gc. apply and_iff_compat_r.
    symmetry. etransitivity.
    apply GoodConstraintSetFact.elements_iff. apply InA_In_eq.
  - transitivity ((∃ l, In (vtn l) (VSet.elements uctx.1) ∧ e = edge_of_level l)
                  ∨ EdgeSet.In e EdgeSet.empty).
    2:{ split. intros [[l [H1 H2]]|H]. ∃ l. split; tas.
        apply InA_In_eq, VSetFact.elements_iff in H1; tas.
        now apply EdgeSetFact.empty_iff in H.
        intros [l [H1 H2]]. left. ∃ l. split.
        apply InA_In_eq, VSetFact.elements_1; tas. tas. }
    unfold add_level_edges; rewrite VSet.fold_spec. generalize EdgeSet.empty.
    induction (VSet.elements uctx.1).
    + cbn. intro E; firstorder.
    + intro E. etransitivity. apply IHl. split.
      × intro HH.
        destruct HH as [[l' Hl]|HH]. left. ∃ l'. intuition.
        destruct a as [|l'|l']. right; tas.
        all: apply EdgeSet.add_spec in HH; destruct HH;
          [left|right; tas].
        ∃ (VariableLevel.Level l'); intuition. ∃ (VariableLevel.Var l'); intuition.
      × intros [[l' [[H1|H1] H2]]|H].
        right. subst a. destruct l'; apply EdgeSet.add_spec; left; tas.
        destruct l'; left; [∃ (VariableLevel.Level t0)|∃ (VariableLevel.Var n)]; intuition.
        right. destruct a; tas; apply EdgeSet.add_spec; right; tas.
Qed.

Global Instance make_graph_invariants uctx (Hi : global_gc_uctx_invariants uctx)
  : invariants (make_graph uctx).
Proof.
  split.
  - intros e He. apply make_graph_E in He.
    destruct He as [[l [Hl He]]|[gc [Hgc He]]].
    + subst e. split. rewrite source_edge_of_level. apply Hi.
      rewrite target_edge_of_level; tas.
    + subst e. split. destruct gc; try apply (Hi.p2 _ Hgc). apply Hi.
      simpl. apply Hi.
      destruct gc; try apply (Hi.p2 _ Hgc). apply Hi.
      simpl. apply Hi.
  - apply Hi.
  - cbn. intros l Hl. sq. destruct l as [|s|n].
    ∃ (pathOf_refl _ _). sq. simpl. reflexivity.
    assert (He: EdgeSet.In (edge_of_level (VariableLevel.Level s)) (wGraph.E (make_graph uctx))). {
      apply make_graph_E. left. ∃ (VariableLevel.Level s). intuition. }
    unshelve eexists _.
    econstructor. 2: constructor.
    eexists; exact He. simpl. sq; lia.
    assert (He: EdgeSet.In (edge_of_level (VariableLevel.Var n)) (wGraph.E (make_graph uctx))). {
      apply make_graph_E. left. ∃ (VariableLevel.Var n). intuition. }
    unshelve eexists _.
    econstructor. 2: constructor.
    eexists; exact He. simpl. sq; auto. lia.
Qed.

Ltac sets_iff :=
  match goal with
  | |- (_ ∧ _) ↔ _
     ⇒ eapply and_iff_compat_l; sets_iff
  | |- (_ ∧ _) ↔ _
     ⇒ eapply and_iff_compat_l; sets_iff
  | |- (_ ∨ _) ↔ _
     ⇒ eapply or_iff_compat_l; sets_iff
  | |- (_ ∨ _) ↔ _
     ⇒ eapply or_iff_compat_l; sets_iff
  | |- VSet.In _ (VSet.add _ _) ↔ _
     ⇒ etransitivity; [eapply VSet.add_spec|sets_iff]
  | |- EdgeSet.In _ (EdgeSet.add _ _) ↔ _
     ⇒ etransitivity; [eapply EdgeSet.add_spec|sets_iff]
  | |- VSet.In _ (VSet.singleton _) ↔ _
     ⇒ etransitivity; [eapply VSet.singleton_spec|sets_iff]
  | |- EdgeSet.In _ (EdgeSet.singleton _) ↔ _
     ⇒ etransitivity; [eapply EdgeSet.singleton_spec|sets_iff]
  | _ ⇒ reflexivity
  end.

Ltac simplify_sets :=
  repeat match goal with
  | |- VSet.In ?A (VSet.add ?B ?C)
    ⇒ let X := fresh in
      simple refine (let X : VSet.In A (VSet.add B C) ↔ _ := _ in _);
      [|sets_iff|apply (proj2 X); clear X]
  | |- EdgeSet.In ?A (EdgeSet.add ?B ?C)
    ⇒ let X := fresh in
      simple refine (let X : EdgeSet.In A (EdgeSet.add B C) ↔ _ := _ in _);
      [|sets_iff|apply (proj2 X); clear X]
  | H : VSet.In ?A (VSet.add ?B ?C) |- _
    ⇒ let X := fresh in
      simple refine (let X : VSet.In A (VSet.add B C) ↔ _ := _ in _);
      [|sets_iff|apply (proj1 X) in H; clear X]
  | H : EdgeSet.In ?A (EdgeSet.add ?B ?C) |- _
    ⇒ let X := fresh in
      simple refine (let X : EdgeSet.In A (EdgeSet.add B C) ↔ _ := _ in _);
      [|sets_iff|apply (proj1 X) in H; clear X]
  | H : VSet.In ?A (VSet.singleton ?B) |- _
    ⇒ let X := fresh in
      simple refine (let X : VSet.In A (VSet.singleton B) ↔ _ := _ in _);
      [|sets_iff|apply (proj1 X) in H; clear X]
  | H : EdgeSet.In ?A (EdgeSet.singleton ?B) |- _
    ⇒ let X := fresh in
      simple refine (let X : EdgeSet.In A (EdgeSet.singleton B) ↔ _ := _ in _);
      [|sets_iff|apply (proj1 X) in H; clear X]
  | H : EdgeSet.In ?A EdgeSet.empty |- _
    ⇒ apply EdgeSetFact.empty_iff in H; contradiction
  end.

Definition labelling_of_valuation (v : valuation) : labelling
  := fun x ⇒ match x with
           | lzero ⇒ 0
           | Level.Level l ⇒ Pos.to_nat (v.(valuation_mono) l)
           | Level.Var n ⇒ (v.(valuation_poly) n)
           end.

Definition valuation_of_labelling (l : labelling) : valuation
  := {| valuation_mono := fun s ⇒ Pos.of_nat (l (vtn (VariableLevel.Level s)));
        valuation_poly := fun n ⇒ l (vtn (VariableLevel.Var n)) |}.

Section MakeGraph.
  Context uctx (Huctx : global_gc_uctx_invariants uctx).
  Let ctrs := uctx.2.
  Let G : universes_graph := make_graph uctx.

  Lemma valuation_labelling_eq l (Hl : correct_labelling G l)
    : ∀ x, VSet.In x uctx.1
           → labelling_of_valuation (valuation_of_labelling l) x = l x.
  Proof using Type.
    destruct x as [|s|n]; cbnr.
    - intros _. now apply proj1 in Hl; cbn in Hl.
    - intro Hs. apply Nat2Pos.id.
      assert (HH: EdgeSet.In (lzero, Z.of_nat 1, vtn (VariableLevel.Level s)) (wGraph.E G)). {
        subst G. apply make_graph_E. left.
        ∃ (VariableLevel.Level s). intuition. }
      apply (proj2 Hl) in HH; cbn in HH. lia.
  Qed.

  Lemma make_graph_spec v :
    gc_satisfies v uctx.2 ↔ correct_labelling G (labelling_of_valuation v).
  Proof using Type.
    unfold gc_satisfies, correct_labelling. split; intro H.
    - split. reflexivity.
      intros e He. cbn in He.
      apply make_graph_E in He.
      destruct He as [[l [Hl He]]|[ctr [Hc He]]]; cbn.
      + subst e; cbn. destruct l; cbn; lia.
      + subst e.
        apply GoodConstraintSet.for_all_spec in H.
        2: intros x y []; reflexivity.
        specialize (H _ Hc). cbn in ×.
        destruct ctr as [[] z []|[] []| |n|n]; cbn in *; toProp H; try lia.
        all:try destruct t0; cbn in *; try lia.
    - apply GoodConstraintSet.for_all_spec.
      intros x y []; reflexivity.
      intros gc Hgc.
      pose proof (XX := proj2 (make_graph_E uctx (edge_of_constraint gc))).
      forward XX. { right. now ∃ gc. }
      specialize (H.p2 _ XX).
      destruct gc as [[] z []|k ?| |n|n]; intro HH; cbn in *; toProp; try lia.
  Qed.

  Corollary make_graph_spec' l :
    
    correct_labelling G l → gc_satisfies (valuation_of_labelling l) uctx.2.
  Proof using Huctx.
    intro H. apply (make_graph_spec (valuation_of_labelling l)).
    unfold correct_labelling. intuition.
    rewrite !valuation_labelling_eq; tas. 3:now apply H.
    all: now apply make_graph_invariants.
  Qed.

  Corollary make_graph_spec2 :
    gc_consistent uctx.2 ↔ ∃ l, correct_labelling G l.
  Proof.
    split.
    - intros [v H]. ∃ (labelling_of_valuation v).
      apply make_graph_spec. assumption.
    - intros [l Hl]. ∃ (valuation_of_labelling l).
      apply make_graph_spec'. assumption.
  Defined.

  Global Instance consistent_no_loop : gc_consistent ctrs → acyclic_no_loop G.
  Proof.
    intro. apply acyclic_caract1, make_graph_spec2.
    now apply make_graph_invariants. assumption.
  Defined.
End MakeGraph.

Existing Class gc_consistent.
Existing Class global_gc_uctx_invariants.
Existing Class global_uctx_invariants.
Global Existing Instance gc_of_uctx_invariants.