Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/auth.v

@@ -69,7 +69,7 @@ Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
 Instance auth_validN : ValidN (auth A) := λ n x,
   match authoritative x with
   | Excl a => own x ≼{n} a ∧ ✓{n} a
-  | ExclUnit => ✓{n} (own x)
+  | ExclUnit => ✓{n} own x
   | ExclBot => False
   end.
 Global Arguments auth_validN _ !_ /.
@@ -91,9 +91,9 @@ Proof.
   split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
   intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
 Qed.
-Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} (authoritative x).
+Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} authoritative x.
 Proof. by destruct x as [[]]. Qed.
-Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} (own x).
+Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} own x.
 Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
 
 Definition auth_cmra_mixin : CMRAMixin (auth A).
@@ -158,7 +158,7 @@ Proof.
 Qed.
 
 Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
-  Lv a → ✓ (L a') →
+  Lv a → ✓ L a' →
   ● a' ⋅ ◯ a ~~> ● L a' ⋅ ◯ L a.
 Proof.
   intros. apply auth_update=>n af ? EQ; split; last done.

algebra/cmra.v

@@ -20,11 +20,12 @@ Infix "⩪" := minus (at level 40) : C_scope.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Instance: Params (@validN) 3.
-Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
+Notation "✓{ n } x" := (validN n x)
+  (at level 20, n at level 1, format "✓{ n }  x").
 
 Class Valid (A : Type) := valid : A → Prop.
 Instance: Params (@valid) 2.
-Notation "✓" := valid (at level 1) : C_scope.
+Notation "✓ x" := (valid x) (at level 20) : C_scope.
 Instance validN_valid `{ValidN A} : Valid A := λ x, ∀ n, ✓{n} x.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
@@ -37,7 +38,7 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
   (* setoids *)
   mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
   mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
-  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (✓{n});
+  mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
   mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
   (* valid *)
   mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
@@ -133,7 +134,7 @@ Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
-  validN_preserving n x : ✓{n} x → ✓{n} (f x)
+  validN_preserving n x : ✓{n} x → ✓{n} f x
 }.
 
 (** * Local updates *)
@@ -225,9 +226,9 @@ Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
 Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
 Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
 Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
-Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} (unit x).
+Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} unit x.
 Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
-Lemma cmra_unit_valid x : ✓ x → ✓ (unit x).
+Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
 Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
 
 (** ** Order *)
@@ -404,7 +405,7 @@ Section cmra_monotone.
   Proof.
     rewrite !cmra_included_includedN; eauto using includedN_preserving.
   Qed.
-  Lemma valid_preserving x : ✓ x → ✓ (f x).
+  Lemma valid_preserving x : ✓ x → ✓ f x.
   Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
 End cmra_monotone.
 
@@ -424,9 +425,9 @@ Section cmra_transport.
   Proof. by destruct H. Qed.
   Lemma cmra_transport_unit x : T (unit x) = unit (T x).
   Proof. by destruct H. Qed.
-  Lemma cmra_transport_validN n x : ✓{n} (T x) ↔ ✓{n} x.
+  Lemma cmra_transport_validN n x : ✓{n} T x ↔ ✓{n} x.
   Proof. by destruct H. Qed.
-  Lemma cmra_transport_valid x : ✓ (T x) ↔ ✓ x.
+  Lemma cmra_transport_valid x : ✓ T x ↔ ✓ x.
   Proof. by destruct H. Qed.
   Global Instance cmra_transport_timeless x : Timeless x → Timeless (T x).
   Proof. by destruct H. Qed.
@@ -444,7 +445,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
   (* setoids *)
   ra_op_ne (x : A) : Proper ((≡) ==> (≡)) (op x);
   ra_unit_ne :> Proper ((≡) ==> (≡)) unit;
-  ra_validN_ne :> Proper ((≡) ==> impl) ✓;
+  ra_validN_ne :> Proper ((≡) ==> impl) valid;
   ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
   (* monoid *)
   ra_associative :> Associative (≡) (⋅);
@@ -502,7 +503,7 @@ Section prod.
   Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
   Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
   Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
-  Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} (x.1) ∧ ✓{n} (x.2).
+  Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} x.1 ∧ ✓{n} x.2.
   Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
   Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
   Proof.

algebra/cmra_big_op.v

@@ -71,8 +71,7 @@ Proof.
   rewrite Hxy -big_opM_insert; last auto using lookup_delete.
   by rewrite insert_delete.
 Qed.
-Lemma big_opM_lookup_valid n m i x :
-  ✓{n} (big_opM m) → m !! i = Some x → ✓{n} x.
+Lemma big_opM_lookup_valid n m i x : ✓{n} big_opM m → m !! i = Some x → ✓{n} x.
 Proof.
   intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
   apply cmra_validN_op_l.

algebra/dra.v

@@ -26,7 +26,7 @@ Proof.
     split; [|intros; transitivity y]; tauto.
 Qed.
 Instance validity_valid_proper `{Equiv A} (P : A → Prop) :
-  Proper ((≡) ==> iff) (✓ : validity P → Prop).
+  Proper ((≡) ==> iff) (valid : validity P → Prop).
 Proof. intros ?? [??]; naive_solver. Qed.
 
 Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
@@ -43,7 +43,7 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
   dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
   (* validity *)
   dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  dra_unit_valid x : ✓ x → ✓ (unit x);
+  dra_unit_valid x : ✓ x → ✓ unit x;
   dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x);
   (* monoid *)
   dra_associative :> Associative (≡) (⋅);
