orders.v 14.4 KB
Newer Older
1
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
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. *)
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
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.
45
    intros [? HXY] ?. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
    * by transitivity Y.
47
    * contradict HXY. by transitivity Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50
  Qed.
  Lemma subset_trans_r X Y Z : X  Y  Y  Z  X  Z.
  Proof.
51
    intros ? [? HYZ]. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
    * by transitivity Y.
53
    * contradict HYZ. by transitivity X.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

65 66
  Section leibniz.
    Context `{!LeibnizEquiv A}.
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 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.
92
End preorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
93

94
Typeclasses Opaque preorder_equiv.
95
Typeclasses Opaque preorder_subset.
96 97
Hint Extern 0 (@Equivalence _ ()) =>
  class_apply preorder_equivalence : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
98

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.

111 112
(** * Join semi lattices *)
(** General purpose theorems on join semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
113 114 115
Section bounded_join_sl.
  Context `{BoundedJoinSemiLattice A}.

116
  Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least.
Robbert Krebbers's avatar
Robbert Krebbers committed
117

118
  Lemma union_subseteq_l_alt x1 x2 y : x1  x2  x1  x2  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
  Proof. intros. transitivity x2; auto. Qed.
120
  Lemma union_subseteq_r_alt x1 x2 y : x1  x2  x1  y  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  Proof. intros. transitivity x2; auto. Qed.
122
  Hint Resolve union_subseteq_l_alt union_subseteq_r_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
123

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's avatar
Robbert Krebbers committed
135
  Proof. auto. Qed.
136

Robbert Krebbers's avatar
Robbert Krebbers committed
137
  Lemma union_empty x : x    x.
138
  Proof. by apply union_least. Qed.
139
  Lemma union_comm_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

146
  Global Instance union_proper: Proper (() ==> () ==> ()) ().
147
  Proof.
148 149
    unfold equiv, preorder_equiv.
    split; apply union_preserving; simpl in *; tauto.
150
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 () ().
158
  Proof. split; apply union_comm_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
171

172 173
  Global Instance union_list_proper:
    Proper (eqlistA () ==> ()) union_list.
174 175 176 177 178 179
  Proof.
    induction 1; simpl.
    * done.
    * by apply union_proper.
  Qed.

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.

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.

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

271 272
(** * Meet semi lattices *)
(** The dual of the above section, but now for meet semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274 275
Section meet_sl.
  Context `{MeetSemiLattice A}.

276
  Hint Resolve intersection_subseteq_l intersection_subseteq_r
277
    intersection_greatest.
Robbert Krebbers's avatar
Robbert Krebbers committed
278

279
  Lemma intersection_subseteq_l_alt x1 x2 y : x1  x2  x1  y  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  Proof. intros. transitivity x1; auto. Qed.
281
  Lemma intersection_subseteq_r_alt x1 x2 y : x1  x2  y  x1  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
  Proof. intros. transitivity x1; auto. Qed.
283
  Hint Resolve intersection_subseteq_l_alt intersection_subseteq_r_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
284

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's avatar
Robbert Krebbers committed
296
  Proof. auto. Qed.
297 298

  Lemma intersection_comm_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 (() ==> () ==> ()) ().
306 307
  Proof.
    unfold equiv, preorder_equiv. split;
308
      apply intersection_preserving; simpl in *; tauto.
309
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310 311 312
  Global Instance: Idempotent () ().
  Proof. split; eauto. Qed.
  Global Instance: Commutative () ().
313
  Proof. split; apply intersection_comm_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
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's avatar
Robbert Krebbers committed
341
End meet_sl.
342 343 344 345 346 347 348 349

(** * Lower bounded lattices *)
Section lower_bounded_lattice.
  Context `{LowerBoundedLattice A}.

  Global Instance: LeftAbsorb ()  ().
  Proof.
    split.
350
    * by apply intersection_subseteq_l.
351 352 353 354
    * by apply subseteq_empty.
  Qed.
  Global Instance: RightAbsorb ()  ().
  Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
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.
407
End lower_bounded_lattice.