Merge branch 'ralf/dfrac' into 'master'

dfrac: do not track discarded fraction

See merge request iris/iris!531

theories/algebra/dfrac.v

@@ -7,10 +7,8 @@
     Ownership of a fraction is denoted [DfracOwn q] and behaves identically to
     [q] of the fractional camera.
 
-    Knowledge that a fraction has been discarded is denoted [DfracDiscarded p].
-    Elements of this form are their own core, making ownership of them
-    persistent. Resource composition combines knowledge that [p] and [p'] have been
-    discarded into the knowledge that [p max p'] has been discarded.
+    Knowledge that a fraction has been discarded is denoted [DfracDiscarded].
+    This elements is its own core, making ownership persistent.
 
     One can make a frame preserving update from _owning_ a fraction to _knowing_
     that the fraction has been discarded.
@@ -18,28 +16,25 @@
     Crucially, ownership over 1 is an exclusive element just as it is in the
     fractional camera. Hence owning 1 implies that no fraction has been
     discarded. Conversely, knowing that a fraction has been discarded implies
-    that no one can own 1. And, since discarding is an irreversible operation, it
-    also implies that no one can own 1 in the future *)
+    that no one can own 1. And, since discarding is an irreversible operation,
+    it also implies that no one can own 1 in the future *)
 From Coq.QArith Require Import Qcanon.
 From iris.algebra Require Export cmra proofmode_classes updates.
 From iris Require Import options.
 
 (** An element of dfrac denotes ownership of a fraction, knowledge that a
-    fraction has been discarded, or both. Note that all elements can be written
-    on the form [DfracOwn q ⋅ DfracDiscarded p]. This should be used instead
+    fraction has been discarded, or both. Note that [DfracBoth] can be written
+    as [DfracOwn q ⋅ DfracDiscarded]. This should be used instead
     of [DfracBoth] which is for internal use only. *)
 Inductive dfrac :=
   | DfracOwn : Qp → dfrac
-  | DfracDiscarded : Qp → dfrac
-  | DfracBoth : Qp → Qp → dfrac.
+  | DfracDiscarded : dfrac
+  | DfracBoth : Qp → dfrac.
 
 Global Instance DfracOwn_inj : Inj (=) (=) DfracOwn.
 Proof. by injection 1. Qed.
 
-Global Instance DfracDiscarded_inj : Inj (=) (=) DfracDiscarded.
-Proof. by injection 1. Qed.
-
-Global Instance DfracBoth_inj : Inj2 (=) (=) (=) DfracBoth.
+Global Instance DfracBoth_inj : Inj (=) (=) DfracBoth.
 Proof. by injection 1. Qed.
 
 Section dfrac.
@@ -54,8 +49,8 @@ Section dfrac.
   Instance dfrac_valid : Valid dfrac := λ x,
     match x with
     | DfracOwn q => q ≤ 1%Qp
-    | DfracDiscarded p => p ≤ 1%Qp
-    | DfracBoth q p => (q + p)%Qp ≤ 1%Qp
+    | DfracDiscarded => True
+    | DfracBoth q => q < 1%Qp
     end%Qc.
 
   (** As in the fractional camera the core is undefined for elements denoting
@@ -64,8 +59,8 @@ Section dfrac.
   Instance dfrac_pcore : PCore dfrac := λ x,
     match x with
     | DfracOwn q => None
-    | DfracDiscarded p => Some (DfracDiscarded p)
-    | DfracBoth q p => Some (DfracDiscarded p)
+    | DfracDiscarded => Some DfracDiscarded
+    | DfracBoth q => Some DfracDiscarded
     end.
 
   (** When elements are combined, ownership is added together and knowledge of
@@ -73,64 +68,54 @@ Section dfrac.
   Instance dfrac_op : Op dfrac := λ x y,
     match x, y with
     | DfracOwn q, DfracOwn q' => DfracOwn (q + q')
-    | DfracOwn q, DfracDiscarded p' => DfracBoth q p'
-    | DfracOwn q, DfracBoth q' p' => DfracBoth (q + q') p'
-    | DfracDiscarded p, DfracOwn q' => DfracBoth q' p
-    | DfracDiscarded p, DfracDiscarded p' => DfracDiscarded (p `max` p')
-    | DfracDiscarded p, DfracBoth q' p' => DfracBoth q' (p `max` p')
-    | DfracBoth q p, DfracOwn q' => DfracBoth (q + q') p
-    | DfracBoth q p, DfracDiscarded p' => DfracBoth q (p `max` p')
-    | DfracBoth q p, DfracBoth q' p' => DfracBoth (q + q') (p `max` p')
+    | DfracOwn q, DfracDiscarded => DfracBoth q
+    | DfracOwn q, DfracBoth q' => DfracBoth (q + q')
+    | DfracDiscarded, DfracOwn q' => DfracBoth q'
+    | DfracDiscarded, DfracDiscarded => DfracDiscarded
+    | DfracDiscarded, DfracBoth q' => DfracBoth q'
+    | DfracBoth q, DfracOwn q' => DfracBoth (q + q')
+    | DfracBoth q, DfracDiscarded => DfracBoth q
+    | DfracBoth q, DfracBoth q' => DfracBoth (q + q')
     end.
 
   Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p + q).
   Proof. done. Qed.
 
