More setoid stuff on lists and maps.

prelude/collections.v

@@ -11,6 +11,8 @@ Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
 (** * Basic theorems *)
 Section simple_collection.
   Context `{SimpleCollection A C}.
+  Implicit Types x y : A.
+  Implicit Types X Y : C.
 
   Lemma elem_of_empty x : x ∈ ∅ ↔ False.
   Proof. split. apply not_elem_of_empty. done. Qed.
@@ -47,9 +49,10 @@ Section simple_collection.
     * intros ??. rewrite elem_of_singleton. by intros ->.
     * intros Ex. by apply (Ex x), elem_of_singleton.
   Qed.
-  Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton.
+  Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
   Proof. by repeat intro; subst. Qed.
-  Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
+  Global Instance elem_of_proper :
+    Proper ((=) ==> (≡) ==> iff) ((∈) : A → C → Prop) | 5.
   Proof. intros ???; subst. firstorder. Qed.
   Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
@@ -59,7 +62,7 @@ Section simple_collection.
     * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
       intros. apply elem_of_union_r; auto.
   Qed.
-  Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
+  Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅.
   Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
   Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
   Proof. by rewrite elem_of_singleton. Qed.
@@ -266,19 +269,21 @@ Tactic Notation "esolve_elem_of" tactic3(tac) :=
   unfold_elem_of;
   naive_solver tac.
 Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.
- 
+
 (** * More theorems *)
 Section collection.
   Context `{Collection A C}.
+  Implicit Types X Y : C.
 
   Global Instance: Lattice C.
   Proof. split. apply _. firstorder auto. solve_elem_of. Qed.
-  Global Instance difference_proper : Proper ((≡) ==> (≡) ==> (≡)) (∖).
+  Global Instance difference_proper :
+     Proper ((≡) ==> (≡) ==> (≡)) (@difference C _).
   Proof.
     intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
     by rewrite !elem_of_difference, HX, HY.
   Qed.
-  Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
+  Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
   Proof. esolve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
   Proof. esolve_elem_of. Qed.
@@ -475,10 +480,12 @@ Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
 
 Section fresh.
   Context `{FreshSpec A C}.
+  Implicit Types X Y : C.
 
-  Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh.
+  Global Instance fresh_proper: Proper ((≡) ==> (=)) (fresh (C:=C)).
   Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-  Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list.
+  Global Instance fresh_list_proper:
+    Proper ((=) ==> (≡) ==> (=)) (fresh_list (C:=C)).
   Proof.
     intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|].
     apply IH. by rewrite E.
@@ -539,7 +546,7 @@ Section collection_monad.
   Proof. esolve_elem_of. Qed.
   Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X.
   Proof. esolve_elem_of. Qed.
-  Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) X :
+  Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
     g ∘ f <$> X ≡ g <$> (f <$> X).
   Proof. esolve_elem_of. Qed.
   Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :

prelude/fin_collections.v

@@ -12,15 +12,16 @@ Definition collection_fold `{Elements A C} {B}
 
 Section fin_collection.
 Context `{FinCollection A C}.
+Implicit Types X Y : C.
 
-Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) elements.
+Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
 Proof.
   intros ?? E. apply NoDup_Permutation.
   * apply NoDup_elements.
   * apply NoDup_elements.
   * intros. by rewrite !elem_of_elements, E.
 Qed.
-Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
+Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 Lemma size_empty : size (∅ : C) = 0.
 Proof.
@@ -148,7 +149,7 @@ Qed.
 Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
-  Proper ((≡) ==> R) (collection_fold f b).
+  Proper ((≡) ==> R) (collection_fold f b : C → B).
 Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
 Global Instance set_Forall_dec `(P : A → Prop)
   `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.

prelude/fin_maps.v

@@ -71,8 +71,8 @@ Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
 Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
   λ f, merge (difference_with f).
 
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 1 := λ m1 m2,
-  ∀ i, m1 !! i ≡ m2 !! i.
+Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+  λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the
 relation [R] holds for each pair in the intersection. *)
@@ -117,9 +117,8 @@ Context `{FinMap K M}.
 
 (** ** Setoids *)
 Section setoid.
-  Context `{Equiv A}.
-  Global Instance map_equivalence `{!Equivalence ((≡) : relation A)} :
-    Equivalence ((≡) : relation (M A)).
+  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+  Global Instance map_equivalence : Equivalence ((≡) : relation (M A)).
   Proof.
     split.
     * by intros m i.
@@ -130,7 +129,7 @@ Section setoid.
     Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance partial_alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) partial_alter.
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
   Proof.
     by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
       rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
