orders.v 6.2 KB
Newer Older
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. *)
5 6
Require Import SetoidList.
Require Export base decidable tactics list.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

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's avatar
Robbert Krebbers committed
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 ().
16 17 18 19 20 21
  Proof.
    split.
    * firstorder.
    * firstorder.
    * intros x y z; split; transitivity y; firstorder.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24

  Global Instance: Proper (() ==> () ==> iff) ().
  Proof.
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's avatar
Robbert Krebbers committed
29 30
  Qed.

31 32 33 34 35
  Context `{ X Y : A, Decision (X  Y)}.
  Global Instance preorder_equiv_dec_slow (X Y : A) :
    Decision (X  Y) | 100 := _.
End preorder.
Typeclasses Opaque preorder_equiv.
36 37
Hint Extern 0 (@Equivalence _ ()) =>
  class_apply preorder_equivalence : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
38

39 40
(** * Join semi lattices *)
(** General purpose theorems on join semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54
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.
55
  Proof. by apply union_least. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60 61 62
  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.

63
  Global Instance union_proper: Proper (() ==> () ==> ()) ().
64 65 66
  Proof.
    unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
  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.
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113

  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's avatar
Robbert Krebbers committed
114 115
End bounded_join_sl.

116 117
(** * Meet semi lattices *)
(** The dual of the above section, but now for meet semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119 120
Section meet_sl.
  Context `{MeetSemiLattice A}.

121 122
  Hint Resolve subseteq_intersection_l subseteq_intersection_r
    intersection_greatest.
Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126 127 128 129

  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.

130 131
  Lemma intersection_compat x1 x2 y1 y2 :
    x1  x2  y1  y2  x1  y1  x2  y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133 134 135 136 137 138 139 140
  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 (() ==> () ==> ()) ().
141 142 143 144
  Proof.
    unfold equiv, preorder_equiv. split;
      apply intersection_compat; simpl in *; tauto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158
  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.
159 160 161 162 163 164 165 166 167 168 169 170 171 172

(** * 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.