From a4363377f87eb51d9bd3dd9f9b9d8f20de8716e1 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 18 Nov 2015 12:29:52 +0100 Subject: [PATCH] More setoid stuff on lists and maps. --- theories/collections.v | 25 +++++++++++++++-------- theories/fin_collections.v | 7 ++++--- theories/fin_maps.v | 25 +++++++++++++++-------- theories/list.v | 30 +++++++++++++++++++++++++++ theories/option.v | 10 ++++++--- theories/orders.v | 42 +++++++++++++++++++------------------- 6 files changed, 95 insertions(+), 44 deletions(-) diff --git a/theories/collections.v b/theories/collections.v index a43a22e..619134d 100644 --- a/theories/collections.v +++ b/theories/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) : diff --git a/theories/fin_collections.v b/theories/fin_collections.v index 28591e6..2aa50c4 100644 --- a/theories/fin_collections.v +++ b/theories/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. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 7e12d0e..ef37ebd 100644 --- a/theories/fin_maps.v +++ b/theories/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 *) diff --git a/theories/list.v b/theories/list.v index 2b39ffe..539388a 100644 --- a/theories/list.v +++ b/theories/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 ++). diff --git a/theories/option.v b/theories/option.v index ed2392d..ed262cf 100644 --- a/theories/option.v +++ b/theories/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. *) diff --git a/theories/orders.v b/theories/orders.v index 09ae83d..2a8b142 100644 --- a/theories/orders.v +++ b/theories/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. -- GitLab