sigT forms an Iris Cofe, very different from sig

sigT_cofe.v

From iris.algebra Require Import ofe.

Import EqNotations.
Unset Program Cases.

(* Subsumed by https://gitlab.mpi-sws.org/iris/stdpp/commit/4978faed45d1a1d84f79d3ec0456dd55d831b684 *)
Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P :=
  let '(ex_intro _ x _) := p in x.
Definition proj2_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : Q (proj1_ex p) :=
  let '(ex_intro _ x H) := p in H.

(** SigmaT *)
Section sigmaT.
  (* Assume UIP on A, e.g. from decidable equality. *)
  Context {A : Type} {HpiA: ∀ x y : A, ProofIrrel (x = y)} {P : A → ofeT}.
  Implicit Types x : sigT P.

  Instance sig_equiv : Equiv (sigT P) := λ x1 x2,
    ∃ eq : projT1 x1 = projT1 x2 , rew eq in projT2 x1 ≡ projT2 x2.
  Instance sig_dist : Dist (sigT P) := λ n x1 x2,
    ∃ eq : projT1 x1 = projT1 x2 , rew eq in projT2 x1 ≡{n}≡ projT2 x2.

  Definition sigT_equiv_alt x1 x2 : x1 ≡ x2 ↔
    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡ projT2 x2 :=
      reflexivity _.
  Definition sigT_equiv_proj1 x y : x ≡ y → projT1 x = projT1 y := proj1_ex.

  Definition sigT_dist_alt n x1 x2 : x1 ≡{n}≡ x2 ↔
    ∃ eq : projT1 x1 = projT1 x2, rew eq in projT2 x1 ≡{n}≡ projT2 x2 :=
      reflexivity _.
  Definition sigT_dist_proj1 n {x y} : x ≡{n}≡ y → projT1 x = projT1 y := proj1_ex.

  Lemma existT_ne n i1 i2 (v1 : P i1) (v2 : P i2) :
    ∀ (eq : i1 = i2), (rew f_equal P eq in v1 ≡{n}≡ v2) →
      existT i1 v1 ≡{n}≡ existT i2 v2.
  Proof. intros ->. move => /= Heq2. exists eq_refl => /=. done. Qed.

  Definition sigT_ofe_mixin : OfeMixin (sigT P).
  Proof.
    split.
    - move => [x Px] [y Py] /=.
      setoid_rewrite sigT_dist_alt; rewrite sigT_equiv_alt /=; split.
      + destruct 1 as [-> Heq]. exists eq_refl => /=.
        by apply equiv_dist.
      + intros Heq. destruct (Heq 0) as [-> _]. exists eq_refl => /=.
        apply equiv_dist => n. case: (Heq n) => [Hrefl].
        have -> //=: Hrefl = eq_refl y. exact: proof_irrel.
    - move => n; split; move; setoid_rewrite sigT_dist_alt.
      + intros. by exists eq_refl.
      + move => [xa x] [ya y] /=. destruct 1 as [-> Heq]. exists eq_refl => /=.
        by symmetry.
      + move => [xa x] [ya y] [za z] /=.
        destruct 1 as [-> Heq1].
        destruct 1 as [-> Heq2]. exists eq_refl => /=. by trans y.
    - setoid_rewrite sigT_dist_alt.
      move => n [xa x] [ya y] /=. destruct 1 as [-> Heq].
      exists eq_refl. exact: dist_S.
  Qed.

  Canonical Structure sigTC : ofeT := OfeT (sigT P) sigT_ofe_mixin.

  Implicit Types (c : chain sigTC).
  Global Instance sig_discrete (x : sigT P) : Discrete (projT2 x) → Discrete x.
  Proof.
    move: x => [xa x] ? [ya y].
    rewrite sigT_dist_alt sigT_equiv_alt /=. destruct 1 as [-> Hxy].
    exists eq_refl. move: Hxy => /=. exact: (discrete _).
  Qed.
  Global Instance sig_ofe_discrete : (∀ a, OfeDiscrete (P a)) → OfeDiscrete sigTC.
  Proof. intros ??. apply _. Qed.

  Lemma idx_cast c n : projT1 (c n) = projT1 (c 0).
  Proof. refine (sigT_dist_proj1 _ (chain_cauchy c 0 n _)). lia. Qed.

  Program Definition chain_map_snd c : chain (P (projT1 (c 0))) :=
    {| chain_car n := rew (idx_cast c n) in projT2 (c n) |}.
  Next Obligation.
    move => c n i Hle /=.
    (* [Hgoal] is our thesis, up to casts: *)
    case: (chain_cauchy c n i Hle) => [Heqin Hgoal] /=.
    (* Pretty delicate. We have two casts to [projT1 (c 0)].
       We replace those by one cast. *)
    move: (idx_cast c i) (idx_cast c n) => Heqi0 Heqn0.
    (* Rewrite [projT1 (c 0)] to [projT1 (c n)] in goal and [Heqi0]: *)
    destruct Heqn0; cbn.
    have {Heqi0} -> /= : Heqi0 = Heqin; first exact: proof_irrel.
    exact Hgoal.
  Qed.

  Section cofe.
    Context `{Hcofe: ∀ a, Cofe (P a)}.
    Definition sigT_compl : Compl sigTC :=
      λ c, existT (projT1 (chain_car c 0)) (compl (chain_map_snd c)).

    Lemma idx_cast_compl {c n} : projT1 (sigT_compl c) = projT1 (c n).
    Proof. rewrite /sigT_compl /= idx_cast //. Defined.

    Global Program Instance sigT_cofe : Cofe sigTC := { compl := sigT_compl }.
    Next Obligation.
      intros n c. rewrite /sigT_compl sigT_dist_alt /=.
      exists (symmetry (idx_cast c n)).
      (* Our thesis, up to casts: *)
      pose proof (conv_compl n (chain_map_snd c)) as Hgoal.
      move: (compl (chain_map_snd c)) Hgoal => pc0 /=.
      destruct (idx_cast c n); cbn. done.
    Qed.
  End cofe.
End sigmaT.

Global Arguments sigTC {_ _} _.

Section sigmaT_cf.
  Context {A : Type} {HpiA: ∀ x y : A, ProofIrrel (x = y)} {F : A → cFunctor}.

  Program Definition sigT_map {P1 P2 : A → ofeT} :
    ofe_funC (λ a, P1 a -n> P2 a) -n>
    sigTC P1 -n> sigTC P2 :=
    λne f '(existT x px), existT x (f _ px).
  Next Obligation.
    move => ?? f n [x px] [y py] [/= Heq]. destruct Heq; cbn.
    exists eq_refl; cbn. by f_equiv.
  Qed.
  Next Obligation.
    move => ?? n f g Heq [x px] /=. exists eq_refl; cbn. apply Heq.
  Qed.

  Program Definition sigT_CF : cFunctor := {|
    cFunctor_car A CA B CB := sigTC (λ a, cFunctor_car (F a) A _ B CB);
    cFunctor_map A1 _ A2 _ B1 _ B2 _ fg := (sigT_map (λ a, cFunctor_map (F a) fg))
  |}.
  Next Obligation.
    repeat intro; cbn; case_match; exists eq_refl => /=.
    solve_proper.
  Qed.
  Next Obligation.
    cbn; intros; case_match; exists eq_refl => /=. apply cFunctor_id.
  Qed.
  Next Obligation.
    cbn; intros; case_match; exists eq_refl => /=. apply cFunctor_compose.
  Qed.

  Global Instance sigT_CF_contractive :
    (∀ a, cFunctorContractive (F a)) → cFunctorContractive sigT_CF.
  Proof.
    repeat intro. apply sigT_map => a. exact: cFunctor_contractive.
  Qed.
End sigmaT_cf.
Arguments sigT_CF {_ _} _%CF.

Notation "{ x  &  P }" := (sigT_CF (fun x => P%CF)) : cFunctor_scope.
Notation "{ x : A &  P }" := (@sigT_CF A%type (fun x => P%CF)) : cFunctor_scope.