@@ -83,8 +83,8 @@ Qed.
 Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
 Hint Unfold dra_included.
 
-Notation T := (validity (✓ : A → Prop)).
-Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ (validity_car z).
+Notation T := (validity (valid : A → Prop)).
+Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
 Proof. apply validity_prf. Qed.
 Hint Resolve validity_valid_car_valid.
 Program Instance validity_unit : Unit T := λ x,

algebra/fin_maps.v

@@ -87,7 +87,7 @@ Context `{Countable K} {A : cmraT}.
 
 Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
-Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m!!i).
+Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
 Instance map_minus : Minus (gmap K A) := merge minus.
 
 Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
@@ -171,7 +171,7 @@ Implicit Types a : A.
 
 Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
-Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
+Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
 Lemma map_singleton_validN n i x : ✓{n} ({[ i ↦ x ]} : gmap K A) ↔ ✓{n} x.
 Proof.

algebra/iprod.v

@@ -118,7 +118,7 @@ Section iprod_cmra.
 
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
-  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} (f x).
+  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
   Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
 
   Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
@@ -197,8 +197,7 @@ Section iprod_cmra.
   (** Properties of iprod_singleton. *)
   Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}.
 
-  Lemma iprod_singleton_validN n x (y : B x) :
-    ✓{n} (iprod_singleton x y) ↔ ✓{n} y.
+  Lemma iprod_singleton_validN n x (y: B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
   Proof.
     split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
     move=>Hx x'; destruct (decide (x = x')) as [->|];

algebra/option.v

@@ -87,13 +87,10 @@ Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
 Definition option_cmra_mixin  : CMRAMixin (option A).
 Proof.
   split.
-  * by intros n [x|]; destruct 1; constructor;
-      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
-  * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
-  * destruct 1; rewrite /validN /option_validN //=.
-    eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto.
-  * by destruct 1; inversion_clear 1; constructor;
-      repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
+  * by intros n [x|]; destruct 1; constructor; cofe_subst.
+  * by destruct 1; constructor; cofe_subst.
+  * by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
+  * by destruct 1; inversion_clear 1; constructor; cofe_subst.
   * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
   * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto.
   * intros [x|] [y|]; constructor; rewrite 1?commutative; auto.

algebra/upred.v

@@ -211,7 +211,7 @@ Notation "∃ x .. y , P" :=
 Notation "▷ P" := (uPred_later P) (at level 20) : uPred_scope.
 Notation "□ P" := (uPred_always P) (at level 20) : uPred_scope.
 Infix "≡" := uPred_eq : uPred_scope.
-Notation "✓" := uPred_valid (at level 1) : uPred_scope.
+Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
 
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Infix "↔" := uPred_iff : uPred_scope.

program_logic/auth.v

@@ -20,9 +20,8 @@ Section auth.
   Qed.
 
   (* TODO: Need this to be proven somewhere. *)
-  (* FIXME ✓ binds too strong, I need parenthesis here. *)
   Hypothesis auth_valid :
-    forall a b, (✓ (Auth (Excl a) b) : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').
+    forall a b, (✓ Auth (Excl a) b : iPropG Λ Σ) ⊑ (∃ b', a ≡ b ⋅ b').
 
   Definition auth_inv (γ : gname) : iPropG Λ Σ :=
     (∃ a, own AuthI γ (● a) ★ φ a)%I.

program_logic/ghost_ownership.v

@@ -33,7 +33,7 @@ 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.
+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.

program_logic/resources.v

@@ -76,7 +76,7 @@ Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅.
 Instance res_unit : Unit (res Λ Σ A) := λ r,
   Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
 Instance res_validN : ValidN (res Λ Σ A) := λ n r,
-  ✓{n} (wld r) ∧ ✓{n} (pst r) ∧ ✓{n} (gst r).
+  ✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
 Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
   Res (wld r1 ⩪ wld r2) (pst r1 ⩪ pst r2) (gst r1 ⩪ gst r2).
 Lemma res_included (r1 r2 : res Λ Σ A) :
@@ -136,9 +136,9 @@ Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
 Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
   Res (wld r) (pst r) (Some m).
 
-Lemma wld_validN n r : ✓{n} r → ✓{n} (wld r).
+Lemma wld_validN n r : ✓{n} r → ✓{n} wld r.
 Proof. by intros (?&?&?). Qed.
-Lemma gst_validN n r : ✓{n} r → ✓{n} (gst r).
+Lemma gst_validN n r : ✓{n} r → ✓{n} gst r.
 Proof. by intros (?&?&?). Qed.
 Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
   Res w1 σ1 m1 ⋅ Res w2 σ2 m2 = Res (w1 ⋅ w2) (σ1 ⋅ σ2) (m1 ⋅ m2).

program_logic/wsat.v

@@ -2,8 +2,8 @@ Require Export program_logic.model prelude.co_pset.
 Require Export algebra.cmra_big_op algebra.cmra_tactics.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 10 (✓{_} _) => solve_validN.
-Local Hint Extern 1 (✓{_} (gst _)) => apply gst_validN.
-Local Hint Extern 1 (✓{_} (wld _)) => apply wld_validN.
+Local Hint Extern 1 (✓{_} gst _) => apply gst_validN.
+Local Hint Extern 1 (✓{_} wld _) => apply wld_validN.
 
 Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
     (σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {