Prove that uPred is complete even if we remove the validity

restriction in uPred_closed.

theories/base_logic/double_negation.v

@@ -194,7 +194,6 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
                   eapply laterN_big; eauto. unseal.
                   eapply (Hnnupdk n k); first omega; eauto.
                   exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
-                  eapply cmra_validN_op_l; eauto.
       ** intros HP. eapply IHk; auto.
          move:HP. unseal. intros (?&?); naive_solver.
 Qed.
@@ -234,7 +233,7 @@ Proof.
     apply and_intro.
     * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
       rewrite nnupd_k_unfold. rewrite and_elim_l.
-      apply wand_intro_l. 
+      apply wand_intro_l.
       rewrite {1}(nnupd_k_intro (S k) (P -∗ ▷^(S k) (False)%I)).
       rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
     * do 2 rewrite nnupd_k_weaken //.

theories/base_logic/primitive.v

@@ -76,7 +76,7 @@ Next Obligation.
   by rewrite Hy Hx assoc.
 Qed.
 Next Obligation.
-  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
+  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?.
   exists x1, x2; ofe_subst; split_and!;
     eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
 Qed.

theories/base_logic/upred.v

@@ -14,35 +14,7 @@ Record uPred (M : ucmraT) : Type := IProp {
      it to only valid elements. *)
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
 
-  (* We have to restrict this to hold only for valid elements,
-     otherwise this condition is no longer limit preserving, and uPred
-     does no longer form a COFE (i.e., [uPred_compl] breaks). This is
-     because the distance and equivalence on this cofe ignores the
-     truth value on invalid elements. This, in turn, is required by
-     the fact that entailment has to ignore invalid elements, which is
-     itself essential for proving [ownM_valid].
-
-     We could, actually, remove this restriction and make this
-     condition apply even to invalid elements: we have proved that
-     uPred is isomorphic to a sub-COFE of the COFE of predicates that
-     are monotonous both with respect to the step index and with
-     respect to x. However, that would essentially require changing
-     (by making it more complicated) the model of many connectives of
-     the logic, which we don't want.
-     This sub-COFE is the sub-COFE of monotonous sProp predicates P
-     such that the following sProp assertion is valid:
-          ∀ x, (V(x) → P(x)) → P(x)
-     Where V is the validity predicate.
-
-     Another way of saying that this is equivalent to this definition of
-     uPred is to notice that our definition of uPred is equivalent to
-     quotienting the COFE of monotonous sProp predicates with the
-     following (sProp) equivalence relation:
-       P1 ≡ P2  :=  ∀ x, V(x) → (P1(x) ↔ P2(x))
-     whose equivalence classes appear to all have one only canonical
-     representative such that ∀ x, (V(x) → P(x)) → P(x).
- *)
-  uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
+  uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → uPred_holds n2 x
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
 Add Printing Constructor uPred.
@@ -55,6 +27,39 @@ Arguments uPred_holds {_} _%I _ _.
 Section cofe.
   Context {M : ucmraT}.
 
