From 8515dc9655a1900e396ec23e146dfffea63e11bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 11:02:16 +0200
Subject: [PATCH] `Inj`/`Forall` results for `list`/`option` similar to std++.

This is an outstanding TODO from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/496
---
 iris/algebra/list.v | 14 ++++++++++----
 iris/algebra/ofe.v  | 10 +++++-----
 2 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 66a05ce0c..d09ab124d 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -9,8 +9,10 @@ Implicit Types l : list A.
 
 Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
+Lemma list_dist_Forall2 n l k : l ≡{n}≡ k ↔ Forall2 (dist n) l k.
+Proof. done. Qed.
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
-Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
+Proof. setoid_rewrite option_dist_Forall2. apply Forall2_lookup. Qed.
 
 Global Instance cons_ne : NonExpansive2 (@cons A) := _.
 Global Instance app_ne : NonExpansive2 (@app A) := _.
@@ -21,7 +23,7 @@ Global Instance drop_ne n : NonExpansive (@drop A n) := _.
 Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
 Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
-Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Proof. intros ????. by apply option_dist_Forall2, Forall2_lookup. Qed.
 Global Instance list_lookup_total_ne `{!Inhabited A} i :
   NonExpansive (lookup_total (M:=list A) i).
 Proof. intros ???. rewrite !list_lookup_total_alt. by intros ->. Qed.
@@ -31,14 +33,14 @@ Global Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i) := _.
 Global Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i) := _.
 Global Instance list_delete_ne i : NonExpansive (delete (M:=list A) i) := _.
 Global Instance option_list_ne : NonExpansive (@option_list A).
-Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
+Proof. intros ????; by apply Forall2_option_list, option_dist_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
 Global Instance replicate_ne n : NonExpansive (@replicate A n) := _.
 Global Instance reverse_ne : NonExpansive (@reverse A) := _.
 Global Instance last_ne : NonExpansive (@last A).
-Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
+Proof. intros ????; by apply option_dist_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.
 
 Global Instance cons_dist_inj n :
@@ -132,6 +134,10 @@ Proof.
   induction 1; destruct 1; simpl; [constructor..|f_equiv; try apply Hf; auto].
 Qed.
 
+Global Instance list_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{list A}≡) (≡{n}@{list B}≡) (fmap f).
+Proof. apply list_fmap_inj. Qed.
+
 Lemma big_opL_ne_2 {M : ofe} {o : M → M → M} `{!Monoid o} {A : ofe} (f g : nat → A → M) l1 l2 n :
   l1 ≡{n}≡ l2 →
   (∀ k y1 y2,
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 99c9f05b1..00626d437 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1222,7 +1222,7 @@ Section option.
   Context {A : ofe}.
 
   Local 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.
+  Lemma option_dist_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
   Proof. done. Qed.
 
   Definition option_ofe_mixin : OfeMixin (option A).
@@ -1295,6 +1295,10 @@ Global Instance option_mjoin_ne {A : ofe} n:
   Proper (dist n ==> dist n) (@mjoin option _ A).
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
+Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
+  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
+Proof. apply option_fmap_inj. Qed.
+
 Lemma fmap_Some_dist {A B : ofe} (f : A → B) (mx : option A) (y : B) n :
   f <$> mx ≡{n}≡ Some y ↔ ∃ x : A, mx = Some x ∧ y ≡{n}≡ f x.
 Proof.
@@ -1330,10 +1334,6 @@ Proof.
     apply optionO_map_ne, oFunctor_map_contractive.
 Qed.
 
-Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
-  Inj (≡{n}≡) (≡{n}≡) f → Inj (≡{n}@{option A}≡) (≡{n}@{option B}≡) (fmap f).
-Proof. apply option_fmap_inj. Qed.
-
 (** * Later type *)
 (** Note that the projection [later_car] is not non-expansive (see also the
 lemma [later_car_anti_contractive] below), so it cannot be used in the logic.
-- 
GitLab