Fix the notation for LookupTotal

In accordance with
<!93>

theories/base.v

@@ -1047,6 +1047,17 @@ Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
 Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
 Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
+(** The function [lookup_total] should be the total over-approximation
+of the partial [lookup] function. *)
+Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
+Hint Mode LookupTotal - - ! : typeclass_instances.
+Instance: Params (@lookup_total) 4 := {}.
+Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
+Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
+Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
+Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope.
+Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
+
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
 Hint Mode SingletonM - - ! : typeclass_instances.

theories/fin_map_dom.v

@@ -19,6 +19,10 @@ Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
 Section fin_map_dom.
 Context `{FinMapDom K M D}.
 
+Lemma lookup_lookup_total_dom `{!Inhabited A} (m : M A) i :
+  i ∈ dom D m → m !! i = Some (m !!! i).
+Proof. rewrite elem_of_dom. apply lookup_lookup_total. Qed.
+
 Lemma dom_map_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
   (∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
   dom D (filter P m) ≡ X.

theories/fin_maps.v

@@ -144,6 +144,10 @@ Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M :=
   | x :: xs => <[start:=x]> (map_seq (S start) xs)
   end.
 
+Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} : LookupTotal K A (M A) | 20 :=
+  λ i m, default inhabitant (m !! i).
+Typeclasses Opaque finmap_lookup_total.
+
 (** * Theorems *)
 Section theorems.
 Context `{FinMap K M}.
@@ -165,6 +169,13 @@ Section setoid.
   Qed.
   Global Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (lookup i).
   Proof. by intros m1 m2 Hm. Qed.
+  Global Instance lookup_total_proper (i : K) `{!Inhabited A} :
+    Proper (≡@{A}) inhabitant →
+    Proper ((≡@{M A}) ==> (≡)) (lookup_total i).
+  Proof.
+    intros ? m1 m2 Hm. unfold lookup_total, finmap_lookup_total.
+    apply from_option_proper; auto. by intros ??.
+  Qed.
   Global Instance partial_alter_proper :
     Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) partial_alter.
   Proof.
@@ -246,6 +257,15 @@ Proof.
   intros m1 m2; rewrite !map_subseteq_spec.
   intros; apply map_eq; intros i; apply option_eq; naive_solver.
 Qed.
