From aa947529888a12f56bbb2757aaee8659a00135e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 13:01:17 +0100
Subject: [PATCH] Simplify CMRA axioms.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I have simplified the following CMRA axioms:

  cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
  cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;

By dropping off the step-index, so into:

  cmra_unit_preservingN x y : x ≼ y → unit x ≼ unit y;
  cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;

The old axioms can be derived.
---
 algebra/agree.v           |  7 ++++++-
 algebra/auth.v            |  6 +++---
 algebra/cmra.v            | 35 ++++++++++++++++++-----------------
 algebra/excl.v            |  4 ++--
 algebra/fin_maps.v        | 10 +++++-----
 algebra/iprod.v           | 15 +++++++++++----
 algebra/option.v          | 20 +++++++++++++++++---
 program_logic/resources.v |  6 +++---
 8 files changed, 65 insertions(+), 38 deletions(-)

diff --git a/algebra/agree.v b/algebra/agree.v
index 1271e9aba..c8d47172b 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -92,6 +92,11 @@ Proof.
     by cofe_subst; rewrite !agree_idemp.
 Qed.
 
+Lemma agree_included (x y : agree A) : x ≼ y ↔ y ≡ x ⋅ y.
+Proof.
+  split; [|by intros ?; exists y].
+  by intros [z Hz]; rewrite Hz assoc agree_idemp.
+Qed.
 Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
 Proof.
   split; [|by intros ?; exists y].
@@ -114,7 +119,7 @@ Proof.
     symmetry; apply dist_le with n; try apply Hx; auto.
   - intros x; apply agree_idemp.
   - by intros n x y [(?&?&?) ?].
-  - by intros n x y; rewrite agree_includedN.
+  - by intros x y; rewrite agree_included.
   - intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
     + by rewrite agree_idemp.
     + by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
diff --git a/algebra/auth.v b/algebra/auth.v
index 69c0ca216..65e52e8e9 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -125,13 +125,13 @@ Proof.
   - by split; simpl; rewrite comm.
   - by split; simpl; rewrite ?cmra_unit_l.
   - by split; simpl; rewrite ?cmra_unit_idemp.
-  - intros n ??; rewrite! auth_includedN; intros [??].
-    by split; simpl; apply cmra_unit_preservingN.
+  - intros ??; rewrite! auth_included; intros [??].
+    by split; simpl; apply cmra_unit_preserving.
   - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
     { intros n a b1 b2 <-; apply cmra_includedN_l. }
    intros n [[a1| |] b1] [[a2| |] b2];
      naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
-  - by intros n ??; rewrite auth_includedN;
+  - by intros ??; rewrite auth_included;
       intros [??]; split; simpl; apply cmra_op_minus.
   - intros n x y1 y2 ? [??]; simpl in *.
     destruct (cmra_extend n (authoritative x) (authoritative y1)
diff --git a/algebra/cmra.v b/algebra/cmra.v
index e2bbe90bf..b0a723e11 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -48,9 +48,9 @@ Record CMRAMixin A
   mixin_cmra_comm : Comm (≡) (⋅);
   mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
   mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
-  mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
+  mixin_cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
   mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
-  mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;
+  mixin_cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;
   mixin_cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }
@@ -112,11 +112,11 @@ Section cmra_mixin.
   Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
   Lemma cmra_unit_idemp x : unit (unit x) ≡ unit x.
   Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
-  Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
+  Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
+  Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
   Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
   Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
-  Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y.
+  Lemma cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y.
   Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
   Lemma cmra_extend n x y1 y2 :
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
@@ -243,12 +243,16 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
 Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
 Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
 
+(** ** Minus *)
+Lemma cmra_op_minus' n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y.
+Proof. intros [z ->]. by rewrite cmra_op_minus; last exists z. Qed.
+
 (** ** Order *)
 Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
 Proof.
   split; [by intros [z Hz] n; exists z; rewrite Hz|].
   intros Hxy; exists (y ⩪ x); apply equiv_dist=> n.
-  symmetry; apply cmra_op_minus, Hxy.
+  by rewrite cmra_op_minus'.
 Qed.
 Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
 Proof.
@@ -281,8 +285,11 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
 Lemma cmra_included_r x y : y ≼ x ⋅ y.
 Proof. rewrite (comm op); apply cmra_included_l. Qed.
 
-Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
-Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
+Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
+Proof.
+  intros [z ->].
+  apply cmra_included_includedN, cmra_unit_preserving, cmra_included_l.
+Qed.
 Lemma cmra_included_unit x : unit x ≼ x.
 Proof. by exists x; rewrite cmra_unit_l. Qed.
 Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
@@ -301,12 +308,6 @@ Proof.
   by rewrite Hx1 Hx2.
 Qed.
 
-(** ** Minus *)
-Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y.
-Proof.
-  rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus.
-Qed.
-
 (** ** Timeless *)
 Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
 Proof.
@@ -565,10 +566,10 @@ Section prod.
     - by split; rewrite /= comm.
     - by split; rewrite /= cmra_unit_l.
     - by split; rewrite /= cmra_unit_idemp.
-    - intros n x y; rewrite !prod_includedN.
-      by intros [??]; split; apply cmra_unit_preservingN.
+    - intros x y; rewrite !prod_included.
+      by intros [??]; split; apply cmra_unit_preserving.
     - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
-    - intros n x y; rewrite prod_includedN; intros [??].
+    - intros x y; rewrite prod_included; intros [??].
       by split; apply cmra_op_minus.
     - intros n x y1 y2 [??] [??]; simpl in *.
       destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
diff --git a/algebra/excl.v b/algebra/excl.v
index da9deda4e..ebdf8f559 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -113,9 +113,9 @@ Proof.
   - by intros [?| |] [?| |]; constructor.
   - by intros [?| |]; constructor.
   - constructor.
-  - by intros n [?| |] [?| |]; exists ∅.
+  - by intros [?| |] [?| |]; exists ∅.
   - by intros n [?| |] [?| |].
-  - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
+  - by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
   - intros n x y1 y2 ? Hx.
     by exists match y1, y2 with
       | Excl a1, Excl a2 => (Excl a1, Excl a2)
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index d8faf339d..fb9a55d7d 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -110,7 +110,7 @@ Proof.
   split.
   - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
   - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus'.
+    by rewrite lookup_op lookup_minus cmra_op_minus.
 Qed.
 Lemma map_includedN_spec (m1 m2 : gmap K A) n :
   m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
@@ -118,7 +118,7 @@ Proof.
   split.
   - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
   - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus.
+    by rewrite lookup_op lookup_minus cmra_op_minus'.
 Qed.
 
 Definition map_cmra_mixin : CMRAMixin (gmap K A).
@@ -136,11 +136,11 @@ Proof.
   - by intros m1 m2 i; rewrite !lookup_op comm.
   - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
   - by intros m i; rewrite !lookup_unit cmra_unit_idemp.
-  - intros n x y; rewrite !map_includedN_spec; intros Hm i.
-    by rewrite !lookup_unit; apply cmra_unit_preservingN.
+  - intros x y; rewrite !map_included_spec; intros Hm i.
+    by rewrite !lookup_unit; apply cmra_unit_preserving.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
-  - intros n x y; rewrite map_includedN_spec=> ? i.
+  - intros x y; rewrite map_included_spec=> ? i.
     by rewrite lookup_op lookup_minus cmra_op_minus.
   - intros n m m1 m2 Hm Hm12.
     assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 5222fad1d..cbd5871fa 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -126,13 +126,20 @@ Section iprod_cmra.
   Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
   Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
 
-  Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
+  Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
     split.
     - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
     - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
       by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
   Qed.
+  Lemma iprod_includedN_spec n (f g : iprod B) : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
+  Proof.
+    split.
+    - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
+    - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
+      by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus'.
+  Qed.
 
   Definition iprod_cmra_mixin : CMRAMixin (iprod B).
   Proof.
@@ -149,10 +156,10 @@ Section iprod_cmra.
     - by intros f1 f2 x; rewrite iprod_lookup_op comm.
     - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
     - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
-    - intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
-      by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf.
+    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
+      by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf.
     - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
-    - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
+    - intros f1 f2; rewrite iprod_included_spec=> Hf x.
       by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
     - intros n f f1 f2 Hf Hf12.
       set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
diff --git a/algebra/option.v b/algebra/option.v
index ad179c513..2357e8008 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -71,6 +71,19 @@ Instance option_unit : Unit (option A) := fmap unit.
 Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
 Instance option_minus : Minus (option A) :=
   difference_with (λ x y, Some (x ⩪ y)).
+
+Lemma option_included (mx my : option A) :
+  mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
+Proof.
+  split.
+  - intros [mz Hmz].
+    destruct mx as [x|]; [right|by left].
+    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
+    destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
+      setoid_subst; eauto using cmra_included_l.
+  - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
+    by exists (Some z); constructor.
+Qed.
 Lemma option_includedN n (mx my : option A) :
   mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
 Proof.
@@ -83,6 +96,7 @@ Proof.
   - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.
 Qed.
+
 Lemma None_includedN n (mx : option A) : None ≼{n} mx.
 Proof. rewrite option_includedN; auto. Qed.
 Lemma Some_Some_includedN n (x y : A) : x ≼{n} y → Some x ≼{n} Some y.
@@ -102,11 +116,11 @@ Proof.
   - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
   - by intros [x|]; constructor; rewrite cmra_unit_l.
   - by intros [x|]; constructor; rewrite cmra_unit_idemp.
-  - intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
-    right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
+  - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto.
+    right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
   - intros n [x|] [y|]; rewrite /validN /option_validN /=;
       eauto using cmra_validN_op_l.
-  - intros n mx my; rewrite option_includedN.
+  - intros mx my; rewrite option_included.
     intros [->|(x&y&->&->&?)]; [by destruct my|].
     by constructor; apply cmra_op_minus.
   - intros n mx my1 my2.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index e15b59ba6..70057ea66 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -111,11 +111,11 @@ Proof.
   - by intros ??; constructor; rewrite /= comm.
   - by intros ?; constructor; rewrite /= cmra_unit_l.
   - by intros ?; constructor; rewrite /= cmra_unit_idemp.
-  - intros n r1 r2; rewrite !res_includedN.
-    by intros (?&?&?); split_and!; apply cmra_unit_preservingN.
+  - intros r1 r2; rewrite !res_included.
+    by intros (?&?&?); split_and!; apply cmra_unit_preserving.
   - intros n r1 r2 (?&?&?);
       split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
-  - intros n r1 r2; rewrite res_includedN; intros (?&?&?).
+  - intros r1 r2; rewrite res_included; intros (?&?&?).
     by constructor; apply cmra_op_minus.
   - intros n r r1 r2 (?&?&?) [???]; simpl in *.
     destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
-- 
GitLab