orders.v 4.04 KB
 Robbert Krebbers committed Jun 11, 2012 1 2 3 4 5 6 7 ``````Require Export base. 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 8 9 10 11 12 13 `````` Proof. split. * firstorder. * firstorder. * intros x y z; split; transitivity y; firstorder. Qed. `````` Robbert Krebbers committed Jun 11, 2012 14 15 16 `````` Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆). Proof. `````` Robbert Krebbers committed Aug 21, 2012 17 18 19 20 `````` 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 21 22 23 `````` Qed. End preorder. `````` Robbert Krebbers committed Aug 21, 2012 24 25 ``````Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances. `````` Robbert Krebbers committed Jun 11, 2012 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 `````` 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 50 51 52 `````` Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 `````` 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. Section meet_sl. Context `{MeetSemiLattice A}. `````` Robbert Krebbers committed Aug 21, 2012 78 79 `````` Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest. `````` Robbert Krebbers committed Jun 11, 2012 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` 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 97 98 99 100 `````` Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed. `````` Robbert Krebbers committed Jun 11, 2012 101 102 103 104 105 106 107 108 109 110 111 112 113 114 `````` 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.``````