Make fin_maps and global more consistent.

algebra/fin_maps.v

@@ -3,8 +3,8 @@ Require Import algebra.functor.
 
 Section cofe.
 Context `{Countable K} {A : cofeT}.
+Implicit Types m : gmap K A.
 
-(* COFE *)
 Instance map_dist : Dist (gmap K A) := λ n m1 m2,
   ∀ i, m1 !! i ={n}= m2 !! i.
 Program Definition map_chain (c : chain (gmap K A))
@@ -36,44 +36,45 @@ Global Instance lookup_ne n k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
-Global Instance insert_ne (i : K) n :
+Global Instance insert_ne i n :
   Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
 Proof.
   intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
-Global Instance singleton_ne (i : K) n :
+Global Instance singleton_ne i n :
   Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
 Proof. by intros ???; apply insert_ne. Qed.
-Global Instance delete_ne (i : K) n :
+Global Instance delete_ne i n :
   Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
 Proof.
   intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
     [by constructor|by apply lookup_ne].
 Qed.
+
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
   inversion_clear Hm; constructor.
 Qed.
-Global Instance map_lookup_timeless (m : gmap K A) i :
-  Timeless m → Timeless (m !! i).
+Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
 Proof.
   intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
   assert (m ={1}= <[i:=x]> m)
     by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
   by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
 Qed.
-Global Instance map_insert_timeless (m : gmap K A) i x :
+Global Instance map_insert_timeless m i x :
   Timeless x → Timeless m → Timeless (<[i:=x]>m).
 Proof.
   intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
   { by apply (timeless _); rewrite -Hm lookup_insert. }
   by apply (timeless _); rewrite -Hm lookup_insert_ne.
 Qed.
-Global Instance map_singleton_timeless (i : K) (x : A) :
+Global Instance map_singleton_timeless i x :
   Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _.
 End cofe.
+
 Arguments mapC _ {_ _} _.
 
 (* CMRA *)
@@ -84,12 +85,14 @@ Instance map_op : Op (gmap K A) := merge op.
 Instance map_unit : Unit (gmap K A) := fmap unit.
 Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m!!i).
 Instance map_minus : Minus (gmap K A) := merge minus.
+
 Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
 Proof. by apply lookup_merge. Qed.
 Lemma lookup_unit m i : unit m !! i = unit (m !! i).
 Proof. by apply lookup_fmap. Qed.
+
 Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
 Proof.
   split.
@@ -105,6 +108,7 @@ Proof.
   * intros Hm; exists (m2 ⩪ m1); intros i.
     by rewrite lookup_op lookup_minus cmra_op_minus.
 Qed.
+
 Definition map_cmra_mixin : CMRAMixin (gmap K A).
 Proof.
   split.
@@ -152,35 +156,32 @@ Proof.
   * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
   * apply map_empty_timeless.
 Qed.
-
 End cmra.
+
 Arguments mapRA _ {_ _} _.
 
 Section properties.
-Context `{Countable K} {A: cmraT}.
+Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
+Implicit Types i : K.
+Implicit Types a : A.
 
 Lemma map_lookup_validN 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 map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
 Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
+Lemma map_singleton_validN n i x : ✓{n} ({[ i ↦ x ]} : gmap K A) ↔ ✓{n} x.
+Proof.
+  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
+  by move=>/(_ i); simplify_map_equality.
+Qed.
 
 Lemma map_insert_op m1 m2 i x :
   m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
 Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
-
-Lemma map_validN_singleton n (i : K) (x : A) :
-  ✓{n} x <-> ✓{n} ({[ i ↦ x ]} : gmap K A).
-Proof.
-  split.
-  - move=>Hx j. destruct (decide (i = j)); simplify_map_equality; done.
-  - move=>Hm. move: (Hm i). by simplify_map_equality.
-Qed.
-
 Lemma map_unit_singleton (i : K) (x : A) :
   unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}.
 Proof. apply map_fmap_singleton. Qed.
-
 Lemma map_op_singleton (i : K) (x y : A) :
   {[ i ↦ x ]} ⋅ {[ i ↦ y ]} = ({[ i ↦ x ⋅ y ]} : gmap K A).
 Proof. by apply (merge_singleton _ _ _ x y). Qed.
@@ -220,7 +221,7 @@ Lemma map_insert_updateP' (P : A → Prop) m i x :
 Proof. eauto using map_insert_updateP. Qed.
 Lemma map_insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
 Proof.
-  rewrite !cmra_update_updateP; eauto using map_insert_updateP with congruence.
+  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
 Qed.
 
 Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
@@ -228,13 +229,9 @@ Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
 Proof. apply map_insert_updateP. Qed.
 Lemma map_singleton_updateP' (P : A → Prop) i x :
   x ~~>: P → {[ i ↦ x ]} ~~>: λ m', ∃ y, m' = {[ i ↦ y ]} ∧ P y.