-  Lemma dfrac_op_discarded q p :
-    DfracDiscarded p ⋅ DfracDiscarded q = DfracDiscarded (p `max` q).
+  Lemma dfrac_op_discarded :
+    DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qc.
   Proof.
     rewrite Qp_lt_sum. split.
-    - rewrite /included /op /dfrac_op. intros [[o|?|?] [= ->]]. by exists o.
+    - rewrite /included /op /dfrac_op. intros [[o| |?] [= ->]]. by exists o.
     - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
   Qed.
 
-  Lemma dfrac_discarded_included q p :
-    DfracDiscarded q ≼ DfracDiscarded p ↔ (q ≤ p)%Qc.
-  Proof. 
-    split.
-    - rewrite /included /op /dfrac_op. intros [[?|?|?] [= ->]]. apply Qp_le_max_l.
-    - intros ?. exists (DfracDiscarded p).
-      by rewrite dfrac_op_discarded /Qp_max decide_True.
-  Qed.
+  (* [dfrac] does not have a unit so reflexivity is not for granted! *)
+  Lemma dfrac_discarded_included :
+    DfracDiscarded ≼ DfracDiscarded.
+  Proof. exists DfracDiscarded. done. Qed.
 
   Definition dfrac_ra_mixin : RAMixin dfrac.
   Proof.
     split; try apply _.
-    - intros [?|?|??] y cx <-; intros [= <-]; eexists _; done.
-    - intros [?|?|??] [?|?|??] [?|?|??];
+    - intros [?| |?] y cx <-; intros [= <-]; eexists _; done.
+    - intros [?| |?] [?| |?] [?| |?];
         rewrite /op /dfrac_op 1?assoc 1?assoc; done.
-    - intros [?|?|??] [?|?|??];
-        rewrite /op /dfrac_op 1?(comm Qp_plus) 1?(comm Qp_max); done.
-    - intros [?|?|??] cx; rewrite /pcore /dfrac_pcore; intros [= <-];
-        rewrite /op /dfrac_op Qp_max_id; done.
-    - intros [?|?|??] ? [= <-]; done.
-    - intros [?|?|??] [?|?|??] ? [[?|?|??] [=]] [= <-]; eexists _; split; try done;
-        apply dfrac_discarded_included; subst; auto; apply Qp_le_max_l.
-    - intros [q|p|q p] [q'|p'|q' p']; rewrite /op /dfrac_op /valid /dfrac_valid.
-      * apply (Qp_plus_weak_r _ _ 1).
+    - intros [?| |?] [?| |?];
+        rewrite /op /dfrac_op 1?(comm Qp_plus); done.
+    - intros [?| |?] cx; rewrite /pcore /dfrac_pcore; intros [= <-];
+        rewrite /op /dfrac_op; done.
+    - intros [?| |?] ? [= <-]; done.
+    - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
+        apply dfrac_discarded_included.
+    - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op /valid /dfrac_valid; try done.
       * apply (Qp_plus_weak_r _ _ 1).
