From 4a45cda038bf11f3205902bd0f56ea861f35bfad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jan 2020 10:49:03 -0600
Subject: [PATCH] Add versions of `option_included` for total cameras.

---
 theories/algebra/cmra.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3ea70b65a..1ef0004d9 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1313,6 +1313,13 @@ Section option.
       + exists None; by constructor.
       + exists (Some c); by constructor.
   Qed.
+  Lemma option_included_total `{!CmraTotal A} ma mb :
+    ma ≼ mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼ b.
+  Proof.
+    rewrite option_included. split; last naive_solver.
+    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
+    right. exists a, b. by rewrite {3}Hab.
+  Qed.
 
   Lemma option_includedN n ma mb :
     ma ≼{n} mb ↔ ma = None ∨ ∃ x y, ma = Some x ∧ mb = Some y ∧ (x ≡{n}≡ y ∨ x ≼{n} y).
@@ -1328,6 +1335,13 @@ Section option.
       + exists None; by constructor.
       + exists (Some c); by constructor.
   Qed.
+  Lemma option_includedN_total `{!CmraTotal A} n ma mb :
+    ma ≼{n} mb ↔ ma = None ∨ ∃ a b, ma = Some a ∧ mb = Some b ∧ a ≼{n} b.
+  Proof.
+    rewrite option_includedN. split; last naive_solver.
+    intros [->|(a&b&->&->&[Hab|?])]; [by eauto| |by eauto 10].
+    right. exists a, b. by rewrite {3}Hab.
+  Qed.
 
   Lemma option_cmra_mixin : CmraMixin (option A).
   Proof.
-- 
GitLab