Make some names more consistent.

algebra/gmap.v

@@ -102,7 +102,7 @@ Proof. by apply lookup_merge. Qed.
 Lemma lookup_core m i : core m !! i = core (m !! i).
 Proof. by apply lookup_fmap. Qed.
 
-Lemma gmap_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
+Lemma lookup_included (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
   split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
   revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
@@ -132,7 +132,7 @@ Proof.
   - by intros m1 m2 i; rewrite !lookup_op comm.
   - by intros m i; rewrite lookup_op !lookup_core cmra_core_l.
   - by intros m i; rewrite !lookup_core cmra_core_idemp.
-  - intros x y; rewrite !gmap_included_spec; intros Hm i.
+  - intros x y; rewrite !lookup_included; intros Hm i.
     by rewrite !lookup_core; apply cmra_core_preserving.
   - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
     by rewrite -lookup_op.
@@ -178,9 +178,9 @@ Implicit Types m : gmap K A.
 Implicit Types i : K.
 Implicit Types a : A.
 
-Lemma lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
+Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
 Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
-Lemma lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x.
+Lemma lookup_valid_Some m i x : ✓ m → m !! i ≡ Some x → ✓ x.
 Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
 Lemma insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
@@ -336,7 +336,7 @@ Instance gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
 Proof.
   split; try apply _.
   - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
-  - intros m1 m2; rewrite !gmap_included_spec=> Hm i.
+  - intros m1 m2; rewrite !lookup_included=> Hm i.
     by rewrite !lookup_fmap; apply: included_preserving.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :

algebra/list.v

-From iris.algebra Require Export option.
-From iris.prelude Require Export list.
+From iris.algebra Require Import cmra option.
+From iris.prelude Require Import list.
+From iris.algebra Require Import upred.
 
 Section cofe.
 Context {A : cofeT}.
 
 Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
+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.
+
 Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
 Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
 Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.

prelude/list.v

@@ -2684,7 +2684,7 @@ Section setoid.
 
   Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
   Proof. split; induction 1; constructor; auto. Qed.
-  Lemma equiv_lookup l k : l ≡ k ↔ (∀ i, l !! i ≡ k !! i).
+  Lemma list_equiv_lookup l k : l ≡ k ↔ ∀ i, l !! i ≡ k !! i.
   Proof.
     rewrite equiv_Forall2, Forall2_lookup.
     by setoid_rewrite equiv_option_Forall2.

program_logic/ownership.v

@@ -65,7 +65,7 @@ Proof.
   rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
     apply Some_dist, symmetry, agree_valid_includedN; last done.
-    by apply lookup_validN with (wld r) i.
+    by apply lookup_validN_Some with (wld r) i.
   - intros ?; split_and?; try apply cmra_unit_leastN; eauto.
 Qed.
 Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.

program_logic/wsat.v

@@ -56,7 +56,7 @@ Proof.
   assert (P' ≡{S n}≡ to_agree $ Next $ iProp_unfold $
                        iProp_fold $ later_car $ P' (S n)) as HPiso.
   { rewrite iProp_unfold_fold later_eta to_agree_car //.
-    apply (lookup_validN _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. }
+    apply (lookup_validN_Some _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. }
   assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'.
   { apply (inj iProp_unfold), (inj Next), (inj to_agree).
     by rewrite -HiP -(dist_le _ _ _ _ HPiso). }