-Proof. eauto using map_singleton_updateP. Qed.
+Proof. apply map_insert_updateP'. Qed.
 Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i ↦ x ]} ~~> {[ i ↦ y ]}.
-Proof.
-  rewrite !cmra_update_updateP=>?. eapply map_singleton_updateP; first eassumption.
-  by move=>? ->.
-Qed.
-
+Proof. apply map_insert_update. Qed.
 
 Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :

algebra/iprod.v

 Require Export algebra.cmra.
 Require Import algebra.functor.
 
-(** Indexed product *)
+(** * Indexed product *)
 (** Need to put this in a definition to make canonical structures to work. *)
 Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
 Definition iprod_insert `{∀ x x' : A, Decision (x = x')} {B : A → cofeT}
     (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Global Instance iprod_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
-Definition iprod_lookup_empty {A} {B : A → cofeT} `{∀ x, Empty (B x)} x : ∅ x = ∅ := eq_refl.
-Definition iprod_singleton
-    `{∀ x x' : A, Decision (x = x')} {B : A → cofeT} `{∀ x : A, Empty (B x)}
+Global Instance iprod_empty {A} {B : A → cofeT}
+  `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
+Definition iprod_singleton {A} {B : A → cofeT} 
+    `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)}
   (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
 
 Section iprod_cofe.
   Context {A} {B : A → cofeT}.
   Implicit Types x : A.
   Implicit Types f g : iprod B.
+
   Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
   Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ={n}= g x.
   Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
@@ -41,6 +42,15 @@ Section iprod_cofe.
   Qed.
   Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
 
+  (** Properties of empty *)
+  Section empty.
+    Context `{∀ x, Empty (B x)}.
+    Definition iprod_lookup_empty  x : ∅ x = ∅ := eq_refl.
+    Instance iprod_empty_timeless :
+      (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
+    Proof. intros ? f Hf x. by apply (timeless _). Qed.
+  End empty.
+
   (** Properties of iprod_insert. *)
   Context `{∀ x x' : A, Decision (x = x')}.
 
@@ -50,7 +60,6 @@ Section iprod_cofe.
     intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
     by destruct (decide _) as [[]|].
   Qed.
-
   Global Instance iprod_insert_proper x :
     Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _.
 
@@ -59,90 +68,62 @@ Section iprod_cofe.
     rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
     by rewrite (proof_irrel Hx eq_refl).
   Qed.
-
   Lemma iprod_lookup_insert_ne f x x' y :
     x ≠ x' → (iprod_insert x y f) x' = f x'.
   Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
 
-  Global Instance iprod_lookup_timeless f x :
-    Timeless f → Timeless (f x).
+  Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x).
   Proof.
-    intros ? y Hf.
+    intros ? y ?.
     cut (f ≡ iprod_insert x y f).
-    { move=>{Hf} Hf. by rewrite (Hf x) iprod_lookup_insert. }
-    apply timeless; first by apply _.
-    move=>x'. destruct (decide (x = x')).
-    - subst x'. rewrite iprod_lookup_insert; done.
-    - rewrite iprod_lookup_insert_ne //.
+    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
+    by apply (timeless _)=>x'; destruct (decide (x = x')) as [->|];
+      rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
   Qed.
-
   Global Instance iprod_insert_timeless f x y :
     Timeless f → Timeless y → Timeless (iprod_insert x y f).
   Proof.
-    intros ?? g Heq x'. destruct (decide (x = x')).
-    - subst x'. rewrite iprod_lookup_insert.
-      apply (timeless _).
-      rewrite -(Heq x) iprod_lookup_insert; done.
-    - rewrite iprod_lookup_insert_ne //.
-      apply (timeless _).
-      rewrite -(Heq x') iprod_lookup_insert_ne; done.
+    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
+    * rewrite iprod_lookup_insert.
+      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert.
+    * rewrite iprod_lookup_insert_ne //.
+      apply (timeless _). by rewrite -(Heq x') iprod_lookup_insert_ne.
   Qed.
 
   (** Properties of iprod_singletom. *)
   Context `{∀ x : A, Empty (B x)}.
+
   Global Instance iprod_singleton_ne x n :
     Proper (dist n ==> dist n) (iprod_singleton x).
   Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
   Global Instance iprod_singleton_proper x :
     Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
+
   Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y.
   Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
-  Lemma iprod_lookup_singleton_ne x x' y :
-    x ≠ x' → (iprod_singleton x y) x' = ∅.
+  Lemma iprod_lookup_singleton_ne x x' y: x ≠ x' → (iprod_singleton x y) x' = ∅.
   Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
 
-  Context `{∀ x : A, Timeless (∅ : B x)}.
-  Instance iprod_empty_timeless : Timeless (∅ : iprod B).
-  Proof. intros f Hf x. by apply (timeless _). Qed.
-
   Global Instance iprod_singleton_timeless x (y : B x) :
-    Timeless y → Timeless (iprod_singleton x y) := _.
-
+    (∀ x : A, Timeless (∅ : B x)) → Timeless y → Timeless (iprod_singleton x y).
+  Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed.
 End iprod_cofe.
 
 Arguments iprodC {_} _.
 
-Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
-  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
-    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
-  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
-Proof. done. Qed.
-Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
-  (∀ x, Proper (dist n ==> dist n) (f x)) →
-  Proper (dist n ==> dist n) (iprod_map f).
-Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
-  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
-  Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
-Proof. intros f1 f2 Hf g x; apply Hf. Qed.
-
 Section iprod_cmra.
   Context {A} {B : A → cmraT}.
   Implicit Types f g : iprod B.
+
   Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
   Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
-  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
   Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} (f x).
   Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
+
+  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
+  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
   Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
+
   Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
   Proof.
     split.
@@ -150,6 +131,7 @@ Section iprod_cmra.
     * intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
       by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
   Qed.
+
   Definition iprod_cmra_mixin : CMRAMixin (iprod B).
   Proof.
     split.
@@ -209,31 +191,27 @@ Section iprod_cmra.
   Lemma iprod_insert_update g x y1 y2 :
     y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
   Proof.
-    rewrite !cmra_update_updateP;
-      eauto using iprod_insert_updateP with congruence.
+    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
   Qed.
 
   (** Properties of iprod_singleton. *)
-  Context `{∀ x, Empty (B x)} `{∀ x, CMRAIdentity (B x)}.
+  Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}.
 
