Library MetaCoq.PCUIC.PCUICUnivLevels


Definition fresh_levels global_levels levels :=
    LevelSet.For_all (fun l ⇒ ¬ LevelSet.In l global_levels) levels.

  Definition declared_constraints_levels levels cstrs :=
    ConstraintSet.For_all (declared_cstr_levels levels) cstrs.

  Definition declared_constraints_levels_union levels cstrs cstrs' :
    declared_constraints_levels levels cstrs
    declared_constraints_levels levels cstrs'
    declared_constraints_levels levels (ConstraintSet.union cstrs cstrs').
  Proof.
    intros decl decl'.
    rewrite /declared_constraints_levels.
    intros x inx.
    eapply ConstraintSetProp.FM.union_1 in inx as [].
    now eapply decl. now eapply decl'.
  Qed.

  Definition declared_constraints_levels_union_left levels levels' cstrs :
    declared_constraints_levels levels cstrs
    declared_constraints_levels (LevelSet.union levels levels') cstrs.
  Proof.
    rewrite /declared_constraints_levels.
    intros hx x inx.
    specialize (hx x inx).
    destruct x as [[l d] r]. split.
    destruct hx. now eapply LevelSetFact.union_2.
    destruct hx.
    now eapply LevelSetFact.union_2.
  Qed.

  Definition declared_constraints_levels_union_right levels levels' cstrs :
    declared_constraints_levels levels' cstrs
    declared_constraints_levels (LevelSet.union levels levels') cstrs.
  Proof.
    rewrite /declared_constraints_levels.
    intros hx x inx.
    specialize (hx x inx).
    destruct x as [[l d] r].
    destruct hx; split. now eapply LevelSetFact.union_3.
    now eapply LevelSetFact.union_3.
  Qed.

  Definition declared_constraints_levels_subset levels levels' cstrs :
    declared_constraints_levels levels cstrs
    LevelSet.Subset levels levels'
    declared_constraints_levels levels' cstrs.
  Proof.
    rewrite /declared_constraints_levels.
    intros hx sub x inx.
    specialize (hx x inx). red in hx.
    destruct x as [[l d] r]; cbn in ×.
    split.
    red in inx.
    now eapply sub.
    now eapply sub.
  Qed.

  Lemma on_udecl_spec `{checker_flags} Σ (udecl : universes_decl) :
    on_udecl Σ udecl =
    let levels := levels_of_udecl udecl in
    let global_levels := global_levels Σ in
    let all_levels := LevelSet.union levels global_levels in
    fresh_levels global_levels levels
    ∧ declared_constraints_levels all_levels (constraints_of_udecl udecl)
    ∧ satisfiable_udecl Σ udecl.
  Proof. unfold on_udecl. reflexivity. Qed.

  Lemma on_udecl_prop_spec `{checker_flags} Σ (udecl : universes_decl) :
    on_udecl_prop Σ udecl =
      let levels := levels_of_udecl udecl in
      let global_levels := global_levels Σ in
      let all_levels := LevelSet.union levels global_levels in
      declared_constraints_levels all_levels (constraints_of_udecl udecl).
  Proof. reflexivity. Qed.

  Notation levels_of_list := LevelSetProp.of_list.

  Lemma levels_of_list_app l l' :
    levels_of_list (l ++ l') =
    LevelSet.union (levels_of_list l)
      (levels_of_list l').
  Proof.
    rewrite /LevelSetProp.of_list fold_right_app.
    induction l; cbn.
    apply LevelSet.eq_leibniz. red.
    rewrite LevelSet_union_empty //.
    apply LevelSet.eq_leibniz. red.
    rewrite IHl. rewrite LevelSetProp.union_add //.
  Qed.

  Definition aulevels inst cstrs :
    AUContext.levels (inst, cstrs) =
    LevelSetProp.of_list (unfold #|inst| Level.Var).
  Proof.
    cbn.
    now rewrite mapi_unfold.
  Qed.

  #[global] Instance unfold_proper {A} : Proper (eq ==> `=1` ==> eq) (@unfold A).
  Proof.
    intros x yf g eqfg.
    induction y; cbn; auto. f_equal; auto. f_equal. apply eqfg.
  Qed.


  Lemma unfold_add {A} n k (f : natA) : unfold (n + k) f = unfold k f ++ unfold n (fun xf (x + k)).
  Proof.
    induction n in k |- ×.
    cbn. now rewrite app_nil_r.
    cbn. rewrite IHn. now rewrite app_assoc.
  Qed.


  Definition unfold_levels_app n k :
    LevelSetProp.of_list (unfold (n + k) Level.Var) =
    LevelSet.union (LevelSetProp.of_list (unfold k Level.Var))
      (LevelSetProp.of_list (unfold n (fun iLevel.Var (k + i)))).
  Proof.
    rewrite unfold_add levels_of_list_app //.
    now setoid_rewrite Nat.add_comm at 1.
  Qed.

  Lemma levels_of_list_spec l ls :
    LevelSet.In l (levels_of_list ls) ↔ In l ls.
  Proof.
    now rewrite LevelSetProp.of_list_1 InA_In_eq.
  Qed.

  Lemma In_unfold k l n :
    In l (unfold n (λ i : nat, Level.Var (k + i))) ↔ ∃ k' : nat, l = Level.Var k'kk' < k + n.
  Proof.
    induction n; cbn ⇒ //. firstorder. lia.
    split. intros [] % in_app_or ⇒ //.
    eapply IHn in H as [k' [eq lt]]. subst l; k'. intuition lia.
    destruct H as []; subst ⇒ //.
     (k + n). intuition lia.
    intros [k' [-> lt]].
    apply/in_or_app.
    destruct (eq_dec k' (k + n)). subst k'.
    right ⇒ //. cbn; auto.
    left. eapply IHn. k'; intuition lia.
  Qed.

  Lemma In_levels_of_list k l n :
    LevelSet.In l (levels_of_list (unfold n (fun iLevel.Var (k + i)))) ↔
     k', l = Level.Var k'kk' < k + n.
  Proof.
    rewrite LevelSetProp.of_list_1 InA_In_eq. now apply In_unfold.
  Qed.

  Lemma In_lift_level k l n : LevelSet.In l (levels_of_list (unfold n (λ i : nat, Level.Var i))) ↔
    LevelSet.In (lift_level k l) (levels_of_list (unfold n (λ i : nat, Level.Var (k + i)))).
  Proof.
    split.
    - move/(In_levels_of_list 0) ⇒ [k' [-> l'lt]].
      eapply In_levels_of_list. (k + k'); cbn; intuition lia.
    - move/(In_levels_of_list k) ⇒ [k' [eq l'lt]].
      eapply (In_levels_of_list 0).
      destruct l; noconf eq. n0; cbn; intuition lia.
  Qed.

  Lemma not_var_lift l k s :
    LS.For_all (λ x : LS.elt, ~~ Level.is_var x) s
    LevelSet.In l s
    LevelSet.In (lift_level k l) s.
  Proof.
    intros.
    specialize (H _ H0). cbn in H.
    destruct l; cbn ⇒ //.
  Qed.

  Lemma declared_constraints_levels_lift s n k cstrs :
    LS.For_all (λ x : LS.elt, (negbLevel.is_var) x) s
    declared_constraints_levels
      (LevelSet.union (levels_of_list (unfold n (λ i : nat, Level.Var i))) s) cstrs
    declared_constraints_levels
      (LevelSet.union (levels_of_list (unfold n (λ i : nat, Level.Var (k + i)))) s)
      (lift_constraints k cstrs).
  Proof.
    rewrite /declared_constraints_levels.
    intros hs ha [[l d] r] inx.
    eapply In_lift_constraints in inx as [c' [eq incs]].
    specialize (ha _ incs). destruct c' as [[l' d'] r']; cbn in eq; noconf eq.
    destruct ha as [inl' inr'].
    apply LevelSetFact.union_1 in inl'. apply LevelSetFact.union_1 in inr'.
    split.
    - apply LevelSet.union_spec.
      destruct inl'.
      + left. now apply In_lift_level.
      + right. apply not_var_lift ⇒ //.
    - apply LevelSet.union_spec.
      destruct inr'.
      + left. now apply In_lift_level.
      + right. apply not_var_lift ⇒ //.
  Qed.

  Definition levels_of_cstr (c : ConstraintSet.elt) :=
    let '(l, d, r) := c in
    LevelSet.add l (LevelSet.add r LevelSet.empty).

  Definition levels_of_cstrs cstrs :=
    ConstraintSet.fold (fun c accLevelSet.union (levels_of_cstr c) acc) cstrs.

  Lemma levels_of_cstrs_acc l cstrs acc :
    LevelSet.In l accLevelSet.In l (levels_of_cstrs cstrs LevelSet.empty) ↔
    LevelSet.In l (levels_of_cstrs cstrs acc).
  Proof.
    rewrite /levels_of_cstrs.
    rewrite !ConstraintSet.fold_spec.
    induction (ConstraintSet.elements cstrs) in acc |- × ⇒ /=.
    split. intros []; auto. inversion H. firstorder.
    split.
    intros []. apply IHl0. left. now eapply LevelSetFact.union_3.
    apply IHl0 in H as []. apply IHl0. left.
    eapply LevelSet.union_spec. left.
    eapply LevelSet.union_spec in H. destruct H ⇒ //. inversion H.
    apply IHl0. right ⇒ //.
    intros. apply IHl0 in H as [].
    eapply LevelSet.union_spec in H. destruct H ⇒ //.
    right. apply IHl0. left. apply LevelSet.union_spec. now left.
    now left. right.
    eapply IHl0. now right.
  Qed.

  Lemma levels_of_cstrs_spec l cstrs :
    LevelSet.In l (levels_of_cstrs cstrs LevelSet.empty) ↔
     d r, ConstraintSet.In (l, d, r) cstrsConstraintSet.In (r, d, l) cstrs.
  Proof.
    rewrite -levels_of_cstrs_acc.
    split.
    - intros []. inversion H.
      move: H.
      rewrite /levels_of_cstrs.
      eapply ConstraintSetProp.fold_rec.
      + intros s' em inl. inversion inl.
      + intros x a s' s'' inx ninx na.
        intros.
        destruct x as [[l' d] r].
        eapply LevelSet.union_spec in H0 as [].
        eapply LevelSet.add_spec in H0 as []; subst.
         d, r. left. now apply na.
        eapply LevelSet.add_spec in H0 as []; subst.
         d, l'. right; now apply na. inversion H0.
        specialize (H H0) as [d' [r' h]].
         d', r'. red in na.
        destruct h. destruct (na (l, d', r')).
        firstorder. firstorder.

    - intros [d [r [indr|indr]]].
      rewrite /levels_of_cstrs. right.
      move: indr; eapply ConstraintSetProp.fold_rec.
      intros. now specialize (H _ indr).
      intros x a s' s'' inx inx' add inih ihih'.
      eapply LevelSet.union_spec.
      eapply add in ihih' as []; subst. left.
      eapply LevelSet.add_spec. now left. firstorder.
      right.
      rewrite /levels_of_cstrs.
      move: indr; eapply ConstraintSetProp.fold_rec.
      intros. now specialize (H _ indr).
      intros x a s' s'' inx inx' add inih ihih'.
      eapply LevelSet.union_spec.
      eapply add in ihih' as []; subst. left.
      eapply LevelSet.add_spec. right. eapply LevelSet.add_spec; now left. firstorder.
  Qed.

  Lemma declared_constraints_levels_in levels cstrs :
    LevelSet.Subset (levels_of_cstrs cstrs LevelSet.empty) levels
    declared_constraints_levels levels cstrs.
  Proof.
    rewrite /declared_constraints_levels.
    intros sub [[l d] r] inx. red in sub.
    split. apply (sub l). eapply levels_of_cstrs_spec. do 2 eexists; firstorder eauto.
    apply (sub r). eapply levels_of_cstrs_spec. do 2 eexists; firstorder eauto.
  Qed.

  Lemma In_variance_cstrs l d r v i i' :
    ConstraintSet.In (l, d, r) (variance_cstrs v i i') →
      (In l iIn l i') ∧ (In r iIn r i').
  Proof.
    induction v in i, i' |- *; destruct i, i'; intros; try solve [inversion H].
    cbn in H.
    destruct a. apply IHv in H. cbn. firstorder auto.
    eapply ConstraintSet.add_spec in H as []. noconf H. cbn; firstorder.
    eapply IHv in H; firstorder.
    eapply ConstraintSet.add_spec in H as []. noconf H. cbn; firstorder.
    eapply IHv in H; firstorder.
  Qed.

  Lemma In_lift l n k : In l (map (lift_level k) (unfold n Level.Var)) ↔
    In l (unfold n (fun iLevel.Var (k + i))).
  Proof.
    induction n; cbn; auto. firstorder.
    firstorder.
    move: H1; rewrite map_app.
    intros [] % in_app_or.
    apply/in_or_app. firstorder.
    apply/in_or_app. firstorder.
    move: H1; intros [] % in_app_or.
    rewrite map_app. apply/in_or_app. firstorder.
    rewrite map_app. apply/in_or_app. firstorder.
  Qed.