From Coq Require Import MSetList MSetAVL MSetFacts MSetProperties MSetDecide.
From Equations Require Import Equations.
From MetaCoq.Template Require Import utils BasicAst config.
Require Import ssreflect.

Local Open Scope nat_scope.
Local Open Scope string_scope2.

Implicit Types (cf : checker_flags).

Ltac absurd :=
  match goal with
  | [H: ¬ True |- _] ⇒ elim (H I)
  | [H : False |- _] ⇒ elim H
  | H: is_true false |- _ ⇒ discriminate H
  | |- False → _ ⇒ let H := fresh in intro H; elim H
  | |- _ → False → _ ⇒ let H := fresh in intros ? H; elim H
  | |- is_true false → _ ⇒ let H := fresh in intro H; discriminate H
  | |- _ → is_true false → _ ⇒ let H := fresh in intros ? H; discriminate H
  end.
#[global]
Hint Extern 10 ⇒ absurd : core.

Record valuation :=
  { valuation_mono : string → positive ;
    valuation_poly : nat → nat }.

Class Evaluable (A : Type) := val : valuation → A → nat.

Module Level.
  Inductive t_ : Set :=
  | lzero
  | Level (_ : string)
  | Var (_ : nat) .
  Derive NoConfusion for t_.

  Definition t := t_.

  Definition is_set (x : t) :=
    match x with
    | lzero ⇒ true
    | _ ⇒ false
    end.

  Definition is_var (l : t) :=
    match l with
    | Var _ ⇒ true
    | _ ⇒ false
    end.

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

  Definition compare (l1 l2 : t) : comparison :=
    match l1, l2 with
    | lzero, lzero ⇒ Eq
    | lzero, _ ⇒ Lt
    | _, lzero ⇒ Gt
    | Level s1, Level s2 ⇒ string_compare s1 s2
    | Level _, _ ⇒ Lt
    | _, Level _ ⇒ Gt
    | Var n, Var m ⇒ Nat.compare n m
    end.

  Definition eq : t → t → Prop := eq.
  Definition eq_equiv : Equivalence eq := _.

  Inductive lt_ : t → t → Prop :=
  | ltSetLevel s : lt_ lzero (Level s)
  | ltSetVar n : lt_ lzero (Var n)
  | ltLevelLevel s s' : StringOT.lt s s' → lt_ (Level s) (Level s')
  | ltLevelVar s n : lt_ (Level s) (Var n)
  | ltVarVar n n' : Nat.lt n n' → lt_ (Var n) (Var n').
  Derive Signature for lt_.

  Definition lt := lt_.

  Definition lt_strorder : StrictOrder lt.
  Proof.
    constructor.
    - intros [| |] X; inversion X.
      now eapply irreflexivity in H1.
      eapply Nat.lt_irrefl; tea.
    - intros [| |] [| |] [| |] X1 X2;
        inversion X1; inversion X2; constructor.
      now transitivity s0.
      etransitivity; tea.
  Qed.

  Definition lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof.
    intros x y e z t e'. unfold eq in *; subst. reflexivity.
  Qed.

  Definition compare_spec :
    ∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
  Proof.
    intros [] []; repeat constructor.
    - eapply CompareSpec_Proper.
      5: eapply CompareSpec_string. 4: reflexivity.
      all: split; [now inversion 1|]. now intros →.
      all: intro; now constructor.
    - eapply CompareSpec_Proper.
      5: eapply Nat.compare_spec. 4: reflexivity.
      all: split; [now inversion 1|]. now intros →.
      all: intro; now constructor.
  Qed.

  Definition eqb (l1 l2 : Level.t) : bool
    := match compare l1 l2 with Eq ⇒ true | _ ⇒ false end.

  Global Instance eqb_refl : Reflexive eqb.
  Proof.
    intros []; unfold eqb; cbnr.
    - rewrite (ssreflect.iffRL (string_compare_eq _ _)). all: auto. reflexivity.
    - rewrite Nat.compare_refl. reflexivity.
  Qed.

  Lemma eqb_spec l l' : reflect (eq l l') (eqb l l').
  Proof.
    destruct l, l'; cbn; try constructor; try reflexivity; try discriminate.
    - apply iff_reflect. unfold eqb; cbn.
      destruct (CompareSpec_string t0 t1); split; intro HH;
        try reflexivity; try discriminate; try congruence.
      all: inversion HH; subst; now apply irreflexivity in H.
    - apply iff_reflect. unfold eqb; cbn.
      destruct (Nat.compare_spec n n0); split; intro HH;
        try reflexivity; try discriminate; try congruence.
      all: inversion HH; subst; now apply Nat.lt_irrefl in H.
  Qed.

  Definition eq_level l1 l2 :=
    match l1, l2 with
    | Level.lzero, Level.lzero ⇒ true
    | Level.Level s1, Level.Level s2 ⇒ ReflectEq.eqb s1 s2
    | Level.Var n1, Level.Var n2 ⇒ ReflectEq.eqb n1 n2
    | _, _ ⇒ false
    end.

  #[global, program] Instance reflect_level : ReflectEq Level.t := {
    eqb := eq_level
  }.
  Next Obligation.
    destruct x, y.
    all: unfold eq_level.
    all: try solve [ constructor ; reflexivity ].
    all: try solve [ constructor ; discriminate ].
    - destruct (ReflectEq.eqb_spec t0 t1) ; nodec.
      constructor. f_equal. assumption.
    - destruct (ReflectEq.eqb_spec n n0) ; nodec.
      constructor. subst. reflexivity.
  Defined.

  Definition eq_leibniz (x y : t) : eq x y → x = y := id.

  Definition eq_dec : ∀ (l1 l2 : t), {l1 = l2}+{l1 ≠ l2} := Classes.eq_dec.

End Level.

Module LevelSet := MSetAVL.Make Level.
Module LevelSetFact := WFactsOn Level LevelSet.
Module LevelSetProp := WPropertiesOn Level LevelSet.
Module LevelSetDecide := WDecide (LevelSet).
Module LS := LevelSet.

Ltac lsets := LevelSetDecide.fsetdec.
Notation "(=_lset)" := LevelSet.Equal (at level 0).
Infix "=_lset" := LevelSet.Equal (at level 30).

Section LevelSetMoreFacts.

  Definition LevelSet_pair x y
    := LevelSet.add y (LevelSet.singleton x).

  Lemma LevelSet_pair_In x y z :
    LevelSet.In x (LevelSet_pair y z) → x = y ∨ x = z.
  Proof.
    intro H. apply LevelSetFact.add_iff in H.
    destruct H; [intuition|].
    apply LevelSetFact.singleton_1 in H; intuition.
  Qed.

  Definition LevelSet_mem_union (s s' : LevelSet.t) x :
    LevelSet.mem x (LevelSet.union s s') ↔ LevelSet.mem x s ∨ LevelSet.mem x s'.
  Proof.
    rewrite LevelSetFact.union_b.
    apply orb_true_iff.
  Qed.

  Lemma LevelSet_In_fold_right_add x l :
    In x l ↔ LevelSet.In x (fold_right LevelSet.add LevelSet.empty l).
  Proof.
    split.
    - induction l; simpl ⇒ //.
      intros [<-|H].
      × eapply LevelSet.add_spec; left; auto.
      × eapply LevelSet.add_spec; right; auto.
    - induction l; simpl ⇒ //.
      × now rewrite LevelSetFact.empty_iff.
      × rewrite LevelSet.add_spec. intuition auto.
  Qed.

  Lemma LevelSet_union_empty s : LevelSet.Equal (LevelSet.union LevelSet.empty s) s.
  Proof.
    intros x; rewrite LevelSet.union_spec. lsets.
  Qed.
End LevelSetMoreFacts.

Module PropLevel.

  Inductive t := lSProp | lProp.
  Derive NoConfusion EqDec for t.

  Definition compare (l1 l2 : t) : comparison :=
    match l1, l2 with
    | lSProp, lSProp ⇒ Eq
    | lProp, lProp ⇒ Eq
    | lProp, lSProp ⇒ Gt
    | lSProp, lProp ⇒ Lt
    end.

  Inductive lt_ : t → t → Prop :=
    ltSPropProp : lt_ lSProp lProp.

  Definition lt := lt_.

  Global Instance lt_strorder : StrictOrder lt.
  split.
  - intros n X. destruct n;inversion X.
  - intros n1 n2 n3 X1 X2. destruct n1,n2,n3;auto; try inversion X1;try inversion X2.
  Defined.

End PropLevel.

Module LevelExpr.
  Definition t := (Level.t × nat)%type.

  Global Instance Evaluable : Evaluable t
    := fun v l ⇒ (snd l + val v (fst l)).

  Definition succ (l : t) := (fst l, S (snd l)).

  Definition get_level (e : t) : Level.t := fst e.

  Definition get_noprop (e : LevelExpr.t) := Some (fst e).

  Definition is_level (e : t) : bool :=
    match e with
    | (_, 0%nat) ⇒ true
    | _ ⇒ false
    end.

  Definition make (l : Level.t) : t := (l, 0%nat).

  Definition set : t := (Level.lzero, 0%nat).
  Definition type1 : t := (Level.lzero, 1%nat).

  Definition from_kernel_repr (e : Level.t × bool) : t
    := (e.1, if e.2 then 1%nat else 0%nat).

  Definition to_kernel_repr (e : t) : Level.t × bool
    := match e with
       | (l, b) ⇒ (l, match b with 0%nat ⇒ false | _ ⇒ true end)
       end.

  Definition eq : t → t → Prop := eq.

  Definition eq_equiv : Equivalence eq := _.

  Inductive lt_ : t → t → Prop :=
  | ltLevelExpr1 l n n' : (n < n')%nat → lt_ (l, n) (l, n')
  | ltLevelExpr2 l l' b b' : Level.lt l l' → lt_ (l, b) (l', b').

  Definition lt := lt_.

  Global Instance lt_strorder : StrictOrder lt.
  Proof.
    constructor.
    - intros x X; inversion X. subst. lia. subst.
      eapply Level.lt_strorder; eassumption.
    - intros x y z X1 X2; invs X1; invs X2; constructor; tea.
      etransitivity; tea.
      etransitivity; tea.
  Qed.

  Definition lt_compat : Proper (Logic.eq ==> Logic.eq ==> iff) lt.
    intros x x' H1 y y' H2; now rewrite H1 H2.
  Qed.

  Definition compare (x y : t) : comparison :=
    match x, y with
    | (l1, b1), (l2, b2) ⇒
      match Level.compare l1 l2 with
      | Eq ⇒ Nat.compare b1 b2
      | x ⇒ x
      end
    end.

  Definition compare_spec :
    ∀ x y : t, CompareSpec (x = y) (lt x y) (lt y x) (compare x y).
  Proof.
    intros [? ?] [? ?]; cbn; repeat constructor.
    destruct (Level.compare_spec t0 t1); repeat constructor; tas.
    subst.
    destruct (Nat.compare_spec n n0); repeat constructor; tas. congruence.
  Qed.

  Global Instance reflect_t : ReflectEq t := reflect_prod _ _ .

  Definition eq_dec : ∀ (l1 l2 : t), {l1 = l2} + {l1 ≠ l2} := Classes.eq_dec.

  Definition eq_leibniz (x y : t) : eq x y → x = y := id.

  Lemma val_make v l
    : val v (LevelExpr.make l) = val v l.
  Proof.
    destruct l eqn:H; cbnr.
  Qed.

  Lemma val_make_npl v (l : Level.t)
    : val v (LevelExpr.make l) = val v l.
  Proof.
    destruct l; cbnr.
  Qed.

End LevelExpr.

Module LevelExprSet := MSetList.MakeWithLeibniz LevelExpr.
Module LevelExprSetFact := WFactsOn LevelExpr LevelExprSet.
Module LevelExprSetProp := WPropertiesOn LevelExpr LevelExprSet.

#[global, program] Instance levelexprset_reflect : ReflectEq LevelExprSet.t :=
  { eqb := LevelExprSet.equal }.
Next Obligation.
  destruct (LevelExprSet.equal x y) eqn:e; constructor.
  eapply LevelExprSet.equal_spec in e.
  now eapply LevelExprSet.eq_leibniz.
  intros e'.
  subst y.
  pose proof (@LevelExprSetFact.equal_1 x x).
  forward H. reflexivity. congruence.
Qed.

#[global] Instance levelexprset_eq_dec : Classes.EqDec LevelExprSet.t := Classes.eq_dec.

Record nonEmptyLevelExprSet
  := { t_set : LevelExprSet.t ;
       t_ne : LevelExprSet.is_empty t_set = false }.

Derive NoConfusion for nonEmptyLevelExprSet.

Coercion t_set : nonEmptyLevelExprSet >-> LevelExprSet.t.

Module NonEmptySetFacts.
  Definition singleton (e : LevelExpr.t) : nonEmptyLevelExprSet
    := {| t_set := LevelExprSet.singleton e;
          t_ne := eq_refl |}.

  Lemma not_Empty_is_empty s :
    ¬ LevelExprSet.Empty s → LevelExprSet.is_empty s = false.
  Proof.
    intro H. apply not_true_is_false. intro H'.
    apply H. now apply LevelExprSetFact.is_empty_2 in H'.
  Qed.

  Program Definition add (e : LevelExpr.t) (u : nonEmptyLevelExprSet) : nonEmptyLevelExprSet
    := {| t_set := LevelExprSet.add e u |}.
  Next Obligation.
    apply not_Empty_is_empty; intro H.
    eapply H. eapply LevelExprSet.add_spec.
    left; reflexivity.
  Qed.

  Lemma add_spec e u e' :
    LevelExprSet.In e' (add e u) ↔ e' = e ∨ LevelExprSet.In e' u.
  Proof.
    apply LevelExprSet.add_spec.
  Qed.

  Definition add_list : list LevelExpr.t → nonEmptyLevelExprSet → nonEmptyLevelExprSet
    := List.fold_left (fun u e ⇒ add e u).

  Lemma add_list_spec l u e :
    LevelExprSet.In e (add_list l u) ↔ In e l ∨ LevelExprSet.In e u.
  Proof.
    unfold add_list. rewrite <- fold_left_rev_right.
    etransitivity. 2:{ eapply or_iff_compat_r. etransitivity.
                       2: apply @InA_In_eq with (A:=LevelExpr.t).
                       eapply InA_rev. }
    induction (List.rev l); cbn.
    - split. intuition. intros [H|H]; tas. invs H.
    - split.
      + intro H. apply add_spec in H. destruct H as [H|H].
        × left. now constructor.
        × apply IHl0 in H. destruct H as [H|H]; [left|now right].
          now constructor 2.
      + intros [H|H]. inv H.
        × apply add_spec; now left.
        × apply add_spec; right. apply IHl0. now left.
        × apply add_spec; right. apply IHl0. now right.
  Qed.

  Program Definition to_nonempty_list (u : nonEmptyLevelExprSet) : LevelExpr.t × list LevelExpr.t
    := match LevelExprSet.elements u with
       | [] ⇒ False_rect _ _
       | e :: l ⇒ (e, l)
       end.
  Next Obligation.
    destruct u as [u1 u2]; cbn in ×. revert u2.
    apply eq_true_false_abs.
    unfold LevelExprSet.is_empty, LevelExprSet.Raw.is_empty,
    LevelExprSet.elements, LevelExprSet.Raw.elements in ×.
    rewrite <- Heq_anonymous; reflexivity.
  Qed.

  Lemma singleton_to_nonempty_list e : to_nonempty_list (singleton e) = (e, []).
  Proof. reflexivity. Defined.

  Lemma to_nonempty_list_spec u :
    let '(e, u') := to_nonempty_list u in
    e :: u' = LevelExprSet.elements u.
  Proof.
    destruct u as [u1 u2].
    unfold to_nonempty_list; cbn.
    set (l := LevelExprSet.elements u1). unfold l at 2 3 4.
    set (e := (eq_refl: l = LevelExprSet.elements u1)); clearbody e.
    destruct l.
    - exfalso. revert u2. apply eq_true_false_abs.
      unfold LevelExprSet.is_empty, LevelExprSet.Raw.is_empty,
      LevelExprSet.elements, LevelExprSet.Raw.elements in ×.
      rewrite <- e; reflexivity.
    - reflexivity.
  Qed.

  Lemma to_nonempty_list_spec' u :
    (to_nonempty_list u).1 :: (to_nonempty_list u).2 = LevelExprSet.elements u.
  Proof.
    pose proof (to_nonempty_list_spec u).
    now destruct (to_nonempty_list u).
  Qed.

  Lemma In_to_nonempty_list (u : nonEmptyLevelExprSet) (e : LevelExpr.t) :
    LevelExprSet.In e u
    ↔ e = (to_nonempty_list u).1 ∨ In e (to_nonempty_list u).2.
  Proof.
    etransitivity. symmetry. apply LevelExprSet.elements_spec1.
    pose proof (to_nonempty_list_spec' u) as H.
    destruct (to_nonempty_list u) as [e' l]; cbn in ×.
    rewrite <- H; clear. etransitivity. apply InA_cons.
    eapply or_iff_compat_l. apply InA_In_eq.
  Qed.

  Lemma In_to_nonempty_list_rev (u : nonEmptyLevelExprSet) (e : LevelExpr.t) :
    LevelExprSet.In e u
    ↔ e = (to_nonempty_list u).1 ∨ In e (List.rev (to_nonempty_list u).2).
  Proof.
    etransitivity. eapply In_to_nonempty_list.
    apply or_iff_compat_l. apply in_rev.
  Qed.

  Definition map (f : LevelExpr.t → LevelExpr.t) (u : nonEmptyLevelExprSet) : nonEmptyLevelExprSet :=
    let '(e, l) := to_nonempty_list u in
    add_list (List.map f l) (singleton (f e)).

  Lemma map_spec f u e :
    LevelExprSet.In e (map f u) ↔ ∃ e0, LevelExprSet.In e0 u ∧ e = (f e0).
  Proof.
    unfold map. symmetry. etransitivity.
    { eapply iff_ex; intro. eapply and_iff_compat_r. eapply In_to_nonempty_list. }
    destruct (to_nonempty_list u) as [e' l]; cbn in ×.
    symmetry. etransitivity. eapply add_list_spec.
    etransitivity. eapply or_iff_compat_l. apply LevelExprSet.singleton_spec.
    etransitivity. eapply or_iff_compat_r.
    apply in_map_iff. clear u. split.
    - intros [[e0 []]|H].
      + ∃ e0. split. right; tas. congruence.
      + ∃ e'. split; tas. left; reflexivity.
    - intros [xx [[H|H] ?]].
      + right. congruence.
      + left. ∃ xx. split; tas; congruence.
  Qed.

  Program Definition non_empty_union (u v : nonEmptyLevelExprSet) : nonEmptyLevelExprSet :=
    {| t_set := LevelExprSet.union u v |}.
  Next Obligation.
    apply not_Empty_is_empty; intro H.
    assert (HH: LevelExprSet.Empty u). {
      intros x Hx. apply (H x).
      eapply LevelExprSet.union_spec. now left. }
    apply LevelExprSetFact.is_empty_1 in HH.
    rewrite t_ne in HH; discriminate.
  Qed.

  Lemma elements_not_empty (u : nonEmptyLevelExprSet) : LevelExprSet.elements u ≠ [].
  Proof.
    destruct u as [u1 u2]; cbn; intro e.
    unfold LevelExprSet.is_empty, LevelExprSet.elements,
    LevelExprSet.Raw.elements in ×.
    rewrite e in u2; discriminate.
  Qed.

  Lemma eq_univ (u v : nonEmptyLevelExprSet) :
    u = v :> LevelExprSet.t → u = v.
  Proof.
    destruct u as [u1 u2], v as [v1 v2]; cbn. intros X; destruct X.
    now rewrite (uip_bool _ _ u2 v2).
  Qed.

  Lemma eq_univ' (u v : nonEmptyLevelExprSet) :
    LevelExprSet.Equal u v → u = v.
  Proof.
    intro H. now apply eq_univ, LevelExprSet.eq_leibniz.
  Qed.

  Lemma eq_univ'' (u v : nonEmptyLevelExprSet) :
    LevelExprSet.elements u = LevelExprSet.elements v → u = v.
  Proof.
    intro H. apply eq_univ.
    destruct u as [u1 u2], v as [v1 v2]; cbn in *; clear u2 v2.
    destruct u1 as [u1 u2], v1 as [v1 v2]; cbn in ×.
    destruct H. now rewrite (uip_bool _ _ u2 v2).
  Qed.

  Lemma univ_expr_eqb_true_iff (u v : nonEmptyLevelExprSet) :
    LevelExprSet.equal u v ↔ u = v.
  Proof.
    split.
    - intros.
      apply eq_univ'. now apply LevelExprSet.equal_spec.
    - intros →. now apply LevelExprSet.equal_spec.
  Qed.

  Lemma univ_expr_eqb_comm (u v : nonEmptyLevelExprSet) :
    LevelExprSet.equal u v ↔ LevelExprSet.equal v u.
  Proof.
    transitivity (u = v). 2: transitivity (v = u).
    - apply univ_expr_eqb_true_iff.
    - split; apply eq_sym.
    - split; apply univ_expr_eqb_true_iff.
  Qed.

  Lemma LevelExprSet_for_all_false f u :
    LevelExprSet.for_all f u = false → LevelExprSet.exists_ (negb ∘ f) u.
  Proof.
    intro H. rewrite LevelExprSetFact.exists_b.
    rewrite LevelExprSetFact.for_all_b in H.
    all: try now intros x y [].
    induction (LevelExprSet.elements u); cbn in *; [discriminate|].
    apply andb_false_iff in H; apply orb_true_iff; destruct H as [H|H].
    left; now rewrite H.
    right; now rewrite IHl.
  Qed.

  Lemma LevelExprSet_For_all_exprs (P : LevelExpr.t → Prop) (u : nonEmptyLevelExprSet)
    : LevelExprSet.For_all P u
      ↔ P (to_nonempty_list u).1 ∧ Forall P (to_nonempty_list u).2.
  Proof.
    etransitivity.
    - eapply iff_forall; intro e. eapply imp_iff_compat_r.
      apply In_to_nonempty_list.
    - cbn; split.
      + intro H. split. apply H. now left.
        apply Forall_forall. intros x H0. apply H; now right.
      + intros [H1 H2] e [He|He]. subst e; tas.
        eapply Forall_forall in H2; tea.
  Qed.

End NonEmptySetFacts.
Import NonEmptySetFacts.

Module LevelAlgExpr.

  Definition t := nonEmptyLevelExprSet.

  #[global, program] Instance levelexprset_reflect : ReflectEq t :=
    { eqb x y := eqb x.(t_set) y.(t_set) }.
  Next Obligation.
    destruct (eqb_spec (t_set x) (t_set y)); constructor.
    destruct x, y; cbn in ×. subst.
    now rewrite (uip t_ne0 t_ne1).
    intros e; subst x; apply H.
    reflexivity.
  Qed.

  #[global] Instance eq_dec_univ0 : EqDec t := eq_dec.

  Definition make (e: LevelExpr.t) : t := singleton e.
  Definition make' (l: Level.t) := singleton (LevelExpr.make l).

  Definition exprs : t → LevelExpr.t × list LevelExpr.t := to_nonempty_list.

  Global Instance Evaluable : Evaluable LevelAlgExpr.t
    := fun v u ⇒
      let '(e, u) := LevelAlgExpr.exprs u in
      List.fold_left (fun n e ⇒ Nat.max (val v e) n) u (val v e).

  Definition is_levels (u : t) : bool :=
    LevelExprSet.for_all LevelExpr.is_level u.

  Definition is_level (u : t) : bool :=
    (LevelExprSet.cardinal u =? 1)%nat && is_levels u.

  Definition succ : t → t := map LevelExpr.succ.

  Definition sup : t → t → t := non_empty_union.

  Definition get_is_level (u : t) : option Level.t :=
    match LevelExprSet.elements u with
    | [(l, 0%nat)] ⇒ Some l
    | _ ⇒ None
    end.

  Lemma val_make v e : val v (make e) = val v e.
  Proof. reflexivity. Qed.

  Lemma val_make' v l
    : val v (make' l) = val v l.
  Proof. reflexivity. Qed.

End LevelAlgExpr.

Ltac u :=
  change LevelSet.elt with Level.t in *;
  change LevelExprSet.elt with LevelExpr.t in ×.

Lemma val_fold_right (u : LevelAlgExpr.t) v :
  val v u = fold_right (fun e x ⇒ Nat.max (val v e) x) (val v (LevelAlgExpr.exprs u).1)
                       (List.rev (LevelAlgExpr.exprs u).2).
Proof.
  unfold val at 1, LevelAlgExpr.Evaluable.
  destruct (LevelAlgExpr.exprs u).
  now rewrite fold_left_rev_right.
Qed.

Lemma val_In_le (u : LevelAlgExpr.t) v e :
  LevelExprSet.In e u → val v e ≤ val v u.
Proof.
  intro H. rewrite val_fold_right.
  apply In_to_nonempty_list_rev in H.
  fold LevelAlgExpr.exprs in H; destruct (LevelAlgExpr.exprs u); cbn in ×.
  destruct H as [H|H].
  - subst. induction (List.rev l); cbnr. lia.
  - induction (List.rev l); cbn; invs H.
    + u; lia.
    + specialize (IHl0 H0). lia.
Qed.

Lemma val_In_max (u : LevelAlgExpr.t) v :
  ∃ e, LevelExprSet.In e u ∧ val v e = val v u.
Proof.
  eapply iff_ex. {
    intro. eapply and_iff_compat_r. apply In_to_nonempty_list_rev. }
  rewrite val_fold_right. fold LevelAlgExpr.exprs; destruct (LevelAlgExpr.exprs u) as [e l]; cbn in ×.
  clear. induction (List.rev l); cbn.
  - ∃ e. split; cbnr. left; reflexivity.
  - destruct IHl0 as [e' [H1 H2]].
    destruct (Nat.max_dec (val v a) (fold_right (fun e0 x0 ⇒ Nat.max (val v e0) x0)
                                               (val v e) l0)) as [H|H];
      rewrite H; clear H.
    + ∃ a. split; cbnr. right. now constructor.
    + rewrite <- H2. ∃ e'. split; cbnr.
      destruct H1 as [H1|H1]; [now left|right]. now constructor 2.
Qed.

Lemma val_ge_caract (u : LevelAlgExpr.t) v k :
  (∀ e, LevelExprSet.In e u → val v e ≤ k) ↔ val v u ≤ k.
Proof.
  split.
  - eapply imp_iff_compat_r. {
      eapply iff_forall; intro. eapply imp_iff_compat_r.
      apply In_to_nonempty_list_rev. }
    rewrite val_fold_right.
    fold LevelAlgExpr.exprs; destruct (LevelAlgExpr.exprs u) as [e l]; cbn; clear.
    induction (List.rev l); cbn.
    + intros H. apply H. left; reflexivity.
    + intros H.
      destruct (Nat.max_dec (val v a) (fold_right (fun e0 x ⇒ Nat.max (val v e0) x)
                                                 (val v e) l0)) as [H'|H'];
        rewrite H'; clear H'.
      × apply H. right. now constructor.
      × apply IHl0. intros x [H0|H0]; apply H. now left.
        right; now constructor 2.
  - intros H e He. eapply val_In_le in He. etransitivity; eassumption.
Qed.

Lemma val_le_caract (u : LevelAlgExpr.t) v k :
  (∃ e, LevelExprSet.In e u ∧ k ≤ val v e) ↔ k ≤ val v u.
Proof.
  split.
  - eapply imp_iff_compat_r. {
      eapply iff_ex; intro. eapply and_iff_compat_r. apply In_to_nonempty_list_rev. }
    rewrite val_fold_right.
    fold LevelAlgExpr.exprs; destruct (LevelAlgExpr.exprs u) as [e l]; cbn; clear.
    induction (List.rev l); cbn.
    + intros H. destruct H as [e' [[H1|H1] H2]].
      × now subst.
      × invs H1.
    + intros [e' [[H1|H1] H2]].
      × forward IHl0; [|lia]. ∃ e'. split; tas. left; assumption.
      × invs H1.
        -- u; lia.
        -- forward IHl0; [|lia]. ∃ e'. split; tas. right; assumption.
  - intros H. destruct (val_In_max u v) as [e [H1 H2]].
    ∃ e. rewrite H2; split; assumption.
Qed.

Lemma val_caract (u : LevelAlgExpr.t) v k :
  val v u = k
  ↔ (∀ e, LevelExprSet.In e u → val v e ≤ k)
    ∧ ∃ e, LevelExprSet.In e u ∧ val v e = k.
Proof.
  split.
  - intros <-; split.
    + apply val_In_le.
    + apply val_In_max.
  - intros [H1 H2].
    apply val_ge_caract in H1.
    assert (k ≤ val v u); [clear H1|lia].
    apply val_le_caract. destruct H2 as [e [H2 H2']].
    ∃ e. split; tas. lia.
Qed.

Lemma val_add v e (s: LevelAlgExpr.t)
  : val v (add e s) = Nat.max (val v e) (val v s).
Proof.
  apply val_caract. split.
  - intros e' H. apply LevelExprSet.add_spec in H. destruct H as [H|H].
    + subst. u; lia.
    + eapply val_In_le with (v:=v) in H. lia.
  - destruct (Nat.max_dec (val v e) (val v s)) as [H|H]; rewrite H; clear H.
    + ∃ e. split; cbnr. apply LevelExprSetFact.add_1. reflexivity.
    + destruct (val_In_max s v) as [e' [H1 H2]].
      ∃ e'. split; tas. now apply LevelExprSetFact.add_2.
Qed.

Lemma val_sup v s1 s2 :
  val v (LevelAlgExpr.sup s1 s2) = Nat.max (val v s1) (val v s2).
Proof.
  eapply val_caract. cbn. split.
  - intros e' H. eapply LevelExprSet.union_spec in H. destruct H as [H|H].
    + eapply val_In_le with (v:=v) in H. lia.
    + eapply val_In_le with (v:=v) in H. lia.
  - destruct (Nat.max_dec (val v s1) (val v s2)) as [H|H]; rewrite H; clear H.
    + destruct (val_In_max s1 v) as [e' [H1 H2]].
      ∃ e'. split; tas. apply LevelExprSet.union_spec. now left.
    + destruct (val_In_max s2 v) as [e' [H1 H2]].
      ∃ e'. split; tas. apply LevelExprSet.union_spec. now right.
Qed.

Ltac proper := let H := fresh in try (intros ? ? H; destruct H; reflexivity).

Lemma for_all_elements (P : LevelExpr.t → bool) u :
  LevelExprSet.for_all P u = forallb P (LevelExprSet.elements u).
Proof.
  apply LevelExprSetFact.for_all_b; proper.
Qed.

Lemma levelalg_get_is_level_correct u l :
  LevelAlgExpr.get_is_level u = Some l → u = LevelAlgExpr.make' l.
Proof.
  intro H.
  unfold LevelAlgExpr.get_is_level in ×.
  destruct (LevelExprSet.elements u) as [|l0 L] eqn:Hu1; [discriminate |].
  destruct l0, L; try discriminate.
  × destruct n; inversion H; subst.
    apply eq_univ''; apply Hu1.
  × destruct n; discriminate.
Qed.

Lemma sup0_comm x1 x2 :
  LevelAlgExpr.sup x1 x2 = LevelAlgExpr.sup x2 x1.
Proof.
  apply eq_univ'; simpl. unfold LevelExprSet.Equal.
  intros H. rewrite !LevelExprSet.union_spec. intuition.
Qed.

Declare Scope univ_scope.
Delimit Scope univ_scope with u.

Section ConcreteUniverses.
  Context {cf}.

  Inductive concreteUniverses :=
    | UProp
    | USProp
    | UType (i : nat).
  Derive NoConfusion EqDec for concreteUniverses.

  Definition leq_cuniverse_n n u u' :=
    match u, u' with
    | UProp, UProp
    | USProp, USProp ⇒ (n = 0)%Z
    | UType u, UType u' ⇒ (Z.of_nat u ≤ Z.of_nat u' - n)%Z
    | UProp, UType u ⇒
      if prop_sub_type then True else False
    | _, _ ⇒ False
    end.

  Definition leq_cuniverse := leq_cuniverse_n 0.
  Definition lt_cuniverse := leq_cuniverse_n 1.

  Notation "x <_ n y" := (leq_cuniverse_n n x y) (at level 10, n name) : univ_scope.
  Notation "x < y" := (lt_cuniverse x y) : univ_scope.
  Notation "x <= y" := (leq_cuniverse x y) : univ_scope.

  Definition cuniv_sup u1 u2 :=
    match u1, u2 with
    | UProp, UProp ⇒ UProp
    | USProp, USProp ⇒ USProp
    | UType v, UType v' ⇒ UType (Nat.max v v')
    | _, UType _ ⇒ u2
    | UType _, _ ⇒ u1
    | UProp, USProp ⇒ UProp
    | USProp, UProp ⇒ UProp
    end.

  Definition is_uprop u := match u with UProp ⇒ True | _ ⇒ False end.
  Definition is_usprop u := match u with USProp ⇒ True | _ ⇒ False end.
  Definition is_uproplevel u := match u with USProp | UProp ⇒ True | _ ⇒ False end.
  Definition is_uproplevel_or_set u := match u with USProp | UProp | UType 0 ⇒ True | _ ⇒ False end.
  Definition is_utype u := match u with UType _ ⇒ True | _ ⇒ False end.

  Definition cuniv_of_product domsort rangsort :=
    match rangsort with
    
    | UProp | USProp ⇒ rangsort
    | _ ⇒ cuniv_sup domsort rangsort
    end.

  Lemma cuniv_sup_comm u u' : cuniv_sup u u' = cuniv_sup u' u.
  Proof using Type. destruct u, u'; cbn; try congruence. f_equal; lia. Qed.

  Lemma cuniv_sup_not_uproplevel u u' :
    ¬ is_uproplevel u → ∑ n, cuniv_sup u u' = UType n.
  Proof using Type.
    destruct u, u'; cbn; intros Hp; try absurd;
    now eexists.
  Qed.

  Lemma cuniv_le_uprop_inv u : (u ≤ UProp)%u → u = UProp.
  Proof using Type. destruct u; simpl; intros Hle; try absurd; now reflexivity. Qed.

  Lemma cuniv_le_usprop_inv u : (u ≤ USProp)%u → u = USProp.
  Proof using Type. destruct u; simpl; intros Hle; try absurd; now reflexivity. Qed.

  Lemma cuniv_uprop_le_inv u : (UProp ≤ u)%u →
    (u = UProp ∨ (prop_sub_type ∧ ∃ n, u = UType n)).
  Proof using Type.
    destruct u; simpl; intros Hle; [ left; reflexivity | absurd | right ].
    destruct prop_sub_type; [| absurd].
    split; [ trivial | now eexists ].
  Qed.

  Lemma cuniv_sup_mon u u' v v' : (u ≤ u')%u → (UType v ≤ UType v')%u →
    (cuniv_sup u (UType v) ≤ cuniv_sup u' (UType v'))%u.
  Proof using Type.
    destruct u, u'; simpl; intros Hle Hle'; try absurd;
    lia.
  Qed.

  Lemma leq_cuniv_of_product_mon u u' v v' :
    (u ≤ u')%u →
    (v ≤ v')%u →
    (cuniv_of_product u v ≤ cuniv_of_product u' v')%u.
  Proof using Type.
    intros Hle1 Hle2.
    destruct v, v'; cbn in Hle2 |- *; auto.
    - destruct u'; cbn; assumption.
    - apply cuniv_sup_mon; assumption.
  Qed.

  Lemma impredicative_cuniv_product {l u} :
    is_uproplevel u →
    (cuniv_of_product l u ≤ u)%u.
  Proof using Type. now destruct u. Qed.

  Global Instance leq_cuniverse_refl : Reflexive leq_cuniverse.
  Proof using Type.
    intros []; cbnr; lia.
  Qed.

  Global Instance leq_cuniverse_n_trans n : Transitive (leq_cuniverse_n (Z.of_nat n)).
  Proof using Type.
    intros [] [] []; cbnr; trivial; try absurd; lia.
  Qed.

  Global Instance leq_cuniverse_trans : Transitive leq_cuniverse.
  Proof using Type. apply (leq_cuniverse_n_trans 0). Qed.

  Global Instance lt_cuniverse_trans : Transitive lt_cuniverse.
  Proof using Type. apply (leq_cuniverse_n_trans 1). Qed.

  Global Instance leq_cuniverse_preorder : PreOrder leq_cuniverse :=
    Build_PreOrder _ _ _.

  Global Instance lt_cuniverse_str_order : StrictOrder lt_cuniverse.
  Proof using Type.
    split.
    - intros []; unfold complement; cbnr; lia.
    - exact _.
  Qed.

  Global Instance leq_cuniverse_antisym : Antisymmetric _ eq leq_cuniverse.
  Proof using Type.
    intros [] []; cbnr; try absurd.
    intros. f_equal; lia.
  Qed.

End ConcreteUniverses.

Inductive allowed_eliminations : Set :=
  | IntoSProp
  | IntoPropSProp
  | IntoSetPropSProp
  | IntoAny.
Derive NoConfusion EqDec for allowed_eliminations.

Definition is_allowed_elimination_cuniv (allowed : allowed_eliminations) : concreteUniverses → Prop :=
  match allowed with
  | IntoSProp ⇒ is_usprop
  | IntoPropSProp ⇒ is_uproplevel
  | IntoSetPropSProp ⇒ is_uproplevel_or_set
  | IntoAny ⇒ fun _ ⇒ True
  end.

Module Universe.
  Inductive t_ :=
    lProp | lSProp | lType (_ : LevelAlgExpr.t).
  Derive NoConfusion for t_.

  Definition t := t_.

  Definition eqb (u1 u2 : t) : bool :=
    match u1, u2 with
    | lSProp, lSProp ⇒ true
    | lProp, lProp ⇒ true
    | lType e1, lType e2 ⇒ eqb e1 e2
    | _, _ ⇒ false
    end.

  #[global, program] Instance reflect_eq_universe : ReflectEq t :=
    { eqb := eqb }.
  Next Obligation.
    destruct x, y; cbn; try constructor; auto; try congruence.
    destruct (eqb_spec t0 t1); constructor. now f_equal.
    congruence.
  Qed.

  #[global] Instance eq_dec_univ : EqDec t := eq_dec.

  Definition on_sort (P: LevelAlgExpr.t → Prop) (def: Prop) (s : t) :=
    match s with
    | lProp | lSProp ⇒ def
    | lType l ⇒ P l
    end.

  Definition make (l : Level.t) : t :=
    lType (LevelAlgExpr.make (LevelExpr.make l)).

  Definition of_expr e := (lType (LevelAlgExpr.make e)).

  Definition add_to_exprs (e : LevelExpr.t) (u : t) : t :=
    match u with
    | lSProp | lProp ⇒ u
    | lType l ⇒ lType (add e l)
    end.

  Definition add_list_to_exprs (es : list LevelExpr.t) (u : t) : t :=
    match u with
    | lSProp | lProp ⇒ u
    | lType l ⇒ lType (add_list es l)
    end.

  Definition is_levels (u : t) : bool :=
    match u with
    | lSProp | lProp ⇒ true
    | lType l ⇒ LevelAlgExpr.is_levels l
    end.

  Definition is_level (u : t) : bool :=
    match u with
    | lSProp | lProp ⇒ true
    | lType l ⇒ LevelAlgExpr.is_level l
    end.

  Definition is_sprop (u : t) : bool :=
    match u with
      | lSProp ⇒ true
      | _ ⇒ false
    end.

  Definition is_prop (u : t) : bool :=
    match u with
      | lProp ⇒ true
      | _ ⇒ false
    end.

  Definition is_type_sort (u : t) : bool :=
    match u with
      | lType _ ⇒ true
      | _ ⇒ false
    end.

  Definition type0 : t := make Level.lzero.
  Definition type1 : t := lType (LevelAlgExpr.make LevelExpr.type1).

  Definition of_levels (l : PropLevel.t + Level.t) : t :=
    match l with
    | inl PropLevel.lSProp ⇒ lSProp
    | inl PropLevel.lProp ⇒ lProp
    | inr l ⇒ lType (LevelAlgExpr.make' l)
    end.

  Definition from_kernel_repr (e : Level.t × bool) (es : list (Level.t × bool)) : t
    := lType (add_list (List.map LevelExpr.from_kernel_repr es)
                (LevelAlgExpr.make (LevelExpr.from_kernel_repr e))).

  Definition super (l : t) : t :=
    match l with
    | lSProp ⇒ type1
    | lProp ⇒ type1
    | lType l ⇒ lType (LevelAlgExpr.succ l)
    end.

  Definition sup (u v : t) : t :=
    match u,v with
    | lSProp, lProp ⇒ lProp
    | lProp, lSProp ⇒ lProp
    | (lSProp | lProp), u' ⇒ u'
    | u', (lSProp | lProp) ⇒ u'
    | lType l1, lType l2 ⇒ lType (LevelAlgExpr.sup l1 l2)
    end.

  Definition get_univ_exprs (u : t) (H1 : is_prop u = false) (H2 : is_sprop u = false) : LevelAlgExpr.t.
  destruct u; try discriminate; easy. Defined.

  Definition sort_of_product (domsort rangsort : t) :=
    
    if Universe.is_prop rangsort || Universe.is_sprop rangsort then rangsort
    else Universe.sup domsort rangsort.

  Lemma eqb_refl u : eqb u u.
  Proof.
    destruct u; auto.
    now apply LevelExprSet.equal_spec.
  Qed.

  Definition get_is_level (u : t) : option Level.t :=
    match u with
    | lSProp ⇒ None
    | lProp ⇒ None
    | lType l ⇒ LevelAlgExpr.get_is_level l
    end.

  Definition to_cuniv v u :=
    match u with
    | lSProp ⇒ USProp
    | lProp ⇒ UProp
    | lType l ⇒ UType (val v l)
    end.

  Lemma val_make v l
    : to_cuniv v (make l) = UType (val v l).
  Proof.
    destruct l; cbnr.
  Qed.

  Lemma make_inj x y :
    make x = make y → x = y.
  Proof.
    destruct x, y; try now inversion 1.
  Qed.

End Universe.

Definition is_propositional u :=
  Universe.is_prop u || Universe.is_sprop u.

Notation "⟦ u ⟧_ v" := (Universe.to_cuniv v u) (at level 0, format "⟦ u ⟧_ v", v name) : univ_scope.

Lemma val_universe_sup v u1 u2 :
  Universe.to_cuniv v (Universe.sup u1 u2) = cuniv_sup (Universe.to_cuniv v u1) (Universe.to_cuniv v u2).
Proof.
  destruct u1 as [ | | l1]; destruct u2 as [ | | l2];cbn;try lia; auto.
  f_equal. apply val_sup.
Qed.

Lemma is_prop_val u :
  Universe.is_prop u → ∀ v, Universe.to_cuniv v u = UProp.
Proof.
  destruct u as [| | u];try discriminate;auto.
Qed.

Lemma is_sprop_val u :
  Universe.is_sprop u → ∀ v, Universe.to_cuniv v u = USProp.
Proof.
  destruct u as [| | u];try discriminate;auto.
Qed.


Lemma val_is_prop u v :
  Universe.to_cuniv v u = UProp ↔ Universe.is_prop u.
Proof.
  destruct u; auto;cbn in *; intuition congruence.
Qed.

Lemma val_is_sprop u v :
  Universe.to_cuniv v u = USProp ↔ Universe.is_sprop u.
Proof.
  destruct u;auto;cbn in *; intuition congruence.
Qed.

Lemma is_prop_and_is_sprop_val_false u :
  Universe.is_prop u = false → Universe.is_sprop u = false →
  ∀ v, ∑ n, Universe.to_cuniv v u = UType n.
Proof.
  intros Hp Hsp v.
  destruct u; try discriminate. simpl. eexists; eauto.
Qed.

Lemma val_is_prop_false u v n :
  Universe.to_cuniv v u = UType n → Universe.is_prop u = false.
Proof.
  pose proof (is_prop_val u) as H. destruct (Universe.is_prop u); cbnr.
  rewrite (H eq_refl v). discriminate.
Qed.

Lemma get_is_level_correct u l :
  Universe.get_is_level u = Some l → u = Universe.lType (LevelAlgExpr.make' l).
Proof.
  intro H; destruct u; cbnr; try discriminate.
  f_equal; now apply levelalg_get_is_level_correct.
Qed.

Lemma eqb_true_iff u v :
  Universe.eqb u v ↔ u = v.
Proof.
  split. 2: intros ->; apply Universe.eqb_refl.
  intro H.
  destruct u, v;auto;try discriminate.
  apply f_equal. now apply univ_expr_eqb_true_iff.
Qed.

Lemma sup_comm x1 x2 :
  Universe.sup x1 x2 = Universe.sup x2 x1.
Proof.
  destruct x1,x2;auto.
  cbn;apply f_equal;apply sup0_comm.
Qed.

Lemma is_not_prop_and_is_not_sprop u :
  Universe.is_prop u = false → Universe.is_sprop u = false →
  ∑ u', u = Universe.lType u'.
Proof.
  intros Hp Hsp.
  destruct u; try discriminate. now eexists.
Qed.

Lemma is_prop_sort_sup x1 x2 :
  Universe.is_prop (Universe.sup x1 x2)
  → Universe.is_prop x2 ∨ Universe.is_sprop x2 .
Proof. destruct x1,x2;auto. Qed.

Lemma is_prop_sort_sup' x1 x2 :
  Universe.is_prop (Universe.sup x1 x2)
  → Universe.is_prop x1 ∨ Universe.is_sprop x1 .
Proof. destruct x1,x2;auto. Qed.

Lemma is_prop_or_sprop_sort_sup x1 x2 :
  Universe.is_sprop (Universe.sup x1 x2) → Universe.is_sprop x2.
Proof. destruct x1,x2;auto. Qed.

Lemma is_prop_sort_sup_prop x1 x2 :
  Universe.is_prop x1 && Universe.is_prop x2 →
  Universe.is_prop (Universe.sup x1 x2).
Proof. destruct x1,x2;auto. Qed.

Lemma is_prop_or_sprop_sort_sup_prop x1 x2 :
  Universe.is_sprop x1 && Universe.is_sprop x2 →
  Universe.is_sprop (Universe.sup x1 x2).
Proof. destruct x1,x2;auto. Qed.

Lemma is_prop_sup u s :
  Universe.is_prop (Universe.sup u s) →
  (Universe.is_prop u ∨ Universe.is_sprop u) ∧
  (Universe.is_prop s ∨ Universe.is_sprop s).
Proof. destruct u,s;auto. Qed.

Lemma is_sprop_sup_iff u s :
  Universe.is_sprop (Universe.sup u s) ↔
  (Universe.is_sprop u ∧ Universe.is_sprop s).
Proof. split;destruct u,s;intuition. Qed.

Lemma is_type_sup_r s1 s2 :
  Universe.is_type_sort s2 →
  Universe.is_type_sort (Universe.sup s1 s2).
Proof. destruct s2; try absurd; destruct s1; cbnr; intros; absurd. Qed.

Lemma is_prop_sort_prod x2 x3 :
  Universe.is_prop (Universe.sort_of_product x2 x3)
  → Universe.is_prop x3.
Proof.
  unfold Universe.sort_of_product.
  destruct x3;cbn;auto.
  intros;simpl in *;destruct x2;auto.
Qed.

Lemma is_sprop_sort_prod x2 x3 :
  Universe.is_sprop (Universe.sort_of_product x2 x3)
  → Universe.is_sprop x3.
Proof.
  unfold Universe.sort_of_product.
  destruct x3;cbn;auto.
  intros;simpl in *;destruct x2;auto.
Qed.

Module ConstraintType.
  Inductive t_ : Set := Le (z : Z) | Eq.
  Derive NoConfusion EqDec for t_.

  Definition t := t_.
  Definition eq : t → t → Prop := eq.
  Definition eq_equiv : Equivalence eq := _.

  Definition Le0 := Le 0.
  Definition Lt := Le 1.

  Inductive lt_ : t → t → Prop :=
  | LeLe n m : (n < m)%Z → lt_ (Le n) (Le m)
  | LeEq n : lt_ (Le n) Eq.
  Derive Signature for lt_.
  Definition lt := lt_.

  Global Instance lt_strorder : StrictOrder lt.
  Proof.
    constructor.
    - intros []; intro X; inversion X. lia.
    - intros ? ? ? X Y; invs X; invs Y; constructor. lia.
  Qed.

  Global Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof.
    intros ? ? X ? ? Y; invs X; invs Y. reflexivity.
  Qed.

  Definition compare (x y : t) : comparison :=
    match x, y with
    | Le n, Le m ⇒ Z.compare n m
    | Le _, Eq ⇒ Datatypes.Lt
    | Eq, Eq ⇒ Datatypes.Eq
    | Eq, _ ⇒ Datatypes.Gt
    end.

  Lemma compare_spec x y : CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
  Proof.
    destruct x, y; repeat constructor. simpl.
    destruct (Z.compare_spec z z0); simpl; constructor.
    subst; constructor. now constructor. now constructor.
  Qed.

  Lemma eq_dec x y : {eq x y} + {¬ eq x y}.
  Proof.
    unfold eq. decide equality. apply Z.eq_dec.
  Qed.
End ConstraintType.

Module UnivConstraint.
  Definition t : Set := Level.t × ConstraintType.t × Level.t.

  Definition eq : t → t → Prop := eq.
  Definition eq_equiv : Equivalence eq := _.

  Definition make l1 ct l2 : t := (l1, ct, l2).

  Inductive lt_ : t → t → Prop :=
  | lt_Level2 l1 t l2 l2' : Level.lt l2 l2' → lt_ (l1, t, l2) (l1, t, l2')
  | lt_Cstr l1 t t' l2 l2' : ConstraintType.lt t t' → lt_ (l1, t, l2) (l1, t', l2')
  | lt_Level1 l1 l1' t t' l2 l2' : Level.lt l1 l1' → lt_ (l1, t, l2) (l1', t', l2').
  Definition lt := lt_.

  Lemma lt_strorder : StrictOrder lt.
  Proof.
    constructor.
    - intros []; intro X; inversion X; subst;
        try (eapply Level.lt_strorder; eassumption).
      eapply ConstraintType.lt_strorder; eassumption.
    - intros ? ? ? X Y; invs X; invs Y; constructor; tea.
      etransitivity; eassumption.
      2: etransitivity; eassumption.
      eapply ConstraintType.lt_strorder; eassumption.
  Qed.

  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof.
    intros ? ? X ? ? Y; invs X; invs Y. reflexivity.
  Qed.

  Definition compare : t → t → comparison :=
    fun '(l1, t, l2) '(l1', t', l2') ⇒
      compare_cont (Level.compare l1 l1')
        (compare_cont (ConstraintType.compare t t')
                    (Level.compare l2 l2')).

  Lemma compare_spec x y
    : CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
  Proof.
    destruct x as [[l1 t] l2], y as [[l1' t'] l2']; cbn.
    destruct (Level.compare_spec l1 l1'); cbn; repeat constructor; tas.
    invs H.
    destruct (ConstraintType.compare_spec t t'); cbn; repeat constructor; tas.
    invs H.
    destruct (Level.compare_spec l2 l2'); cbn; repeat constructor; tas.
    invs H. reflexivity.
  Qed.

  Lemma eq_dec x y : {eq x y} + {¬ eq x y}.
  Proof.
    unfold eq. decide equality; apply eq_dec.
  Defined.

  Definition eq_leibniz (x y : t) : eq x y → x = y := id.
End UnivConstraint.

Module ConstraintSet := MSetAVL.Make UnivConstraint.
Module ConstraintSetFact := WFactsOn UnivConstraint ConstraintSet.
Module ConstraintSetProp := WPropertiesOn UnivConstraint ConstraintSet.
Module CS := ConstraintSet.
Module ConstraintSetDecide := WDecide (ConstraintSet).
Ltac csets := ConstraintSetDecide.fsetdec.

Notation "(=_cset)" := ConstraintSet.Equal (at level 0).
Infix "=_cset" := ConstraintSet.Equal (at level 30).

Definition declared_cstr_levels levels (cstr : UnivConstraint.t) :=
  let '(l1,_,l2) := cstr in
  LevelSet.In l1 levels ∧ LevelSet.In l2 levels.

Definition is_declared_cstr_levels levels (cstr : UnivConstraint.t) : bool :=
  let '(l1,_,l2) := cstr in
  LevelSet.mem l1 levels && LevelSet.mem l2 levels.

Lemma CS_union_empty s : ConstraintSet.union ConstraintSet.empty s =_cset s.
Proof.
  intros x; rewrite ConstraintSet.union_spec. lsets.
Qed.

Lemma CS_For_all_union f cst cst' : ConstraintSet.For_all f (ConstraintSet.union cst cst') →
  ConstraintSet.For_all f cst.
Proof.
  unfold CS.For_all.
  intros IH x inx. apply (IH x).
  now eapply CS.union_spec; left.
Qed.

Lemma CS_For_all_add P x s : CS.For_all P (CS.add x s) → P x ∧ CS.For_all P s.
Proof.
  intros.
  split.
  × apply (H x), CS.add_spec; left ⇒ //.
  × intros y iny. apply (H y), CS.add_spec; right ⇒ //.
Qed.

#[global] Instance CS_For_all_proper P : Morphisms.Proper ((=_cset) ==> iff)%signature (ConstraintSet.For_all P).
Proof.
  intros s s' eqs.
  unfold CS.For_all. split; intros IH x inxs; apply (IH x);
  now apply eqs.
Qed.