-  Lemma iprod_validN_singleton n x (y : B x) :
-    ✓{n} y <-> ✓{n} (iprod_singleton x y).
+  Lemma iprod_singleton_validN n x (y : B x) :
+    ✓{n} (iprod_singleton x y) ↔ ✓{n} y.
   Proof.
-    split.
-    - move=>Hx x'. destruct (decide (x = x')).
-      + subst x'. by rewrite iprod_lookup_singleton.
-      + rewrite iprod_lookup_singleton_ne //; [].
-        by apply cmra_empty_valid.
-    - move=>Hm. move: (Hm x). by rewrite iprod_lookup_singleton.
+    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
+    move=>Hx x'; destruct (decide (x = x')) as [->|];
+      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
+    by apply cmra_empty_valid.
   Qed.
 
   Lemma iprod_unit_singleton x (y : B x) :
     unit (iprod_singleton x y) ≡ iprod_singleton x (unit y).
   Proof.
-    move=>x'. rewrite iprod_lookup_unit. destruct (decide (x = x')).
-    - subst x'. by rewrite !iprod_lookup_singleton.
-    - rewrite !iprod_lookup_singleton_ne //; [].
-      by apply cmra_unit_empty.
+    by move=>x'; destruct (decide (x = x')) as [->|];
+      rewrite iprod_lookup_unit ?iprod_lookup_singleton
+      ?iprod_lookup_singleton_ne // cmra_unit_empty.
   Qed.
 
   Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
@@ -248,32 +226,45 @@ Section iprod_cmra.
     y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
     iprod_singleton x y1 ~~>: Q.
   Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
-
   Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
     y1 ~~>: P →
     iprod_singleton x y1 ~~>: λ g', ∃ y2, g' = iprod_singleton x y2 ∧ P y2.
   Proof. eauto using iprod_singleton_updateP. Qed.
+  Lemma iprod_singleton_update x y1 y2 :
+    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
+  Proof. eauto using iprod_insert_update. Qed.
 
   Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
-    (∅ ~~>: P) → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
-    ∅ ~~>: Q.
+    ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
   Proof.
-    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?).
-    { apply: Hg. }
-    exists (iprod_singleton x y2).
-    split; first by apply HQ.
-    intros x'; destruct (decide (x' = x)) as [->|];
-      rewrite iprod_lookup_op /iprod_singleton ?iprod_lookup_insert //; [].
-    move:(Hg x'). by rewrite iprod_lookup_insert_ne // left_id.
+    intros Hx HQ gf n Hg. destruct (Hx (gf x) n) as (y2&?&?); first apply Hg.
+    exists (iprod_singleton x y2); split; [by apply HQ|].
+    intros x'; destruct (decide (x' = x)) as [->|].
+    * by rewrite iprod_lookup_op iprod_lookup_singleton.
+    * rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
   Qed.
-
-  Lemma iprod_singleton_update x y1 y2 :
-    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
-  Proof. by intros; apply iprod_insert_update. Qed.
 End iprod_cmra.
 
 Arguments iprodRA {_} _.
 
+(** * Functor *)
+Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
+  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
+
+Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
+  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
+Proof. done. Qed.
+Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
+Proof. done. Qed.
+Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
+    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
+  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
+Proof. done. Qed.
+
+Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
+  (∀ x, Proper (dist n ==> dist n) (f x)) →
+  Proper (dist n ==> dist n) (iprod_map f).
+Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
 Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
   (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
 Proof.