From 1c87b96ab64640dac59f04f970440bfa09f87316 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 May 2016 18:30:38 +0200
Subject: [PATCH] Define dist on option using option_Forall2.

---
 algebra/cofe.v            | 13 ++++---------
 algebra/list.v            |  4 ++--
 program_logic/ownership.v |  2 +-
 3 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index fe969f567..1bfcc6612 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -454,13 +454,10 @@ Canonical Structure boolC := leibnizC bool.
 Section option.
   Context {A : cofeT}.
 
-  Inductive option_dist' (n : nat) : relation (option A) :=
-    | Some_dist x y : x ≡{n}≡ y → option_dist' n (Some x) (Some y)
-    | None_dist : option_dist' n None None.
-  Instance option_dist : Dist (option A) := option_dist'.
+  Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
 
   Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
-  Proof. split; destruct 1; constructor; auto. Qed.
+  Proof. done. Qed.
 
   Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
     {| chain_car n := from_option x (c n) |}.
@@ -474,10 +471,7 @@ Section option.
     - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
       intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
       by intros n; feed inversion (Hxy n).
-    - intros n; split.
-      + by intros [x|]; constructor.
-      + by destruct 1; constructor.
-      + destruct 1; inversion_clear 1; constructor; etrans; eauto.
+    - apply _.
     - destruct 1; constructor; by apply dist_S.
     - intros n c; rewrite /compl /option_compl.
       feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
@@ -503,6 +497,7 @@ Section option.
   Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
 End option.
 
+Typeclasses Opaque option_dist.
 Arguments optionC : clear implicits.
 
 Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
diff --git a/algebra/list.v b/algebra/list.v
index 47a509cef..16aa941fa 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -62,8 +62,8 @@ Proof.
     destruct (c 0) as [|x l] eqn:Hc0 at 1.
     { by destruct (chain_cauchy c 0 n); auto with omega. }
     rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
-    apply Forall2_lookup=> i; apply dist_option_Forall2.
-    rewrite list_lookup_fmap. destruct (decide (i < length (c n))); last first.
+    apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
+    destruct (decide (i < length (c n))); last first.
     { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
     rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
     by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 1ae5caeeb..cffff257a 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -64,7 +64,7 @@ Proof.
   intros (?&?&?). rewrite /ownI; uPred.unseal.
   rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
-    apply Some_dist, symmetry, agree_valid_includedN; last done.
+    constructor; symmetry; apply agree_valid_includedN; last done.
     by apply lookup_validN_Some with (wld r) i.
   - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
 Qed.
-- 
GitLab