orders.v 4.65 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 Jun 11, 2012 5 6 ``````Require Export base. `````` Robbert Krebbers committed Aug 29, 2012 7 8 9 ``````(** * 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 10 11 12 13 14 ``````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 15 16 17 18 19 20 `````` Proof. split. * firstorder. * firstorder. * intros x y z; split; transitivity y; firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 21 22 23 `````` Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆). Proof. `````` Robbert Krebbers committed Aug 21, 2012 24 25 26 27 `````` 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 28 29 30 `````` Qed. End preorder. `````` Robbert Krebbers committed Aug 21, 2012 31 32 ``````Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. `````` Robbert Krebbers committed Jun 11, 2012 33 `````` `````` Robbert Krebbers committed Aug 29, 2012 34 35 ``````(** * Join semi lattices *) (** General purpose theorems on join semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 ``````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. Proof. apply union_least. easy. auto. Qed. 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. Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∪). `````` Robbert Krebbers committed Aug 21, 2012 59 60 61 `````` Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 `````` 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. End bounded_join_sl. `````` Robbert Krebbers committed Aug 29, 2012 84 85 ``````(** * Meet semi lattices *) (** The dual of the above section, but now for meet semi lattices. *) `````` Robbert Krebbers committed Jun 11, 2012 86 87 88 ``````Section meet_sl. Context `{MeetSemiLattice A}. `````` Robbert Krebbers committed Aug 21, 2012 89 90 `````` Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest. `````` Robbert Krebbers committed Jun 11, 2012 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 `````` 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. Lemma intersection_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∩ y1 ⊆ x2 ∩ y2. 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 108 109 110 111 `````` Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 112 113 114 115 116 117 118 119 120 121 122 123 124 125 `````` 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.``````