Change styling

stdpp/fin_map_img.v

@@ -14,28 +14,28 @@ Class FinMapImg K A M D
     Union D, Intersection D, Difference D} := {
   finmap_img_map :> FinMap K M;
   finmap_img_set :> Set_ A D;
-  elem_of_img (m:M A) (v:A) : v ∈ img m <-> ∃ (k:K), m !! k = Some v
+  elem_of_img (m : M A) (v : A) : v ∈ img m ↔ ∃ (k : K), m !! k = Some v
 }.
 
 Section fin_map_img.
   Context `{FinMapImg K A M D}.
-  Implicit Types (m:M A) (k:K) (v:A).
+  Implicit Types (m : M A) (k : K) (v : A).
 
   (* avoid writing ≡@{D} everywhere... *)
   Infix "≡" := (@equiv D _) (at level 70).
 
-  Lemma elem_of_img_2 m k v: m !! k = Some v -> v ∈ img m.
+  Lemma elem_of_img_2 m k v : m !! k = Some v → v ∈ img m.
   Proof. intros Hmkv. rewrite elem_of_img. exists k. exact Hmkv. Qed.
 
-  Lemma not_elem_of_img m v: v ∉ img m <-> ∀ k, m !! k ≠ Some v.
+  Lemma not_elem_of_img m v : v ∉ img m ↔ ∀ k, m !! k ≠ Some v.
   Proof. rewrite elem_of_img. split.
   - intros Hm k Hk. contradiction (Hm (ex_intro _ k Hk)).
   - intros Hm [k Hk]. contradiction (Hm k Hk).
   Qed.
-  Lemma not_elem_of_img_1 m v k: v ∉ img m -> m !! k ≠ Some v.
+  Lemma not_elem_of_img_1 m v k : v ∉ img m → m !! k ≠ Some v.
   Proof. intros Hm. apply not_elem_of_img. exact Hm. Qed.
 
-  Lemma subseteq_img (m1 m2:M A): m1 ⊆ m2 -> img m1 ⊆ img m2.
+  Lemma subseteq_img (m1 m2 : M A) : m1 ⊆ m2 → img m1 ⊆ img m2.
   Proof.
     intros Hm v Hv. rewrite elem_of_img.
     apply elem_of_img in Hv as [k Hv]. exists k.
@@ -43,25 +43,25 @@ Section fin_map_img.
     apply (Hm k v Hv).
   Qed.
 
-  Lemma img_filter (P : K * A → Prop) `{!∀ x, Decision (P x)} m (X:D):
+  Lemma img_filter (P : K * A → Prop) `{!∀ x, Decision (P x)} m (X : D) :
     (∀ v, v ∈ X ↔ ∃ k, m !! k = Some v ∧ P (k, v)) →
     img (filter P m) ≡ X.
   Proof.
     intros HX i. rewrite elem_of_img, HX.
     unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
   Qed.
-  Lemma img_filter_subseteq (P : K * A → Prop) `{!∀ x, Decision (P x)} m:
+  Lemma img_filter_subseteq (P : K * A → Prop) `{!∀ x, Decision (P x)} m :
     img (filter P m) ⊆ img m.
   Proof. apply subseteq_img, map_filter_subseteq. Qed.
 
-  Lemma img_empty: img (∅ : M A) ≡ ∅.
+  Lemma img_empty : img (∅ : M A) ≡ ∅.
   Proof.
     rewrite set_equiv. intros x. split; intros Hempty.
     - apply elem_of_img in Hempty. destruct Hempty as [k Hk].
       rewrite lookup_empty in Hk. discriminate.
     - rewrite elem_of_empty in Hempty. contradiction Hempty.
   Qed.
-  Lemma img_empty_iff m: img m ≡ ∅ ↔ m = ∅.
+  Lemma img_empty_iff m : img m ≡ ∅ ↔ m = ∅.
   Proof.
     split; [|intros ->; by rewrite img_empty].
     intros E. apply map_empty. intros i.
@@ -69,26 +69,26 @@ Section fin_map_img.
     - apply elem_of_img_2 in Hm. set_solver.
     - reflexivity.
   Qed.
-  Lemma img_empty_inv m: img m ≡ ∅ → m = ∅.
+  Lemma img_empty_inv m : img m ≡ ∅ → m = ∅.
   Proof. apply img_empty_iff. Qed.
 
-  Lemma img_insert k v m: img (<[k:=v]> m) ⊆ {[ v ]} ∪ img m.
+  Lemma img_insert k v m : img (<[k:=v]> m) ⊆ {[ v ]} ∪ img m.
   Proof.
     intros w Hw. apply elem_of_img in Hw as [k' Hw].
     apply lookup_insert_Some in Hw as [[Hkk' Hvw] | [Hkk' Hmk']].
     - apply elem_of_union_l, elem_of_singleton. symmetry. apply Hvw.
     - apply elem_of_union_r, elem_of_img. exists k'. apply Hmk'.
   Qed.
-  Lemma elem_of_img_insert k v m: v ∈ img (<[k:=v]> m).
+  Lemma elem_of_img_insert k v m : v ∈ img (<[k:=v]> m).
   Proof. apply elem_of_img. exists k. apply lookup_insert. Qed.
-  Lemma elem_of_img_insert_ne k v w m: v ≠ w -> w ∈ img(<[k:=v]> m) -> w ∈ img m.
+  Lemma elem_of_img_insert_ne k v w m : v ≠ w → w ∈ img(<[k:=v]> m) → w ∈ img m.
   Proof. rewrite !elem_of_img. intros Hv [k' Hk].
     destruct (decide (k=k')) as [Heq|Heq].
     - rewrite Heq, lookup_insert in Hk.
       apply Some_inj in Hk. contradiction (Hv Hk).
     - rewrite (lookup_insert_ne _ _ _ _ Heq) in Hk. exists k'. exact Hk.
   Qed.
-  Lemma img_insert_notin k v m: m!!k = None -> img (<[k:=v]> m) ≡ {[ v ]} ∪ img m.
+  Lemma img_insert_notin k v m : m!!k = None → img (<[k:=v]> m) ≡ {[ v ]} ∪ img m.
   Proof.
     intros Hm w. rewrite elem_of_union, !elem_of_img, elem_of_singleton.
     setoid_rewrite lookup_insert_Some.
@@ -105,9 +105,9 @@ Section fin_map_img.
     setoid_rewrite lookup_singleton_Some. set_solver.
   Qed.
 
-  Lemma elem_of_img_union m1 m2 v:
-    v ∈ img (m1 ∪ m2) ->
-    v ∈ img m1 \/ v ∈ img m2.
+  Lemma elem_of_img_union m1 m2 v :
+    v ∈ img (m1 ∪ m2) →
+    v ∈ img m1 ∨ v ∈ img m2.
   Proof.
     intros Hv12.
     (* destruct (elem_of_img (m1 ∪ m2) v) as . *)
@@ -117,9 +117,9 @@ Section fin_map_img.
     destruct (Hspec Hv12) as [Hm | [_ Hm]];
     [ left | right ]; rewrite elem_of_img; exists k; exact Hm.
   Qed.
-  Lemma img_union_subseteq m1 m2: img (m1 ∪ m2) ⊆ img m1 ∪ img m2.
+  Lemma img_union_subseteq m1 m2 : img (m1 ∪ m2) ⊆ img m1 ∪ img m2.
   Proof. intros v Hv. apply elem_of_union, elem_of_img_union. exact Hv. Qed.
-  Lemma img_union_subseteq_l m1 m2: img m1 ⊆ img (m1 ∪ m2).
+  Lemma img_union_subseteq_l m1 m2 : img m1 ⊆ img (m1 ∪ m2).
   Proof.
     intros v Hv. apply elem_of_img in Hv as [k Hv].
     rewrite elem_of_img.
@@ -127,7 +127,7 @@ Section fin_map_img.
   Qed.
 
   Lemma img_fmap `{Img (M B) D2, ElemOf B D2, Empty D2, Singleton B D2, Union D2, Intersection D2, Difference D2, !FinMapImg K B M D2}
