orders.v 7.25 KB
 Robbert Krebbers committed Aug 29, 2012 1 2 3 4 ``````(* Copyright (c) 2012, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) (** This file collects common properties of pre-orders and semi lattices. This theory will mainly be used for the theory on collections and finite maps. *) `````` Robbert Krebbers committed Oct 19, 2012 5 6 ``````Require Import SetoidList. Require Export base decidable tactics list. `````` Robbert Krebbers committed Jun 11, 2012 7 `````` `````` Robbert Krebbers committed Aug 29, 2012 8 9 10 ``````(** * Pre-orders *) (** We extend a pre-order to a partial order by defining equality as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a setoid. *) `````` Robbert Krebbers committed Jun 11, 2012 11 12 13 14 15 ``````Section preorder. Context `{SubsetEq A} `{!PreOrder (⊆)}. Global Instance preorder_equiv: Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X. Instance preorder_equivalence: @Equivalence A (≡). `````` Robbert Krebbers committed Aug 21, 2012 16 17 18 19 20 21 `````` Proof. split. * firstorder. * firstorder. * intros x y z; split; transitivity y; firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 22 23 24 `````` Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆). Proof. `````` Robbert Krebbers committed Aug 21, 2012 25 26 27 28 `````` unfold equiv, preorder_equiv. intros x1 y1 ? x2 y2 ?. split; intro. * transitivity x1. tauto. transitivity x2; tauto. * transitivity y1. tauto. transitivity y2; tauto. `````` Robbert Krebbers committed Jun 11, 2012 29 30 `````` Qed. `````` Robbert Krebbers committed Jan 05, 2013 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 `````` Global Instance preorder_subset: Subset A := λ X Y, X ⊆ Y ∧ Y ⊈ X. Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X. Proof. done. Qed. Lemma subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. by intros [? _]. Qed. Lemma subset_trans_l X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z. Proof. intros [? Hxy] ?. split. * by transitivity Y. * contradict Hxy. by transitivity Z. Qed. Lemma subset_trans_r X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z. Proof. intros ? [? Hyz]. split. * by transitivity Y. * contradict Hyz. by transitivity X. Qed. Global Instance: StrictOrder (⊂). Proof. split. * firstorder. * eauto using subset_trans_r, subset_subseteq. Qed. Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊂). Proof. unfold subset, preorder_subset. solve_proper. Qed. `````` Robbert Krebbers committed Oct 19, 2012 59 60 61 `````` Context `{∀ X Y : A, Decision (X ⊆ Y)}. Global Instance preorder_equiv_dec_slow (X Y : A) : Decision (X ≡ Y) | 100 := _. `````` Robbert Krebbers committed Jan 05, 2013 62 63 64 65 66 67 68 69 70 `````` Global Instance preorder_subset_dec_slow (X Y : A) : Decision (X ⊂ Y) | 100 := _. Lemma subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y. Proof. destruct (decide (Y ⊆ X)). * by right. * by left. Qed. `````` Robbert Krebbers committed Oct 19, 2012 71 ``````End preorder. `````` Robbert Krebbers committed Jan 05, 2013 72 `````` `````` Robbert Krebbers committed Oct 19, 2012 73 ``````Typeclasses Opaque preorder_equiv. `````` Robbert Krebbers committed Aug 21, 2012 74 75 ``````Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. `````` Robbert Krebbers committed Jun 11, 2012 76 `````` `````` Robbert Krebbers committed Aug 29, 2012 77 78 ``````(** * Join semi lattices *) (** General purpose theorems on join semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 79 80 81 82 83 84 85 86 87 88 89 90 91 92 ``````Section bounded_join_sl. Context `{BoundedJoinSemiLattice A}. Hint Resolve subseteq_empty subseteq_union_l subseteq_union_r union_least. Lemma union_compat_l x1 x2 y : x1 ⊆ x2 → x1 ⊆ x2 ∪ y. Proof. intros. transitivity x2; auto. Qed. Lemma union_compat_r x1 x2 y : x1 ⊆ x2 → x1 ⊆ y ∪ x2. Proof. intros. transitivity x2; auto. Qed. Hint Resolve union_compat_l union_compat_r. Lemma union_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∪ y1 ⊆ x2 ∪ y2. Proof. auto. Qed. Lemma union_empty x : x ∪ ∅ ⊆ x. `````` Robbert Krebbers committed Oct 19, 2012 93 `````` Proof. by apply union_least. Qed. `````` Robbert Krebbers committed Jun 11, 2012 94 95 96 97 98 99 100 `````` Lemma union_comm x y : x ∪ y ⊆ y ∪ x. Proof. auto. Qed. Lemma union_assoc_1 x y z : (x ∪ y) ∪ z ⊆ x ∪ (y ∪ z). Proof. auto. Qed. Lemma union_assoc_2 x y z : x ∪ (y ∪ z) ⊆ (x ∪ y) ∪ z. Proof. auto. Qed. `````` Robbert Krebbers committed Oct 19, 2012 101 `````` Global Instance union_proper: Proper ((≡) ==> (≡) ==> (≡)) (∪). `````` Robbert Krebbers committed Aug 21, 2012 102 103 104 `````` Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 `````` Global Instance: Idempotent (≡) (∪). Proof. split; eauto. Qed. Global Instance: LeftId (≡) ∅ (∪). Proof. split; eauto. Qed. Global Instance: RightId (≡) ∅ (∪). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∪). Proof. split; apply union_comm. Qed. Global Instance: Associative (≡) (∪). Proof. split. apply union_assoc_2. apply union_assoc_1. Qed. Lemma subseteq_union X Y : X ⊆ Y ↔ X ∪ Y ≡ Y. Proof. repeat split; eauto. intros E. rewrite <-E. auto. Qed. Lemma subseteq_union_1 X Y : X ⊆ Y → X ∪ Y ≡ Y. Proof. apply subseteq_union. Qed. Lemma subseteq_union_2 X Y : X ∪ Y ≡ Y → X ⊆ Y. Proof. apply subseteq_union. Qed. Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅. Proof. split; eauto. Qed. `````` Robbert Krebbers committed Oct 19, 2012 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 `````` Global Instance: Proper (eqlistA (≡) ==> (≡)) union_list. Proof. induction 1; simpl. * done. * by apply union_proper. Qed. Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅. Proof. split. * intros E. split; apply equiv_empty; by transitivity (X ∪ Y); [auto | rewrite E]. * intros [E1 E2]. by rewrite E1, E2, (left_id _ _). Qed. Lemma empty_list_union Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs. Proof. split. * induction Xs; simpl; rewrite ?empty_union; intuition. * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union. Qed. Context `{∀ X Y : A, Decision (X ⊆ Y)}. Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅. Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed. Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs. Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed. `````` Robbert Krebbers committed Jun 11, 2012 152 153 ``````End bounded_join_sl. `````` Robbert Krebbers committed Aug 29, 2012 154 155 ``````(** * Meet semi lattices *) (** The dual of the above section, but now for meet semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 156 157 158 ``````Section meet_sl. Context `{MeetSemiLattice A}. `````` Robbert Krebbers committed Aug 21, 2012 159 160 `````` Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest. `````` Robbert Krebbers committed Jun 11, 2012 161 162 163 164 165 166 167 `````` Lemma intersection_compat_l x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2. Proof. intros. transitivity x1; auto. Qed. Lemma intersection_compat_r x1 x2 y : x1 ⊆ x2 → y ∩ x1 ⊆ x2. Proof. intros. transitivity x1; auto. Qed. Hint Resolve intersection_compat_l intersection_compat_r. `````` Robbert Krebbers committed Nov 12, 2012 168 169 `````` Lemma intersection_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2. `````` Robbert Krebbers committed Jun 11, 2012 170 171 172 173 174 175 176 177 178 `````` Proof. auto. Qed. Lemma intersection_comm x y : x ∩ y ⊆ y ∩ x. Proof. auto. Qed. Lemma intersection_assoc_1 x y z : (x ∩ y) ∩ z ⊆ x ∩ (y ∩ z). Proof. auto. Qed. Lemma intersection_assoc_2 x y z : x ∩ (y ∩ z) ⊆ (x ∩ y) ∩ z. Proof. auto. Qed. Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩). `````` Robbert Krebbers committed Aug 21, 2012 179 180 181 182 `````` Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 183 184 185 186 187 188 189 190 191 192 193 194 195 196 `````` Global Instance: Idempotent (≡) (∩). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∩). Proof. split; apply intersection_comm. Qed. Global Instance: Associative (≡) (∩). Proof. split. apply intersection_assoc_2. apply intersection_assoc_1. Qed. Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X. Proof. repeat split; eauto. intros E. rewrite <-E. auto. Qed. Lemma subseteq_intersection_1 X Y : X ⊆ Y → X ∩ Y ≡ X. Proof. apply subseteq_intersection. Qed. Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y. Proof. apply subseteq_intersection. Qed. End meet_sl. `````` Robbert Krebbers committed Oct 19, 2012 197 198 199 200 201 202 203 204 205 206 207 208 209 210 `````` (** * Lower bounded lattices *) Section lower_bounded_lattice. Context `{LowerBoundedLattice A}. Global Instance: LeftAbsorb (≡) ∅ (∩). Proof. split. * by apply subseteq_intersection_l. * by apply subseteq_empty. Qed. Global Instance: RightAbsorb (≡) ∅ (∩). Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed. End lower_bounded_lattice.``````