From Coq Require Import OrdersAlt MSetList MSetAVL MSetFacts MSetProperties MSetDecide FMapAVL.
From Equations Require Import Equations.
From MetaCoq.Utils Require Import utils MCMSets MCFSets.
From MetaCoq.Common Require Import 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)
  | lvar (_ : nat) (* these are debruijn indices *).
  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
    | lvar _ ⇒ 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))
               | lvar 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
    | lvar n, lvar 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)
  | ltSetlvar n : lt_ lzero (lvar n)
  | ltLevelLevel s s' : StringOT.lt s s' → lt_ (level s) (level s')
  | ltLevellvar s n : lt_ (level s) (lvar n)
  | ltlvarlvar n n' : Nat.lt n n' → lt_ (lvar n) (lvar 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 eq_level l1 l2 :=
    match l1, l2 with
    | Level.lzero, Level.lzero ⇒ true
    | Level.level s1, Level.level s2 ⇒ ReflectEq.eqb s1 s2
    | Level.lvar n1, Level.lvar 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.

  Global Instance eqb_refl : @Reflexive Level.t eqb.
  Proof.
    intros x. apply ReflectEq.eqb_refl.
  Qed.

  Definition eqb := eq_level.

  Lemma eqb_spec l l' : reflect (eq l l') (eqb l l').
  Proof.
    apply reflectProp_reflect.
    now generalize (eqb_spec l l').
  Qed.

  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 LevelSetOrdProp := MSetProperties.OrdProperties LevelSet.
Module LevelSetProp := LevelSetOrdProp.P.
Module LevelSetDecide := LevelSetProp.Dec.
Module LevelSetExtraOrdProp := MSets.ExtraOrdProperties LevelSet LevelSetOrdProp.
Module LevelSetExtraDecide := MSetAVL.Decide Level 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.

(* prop level is Prop or SProp *)
Module PropLevel.

  Inductive t := lSProp | lProp.
  Derive NoConfusion EqDec for t.
  (* Global Instance PropLevel_Evaluable : Evaluable t :=
    fun v l => match l with
              lSProp => -1
            | lProp => -1
            end. *)

  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.
  (* npe = no prop expression *)
  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).

  (* Used for (un)quoting. *)
  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 LevelExprSetOrdProp := MSetProperties.OrdProperties LevelExprSet.
Module LevelExprSetProp := LevelExprSetOrdProp.P.
Module LevelExprSetDecide := LevelExprSetProp.Dec.
Module LevelExprSetExtraOrdProp := MSets.ExtraOrdProperties LevelExprSet LevelExprSetOrdProp.

(* We have decidable equality w.r.t leibniz equality for sets of levels.
  This means concreteUniverses also have a decidable equality. *)
#[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.

  (* We use uip on the is_empty condition *)
  #[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.

  Definition lt : t → t → Prop := LevelExprSet.lt.
  Definition lt_compat : Proper (eq ==> eq ==> iff) lt.
  Proof. repeat intro; subst; reflexivity. Qed.
  #[global] Instance lt_strorder : StrictOrder lt.
  Proof.
    cbv [lt]; constructor.
    { intros ? H. apply irreflexivity in H; assumption. }
    { intros ??? H1 H2; etransitivity; tea. }
  Qed.
End LevelAlgExpr.

Ltac u :=
  change LevelSet.elt with Level.t in *;
  change LevelExprSet.elt with LevelExpr.t in ×.
  (* change ConstraintSet.elt with UnivConstraint.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
    (* Prop and SProp impredicativity *)
    | 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.

  (* Used for quoting. *)
  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 uex_to_kernel_repr (e : LevelExpr.t) : Level.t * bool := *)
  (*   match e with *)
  (*   | LevelExpr.npe (l, b) => (NoPropLevel.to_level l, b) *)
  (*   end. *)

  (* Definition to_kernel_repr (u : t) : list (Level.t * bool) *)
  (*   :=  map (LevelExpr.to_kernel_repr) (LevelExprSet.elements u). *)
  (* match u with *)
  (*      | lProp => (Level.lProp, false) *)
  (*      | lSProp => (Level.lSProp, false) *)
  (*      | lType l => map uex_to_kernel_repr (LevelExprSet.elements l) *)
  (*      end. *)

  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) :=
    (* Prop and SProp impredicativity *)
    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.

  Inductive lt_ : t → t → Prop :=
  | ltPropSProp : lt_ lProp lSProp
  | ltPropType s : lt_ lProp (lType s)
  | ltSPropType s : lt_ lSProp (lType s)
  | ltTypeType s1 s2 : LevelAlgExpr.lt s1 s2 → lt_ (lType s1) (lType s2).
  Derive Signature for lt_.

  Definition lt := lt_.

  Module OT <: OrderedType.
    Definition t := t.
    #[local] Definition eq : t → t → Prop := eq.
    #[local] Definition eq_equiv : Equivalence eq := _.
    Definition lt := lt.
    #[local] Instance lt_strorder : StrictOrder lt.
    Proof.
      constructor.
      - intros [| |] X; inversion X.
        now eapply irreflexivity in H1.
      - intros [| |] [| |] [| |] X1 X2;
          inversion X1; inversion X2; constructor.
        subst.
        etransitivity; tea.
    Qed.

    Definition lt_compat : Proper (eq ==> eq ==> iff) lt.
    Proof.
      intros x y e z t e'. hnf in × |- ; subst. reflexivity.
    Qed.
    Definition compare (x y : t) : comparison
      := match x, y with
         | lProp, lProp ⇒ Eq
         | lProp, _ ⇒ Lt
         | _, lProp ⇒ Gt
         | lSProp, lSProp ⇒ Eq
         | lSProp, _ ⇒ Lt
         | _, lSProp ⇒ Gt
         | lType x, lType y ⇒ LevelExprSet.compare x y
         end.
    Lemma compare_spec x y : CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
    Proof.
      cbv [compare eq].
      destruct x, y.
      all: lazymatch goal with
           | [ |- context[LevelExprSet.compare ?x ?y] ]
             ⇒ destruct (LevelExprSet.compare_spec x y)
           | _ ⇒ idtac
           end.
      all: lazymatch goal with
           | [ H : LevelExprSet.eq (?f ?x) (?f ?y) |- _ ]
             ⇒ apply LevelExprSet.eq_leibniz in H;
                is_var x; is_var y; destruct x, y; cbn in H; subst
           | _ ⇒ idtac
           end.
      all: repeat constructor; try apply f_equal; try assumption.
      f_equal; apply Eqdep_dec.UIP_dec; decide equality.
    Qed.
    Definition eq_dec (x y : t) : {x = y} + {x ≠ y}.
    Proof. repeat decide equality. apply LevelAlgExpr.eq_dec_univ0. Defined.
  End OT.
  Module OTOrig <: OrderedTypeOrig := Backport_OT OT.
End Universe.

Module UniverseMap := FMapAVL.Make Universe.OTOrig.
Module UniverseMapFact := FMapFacts.WProperties UniverseMap.
Module UniverseMapExtraFact := FSets.WFactsExtra_fun Universe.OTOrig UniverseMap UniverseMapFact.F.
Module UniverseMapDecide := FMapAVL.Decide Universe.OTOrig UniverseMap.

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_zero_exprs v (l : LevelAlgExpr.t) : 0 <= val v l.
Proof.
  rewrite val_fold_right.
  destruct (LevelAlgExpr.exprs l) as e u'; clear l; cbn.
  induction (List.rev u'); simpl.
  - destruct e as npl_expr.
    destruct npl_expr as t b.
    cbn.
    assert (0 <= val v t) by apply Level.val_zero.
    destruct b;lia.
  - pose proof (LevelExpr.val_zero a v); lia.
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 ConstraintSetOrdProp := MSetProperties.OrdProperties ConstraintSet.
Module ConstraintSetProp := ConstraintSetOrdProp.P.
Module CS := ConstraintSet.
Module ConstraintSetDecide := ConstraintSetProp.Dec.
Module ConstraintSetExtraOrdProp := MSets.ExtraOrdProperties ConstraintSet ConstraintSetOrdProp.
Module ConstraintSetExtraDecide := MSetAVL.Decide UnivConstraint 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.