-      * apply Qcle_trans. etrans; last apply Qp_le_plus_l. apply Qp_le_plus_l.
-      * apply (Qp_plus_weak_l _ _ 1).
-      * apply (Qp_max_lub_l _ _ 1).
-      * by intros ?%(Qp_plus_weak_l _ _ 1)%(Qp_max_lub_l _ _ 1).
-      * rewrite (comm _ _ q') -assoc. apply (Qp_plus_weak_l _ _ 1).
-      * intros H. etrans; last apply H.
-        apply Qcplus_le_mono_l. apply Qp_le_max_l.
-      * intros H. etrans; last apply H.
-        rewrite -assoc. apply Qcplus_le_mono_l, Qp_plus_weak_2_r, Qp_le_max_l.
+      * apply Qclt_le_weak.
+      * move=> /Qclt_le_weak. apply Qcle_trans. etrans; last apply Qp_le_plus_l. done.
+      * apply Qclt_trans. apply Qp_lt_sum. eauto.
+      * apply Qclt_trans. apply Qp_lt_sum. eauto.
   Qed.
   Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
@@ -139,57 +124,61 @@ Section dfrac.
 
   Global Instance dfrac_full_exclusive : Exclusive (DfracOwn 1).
   Proof.
-    intros [q|p|q p];
+    intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid /=.
     - apply (Qp_not_plus_ge 1 q).
-    - apply (Qp_not_plus_ge 1 p).
-    - rewrite -Qcplus_assoc. apply (Qp_not_plus_ge 1 (q + p)).
+    - intros []%irreflexivity. apply _.
+    - move=> /Qclt_le_weak. apply (Qp_not_plus_ge 1 q).
   Qed.
 
   Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
   Proof.
     apply: discrete_cancelable.
-    intros [q1|p1|q1 p1][q2|p2|q2 p2] _; rewrite /op /cmra_op; simpl;
+    intros [q1| |q1] [q2| |q2] _; rewrite /op /cmra_op; simpl;
       try by intros [= ->].
     - by intros ->%(inj _)%(inj _).
-    - by intros [?%symmetry%Qp_plus_id_free _]%(inj2 _).
-    - by intros [?%Qp_plus_id_free ?]%(inj2 _).
-    - by intros [->%(inj _) ->]%(inj2 _).
+    - done.
+    - intros Hq%(inj _). symmetry in Hq. apply Qp_plus_id_free in Hq. done.
+    - by intros Hq%(inj _)%Qp_plus_id_free.
+    - by intros ->%(inj _)%(inj _).
   Qed.
 
   Global Instance frac_id_free q : IdFree (DfracOwn q).
   Proof.
-    intros [q'|p'|q' p'] _; rewrite /op /cmra_op; simpl; try by intros [=].
+    intros [q'| |q'] _; rewrite /op /cmra_op; simpl; try by intros [=].
     by intros [= ?%Qp_plus_id_free].
   Qed.
 
-  Global Instance dfrac_discarded_core_id p : CoreId (DfracDiscarded p).
+  Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
 
   Lemma dfrac_valid_own p : ✓ DfracOwn p ↔ (p ≤ 1%Qp)%Qc.
   Proof. done. Qed.
 
-  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded p ↔ (p ≤ 1%Qp)%Qc.
+  Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
 
   Lemma dfrac_valid_own_discarded q p :
-    ✓ (DfracOwn q ⋅ DfracDiscarded p) ↔ (q + p ≤ 1%Qp)%Qc.
+    ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1%Qp)%Qc.
   Proof. done. Qed.
 
   Global Instance is_op_frac q : IsOp' (DfracOwn q) (DfracOwn (q/2)) (DfracOwn (q/2)).
   Proof. by rewrite /IsOp' /IsOp dfrac_op_own Qp_div_2. Qed.
 
   (** Discarding a fraction is a frame preserving update. *)
-  Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded q.
+  Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
   Proof.
-    intros n [[q'|p'|q' p']|];
+    intros n [[q'| |q']|];
       rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid /=.
-    - by rewrite Qcplus_comm.
-    - intro. etrans. apply Qp_max_plus. done.
-    - intro. etrans; last done.
-      rewrite -Qcplus_assoc. rewrite (Qcplus_comm q _). rewrite -Qcplus_assoc.
-      apply Qcplus_le_mono_l. rewrite Qcplus_comm. apply Qp_max_plus.
+    - intros [Hq|Hq]%Qcle_lt_or_eq.
+      + etrans; last eassumption. change (q' < (q + q')%Qp)%Qc. apply Qp_lt_sum.
+        rewrite {1}comm. eauto.
+      + change (q' < 1%Qp)%Qc. apply Qp_lt_sum. exists q.
+        rewrite (comm Qp_plus). apply Qp_eq. simpl. rewrite Hq. done.
+    - done.
+    - apply Qclt_trans. change (q' < (q + q')%Qp)%Qc. apply Qp_lt_sum.
+      rewrite {1}comm. eauto.
     - done.
   Qed.
 
-End dfrac.
\ No newline at end of file
+End dfrac.