Address feedback

Fixed a few things, added lemmas involving `option fracR`
validity/composition.

theories/algebra/dfrac.v

@@ -20,6 +20,7 @@
     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.algebra Require Import frac.
 From iris Require Import options.
 
 (** An element of dfrac denotes ownership of a fraction, knowledge that a
@@ -107,6 +108,23 @@ Section dfrac.
     Dfrac None ≼ Dfrac None.
   Proof. exists DfracDiscarded. done. Qed.
 
+  Lemma dfrac_own_included_discarded q :
+    Dfrac (Some q) ≼ Dfrac None → False.
+  Proof.
+    intros [ [o| | ] H%leibniz_equiv];
+      rewrite /op /dfrac_op /= in H; discriminate.
+  Qed.
+
+  (** The other direction does not hold because [Some q ≼ Some q] but [Dfrac
+      (Some q1) ≼ Dfrac (Some q2)] is equivalent to [q1 < q2]. *)
+  Lemma dfrac_included mq1 mq2 : Dfrac mq1 ≼ Dfrac mq2 → mq1 ≼ mq2.
+  Proof.
+    destruct mq1 as [q1|], mq2 as [q2|];
+      rewrite ?dfrac_own_included ?Some_included ?option_included ?frac_included;
+      auto.
+    intros []%dfrac_own_included_discarded.
+  Qed.
+
   Definition dfrac_ra_mixin : RAMixin dfrac.
   Proof.
     split; try apply _.
@@ -153,7 +171,7 @@ Section dfrac.
     - by intros ->%(inj _)%(inj _).
   Qed.
 
-  Global Instance dfrac_id_free q : IdFree (DfracOwn q).
+  Global Instance dfrac_id_free q : IdFree (Dfrac (Some q)).
   Proof.
     intros [q'| |q'] _; rewrite /op /cmra_op; simpl; try by intros [=].
     by intros [= ?%Qp_plus_id_free].
@@ -168,10 +186,21 @@ Section dfrac.
   Lemma dfrac_valid_discarded p : ✓ Dfrac None.
   Proof. done. Qed.
 
+  Lemma dfrac_valid_Dfrac mq : ✓ Dfrac mq ↔ ✓ mq.
+  Proof. destruct mq; auto using dfrac_valid_own, dfrac_valid_discarded. Qed.
+
   Lemma dfrac_valid_own_discarded q :
     ✓ (Dfrac (Some q) ⋅ Dfrac None) ↔ (q < 1%Qp)%Qc.
   Proof. done. Qed.
 
+  (** The other direction does not hold; consider [mq1 = Some 1], [mq2 = None]. *)
+  Lemma dfrac_valid_dfrac_op mq1 mq2 : ✓ (Dfrac mq1 ⋅ Dfrac mq2) → ✓ (mq1 ⋅ mq2).
+  Proof.
+    destruct mq1, mq2; try done.
+    - move=> /dfrac_valid_own_discarded /Qclt_le_weak. done.
+    - rewrite comm. move=> /dfrac_valid_own_discarded /Qclt_le_weak. done.
+  Qed.
+
   Global Instance is_op_dfrac q : IsOp' (Dfrac (Some q)) (Dfrac (Some (q/2)%Qp)) (Dfrac (Some (q/2)%Qp)).
   Proof. by rewrite /IsOp' /IsOp dfrac_op_own Qp_div_2. Qed.
 
@@ -193,4 +222,4 @@ Section dfrac.
 
 End dfrac.
 
-Opaque Dfrac.
+Typeclasses Opaque Dfrac.