+Lemma lookup_total_alt `{!Inhabited A} (m : M A) i :
+  m !!! i = default inhabitant (m !! i).
+Proof. reflexivity. Qed.
+Lemma lookup_total_correct `{!Inhabited A} (m : M A) i x :
+  m !! i = Some x → m !!! i = x.
+Proof. rewrite lookup_total_alt. by intros ->. Qed.
+Lemma lookup_lookup_total `{!Inhabited A} (m : M A) i :
+  is_Some (m !! i) → m !! i = Some (m !!! i).
+Proof. intros [x Hx]. by rewrite (lookup_total_correct m i x). Qed.
 Lemma lookup_weaken {A} (m1 m2 : M A) i x :
   m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
 Proof. rewrite !map_subseteq_spec. auto. Qed.

theories/list.v

@@ -70,6 +70,15 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
   | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
   end.
 
+(** The operation [l !!! i] is a total version of the lookup operation
+[l !! i]. *)
+Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
+  fix go i l {struct l} : A := let _ : LookupTotal _ _ _ := @go in
+  match l with
+  | [] => inhabitant
+  | x :: l => match i with 0 => x | S i => l !!! i end
+  end.
+
 (** The operation [alter f i l] applies the function [f] to the [i]th element
 of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
 Instance list_alter {A} : Alter nat A (list A) := λ f,
@@ -542,6 +551,19 @@ Proof.
   rewrite nth_lookup. destruct (l !! i) eqn:?; eauto using lookup_ge_None_1.
 Qed.
 
+Lemma list_lookup_total_alt `{!Inhabited A} l i :
+  l !!! i = default inhabitant (l !! i).
+Proof. revert i. induction l; intros []; naive_solver. Qed.
+Lemma list_lookup_total_correct `{!Inhabited A} l i x :
+  l !! i = Some x → l !!! i = x.
+Proof. rewrite list_lookup_total_alt. by intros ->. Qed.
+Lemma list_lookup_lookup_total `{!Inhabited A} l i :
+  is_Some (l !! i) → l !! i = Some (l !!! i).
+Proof. rewrite list_lookup_total_alt; by intros [x ->]. Qed.
+Lemma list_lookup_lookup_total_lt `{!Inhabited A} l i :
+  i < length l → l !! i = Some (l !!! i).
+Proof. intros ?. by apply list_lookup_lookup_total, lookup_lt_is_Some_2. Qed.
+
 Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
 Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
 Lemma alter_length f l i : length (alter f i l) = length l.
@@ -2966,6 +2988,10 @@ Section setoid.
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i).
   Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
+  Global Instance list_lookup_total_proper `{!Inhabited A} i :
+    Proper (≡) inhabitant →
+    Proper ((≡@{list A}) ==> (≡)) (lookup_total i).
+  Proof. intros ?. induction i; destruct 1; simpl; auto. Qed.
   Global Instance list_alter_proper f i :
     Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{list A})) (alter f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.

theories/vector.v

@@ -31,10 +31,26 @@ Notation "(+++)" := vapp (only parsing) : vector_scope.
 Notation "( v +++.)" := (vapp v) (only parsing) : vector_scope.
 Notation "(.+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
 
+(** Similar to [fin], we provide an inversion principle that keeps the length
+fixed. We define a tactic [inv_vec v] to perform case analysis on [v], using
+this inversion principle. *)
+Notation vec_0_inv := Vector.case0.
+Definition vec_S_inv {A n} (P : vec A (S n) → Type)
+  (Hcons : ∀ x v, P (x ::: v)) v : P v.
+Proof.
+  revert P Hcons.
+  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
+Defined.
+
 (** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
 type class, as it has a dependent type. *)
 Arguments Vector.nth {_ _} !_ !_%fin /.
-Infix "!!!" := Vector.nth (at level 20) : vector_scope.
+Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
+  fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
+  match i in fin m return vec A m → A with
+  | 0%fin => vec_S_inv (λ _, A) (λ x _, x)
+  | FS j => vec_S_inv (λ _, A) (λ _ v, v !!! j)
+  end.
 
 (** The tactic [vec_double_ind v1 v2] performs double induction on [v1] and [v2]
 provided that they have the same length. *)
@@ -71,17 +87,6 @@ Proof.
   f_equal; eauto using vcons_inj_1, vcons_inj_2.
 Defined.
 
-(** Similar to [fin], we provide an inversion principle that keeps the length
-fixed. We define a tactic [inv_vec v] to perform case analysis on [v], using
-this inversion principle. *)
-Notation vec_0_inv := Vector.case0.
-Definition vec_S_inv {A n} (P : vec A (S n) → Type)
-  (Hcons : ∀ x v, P (x ::: v)) v : P v.
-Proof.
-  revert P Hcons.
-  refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
-Defined.
-
 Ltac inv_vec v :=
   let T := type of v in
   match eval hnf in T with
@@ -213,7 +218,7 @@ Notation vmap := Vector.map.
 
 Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i :
   vmap f v !!! i = f (v !!! i).
-Proof. by apply Vector.nth_map. Qed.
+Proof. by induction v; inv_fin i; eauto. Qed.
 Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) :
   vec_to_list (vmap f v) = f <$> vec_to_list v.
 Proof. induction v; simpl. done. by rewrite IHv. Qed.
@@ -224,7 +229,12 @@ Notation vzip_with := Vector.map2.
 
 Lemma vlookup_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i :
   vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
-Proof. by apply Vector.nth_map2. Qed.
+Proof.
+  vec_double_ind v1 v2.
+  - intros i; inv_fin i.
+  - intros n v1 v2 IH a b i.
+    inv_fin i; eauto.
+Qed.
 Lemma vec_to_list_zip_with `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) :
   vec_to_list (vzip_with f v1 v2) =
     zip_with f (vec_to_list v1) (vec_to_list v2).