orders.v 14.4 KB
 Robbert Krebbers committed Feb 19, 2013 1 ``````(* Copyright (c) 2012-2013, Robbert Krebbers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 3 4 ``````(* 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 `````` 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. `````` Robbert Krebbers committed Feb 19, 2013 34 35 36 37 38 39 `````` Lemma subset_spec_alt X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y. Proof. split. * intros [? HYX]. split. done. contradict HYX. by rewrite HYX. * intros [? HXY]. split. done. by contradict HXY. Qed. `````` Robbert Krebbers committed Jan 05, 2013 40 41 42 43 44 `````` 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. `````` Robbert Krebbers committed Feb 19, 2013 45 `````` intros [? HXY] ?. split. `````` Robbert Krebbers committed Jan 05, 2013 46 `````` * by transitivity Y. `````` Robbert Krebbers committed Feb 19, 2013 47 `````` * contradict HXY. by transitivity Z. `````` Robbert Krebbers committed Jan 05, 2013 48 49 50 `````` Qed. Lemma subset_trans_r X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z. Proof. `````` Robbert Krebbers committed Feb 19, 2013 51 `````` intros ? [? HYZ]. split. `````` Robbert Krebbers committed Jan 05, 2013 52 `````` * by transitivity Y. `````` Robbert Krebbers committed Feb 19, 2013 53 `````` * contradict HYZ. by transitivity X. `````` Robbert Krebbers committed Jan 05, 2013 54 55 56 57 58 59 60 61 62 63 64 `````` 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 Feb 19, 2013 65 66 `````` Section leibniz. Context `{!LeibnizEquiv A}. `````` Robbert Krebbers committed Jan 05, 2013 67 `````` `````` Robbert Krebbers committed Feb 19, 2013 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 `````` Lemma subset_spec_alt_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y. Proof. unfold_leibniz. apply subset_spec_alt. Qed. End leibniz. Section dec. Context `{∀ X Y : A, Decision (X ⊆ Y)}. Global Instance preorder_equiv_dec_slow (X Y : A) : Decision (X ≡ Y) | 100 := _. 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. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed. Lemma not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y. Proof. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed. Context `{!LeibnizEquiv A}. Lemma subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y. Proof. unfold_leibniz. apply subseteq_inv. Qed. Lemma not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y. Proof. unfold_leibniz. apply not_subset_inv. Qed. End dec. `````` Robbert Krebbers committed Oct 19, 2012 92 ``````End preorder. `````` Robbert Krebbers committed Jan 05, 2013 93 `````` `````` Robbert Krebbers committed Oct 19, 2012 94 ``````Typeclasses Opaque preorder_equiv. `````` Robbert Krebbers committed Feb 19, 2013 95 ``````Typeclasses Opaque preorder_subset. `````` Robbert Krebbers committed Aug 21, 2012 96 97 ``````Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. `````` Robbert Krebbers committed Jun 11, 2012 98 `````` `````` Robbert Krebbers committed Feb 19, 2013 99 100 101 102 103 104 105 106 107 108 109 110 ``````(** * Partial orders *) Section partialorder. Context `{PartialOrder A}. Global Instance: LeibnizEquiv A. Proof. split. * intros [??]. by apply (anti_symmetric _). * intros. by subst. Qed. End partialorder. `````` Robbert Krebbers committed Aug 29, 2012 111 112 ``````(** * Join semi lattices *) (** General purpose theorems on join semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 113 114 115 ``````Section bounded_join_sl. Context `{BoundedJoinSemiLattice A}. `````` Robbert Krebbers committed Feb 19, 2013 116 `````` Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least. `````` Robbert Krebbers committed Jun 11, 2012 117 `````` `````` Robbert Krebbers committed Feb 19, 2013 118 `````` Lemma union_subseteq_l_alt x1 x2 y : x1 ⊆ x2 → x1 ⊆ x2 ∪ y. `````` Robbert Krebbers committed Jun 11, 2012 119 `````` Proof. intros. transitivity x2; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 120 `````` Lemma union_subseteq_r_alt x1 x2 y : x1 ⊆ x2 → x1 ⊆ y ∪ x2. `````` Robbert Krebbers committed Jun 11, 2012 121 `````` Proof. intros. transitivity x2; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 122 `````` Hint Resolve union_subseteq_l_alt union_subseteq_r_alt. `````` Robbert Krebbers committed Jun 11, 2012 123 `````` `````` Robbert Krebbers committed Feb 19, 2013 124 125 126 127 128 129 130 131 132 133 134 `````` Lemma union_preserving_l x y1 y2 : y1 ⊆ y2 → x ∪ y1 ⊆ x ∪ y2. Proof. auto. Qed. Lemma union_preserving_r x1 x2 y : x1 ⊆ x2 → x1 ∪ y ⊆ x2 ∪ y. Proof. auto. Qed. Lemma union_preserving x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∪ y1 ⊆ x2 ∪ y2. `````` Robbert Krebbers committed Jun 11, 2012 135 `````` Proof. auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 136 `````` `````` Robbert Krebbers committed Jun 11, 2012 137 `````` Lemma union_empty x : x ∪ ∅ ⊆ x. `````` Robbert Krebbers committed Oct 19, 2012 138 `````` Proof. by apply union_least. Qed. `````` Robbert Krebbers committed Feb 19, 2013 139 `````` Lemma union_comm_1 x y : x ∪ y ⊆ y ∪ x. `````` Robbert Krebbers committed Jun 11, 2012 140 141 142 143 144 145 `````` 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 146 `````` Global Instance union_proper: Proper ((≡) ==> (≡) ==> (≡)) (∪). `````` Robbert Krebbers committed Aug 21, 2012 147 `````` Proof. `````` Robbert Krebbers committed Feb 19, 2013 148 149 `````` unfold equiv, preorder_equiv. split; apply union_preserving; simpl in *; tauto. `````` Robbert Krebbers committed Aug 21, 2012 150 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 151 152 153 154 155 156 157 `````` Global Instance: Idempotent (≡) (∪). Proof. split; eauto. Qed. Global Instance: LeftId (≡) ∅ (∪). Proof. split; eauto. Qed. Global Instance: RightId (≡) ∅ (∪). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∪). `````` Robbert Krebbers committed Feb 19, 2013 158 `````` Proof. split; apply union_comm_1. Qed. `````` Robbert Krebbers committed Jun 11, 2012 159 160 161 162 163 164 165 166 167 168 169 170 `````` 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 171 `````` `````` Robbert Krebbers committed Feb 19, 2013 172 173 `````` Global Instance union_list_proper: Proper (eqlistA (≡) ==> (≡)) union_list. `````` Robbert Krebbers committed Oct 19, 2012 174 175 176 177 178 179 `````` Proof. induction 1; simpl. * done. * by apply union_proper. Qed. `````` Robbert Krebbers committed Feb 19, 2013 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 `````` Lemma union_list_nil : ⋃ @nil A = ∅. Proof. done. Qed. Lemma union_list_cons (X : A) (Xs : list A) : ⋃ (X :: Xs) = X ∪ ⋃ Xs. Proof. done. Qed. Lemma union_list_singleton (X : A) : ⋃ [X] ≡ X. Proof. simpl. by rewrite (right_id ∅ _). Qed. Lemma union_list_app (Xs1 Xs2 : list A) : ⋃ (Xs1 ++ Xs2) ≡ ⋃ Xs1 ∪ ⋃ Xs2. Proof. induction Xs1 as [|X Xs1 IH]; simpl. * by rewrite (left_id ∅ _). * by rewrite IH, (associative _). Qed. Lemma union_list_reverse (Xs : list A) : ⋃ (reverse Xs) ≡ ⋃ Xs. Proof. induction Xs as [|X Xs IH]; simpl; [done |]. by rewrite reverse_cons, union_list_app, union_list_singleton, (commutative _), IH. Qed. Lemma union_list_preserving (Xs Ys : list A) : Forall2 (⊆) Xs Ys → ⋃ Xs ⊆ ⋃ Ys. Proof. induction 1; simpl; auto using union_preserving. Qed. `````` Robbert Krebbers committed Oct 19, 2012 205 206 207 208 209 210 211 212 213 214 215 216 217 218 `````` 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. `````` Robbert Krebbers committed Feb 19, 2013 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 `````` Section leibniz. Context `{!LeibnizEquiv A}. Global Instance: Idempotent (=) (∪). Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed. Global Instance: LeftId (=) ∅ (∪). Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed. Global Instance: RightId (=) ∅ (∪). Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed. Global Instance: Commutative (=) (∪). Proof. intros ??. unfold_leibniz. apply (commutative _). Qed. Global Instance: Associative (=) (∪). Proof. intros ???. unfold_leibniz. apply (associative _). Qed. Lemma subseteq_union_L X Y : X ⊆ Y ↔ X ∪ Y = Y. Proof. unfold_leibniz. apply subseteq_union. Qed. Lemma subseteq_union_1_L X Y : X ⊆ Y → X ∪ Y = Y. Proof. unfold_leibniz. apply subseteq_union_1. Qed. Lemma subseteq_union_2_L X Y : X ∪ Y = Y → X ⊆ Y. Proof. unfold_leibniz. apply subseteq_union_2. Qed. Lemma equiv_empty_L X : X ⊆ ∅ → X = ∅. Proof. unfold_leibniz. apply equiv_empty. Qed. Lemma union_list_singleton_L (X : A) : ⋃ [X] = X. Proof. unfold_leibniz. apply union_list_singleton. Qed. Lemma union_list_app_L (Xs1 Xs2 : list A) : ⋃ (Xs1 ++ Xs2) = ⋃ Xs1 ∪ ⋃ Xs2. Proof. unfold_leibniz. apply union_list_app. Qed. Lemma union_list_reverse_L (Xs : list A) : ⋃ (reverse Xs) = ⋃ Xs. Proof. unfold_leibniz. apply union_list_reverse. Qed. Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅. Proof. unfold_leibniz. apply empty_union. Qed. Lemma empty_list_union_L Xs : ⋃ Xs = ∅ ↔ Forall (= ∅) Xs. Proof. unfold_leibniz. apply empty_list_union. Qed. End leibniz. Section dec. 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. Context `{!LeibnizEquiv A}. Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ → X ≠ ∅ ∨ Y ≠ ∅. Proof. unfold_leibniz. apply non_empty_union. Qed. Lemma non_empty_list_union_L Xs : ⋃ Xs ≠ ∅ → Exists (≠ ∅) Xs. Proof. unfold_leibniz. apply non_empty_list_union. Qed. End dec. `````` Robbert Krebbers committed Jun 11, 2012 269 270 ``````End bounded_join_sl. `````` Robbert Krebbers committed Aug 29, 2012 271 272 ``````(** * Meet semi lattices *) (** The dual of the above section, but now for meet semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 273 274 275 ``````Section meet_sl. Context `{MeetSemiLattice A}. `````` Robbert Krebbers committed Feb 19, 2013 276 `````` Hint Resolve intersection_subseteq_l intersection_subseteq_r `````` Robbert Krebbers committed Aug 21, 2012 277 `````` intersection_greatest. `````` Robbert Krebbers committed Jun 11, 2012 278 `````` `````` Robbert Krebbers committed Feb 19, 2013 279 `````` Lemma intersection_subseteq_l_alt x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2. `````` Robbert Krebbers committed Jun 11, 2012 280 `````` Proof. intros. transitivity x1; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 281 `````` Lemma intersection_subseteq_r_alt x1 x2 y : x1 ⊆ x2 → y ∩ x1 ⊆ x2. `````` Robbert Krebbers committed Jun 11, 2012 282 `````` Proof. intros. transitivity x1; auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 283 `````` Hint Resolve intersection_subseteq_l_alt intersection_subseteq_r_alt. `````` Robbert Krebbers committed Jun 11, 2012 284 `````` `````` Robbert Krebbers committed Feb 19, 2013 285 286 287 288 289 290 291 292 293 294 295 `````` Lemma intersection_preserving_l x y1 y2 : y1 ⊆ y2 → x ∩ y1 ⊆ x ∩ y2. Proof. auto. Qed. Lemma intersection_preserving_r x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2 ∩ y. Proof. auto. Qed. Lemma intersection_preserving x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2. `````` Robbert Krebbers committed Jun 11, 2012 296 `````` Proof. auto. Qed. `````` Robbert Krebbers committed Feb 19, 2013 297 298 `````` Lemma intersection_comm_1 x y : x ∩ y ⊆ y ∩ x. `````` Robbert Krebbers committed Jun 11, 2012 299 300 301 302 303 304 305 `````` 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 306 307 `````` Proof. unfold equiv, preorder_equiv. split; `````` Robbert Krebbers committed Feb 19, 2013 308 `````` apply intersection_preserving; simpl in *; tauto. `````` Robbert Krebbers committed Aug 21, 2012 309 `````` Qed. `````` Robbert Krebbers committed Jun 11, 2012 310 311 312 `````` Global Instance: Idempotent (≡) (∩). Proof. split; eauto. Qed. Global Instance: Commutative (≡) (∩). `````` Robbert Krebbers committed Feb 19, 2013 313 `````` Proof. split; apply intersection_comm_1. Qed. `````` Robbert Krebbers committed Jun 11, 2012 314 315 316 317 318 319 320 321 322 `````` 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. `````` Robbert Krebbers committed Feb 19, 2013 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 `````` Section leibniz. Context `{!LeibnizEquiv A}. Global Instance: Idempotent (=) (∩). Proof. intros ?. unfold_leibniz. apply (idempotent _). Qed. Global Instance: Commutative (=) (∩). Proof. intros ??. unfold_leibniz. apply (commutative _). Qed. Global Instance: Associative (=) (∩). Proof. intros ???. unfold_leibniz. apply (associative _). Qed. Lemma subseteq_intersection_L X Y : X ⊆ Y ↔ X ∩ Y = X. Proof. unfold_leibniz. apply subseteq_intersection. Qed. Lemma subseteq_intersection_1_L X Y : X ⊆ Y → X ∩ Y = X. Proof. unfold_leibniz. apply subseteq_intersection_1. Qed. Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y. Proof. unfold_leibniz. apply subseteq_intersection_2. Qed. End leibniz. `````` Robbert Krebbers committed Jun 11, 2012 341 ``````End meet_sl. `````` Robbert Krebbers committed Oct 19, 2012 342 343 344 345 346 347 348 349 `````` (** * Lower bounded lattices *) Section lower_bounded_lattice. Context `{LowerBoundedLattice A}. Global Instance: LeftAbsorb (≡) ∅ (∩). Proof. split. `````` Robbert Krebbers committed Feb 19, 2013 350 `````` * by apply intersection_subseteq_l. `````` Robbert Krebbers committed Oct 19, 2012 351 352 353 354 `````` * by apply subseteq_empty. Qed. Global Instance: RightAbsorb (≡) ∅ (∩). Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed. `````` Robbert Krebbers committed Feb 19, 2013 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 `````` Global Instance: LeftDistr (≡) (∪) (∩). Proof. intros x y z. split. * apply union_least. { apply intersection_greatest; auto using union_subseteq_l. } apply intersection_greatest. + apply union_subseteq_r_alt, intersection_subseteq_l. + apply union_subseteq_r_alt, intersection_subseteq_r. * apply lbl_distr. Qed. Global Instance: RightDistr (≡) (∪) (∩). Proof. intros x y z. by rewrite !(commutative _ _ z), (left_distr _ _). Qed. Global Instance: LeftDistr (≡) (∩) (∪). Proof. intros x y z. split. * rewrite (left_distr (∪) (∩)). apply intersection_greatest. { apply union_subseteq_r_alt, intersection_subseteq_l. } rewrite (right_distr (∪) (∩)). apply intersection_preserving. + apply union_subseteq_l. + done. * apply intersection_greatest. { apply union_least; auto using intersection_subseteq_l. } apply union_least. + apply intersection_subseteq_r_alt, union_subseteq_l. + apply intersection_subseteq_r_alt, union_subseteq_r. Qed. Global Instance: RightDistr (≡) (∩) (∪). Proof. intros x y z. by rewrite !(commutative _ _ z), (left_distr _ _). Qed. Section leibniz. Context `{!LeibnizEquiv A}. Global Instance: LeftAbsorb (=) ∅ (∩). Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed. Global Instance: RightAbsorb (=) ∅ (∩). Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed. Global Instance: LeftDistr (=) (∪) (∩). Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. Global Instance: RightDistr (=) (∪) (∩). Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. Global Instance: LeftDistr (=) (∩) (∪). Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. Global Instance: RightDistr (=) (∩) (∪). Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. End leibniz. `````` Robbert Krebbers committed Oct 19, 2012 407 ``End lower_bounded_lattice.``