@@ -151,12 +150,12 @@ Section setoid.
   Lemma merge_ext f g
       `{!PropHolds (f None None = None), !PropHolds (g None None = None)} :
     ((≡) ==> (≡) ==> (≡))%signature f g →
-    ((≡) ==> (≡) ==> (≡))%signature (merge f) (merge g).
+    ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
   Proof.
     by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
   Qed.
   Global Instance union_with_proper :
-    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==> (≡)) union_with.
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
   Proof.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
@@ -167,6 +166,16 @@ Section setoid.
     * by intros Hm; apply map_eq; intros i; unfold_leibniz; apply lookup_proper.
     * by intros <-; intros i; fold_leibniz.
   Qed.
+  Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
+  Proof.
+    split; [intros Hm; apply map_eq; intros i|by intros ->].
+    by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
+  Qed.
+  Lemma map_equiv_lookup (m1 m2 : M A) i x :
+    m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
+  Proof.
+    intros Hm ?. destruct (equiv_Some (m1 !! i) (m2 !! i) x) as (y&?&?); eauto.
+  Qed.
 End setoid.
 
 (** ** General properties *)

prelude/list.v

@@ -35,6 +35,12 @@ Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
 Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
 
 (** * Definitions *)
+(** Setoid equality lifted to lists *)
+Inductive list_equiv `{Equiv A} : Equiv (list A) :=
+  | nil_equiv : [] ≡ []
+  | cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
+Existing Instance list_equiv.
+
 (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
 in case [i] is out of bounds. *)
 Instance list_lookup {A} : Lookup nat A (list A) :=
@@ -356,6 +362,30 @@ Context {A : Type}.
 Implicit Types x y z : A.
 Implicit Types l k : list A.
 
+Section setoid.
+  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
+  Global Instance map_equivalence : Equivalence ((≡) : relation (list A)).
+  Proof.
+    split.
+    * intros l; induction l; constructor; auto.
+    * induction 1; constructor; auto.
+    * intros l1 l2 l3 Hl; revert l3.
+      induction Hl; inversion_clear 1; constructor; try etransitivity; eauto.
+  Qed.
+  Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
+  Proof. by constructor. Qed.
+  Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
+  Proof.
+    induction 1 as [|x y l k ?? IH]; intros ?? Htl; simpl; auto.
+    by apply cons_equiv, IH.
+  Qed.
+  Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
+  Proof.
+    intros l1 l2; split; [|by intros <-].
+    induction 1; f_equal; fold_leibniz; auto.
+  Qed.
+End setoid.
+
 Global Instance: Injective2 (=) (=) (=) (@cons A).
 Proof. by injection 1. Qed.
 Global Instance: ∀ k, Injective (=) (=) (k ++).

prelude/option.v

@@ -89,10 +89,9 @@ Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B →
 
 (** Setoids *)
 Section setoids.
-  Context `{Equiv A}.
+  Context `{Equiv A} `{!Equivalence ((≡) : relation A)}.
   Global Instance option_equiv : Equiv (option A) := option_Forall2 (≡).
-  Global Instance option_equivalence `{!Equivalence ((≡) : relation A)} :
-    Equivalence ((≡) : relation (option A)).
+  Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
   Proof.
     split.
     * by intros []; constructor.
@@ -106,6 +105,11 @@ Section setoids.
     intros x y; split; [destruct 1; fold_leibniz; congruence|].
     by intros <-; destruct x; constructor; fold_leibniz.
   Qed.
+  Lemma equiv_None (mx : option A) : mx ≡ None ↔ mx = None.
+  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
+  Lemma equiv_Some (mx my : option A) x :
+    mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
+  Proof. destruct 1; naive_solver. Qed.
 End setoids.
 
 (** Equality on [option] is decidable. *)

prelude/orders.v

@@ -309,7 +309,7 @@ End merge_sort_correct.
 (** We extend the canonical pre-order [⊆] to a partial order by defining setoid
 equality as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a
 setoid. *)
