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
Require Export base decidable tactics list.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
30 31 32
  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.
33 34 35 36 37 38
  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
39 40 41

  Lemma subset_subseteq X Y : X  Y  X  Y.
  Proof. by intros [? _]. Qed.
42
  Lemma subset_transitive_l X Y Z : X  Y  Y  Z  X  Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Proof.
44
    intros [? HXY] ?. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
    * by transitivity Y.
46
    * contradict HXY. by transitivity Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  Qed.
48
  Lemma subset_transitive_r X Y Z : X  Y  Y  Z  X  Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  Proof.
50
    intros ? [? HYZ]. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
    * by transitivity Y.
52
    * contradict HYZ. by transitivity X.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55 56 57 58
  Qed.

  Global Instance: StrictOrder ().
  Proof.
    split.
    * firstorder.
59
    * eauto using subset_transitive_r, subset_subseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
60 61 62 63
  Qed.
  Global Instance: Proper (() ==> () ==> iff) ().
  Proof. unfold subset, preorder_subset. solve_proper. Qed.

64 65
  Section leibniz.
    Context `{!LeibnizEquiv A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66

67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
    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.
91
End preorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
92

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

98 99
(** * Partial orders *)
Section partialorder.
100
  Context `{SubsetEq A} `{!PartialOrder ()}.
101 102 103 104 105 106 107 108 109

  Global Instance: LeibnizEquiv A.
  Proof.
    split.
    * intros [??]. by apply (anti_symmetric _).
    * intros. by subst.
  Qed.
End partialorder.

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

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

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

123
  Lemma union_preserving_l x y1 y2 : y1  y2  x  y1  x  y2.
124
  Proof. auto. Qed.
125
  Lemma union_preserving_r x1 x2 y : x1  x2  x1  y  x2  y.
126
  Proof. auto. Qed.
127
  Lemma union_preserving x1 x2 y1 y2 : x1  x2  y1  y2  x1  y1  x2  y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  Proof. auto. Qed.
129

Robbert Krebbers's avatar
Robbert Krebbers committed
130
  Lemma union_empty x : x    x.
131
  Proof. by apply union_least. Qed.
132
  Lemma union_commutative_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  Proof. auto. Qed.
134
  Lemma union_associative_1 x y z : (x  y)  z  x  (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  Proof. auto. Qed.
136
  Lemma union_associative_2 x y z : x  (y  z)  (x  y)  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
  Proof. auto. Qed.

139
  Global Instance union_proper: Proper (() ==> () ==> ()) ().
140
  Proof.
141 142
    unfold equiv, preorder_equiv.
    split; apply union_preserving; simpl in *; tauto.
143
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
144 145 146 147 148 149 150
  Global Instance: Idempotent () ().
  Proof. split; eauto. Qed.
  Global Instance: LeftId ()  ().
  Proof. split; eauto. Qed.
  Global Instance: RightId ()  ().
  Proof. split; eauto. Qed.
  Global Instance: Commutative () ().
151
  Proof. split; apply union_commutative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  Global Instance: Associative () ().
153
  Proof. split. apply union_associative_2. apply union_associative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154 155 156 157 158 159 160 161 162 163

  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.
164

165
  Global Instance union_list_proper: Proper (Forall2 () ==> ()) union_list.
166 167 168 169 170 171
  Proof.
    induction 1; simpl.
    * done.
    * by apply union_proper.
  Qed.

172 173 174 175 176 177 178 179 180 181 182 183
  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.
184
  Lemma union_list_reverse (Xs : list A) :  (reverse Xs)   Xs.
185 186 187 188 189
  Proof.
    induction Xs as [|X Xs IH]; simpl; [done |].
    by rewrite reverse_cons, union_list_app,
      union_list_singleton, (commutative _), IH.
  Qed.
190
  Lemma union_list_preserving (Xs Ys : list A) : Xs * Ys   Xs   Ys.
191 192
  Proof. induction 1; simpl; auto using union_preserving. Qed.

193 194 195 196 197 198 199
  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.
200
  Lemma empty_union_list Xs :  Xs    Forall ( ) Xs.
201 202 203 204 205 206
  Proof.
    split.
    * induction Xs; simpl; rewrite ?empty_union; intuition.
    * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
  Qed.

207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
  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.
239 240
    Lemma empty_union_list_L Xs :  Xs =   Forall (= ) Xs.
    Proof. unfold_leibniz. apply empty_union_list. Qed.
241 242 243 244 245 246 247
  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.
248 249
    Lemma non_empty_union_list Xs :  Xs    Exists ( ) Xs.
    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
250 251 252 253

    Context `{!LeibnizEquiv A}.
    Lemma non_empty_union_L X Y : X  Y    X    Y  .
    Proof. unfold_leibniz. apply non_empty_union. Qed.
254 255
    Lemma non_empty_union_list_L Xs :  Xs    Exists ( ) Xs.
    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
256
  End dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258
End bounded_join_sl.

259 260
(** * Meet semi lattices *)
(** The dual of the above section, but now for meet semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263
Section meet_sl.
  Context `{MeetSemiLattice A}.

264
  Hint Resolve intersection_subseteq_l intersection_subseteq_r
265
    intersection_greatest.
Robbert Krebbers's avatar
Robbert Krebbers committed
266

267
  Lemma intersection_subseteq_l_alt x1 x2 y : x1  x2  x1  y  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
268
  Proof. intros. transitivity x1; auto. Qed.
269
  Lemma intersection_subseteq_r_alt x1 x2 y : x1  x2  y  x1  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
270
  Proof. intros. transitivity x1; auto. Qed.
271
  Hint Resolve intersection_subseteq_l_alt intersection_subseteq_r_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
272

273
  Lemma intersection_preserving_l x y1 y2 : y1  y2  x  y1  x  y2.
274
  Proof. auto. Qed.
275
  Lemma intersection_preserving_r x1 x2 y : x1  x2  x1  y  x2  y.
276 277
  Proof. auto. Qed.
  Lemma intersection_preserving x1 x2 y1 y2 :
278
    x1  x2  y1  y2  x1  y1  x2  y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
279
  Proof. auto. Qed.
280

281
  Lemma intersection_commutative_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
282
  Proof. auto. Qed.
283
  Lemma intersection_associative_1 x y z : (x  y)  z  x  (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
284
  Proof. auto. Qed.
285
  Lemma intersection_associative_2 x y z : x  (y  z)  (x  y)  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287 288
  Proof. auto. Qed.

  Global Instance: Proper (() ==> () ==> ()) ().
289 290
  Proof.
    unfold equiv, preorder_equiv. split;
291
      apply intersection_preserving; simpl in *; tauto.
292
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294 295
  Global Instance: Idempotent () ().
  Proof. split; eauto. Qed.
  Global Instance: Commutative () ().
296
  Proof. split; apply intersection_commutative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Global Instance: Associative () ().
298 299 300
  Proof.
    split. apply intersection_associative_2. apply intersection_associative_1.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302 303 304 305 306 307

  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.
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325

  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
326
End meet_sl.
327 328 329 330 331 332 333 334

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

  Global Instance: LeftAbsorb ()  ().
  Proof.
    split.
335
    * by apply intersection_subseteq_l.
336 337 338 339
    * by apply subseteq_empty.
  Qed.
  Global Instance: RightAbsorb ()  ().
  Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 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

  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.
392
End lower_bounded_lattice.