Internalize specs of valid and equiv for all cofe/cmras.

(missed practically everything in the previous commit)

algebra/agree.v

@@ -131,7 +131,7 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
 Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 
 (** Internalized properties *)
-Lemma agree_valid_uPred {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
+Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
 Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
 End agree.
 

algebra/auth.v

 From algebra Require Export excl.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -131,6 +131,18 @@ Qed.
 Canonical Structure authRA : cmraT :=
   CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
 
+(** Internalized properties *)
+Lemma auth_equivI {M} (x y : auth A) :
+  (x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
+Proof. done. Qed.
+Lemma auth_validI {M} (x : auth A) :
+  (✓ x)%I ≡ (match authoritative x with
+             | Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
+             | ExclUnit => ✓ own x
+             | ExclBot => False
+             end : uPred M)%I.
+Proof. by destruct x as [[]]. Qed.
+
 (** The notations ◯ and ● only work for CMRAs with an empty element. So, in
 what follows, we assume we have an empty element. *)
 Context `{Empty A, !CMRAIdentity A}.

algebra/excl.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -138,6 +138,18 @@ Proof.
   by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
 Qed.
 
+(** Internalized properties *)
+Lemma excl_equivI {M} (x y : excl A) :
+  (x ≡ y)%I ≡ (match x, y with
+               | Excl a, Excl b => a ≡ b
+               | ExclUnit, ExclUnit | ExclBot, ExclBot => True
+               | _, _ => False
+               end : uPred M)%I.
+Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Lemma excl_validI {M} (x : excl A) :
+  (✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
+Proof. by destruct x. Qed.
+
 (** ** Local updates *)
 Global Instance excl_local_update b :
   LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).

algebra/fin_maps.v

 From algebra Require Export cmra option.
 From prelude Require Export gmap.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
@@ -85,6 +85,7 @@ Arguments mapC _ {_ _} _.
 (* CMRA *)
 Section cmra.
 Context `{Countable K} {A : cmraT}.
+Implicit Types m : gmap K A.
 
 Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
@@ -160,6 +161,12 @@ Proof.
   * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   * apply map_empty_timeless.
 Qed.
+
+(** Internalized properties *)
+Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.
+Proof. done. Qed.
+Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
+Proof. done. Qed.
 End cmra.
 
 Arguments mapRA _ {_ _} _.

algebra/iprod.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 (** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
@@ -169,6 +169,12 @@ Section iprod_cmra.
     * by apply _.
   Qed.
 
+  (** Internalized properties *)
+  Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
+  Proof. done. Qed.
+  Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
+  Proof. done. Qed.
+
   (** Properties of iprod_insert. *)
   Context `{∀ x x' : A, Decision (x = x')}.
 

algebra/option.v

 From algebra Require Export cmra.
-From algebra Require Import functor.
+From algebra Require Import functor upred.
 
 (* COFE *)
 Section cofe.
@@ -121,6 +121,7 @@ Canonical Structure optionRA :=
 Global Instance option_cmra_identity : CMRAIdentity optionRA.
 Proof. split. done. by intros []. by inversion_clear 1. Qed.
 
+(** Misc *)
 Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
 Proof.
   destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
@@ -130,6 +131,17 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
 Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
 Proof. by destruct mx, my; inversion_clear 1. Qed.
 
+(** Internalized properties *)
+Lemma option_equivI {M} (x y : option A) :
+  (x ≡ y)%I ≡ (match x, y with
+               | Some a, Some b => a ≡ b | None, None => True | _, _ => False
+               end : uPred M)%I.
+Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
+Lemma option_validI {M} (x : option A) :
+  (✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
+Proof. by destruct x. Qed.
+
+(** Updates *)
 Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
   x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
 Proof.

algebra/upred.v

@@ -790,7 +790,7 @@ Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
-(* Own and valid *)
+(* Own *)
 Lemma ownM_op (a1 a2 : M) :
   uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
 Proof.
@@ -813,17 +813,29 @@ Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
 Proof. intros x n ??. by exists x; simpl. Qed.
 Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
 Proof. intros x n ??; by  exists x; rewrite left_id. Qed.
+
+(* Valid *)
 Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
 Proof. intros x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
 Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
 Proof. intros Ha x n ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma valid_mono {A B : cmraT} (a : A) (b : B) :
-  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊑ ✓ b.
-Proof. by intros ? x n ?; simpl; auto. Qed.
 Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
 Proof. done. Qed.
+Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
+Proof. intros r n _; apply cmra_validN_op_l. Qed.
+
+Lemma prod_equivI {A B : cofeT} (x y : A * B) :
+  (x ≡ y)%I ≡ (x.1 ≡ y.1 ∧ x.2 ≡ y.2 : uPred M)%I.
+Proof. done. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) :
+  (✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
+Proof. done. Qed.
+Print later.
+Lemma later_equivI {A : cofeT} (x y : later A) :
+  (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
+Proof. done. Qed.
 
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.

program_logic/auth.v

@@ -3,18 +3,16 @@ From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
 Section auth.
+  Context {Λ : language} {Σ : iFunctorG}.
   Context {A : cmraT} `{Empty A, !CMRAIdentity A} `{!∀ a : A, Timeless a}.
-  Context {Λ : language} {Σ : iFunctorG} (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
-  Context (N : namespace) (φ : A → iPropG Λ Σ).
+  Context (AuthI : gid) `{!InG Λ Σ AuthI (authRA A)}.
+  Context (N : namespace).
+  Context (φ : A → iPropG Λ Σ) {Hφ : ∀ n, Proper (dist n ==> dist n) φ}.
 
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types a b : A.
   Implicit Types γ : gname.
 
-  (* TODO: Need this to be proven somewhere. *)
-  Hypothesis auth_valid :
-    forall a b, (✓ Auth (Excl a) b : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').
-
   Definition auth_inv (γ : gname) : iPropG Λ Σ :=
     (∃ a, own AuthI γ (● a) ★ φ a)%I.
   Definition auth_own (γ : gname) (a : A) : iPropG Λ Σ := own AuthI γ (◯ a).
@@ -39,15 +37,14 @@ Section auth.
     True ⊑ pvs E E (auth_own γ ∅).
   Proof. by rewrite own_update_empty /auth_own. Qed.
 
-  Context {Hφ : ∀ n, Proper (dist n ==> dist n) φ}.
-
   Lemma auth_opened E a γ :
     (▷auth_inv γ ★ auth_own γ a) ⊑ pvs E E (∃ a', ▷φ (a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a)).
   Proof.
     rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
     rewrite later_sep [(▷own _ _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
     rewrite /auth_own [(_ ★ ▷φ _)%I]comm -assoc -own_op.
-    rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
+    rewrite own_valid_r auth_validI /= and_elim_l !sep_exist_l /=.
+    apply exist_elim=>a'.
     rewrite [∅ ⋅ _]left_id -(exist_intro a').
     apply (eq_rewrite b (a ⋅ a')
               (λ x, ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I); first by solve_ne.
@@ -58,7 +55,7 @@ Section auth.
 
   Lemma auth_closing E `{!LocalUpdate Lv L} a a' γ :
     Lv a → ✓ (L a ⋅ a') →
-    (▷φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
+    (▷ φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
     ⊑ pvs E E (▷auth_inv γ ★ auth_own γ (L a)).
   Proof.
     intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a ⋅ a')).

program_logic/ghost_ownership.v

@@ -34,11 +34,6 @@ Implicit Types a : A.
 (** * Properties of to_globalC *)
 Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
 Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
-Lemma to_globalF_validN n γ a : ✓{n} to_globalF i γ a ↔ ✓{n} a.
-Proof.
-  by rewrite /to_globalF
-    iprod_singleton_validN map_singleton_validN cmra_transport_validN.
-Qed.
 Lemma to_globalF_op γ a1 a2 :
   to_globalF i γ (a1 ⋅ a2) ≡ to_globalF i γ a1 ⋅ to_globalF i γ a2.
 Proof.
@@ -75,7 +70,10 @@ Lemma always_own_unit γ a : (□ own i γ (unit a))%I ≡ own i γ (unit a).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
 Lemma own_valid γ a : own i γ a ⊑ ✓ a.
 Proof.
-  rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalF_validN.
+  rewrite /own ownG_valid /to_globalF.
+  rewrite iprod_validI (forall_elim i) iprod_lookup_singleton.
+  rewrite map_validI (forall_elim γ) lookup_singleton option_validI.
+  by destruct inG.
 Qed.
 Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r _ _), own_valid. Qed.

program_logic/ownership.v

@@ -55,9 +55,11 @@ Proof.
   apply uPred.always_ownM.
   by rewrite Res_unit !cmra_unit_empty -{2}(cmra_unit_idemp m).
 Qed.
-Lemma ownG_valid m : (ownG m) ⊑ (✓ m).
-Proof. by rewrite /ownG uPred.ownM_valid; apply uPred.valid_mono=> n [? []]. Qed.
-Lemma ownG_valid_r m : (ownG m) ⊑ (ownG m ★ ✓ m).
+Lemma ownG_valid m : ownG m ⊑ ✓ m.
+Proof.
+  rewrite /ownG uPred.ownM_valid res_validI /= option_validI; auto with I.
+Qed.
+Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
 Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.

program_logic/resources.v

 From algebra Require Export fin_maps agree excl functor.
+From algebra Require Import upred.
 From program_logic Require Export language.
 
 Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
@@ -154,20 +155,23 @@ Proof.
 Qed.
 Lemma lookup_wld_op_r n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
-Proof.
-  rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l.
-Qed.
+Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
 Global Instance Res_timeless eσ m : Timeless m → Timeless (Res ∅ eσ m).
 Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
+
+(** Internalized properties *)
+Lemma res_equivI {M} r1 r2 :
+  (r1 ≡ r2)%I ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M)%I.
+Proof. split. by destruct 1. by intros (?&?&?); constructor. Qed.
+Lemma res_validI {M} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M)%I.
+Proof. done. Qed.
 End res.
 
 Arguments resC : clear implicits.
 Arguments resRA : clear implicits.
 
 Definition res_map {Λ Σ A B} (f : A -n> B) (r : res Λ Σ A) : res Λ Σ B :=
-  Res (agree_map f <$> wld r)
-      (pst r)
-      (ifunctor_map Σ f <$> gst r).
+  Res (agree_map f <$> wld r) (pst r) (ifunctor_map Σ f <$> gst r).
 Instance res_map_ne Λ Σ (A B : cofeT) (f : A -n> B) :
   (∀ n, Proper (dist n ==> dist n) f) →
   ∀ n, Proper (dist n ==> dist n) (@res_map Λ Σ _ _ f).