-Instance preorder_equiv `{SubsetEq A} : Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X.
+Instance preorder_equiv `{SubsetEq A} : Equiv A | 20 := λ X Y, X ⊆ Y ∧ Y ⊆ X.
 
 Section preorder.
   Context `{SubsetEq A, !PreOrder (@subseteq A _)}.
@@ -321,13 +321,13 @@ Section preorder.
     * by intros ?? [??].
     * by intros X Y Z [??] [??]; split; transitivity Y.
   Qed.
-  Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆).
+  Global Instance: Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation A).
   Proof.
     unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro.
     * transitivity X1. tauto. transitivity X2; tauto.
     * transitivity Y1. tauto. transitivity Y2; tauto.
   Qed.
-  Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
+  Lemma subset_spec (X Y : A) : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
   Proof.
     split.
     * intros [? HYX]. split. done. contradict HYX. by rewrite <-HYX.
@@ -388,20 +388,20 @@ Section join_semi_lattice.
   Proof. auto. Qed.
   Lemma union_empty X : X ∪ ∅ ⊆ X.
   Proof. by apply union_least. Qed.
-  Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (∪).
+  Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (@union A _).
   Proof.
     unfold equiv, preorder_equiv.
     split; apply union_preserving; simpl in *; tauto.
   Qed.
-  Global Instance: Idempotent (≡) (∪).
+  Global Instance: Idempotent ((≡) : relation A) (∪).
   Proof. split; eauto. Qed.
-  Global Instance: LeftId (≡) ∅ (∪).
+  Global Instance: LeftId ((≡) : relation A) ∅ (∪).
   Proof. split; eauto. Qed.
-  Global Instance: RightId (≡) ∅ (∪).
+  Global Instance: RightId ((≡) : relation A) ∅ (∪).
   Proof. split; eauto. Qed.
-  Global Instance: Commutative (≡) (∪).
+  Global Instance: Commutative ((≡) : relation A) (∪).
   Proof. split; auto. Qed.
-  Global Instance: Associative (≡) (∪).
+  Global Instance: Associative ((≡) : relation A) (∪).
   Proof. split; auto. Qed.
   Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y ≡ Y.
   Proof. repeat split; eauto. intros HXY. rewrite <-HXY. auto. Qed.
@@ -411,8 +411,8 @@ Section join_semi_lattice.
   Proof. apply subseteq_union. Qed.
   Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅.
   Proof. split; eauto. Qed.
-  Global Instance union_list_proper: Proper (Forall2 (≡) ==> (≡)) union_list.
-  Proof. induction 1; simpl. done. by apply union_proper. Qed.
+  Global Instance union_list_proper: Proper ((≡) ==> (≡)) (union_list (A:=A)).
+  Proof. by induction 1; simpl; try apply union_proper. Qed.
   Lemma union_list_nil : ⋃ @nil A = ∅.
   Proof. done. Qed.
   Lemma union_list_cons X Xs : ⋃ (X :: Xs) = X ∪ ⋃ Xs.
@@ -514,16 +514,16 @@ Section meet_semi_lattice.
   Lemma intersection_preserving X1 X2 Y1 Y2 :
     X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2.
   Proof. auto. Qed.
-  Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩).
+  Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (@intersection A _).
   Proof.
     unfold equiv, preorder_equiv. split;
       apply intersection_preserving; simpl in *; tauto.
   Qed.
-  Global Instance: Idempotent (≡) (∩).
+  Global Instance: Idempotent ((≡) : relation A) (∩).
   Proof. split; eauto. Qed.
-  Global Instance: Commutative (≡) (∩).
+  Global Instance: Commutative ((≡) : relation A) (∩).
   Proof. split; auto. Qed.
-  Global Instance: Associative (≡) (∩).
+  Global Instance: Associative ((≡) : relation A) (∩).
   Proof. split; auto. Qed.
   Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
   Proof. repeat split; eauto. intros HXY. rewrite <-HXY. auto. Qed.
@@ -553,11 +553,11 @@ End meet_semi_lattice.
 Section lattice.
   Context `{Empty A, Lattice A, !EmptySpec A}.
 
-  Global Instance: LeftAbsorb (≡) ∅ (∩).
+  Global Instance: LeftAbsorb ((≡) : relation A) ∅ (∩).
   Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed.
-  Global Instance: RightAbsorb (≡) ∅ (∩).
+  Global Instance: RightAbsorb ((≡) : relation A) ∅ (∩).
   Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
-  Global Instance: LeftDistr (≡) (∪) (∩).
+  Global Instance: LeftDistr ((≡) : relation A) (∪) (∩).
   Proof.
     intros X Y Z. split; [|apply lattice_distr].
     apply union_least.
@@ -566,9 +566,9 @@ Section lattice.
     * apply union_subseteq_r_transitive, intersection_subseteq_l.
     * apply union_subseteq_r_transitive, intersection_subseteq_r.
   Qed.
-  Global Instance: RightDistr (≡) (∪) (∩).
+  Global Instance: RightDistr ((≡) : relation A) (∪) (∩).
   Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed.
-  Global Instance: LeftDistr (≡) (∩) (∪).
+  Global Instance: LeftDistr ((≡) : relation A) (∩) (∪).
   Proof.
     intros X Y Z. split.
     * rewrite (left_distr (∪) (∩)).
@@ -582,7 +582,7 @@ Section lattice.
       + apply intersection_subseteq_r_transitive, union_subseteq_l.
       + apply intersection_subseteq_r_transitive, union_subseteq_r.
   Qed.
-  Global Instance: RightDistr (≡) (∩) (∪).
+  Global Instance: RightDistr ((≡) : relation A) (∩) (∪).
   Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed.
 
   Section leibniz.