-        `{Elements A D, EqDecision A, !FinSet A D} (f: A -> B) m:
+        `{Elements A D, EqDecision A, !FinSet A D} (f : A → B) m :
     img (f <$> m) ≡@{D2} set_map f (img m).
   Proof.
     apply set_equiv. intros v. rewrite elem_of_img, elem_of_map. split.
@@ -141,7 +141,7 @@ Section fin_map_img.
   Qed.
 
   Lemma img_kmap `{Img (M2 A) D, FinMap K2 M2, !FinMapImg K2 A M2 D}
-        (f: K -> K2) `{!Inj (=) (=) f} m:
+        (f : K → K2) `{!Inj (=) (=) f} m :
     img (kmap (M2:=M2) f m) ≡ img m.
   Proof.
     apply set_equiv. intros v.
@@ -150,7 +150,7 @@ Section fin_map_img.
     - exists (f k). rewrite lookup_kmap; done.
   Qed.
 
-  Lemma img_finite m: set_finite (img m).
+  Lemma img_finite m : set_finite (img m).
   Proof.
     induction m as [|x i m Hm IHm] using map_ind .
     - rewrite img_empty. apply empty_finite.
@@ -158,18 +158,18 @@ Section fin_map_img.
       apply union_finite; [ apply singleton_finite | apply IHm ].
   Qed.
 
-  Lemma img_list_to_map l:
-    (∀ k v v', (k,v) ∈ l -> (k,v') ∈ l -> v = v') ->
+  Lemma img_list_to_map l :
+    (∀ k v v', (k,v) ∈ l → (k,v') ∈ l → v = v') →
     img (list_to_map l : M A) ≡ list_to_set l.*2.
   Proof.
     induction l as [|a l IH].
     - by rewrite img_empty.
     - intros Hl. destruct a as [k v]. simpl.
-      assert (IH': img (list_to_map l: M A) ≡ list_to_set l.*2).
+      assert (IH' : img (list_to_map l : M A) ≡ list_to_set l.*2).
       { apply IH. intros k' v' v'' Hv' Hv''. apply (Hl k' v' v''); apply elem_of_list_further; assumption. }
       rewrite <- IH'.
       destruct ((list_to_map l : M A)!!k) as [w|] eqn:Hw.
-      + assert (Hvw: v = w).
+      + assert (Hvw : v = w).
         { apply (Hl k); [ apply elem_of_list_here | apply elem_of_list_further ].
           apply elem_of_list_to_map_2. exact Hw. }
         rewrite <- Hvw in Hw. apply set_equiv. intros x. split.
@@ -183,7 +183,7 @@ Section fin_map_img.
   Qed.
 
   (** Alternative definition of [img] in terms of [map_to_list]. *)
-  Lemma img_alt m: img m ≡ list_to_set (map_to_list m).*2.
+  Lemma img_alt m : img m ≡ list_to_set (map_to_list m).*2.
   Proof.
     rewrite <-(list_to_map_to_list m) at 1.
     rewrite img_list_to_map; [reflexivity|].
@@ -191,8 +191,8 @@ Section fin_map_img.
     rewrite Hv in Hv'. apply Some_inj. exact Hv'.
   Qed.
 
-  Lemma img_singleton_inv m v:
-    img m ≡ {[ v ]} -> ∀ k, m !! k = None \/ m !! k = Some v.
+  Lemma img_singleton_inv m v :
+    img m ≡ {[ v ]} → ∀ k, m !! k = None ∨ m !! k = Some v.
   Proof.
     intros Hm k. destruct (m!!k) eqn:Hmk.
     - right. apply elem_of_img_2 in Hmk. rewrite Hm, elem_of_singleton in Hmk.
@@ -200,14 +200,14 @@ Section fin_map_img.
     - left. reflexivity.
   Qed.
 
-  Lemma img_union_inv `{!RelDecision (∈@{D})} X Y m:
-    X ## Y ->
-    img m ≡ X ∪ Y ->
-    ∃ m1 m2, m = m1 ∪ m2 /\ m1 ##ₘ m2 /\ img m1 ≡ X /\ img m2 ≡ Y.
+  Lemma img_union_inv `{!RelDecision (∈@{D})} X Y m :
+    X ## Y →
+    img m ≡ X ∪ Y →
+    ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ img m1 ≡ X ∧ img m2 ≡ Y.
   Proof.
     intros Hsep Himg.
     exists (filter (λ '(_,x), x ∈ X) m), (filter (λ '(_,x), x ∉ X) m).
-    assert (Hdisj: filter (λ '(_, x), x ∈ X) m ##ₘ filter (λ '(_, x), x ∉ X) m).
+    assert (Hdisj : filter (λ '(_, x), x ∈ X) m ##ₘ filter (λ '(_, x), x ∉ X) m).
     { apply map_disjoint_filter_complement. }
     split_and!.
     - symmetry. apply map_filter_union_complement.
@@ -226,46 +226,46 @@ Section fin_map_img.
   Section Leibniz.
     Context `{!LeibnizEquiv D}.
 
