Upred is isomorphic to some kind of monotonous SProp predicate. (WIP)

theories/algebra/sprop.v

+From iris.algebra Require Export ofe.
+Set Default Proof Using "Type".
+
+Record sProp : Type := SProp {
+  sProp_holds :> nat → Prop;
+  sProp_closed n1 n2 : sProp_holds n1 → n2 ≤ n1 → sProp_holds n2
+}.
+Add Printing Constructor sProp.
+
+Section cofe.
+Instance sProp_dist : Dist sProp := λ n P Q,
+  ∀ n', n' ≤ n → P n' ↔ Q n'.
+
+Instance sProp_equiv : Equiv sProp := λ P Q,
+  ∀ n, P n ↔ Q n.
+
+Definition sProp_ofe_mixin : OfeMixin sProp.
+Proof.
+  split.
+  - intros x y; split=> Hxy n.
+    + intros n' Hn'. apply Hxy.
+    + by apply (Hxy n).
+  - split.
+    + by intros ???.
+    + intros x y Hxy n' Hn'. symmetry. by apply Hxy.
+    + intros x y z Hxy Hyz n' Hn'. by etrans; [apply Hxy|apply Hyz].
+  - intros n x y Hxy n' Hn'. apply Hxy. lia.
+Qed.
+Canonical Structure sPropC := OfeT sProp sProp_ofe_mixin.
+
+Program Definition sProp_compl : Compl sPropC := λ c,
+  {| sProp_holds n := c n n |}.
+Next Obligation.
+  move =>/= c n1 n2 Hc Hn. by eapply (chain_cauchy c _ _  Hn), sProp_closed.
+Qed.
+Global Program Instance sProp_cofe : Cofe sPropC := {| compl := sProp_compl |}.
+Next Obligation. intros n c n' Hn'. symmetry. by apply (chain_cauchy c). Qed.
+End cofe.
+
+Typeclasses Opaque sProp_dist sProp_equiv.
+
+Definition sProp_entails (P Q : sProp) : Prop := ∀ n, P n → Q n.
+Notation "P ⊢s Q" := (sProp_entails P Q)
+  (at level 99, Q at level 200, right associativity) : C_scope.
+
+Global Instance sProp_entails_po : PreOrder sProp_entails.
+Proof.
+  split.
+  - by intros P n.
+  - by intros P Q Q' HP HQ n ?; eapply HQ, HP.
+Qed.
+Global Instance sProp_entails_anti_sym : AntiSymm (equiv) sProp_entails.
+Proof. intros P Q HPQ HQP. split; auto. Qed.
+
+Lemma sProp_entails_lim (cP cQ : chain sPropC) :
+  (∀ n, cP n ⊢s cQ n) → compl cP ⊢s compl cQ.
+Proof. intros Hlim n HP. by apply (conv_compl n cQ), Hlim, (conv_compl n cP). Qed.
+
+Lemma limit_preserving_sProp_entails `{Cofe A} (Φ Ψ : A → sProp) :
+  NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢s Ψ x).
+Proof. intros HΦ HΨ c Hc n Hn. by eapply HΨ, Hc, HΦ, Hn; rewrite ?conv_compl. Qed.

theories/base_logic/upred_sprop.v

+From iris.algebra Require Export cmra sprop.
+From iris.base_logic Require Export upred.
+Set Default Proof Using "Type".
+
+Definition uPred_sPropC (M : ucmraT) : ofeT :=
+  sigC (λ P : M -n> sPropC,
+          (∀ x1 x2 n, x1 ≼{n} x2 → P x1 n → P x2 n) ∧
+          (∀ x n, (∀ n', n' ≤ n → ✓{n'} x → P x n') → P x n)).
+
+Instance uPred_sPropC_cofe M : Cofe (uPred_sPropC M).
+Proof.
+   eapply @sig_cofe, limit_preserving_and.
+  - intros c Hc x1 x2 n Hx Hn. by eapply (conv_compl _ c), Hc.
+  - intros c Hc x n Hn. specialize (Hc n x n).
+    apply (conv_compl n c), Hc=>// ???. apply (conv_compl _ c); auto.
+Qed.
+
+Program Definition uPred_of_sProp {M : ucmraT} (P : uPred_sPropC M) : uPred M :=
+  {| uPred_holds n x := `P x n |}.
+Next Obligation. move=>/= M P /= n x1 x2 H Hx. by eapply (proj2_sig P) in Hx. Qed.
+Next Obligation. move=>/= M P n1 n2 x ? Hn ?. by eapply sProp_closed. Qed.
+
+Instance uPred_of_sProp_proper M : Proper (equiv ==> equiv) (@uPred_of_sProp M).
+Proof. intros x y Hxy. constructor=>n' z Hv. by apply Hxy. Qed.
+Instance uPred_of_sProp_ne M : NonExpansive (@uPred_of_sProp M).
+Proof. intros n x y Hxy. constructor=>n' z Hn' Hv. by apply Hxy. Qed.
+
+Program Definition uPred_to_sProp {M} (P : uPred M) : uPred_sPropC M :=
+  λne x, {| sProp_holds n := ∀ n', n' ≤ n → ✓{n'}x → P n' x |}.
+Next Obligation. move=>/= M P x n1 n2 HP Hn n' Hn' Hv. apply HP; last done. lia. Qed.
+Next Obligation.
+  move=> M P n x1 x2 Hx n' Hn' /=. split=>H n'' Hn'' Hv.
+  - eapply uPred_mono.
+    { apply H; first done. eapply cmra_validN_ne, Hv. eapply dist_le. done. lia. }
+    exists ∅. rewrite right_id. eapply dist_le. done. lia.
+  - eapply uPred_mono.
+    { apply H; first done. eapply cmra_validN_ne, Hv. eapply dist_le. done. lia. }
+    exists ∅. rewrite right_id. eapply dist_le. done. lia.
+Qed.
+Next Obligation.
+  move=> M P /=. split; last by eauto.
+  move=> x1 x2 n Hx /= H n' Hn' Hv.
+  eapply uPred_mono, cmra_includedN_le, Hn'; last apply Hx.
+  by eapply H, cmra_validN_includedN, cmra_includedN_le.
+Qed.
+
+Instance uPred_to_sProp_proper M : Proper (equiv ==> equiv) (@uPred_to_sProp M).
+Proof. by move=>x y Hxy z n /=; split=>H n' Hn' Hv; apply Hxy, H. Qed.
+Instance uPred_to_sProp_ne M : NonExpansive (@uPred_to_sProp M).
+Proof. by move=>n x y Hxy z n' Hn' /=; split=>H n'' Hn'' Hv; apply Hxy, H=>//; lia. Qed.
+
+Lemma uPred_of_to_sProp M (P : uPred M) :
+  uPred_of_sProp (uPred_to_sProp P) ≡ P.
+Proof.
+  constructor=>n x Hv; split=>H.
+  - by apply H.
+  - intros n' Hn' ?. by eapply uPred_closed.
+Qed.
+
+Lemma uPred_to_of_sProp M (P : uPred_sPropC M) :
+  uPred_to_sProp (uPred_of_sProp P) ≡ P.
+Proof.
+  move=>x n /=. unfold uPred_holds=>/=; split.
+  - apply (proj2_sig P).
+  - intros. by eapply sProp_closed.
+Qed.