+  (* A good way of understanding this defintion of the uPred OFE is to
+     consider the OFE uPred0 of monotonous SProp predicates. That is,
+     uPred0 is the OFE of non-expanding functions from M to SProp that
+     are monotonous with respect to CMRA inclusion. This notion of
+     monotonicity has to be stated in the SProp logic. It is exactly
+     uPred_mono.
+
+     Then, we quotient uPred0 *in the sProp logic* with respect to
+     equivalence on valid elements of M. That is, we quotient with
+     respect to the following *sProp* equivalence relation:
+        P1 ≡ P2 := ∀ x, ✓ x → (P1(x) ↔ P2(x))       (1)
+     When seen from the ambiant logic, computing this logic require
+     redefinig both a custom Equiv and Dist.
+
+
+     It is worth noting that this equivalence relation admit canonical
+     representatives. More precisely, one can show that every
+     equivalence class contain exactly one element P0 such that:
+        ∀ x, (✓ x → P(x)) → P(x)                   (2)
+     (Again, this assertion has to be understood in sProp). Starting
+     from an element P of a given class, one can build this canonical
+     representative by chosing:
+        P0(x) = ✓ x → P(x)                         (3)
+
+     Hence, as an alternative definition of uPred, we could use the set
+     of canonical representatives (i.e., the subtype of monotonous
+     sProp predicates that verify (2)). This alternative definition would
+     save us from using a quotient. However, the definitions of the various
+     connectives would get more complicated, because we have to make sure
+     they all verify (2), which sometimes requires some adjustments. We would
+     moreover need to prove one more property for every logical connective.
+   *)
+
   Inductive uPred_equiv' (P Q : uPred M) : Prop :=
     { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
   Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
@@ -77,15 +82,20 @@ Section cofe.
   Canonical Structure uPredC : ofeT := OfeT (uPred M) uPred_ofe_mixin.
 
   Program Definition uPred_compl : Compl uPredC := λ c,
-    {| uPred_holds n x := c n n x |}.
-  Next Obligation. naive_solver eauto using uPred_mono. Qed.
+    {| uPred_holds n x := ∀ n', n' ≤ n → ✓{n'}x → c n' n' x |}.
+  Next Obligation.
+    move=> /= c n x1 x2 Hx1 Hx12 n' Hn'n Hv.
+    eapply uPred_mono. by eapply Hx1, cmra_validN_includedN, cmra_includedN_le.
+    by eapply cmra_includedN_le.
+  Qed.
   Next Obligation.
-    intros c n1 n2 x ???; simpl in *.
-    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
+    move=> /= c n1 n2 x Hc Hn12 n3 Hn23 Hv. apply Hc. lia. done.
   Qed.
   Global Program Instance uPred_cofe : Cofe uPredC := {| compl := uPred_compl |}.
   Next Obligation.
-    intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
+    intros n c; split=>i x Hin Hv.
+    etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
+    repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_closed.
   Qed.
 End cofe.
 Arguments uPredC : clear implicits.

theories/base_logic/upred_iso.v

+From iris.base_logic Require Export upred.
+
+Record sProp := SProp {
+  sProp_holds :> nat → Prop;
+  sProp_holds_mono : Proper (flip (≤) ==> impl) sProp_holds
+}.
+
+Existing Instance sProp_holds_mono.
+Instance sprop_holds_mono_flip (P : sProp) : Proper ((≤) ==> flip impl) P.
+Proof. solve_proper. Qed.
+
+Arguments sProp_holds _ _ : simpl never.
+Add Printing Constructor sProp.
+
+Section sProp_cofe.
+  Inductive sProp_equiv' (P Q : sProp) : Prop :=
+    { sProp_in_equiv : ∀ n, P n ↔ Q n }.
+  Instance sProp_equiv : Equiv sProp := sProp_equiv'.
+  Inductive sProp_dist' (n : nat) (P Q : sProp) : Prop :=
+    { sProp_in_dist : ∀ n', n' ≤ n → P n' ↔ Q n' }.
+  Instance sProp_dist : Dist sProp := sProp_dist'.
+  Definition sProp_ofe_mixin : OfeMixin sProp.
+  Proof.
+    split.
+    - intros P Q; split.
+      + intros HPQ n; split=>??; apply HPQ.
+      + intros HPQ; split=>?; eapply HPQ; auto.
+    - intros n; split.
+      + by intros P; split.
+      + by intros P Q HPQ; split=> ??; symmetry; apply HPQ.
+      + by intros P Q Q' HP HQ; split=> n' ?; trans (Q n'); [apply HP|apply HQ].
+    - intros n P Q HPQ; split=> ??. apply HPQ. auto.
+  Qed.
+  Canonical Structure sPropC : ofeT := OfeT (sProp) sProp_ofe_mixin.
+
+  Program Definition sProp_compl : Compl sPropC := λ c,
+    {| sProp_holds n := c n n |}.
+  Next Obligation.
+    move => c n1 n2 Hn12 /(sProp_holds_mono _ _ _ Hn12) H.
+    by apply (chain_cauchy c _ _ Hn12).
+  Qed.
+  Global Program Instance sProp_cofe : Cofe sPropC := {| compl := sProp_compl |}.
+  Next Obligation. intros n. split=>n' Hn'. symmetry. by apply (chain_cauchy c). Qed.
+End sProp_cofe.
+Arguments sPropC : clear implicits.
+
+Instance sProp_proper : Proper ((≡) ==> (=) ==> iff) sProp_holds.
+Proof. by move=> ??[?]??->. Qed.
+
+Global Instance limit_preserving_sprop `{Cofe A} (P : A → sPropC) :
+  NonExpansive P → LimitPreserving (λ x, ∀ n, P x n).
+Proof.
+  intros ? c Hc n. specialize (Hc n n).
+  assert (Hcompl : P (compl c) ≡{n}≡ P (c n)) by by rewrite (conv_compl n c).
+  by apply Hcompl.
+Qed.
+
+Section uPred1.
+
+Context {M : ucmraT}.
+
+(* TODO : use logical connectives in sProp *)
+Program Definition uPred1_valid (P : M -n> sPropC) : sPropC :=
+  SProp (λ n, ∀ n', n' ≤ n →
+         (∀ x1 x2, x1 ≼{n'} x2 → P x1 n' → P x2 n') ∧
+         (∀ x, (∀ n'', n'' ≤ n' → ✓{n''} x → P x n'') → P x n')) _.
+Next Obligation. move=>??? /= H. by setoid_rewrite H. Qed.
+Instance uPred1_valid_ne : NonExpansive uPred1_valid.
+Proof.
+  split=>??. repeat ((apply forall_proper=>?) || f_equiv).
+  - split=> HH ?; apply H, HH, H=>//; lia.
+  - split=> HH ?; (apply H, HH; [lia|])=> ???; (apply H; [lia|auto]).
+Qed.
+
+Definition uPred1 :=
+  sigC (λ (P : M -n> sPropC), ∀ n, uPred1_valid P n).
+Global Instance uPred1_cofe : Cofe uPred1.
+Proof. eapply @sig_cofe, limit_preserving_sprop, _. Qed.
+
+Program Definition uPred_of_uPred1 (P : uPred1) : uPred M :=
+  {| uPred_holds n x := `P x n |}.
+Next Obligation.
+  intros P ?????. by eapply (proj1 (proj2_sig P _ _ (le_refl _))).
+Qed.
+Next Obligation. move => /= ????? Hle. by rewrite ->Hle. Qed.
+
+Global Instance uPred_of_uPred1_ne : NonExpansive uPred_of_uPred1.
+Proof.
+  move=>??? EQ. split=>? x ??. specialize (EQ x). by split=>H; apply EQ.
+Qed.
+Global Instance uPred_of_uPred1_proper : Proper ((≡) ==> (≡)) uPred_of_uPred1.
+Proof. apply (ne_proper _). Qed.
+
+Program Definition uPred1_of_uPred (P : uPred M) : uPred1 :=
+  λne x, SProp (λ n, ∀ n', n' ≤ n → ✓{n'}x → P n' x) _.
+Next Obligation. move => ???? /= Hle ?. by setoid_rewrite -> Hle. Qed. 
+Next Obligation.
+  move => ???? H. split=>??. do 2 apply forall_proper=>?.
+  split=>HH ?;
+    (eapply uPred_ne; [eapply dist_le; [by symmetry|lia]|]);
+    (eapply HH, cmra_validN_ne; [eapply dist_le|]=>//; lia).
+Qed.
+Next Obligation.
+  split.
+  - move=>??? HP ???. eapply uPred_mono, cmra_includedN_le=>//.
+    eapply HP, cmra_validN_includedN=>//. eapply cmra_includedN_le=>//.
+  - move=>? HP ???. by eapply HP.
+Qed.
+
+Global Instance uPred1_of_uPred_ne : NonExpansive uPred1_of_uPred.
+Proof.
+  move=>??? EQ. split=>??. do 3 apply forall_proper=>?. apply EQ=>//. lia.
+Qed.
+Global Instance uPred1_of_uPred_proper : Proper ((≡) ==> (≡)) uPred1_of_uPred.
+Proof. apply (ne_proper _). Qed.
+
+Lemma uPred1_of_uPred_of_uPred1 P : uPred1_of_uPred (uPred_of_uPred1 P) ≡ P.
+Proof.
+  split=>?; split=>HP.
+  - apply (proj2 (proj2_sig P _ _ (le_refl _)))=>???. by apply HP.
+  - move=>? Hle ?. unfold uPred_holds=>/=. by rewrite ->Hle.
+Qed.
+
+Lemma uPred_of_uPred1_of_uPred P : uPred_of_uPred1 (uPred1_of_uPred P) ≡ P.
+Proof.
+  split=>?; split=>HP.
+  - by apply HP.
+  - move=>???. by eapply uPred_closed.
+Qed.
+
+End uPred1.
+Arguments  uPred1 _ : clear implicits.
+
+Section uPred2.
+Context {M : ucmraT}.
+
+Record uPred2 : Type := IProp {
+  uPred2_holds :> M → sProp;
+  uPred2_mono n x1 x2 : uPred2_holds x1 n → x1 ≼{n} x2 → uPred2_holds x2 n
+}.
+
+Section cofe.
+  Inductive uPred2_equiv' (P Q : uPred2) : Prop :=
+    { uPred_in_equiv : ∀ n x, ✓{n} x → P x n ↔ Q x n }.
+  Instance uPred2_equiv : Equiv uPred2 := uPred2_equiv'.
+  Inductive uPred2_dist' (n : nat) (P Q : uPred2) : Prop :=
+    { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P x n' ↔ Q x n' }.
+  Instance uPred_dist : Dist uPred2 := uPred2_dist'.
+  Definition uPred2_ofe_mixin : OfeMixin uPred2.
+  Proof.
+    split.
+    - intros P Q; split.
+      + by intros HPQ n; split=> i x ??; apply HPQ.
+      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
+    - intros n; split.
+      + by intros P; split=> x i.
+      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+      + intros P Q Q' HP HQ; split=> i x ??.
+        by trans (Q x i);[apply HP|apply HQ].
+    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
+  Qed.
+  Canonical Structure uPred2C : ofeT := OfeT uPred2 uPred2_ofe_mixin.
+
+  Program Definition uPred2_compl : Compl uPred2C := λ c,
+    {| uPred2_holds x := SProp (λ n, ∀ n', n' ≤ n → ✓{n'}x → c n x n') _ |}.
+  Next Obligation.
+    move => c ? n1 n2 /= Hn12 H ???. apply (chain_cauchy c _ _ Hn12)=>//.
+    apply H. lia. done.
+  Qed.
+  Next Obligation.
+    move => ???? HH ????. eapply uPred2_mono, cmra_includedN_le=>//.
+    apply HH=>//. eapply cmra_validN_includedN=>//.
+    by eapply cmra_includedN_le.
+  Qed.
+  Global Program Instance uPred2_cofe :
+    Cofe uPred2C := {| compl := uPred2_compl |}.
+  Next Obligation.
+    intro n. split. move => ?? Hle. split=>HP.
+    - apply (chain_cauchy c _ _ Hle)=>//. by apply HP.
+    - move=> ???. eapply sProp_holds_mono=>//.
+      eapply (chain_cauchy c _ n), HP=>//.
+  Qed.
+End cofe.
+
+Program Definition uPred2_of_uPred1 (P : uPred1 M) : uPred2 :=
+  {| uPred2_holds x := `P x |}.
+Next Obligation.
+  move=>/= P ?????. by eapply (proj1 (proj2_sig P _ _ (le_refl _))).
+Qed.
+Global Instance uPred2_of_uPred1_ne : NonExpansive uPred2_of_uPred1.
+Proof. move=>??? EQ. split=>????. by apply EQ. Qed.
+Global Instance uPred2_of_uPred1_proper : Proper ((≡) ==> (≡)) uPred2_of_uPred1.
+Proof. apply (ne_proper _). Qed.
+
+Program Definition uPred1_of_uPred2 (P : uPred2) : uPred1 M :=
+  λne x, SProp (λ n, ∀ n', n' ≤ n → ✓{n'}x → P x n') _.
+Next Obligation. move=>???? HLE ??. rewrite <-HLE. auto. Qed.
+Next Obligation.
+  split=>??. do 2 apply forall_proper=>?.
+  split=>HH ?; (eapply uPred2_mono, cmra_includedN_le;
+   [eapply HH, cmra_validN_ne; [eapply dist_le; [done|lia]|done]|
+                                by rewrite H|lia]).
+Qed.
+Next Obligation.
+  split.
+  - move=>??? HH ???. eapply uPred2_mono; [|by eapply cmra_includedN_le].
+    by eapply HH, cmra_validN_includedN, cmra_includedN_le.
+  - move=>? HH ???. by eapply HH.
+Qed.
+Global Instance uPred1_of_uPred2_ne : NonExpansive uPred1_of_uPred2.
+Proof.
+  move=> ??? EQ. split=>??. do 3 eapply forall_proper=>?.
+  apply EQ. lia. done.
+Qed.
+
+Lemma uPred1_of_uPred2_of_uPred1 P : uPred1_of_uPred2 (uPred2_of_uPred1 P) ≡ P.
+Proof.
+  split=>?. split=>HP.
+  - apply (proj2 (proj2_sig P _ _ (le_refl _))). intros. by apply HP.
+  - intros ???. by eapply sProp_holds_mono, HP.
+Qed.
+
+Lemma uPred2_of_uPred1_of_uPred2 P : uPred2_of_uPred1 (uPred1_of_uPred2 P) ≡ P.
+Proof.
+  split=>?. split=>HP.
+  - by apply HP.
+  - intros ???. by eapply sProp_holds_mono, HP.
+Qed.
+
+End uPred2.
+Arguments uPred2 _ : clear implicits.
+Arguments uPred2C _ : clear implicits.