-    Lemma img_empty_L: img (@empty (M A) _) = ∅.
+    Lemma img_empty_L : img (@empty (M A) _) = ∅.
     Proof. unfold_leibniz. exact img_empty. Qed.
 
-    Lemma img_empty_iff_L m: img m = ∅ ↔ m = ∅.
+    Lemma img_empty_iff_L m : img m = ∅ ↔ m = ∅.
     Proof. unfold_leibniz. apply img_empty_iff. Qed.
-    Lemma img_empty_inv_L m: img m = ∅ → m = ∅.
+    Lemma img_empty_inv_L m : img m = ∅ → m = ∅.
     Proof. apply img_empty_iff_L. Qed.
 
-    Lemma img_singleton_L k v: img ({[ k := v ]} : M A) = {[ v ]}.
+    Lemma img_singleton_L k v : img ({[ k := v ]} : M A) = {[ v ]}.
     Proof. unfold_leibniz. apply img_singleton. Qed.
 
-    Lemma img_insert_notin_L k v m: m!!k=None -> img (<[k:=v]> m) = {[ v ]} ∪ img m.
+    Lemma img_insert_notin_L k v m : m!!k=None → img (<[k:=v]> m) = {[ v ]} ∪ img m.
     Proof. unfold_leibniz. apply img_insert_notin. Qed.
 
     Lemma img_fmap_L `{Img (M B) D2, ElemOf B D2, Empty D2, Singleton B D2, Union D2, Intersection D2, Difference D2, !FinMapImg K B M D2}
-          `{Elements A D, EqDecision A, !FinSet A D, !LeibnizEquiv D2} (f: A -> B) m:
+          `{Elements A D, EqDecision A, !FinSet A D, !LeibnizEquiv D2} (f : A → B) m :
       img (f <$> m) = set_map f (img m).
     Proof. unfold_leibniz. apply img_fmap. Qed.
 
     Lemma img_kmap_L `{Img (M2 A) D, FinMap K2 M2, !FinMapImg K2 A M2 D}
-          (f: K -> K2) `{!Inj (=) (=) f} m:
+          (f : K → K2) `{!Inj (=) (=) f} m :
       img (kmap (M2:=M2) f m) = img m.
     Proof. unfold_leibniz. apply img_kmap. done. Qed.
 
-    Lemma img_list_to_map_L l:
-      (∀ k v v', (k,v) ∈ l -> (k,v') ∈ l -> v = v') ->
+    Lemma img_list_to_map_L l :
+      (∀ k v v', (k,v) ∈ l → (k,v') ∈ l → v = v') →
       img (list_to_map l : M A) = list_to_set l.*2.
     Proof. unfold_leibniz. apply img_list_to_map. Qed.
 
-    Lemma img_alt_L m: img m = list_to_set (map_to_list m).*2.
+    Lemma img_alt_L m : img m = list_to_set (map_to_list m).*2.
     Proof. unfold_leibniz. apply img_alt. Qed.
 
-    Lemma img_singleton_inv_L m v:
-      img m = {[ v ]} -> ∀ k, m !! k = None \/ m !! k = Some v.
+    Lemma img_singleton_inv_L m v :
+      img m = {[ v ]} → ∀ k, m !! k = None ∨ m !! k = Some v.
     Proof. unfold_leibniz. apply img_singleton_inv. Qed.
 
-    Lemma img_union_inv_L `{!RelDecision (∈@{D})} X Y m:
-      X ## Y ->
-      img m = X ∪ Y ->
-      ∃ m1 m2, m = m1 ∪ m2 /\ m1 ##ₘ m2 /\ img m1 = X /\ img m2 = Y.
+    Lemma img_union_inv_L `{!RelDecision (∈@{D})} X Y m :
+      X ## Y →
+      img m = X ∪ Y →
+      ∃ m1 m2, m = m1 ∪ m2 ∧ m1 ##ₘ m2 ∧ img m1 = X ∧ img m2 = Y.
     Proof. unfold_leibniz. apply img_union_inv. Qed.
   End Leibniz.
 
@@ -279,7 +279,7 @@ Global Instance fin_map_img K A M D
 : Img M D := map_to_set (fun _ a => a).
 
 Global Instance fin_map_img_spec K A M D
-  `{HFinMap:FinMap K M} `{HFinSet:FinSet A D} : FinMapImg K A M D.
+  `{HFinMap : FinMap K M} `{HFinSet : FinSet A D} : FinMapImg K A M D.
 Proof.
   split; [exact HFinMap | apply fin_set_set |].
   unfold img, fin_map_img. intros m v. rewrite elem_of_map_to_set. split.