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

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 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 78 79 80 81 82 83 84 85 86 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 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 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 205 206 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 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 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
(** * Arbitrary pre-, parial and total orders *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
Section orders.
  Context {A} {R : relation A}.
  Implicit Types X Y : A.

  Infix "⊆" := R.
  Notation "X ⊈ Y" := (¬X  Y).
  Infix "⊂" := (strict R).

  Lemma reflexive_eq `{!Reflexive R} X Y : X = Y  X  Y.
  Proof. by intros <-. Qed.
  Lemma anti_symmetric_iff `{!PartialOrder R} X Y : X = Y  R X Y  R Y X.
  Proof. intuition (subst; auto). Qed.

  Lemma strict_spec X Y : X  Y  X  Y  Y  X.
  Proof. done. Qed.
  Lemma strict_include X Y : X  Y  X  Y.
  Proof. by intros [? _]. Qed.
  Lemma strict_ne X Y : X  Y  X  Y.
  Proof. by intros [??] <-. Qed.
  Lemma strict_ne_sym X Y : X  Y  Y  X.
  Proof. by intros [??] <-. Qed.
  Lemma strict_transitive_l `{!Transitive R} X Y Z : X  Y  Y  Z  X  Z.
  Proof.
    intros [? HXY] ?. split.
    * by transitivity Y.
    * contradict HXY. by transitivity Z.
  Qed.
  Lemma strict_transitive_r `{!Transitive R} X Y Z : X  Y  Y  Z  X  Z.
  Proof.
    intros ? [? HYZ]. split.
    * by transitivity Y.
    * contradict HYZ. by transitivity X.
  Qed.

  Global Instance: Irreflexive (strict R).
  Proof. firstorder. Qed.
  Global Instance: Transitive R  StrictOrder (strict R).
  Proof.
    split; try apply _.
    eauto using strict_transitive_r, strict_include.
  Qed.

  Global Instance preorder_subset_dec_slow `{ X Y, Decision (X  Y)}
    (X Y : A) : Decision (X  Y) | 100 := _.

  Lemma strict_spec_alt `{!PartialOrder R} X Y : X  Y  X  Y  X  Y.
  Proof.
    split.
    * intros [? HYX]. split. done. by intros <-.
    * intros [? HXY]. split. done. by contradict HXY; apply (anti_symmetric R).
  Qed.
  Lemma po_eq_dec `{!PartialOrder R} `{ X Y, Decision (X  Y)} (X Y : A) :
    Decision (X = Y).
  Proof.
    refine (cast_if_and (decide (X  Y)) (decide (Y  X)));
     abstract (rewrite anti_symmetric_iff; tauto).
  Defined.

  Lemma total_not `{!Total R} X Y : X  Y  Y  X.
  Proof. intros. destruct (total R X Y); tauto. Qed.
  Lemma total_not_strict `{!Total R} X Y : X  Y  Y  X.
  Proof. red; auto using total_not. Qed.

  Global Instance trichotomyT_dec `{!TrichotomyT R} `{!Reflexive R} X Y :
      Decision (X  Y) :=
    match trichotomyT R X Y with
    | inleft (left H) => left (proj1 H)
    | inleft (right H) => left (reflexive_eq _ _ H)
    | inright H => right (proj2 H)
    end.
  Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R.
  Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed.
  Global Instance trichotomy_total `{!Trichotomy R} `{!Reflexive R} : Total R.
  Proof.
    intros X Y. destruct (trichotomy R X Y) as [[??]|[<-|[??]]]; intuition.
  Qed.
End orders.

Ltac simplify_order := repeat
  match goal with
  | _ => progress simplify_equality
  | H : strict _ ?x ?x |- _ => by destruct (irreflexivity _ _ H)
  | H1 : ?R ?x ?y |- _ =>
    match goal with
    | H2 : R y x |- _ =>
      assert (x = y) by (by apply (anti_symmetric R)); clear H1 H2
    | H2 : R y ?z |- _ =>
      unless (R x z) by done;
      assert (R x z) by (by transitivity y)
    end
  end.

(** * Sorting *)
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *)
Section merge_sort.
  Context  {A} (R : relation A) `{ x y, Decision (R x y)}.

  Fixpoint list_merge (l1 : list A) : list A  list A :=
    fix list_merge_aux l2 :=
    match l1, l2 with
    | [], _ => l2
    | _, [] => l1
    | x1 :: l1, x2 :: l2 =>
       if decide_rel R x1 x2 then x1 :: list_merge l1 (x2 :: l2)
       else x2 :: list_merge_aux l2
    end.
  Global Arguments list_merge !_ !_ /.

  Local Notation stack := (list (option (list A))).
  Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack :=
    match st with
    | [] => [Some l]
    | None :: st => Some l :: st
    | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l)
    end.
  Fixpoint merge_stack (st : stack) : list A :=
    match st with
    | [] => []
    | None :: st => merge_stack st
    | Some l :: st => list_merge l (merge_stack st)
    end.
  Fixpoint merge_sort_aux (st : stack) (l : list A) : list A :=
    match l with
    | [] => merge_stack st
    | x :: l => merge_sort_aux (merge_list_to_stack st [x]) l
    end.
  Definition merge_sort : list A  list A := merge_sort_aux [].
End merge_sort.

(** ** Properties of the [Sorted] and [StronglySorted] predicate *)
Section sorted.
  Context {A} (R : relation A).

  Lemma Sorted_StronglySorted `{!Transitive R} l :
    Sorted R l  StronglySorted R l.
  Proof. by apply Sorted.Sorted_StronglySorted. Qed.
  Lemma StronglySorted_unique `{!AntiSymmetric (=) R} l1 l2 :
    StronglySorted R l1  StronglySorted R l2  l1  l2  l1 = l2.
  Proof.
    intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
    { symmetry. by apply Permutation_nil. }
    destruct Hl2 as [|x2 l2 ? Hx2].
    { by apply Permutation_nil in E. }
    assert (x1 = x2); subst.
    { rewrite Forall_forall in Hx1, Hx2.
      assert (x2  x1 :: l1) as Hx2' by (by rewrite E; left).
      assert (x1  x2 :: l2) as Hx1' by (by rewrite <-E; left).
      inversion Hx1'; inversion Hx2'; simplify_equality; auto. }
    f_equal. by apply IH, (injective (x2 ::)).
  Qed.
  Lemma Sorted_unique `{!Transitive R} `{!AntiSymmetric (=) R} l1 l2 :
    Sorted R l1  Sorted R l2  l1  l2  l1 = l2.
  Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.

  Global Instance HdRel_dec x `{ y, Decision (R x y)} l :
    Decision (HdRel R x l).
  Proof.
   refine
    match l with
    | [] => left _
    | y :: l => cast_if (decide (R x y))
    end; abstract first [by constructor | by inversion 1].
  Defined.

  Global Instance Sorted_dec `{ x y, Decision (R x y)} :  l,
    Decision (Sorted R l).
  Proof.
   refine
    (fix go l :=
    match l return Decision (Sorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
    end); clear go; abstract first [by constructor | by inversion 1].
  Defined.
  Global Instance StronglySorted_dec `{ x y, Decision (R x y)} :  l,
    Decision (StronglySorted R l).
  Proof.
   refine
    (fix go l :=
    match l return Decision (StronglySorted R l) with
    | [] => left _
    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
    end); clear go; abstract first [by constructor | by inversion 1].
  Defined.

  Context {B} (f : A  B).
  Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
    ( y, R1 x y  R2 (f x) (f y))  HdRel R1 x l  HdRel R2 (f x) (f <$> l).
  Proof. destruct 2; constructor; auto. Qed.
  Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
    ( x y, R1 x y  R2 (f x) (f y))  Sorted R1 l  Sorted R2 (f <$> l).
  Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
  Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
    ( x y, R1 x y  R2 (f x) (f y)) 
    StronglySorted R1 l  StronglySorted R2 (f <$> l).
  Proof.
    induction 2; simpl; constructor;
      rewrite ?Forall_fmap; eauto using Forall_impl.
  Qed.
End sorted.

(** ** Correctness of merge sort *)
Section merge_sort_correct.
  Context  {A} (R : relation A) `{ x y, Decision (R x y)} `{!Total R}.

  Lemma list_merge_cons x1 x2 l1 l2 :
    list_merge R (x1 :: l1) (x2 :: l2) =
      if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
      else x2 :: list_merge R (x1 :: l1) l2.
  Proof. done. Qed.

  Lemma HdRel_list_merge x l1 l2 :
    HdRel R x l1  HdRel R x l2  HdRel R x (list_merge R l1 l2).
  Proof.
    destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
      rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
  Qed.
  Lemma Sorted_list_merge l1 l2 :
    Sorted R l1  Sorted R l2  Sorted R (list_merge R l1 l2).
  Proof.
    intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
      induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
      repeat case_decide;
      constructor; eauto using HdRel_list_merge, HdRel_cons, total_not.
  Qed.
  Lemma merge_Permutation l1 l2 : list_merge R l1 l2  l1 ++ l2.
  Proof.
    revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
      induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
      repeat case_decide; auto.
    * by rewrite (right_id_L [] (++)).
    * by rewrite IH2, Permutation_middle.
  Qed.

  Local Notation stack := (list (option (list A))).
  Inductive merge_stack_Sorted : stack  Prop :=
    | merge_stack_Sorted_nil : merge_stack_Sorted []
    | merge_stack_Sorted_cons_None st :
       merge_stack_Sorted st  merge_stack_Sorted (None :: st)
    | merge_stack_Sorted_cons_Some l st :
       Sorted R l  merge_stack_Sorted st  merge_stack_Sorted (Some l :: st).
  Fixpoint merge_stack_flatten (st : stack) : list A :=
    match st with
    | [] => []
    | None :: st => merge_stack_flatten st
    | Some l :: st => l ++ merge_stack_flatten st
    end.

  Lemma Sorted_merge_list_to_stack st l :
    merge_stack_Sorted st  Sorted R l 
    merge_stack_Sorted (merge_list_to_stack R st l).
  Proof.
    intros Hst. revert l.
    induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge.
  Qed.
  Lemma merge_list_to_stack_Permutation st l :
    merge_stack_flatten (merge_list_to_stack R st l) 
      l ++ merge_stack_flatten st.
  Proof.
    revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
    by rewrite IH, merge_Permutation, (associative_L _), (commutative (++) l).
  Qed.
  Lemma Sorted_merge_stack st :
    merge_stack_Sorted st  Sorted R (merge_stack R st).
  Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
  Lemma merge_stack_Permutation st : merge_stack R st  merge_stack_flatten st.
  Proof.
    induction st as [|[] ? IH]; intros; simpl; auto.
    by rewrite merge_Permutation, IH.
  Qed.
  Lemma Sorted_merge_sort_aux st l :
    merge_stack_Sorted st  Sorted R (merge_sort_aux R st l).
  Proof.
    revert st. induction l; simpl;
      auto using Sorted_merge_stack, Sorted_merge_list_to_stack.
  Qed.
  Lemma merge_sort_aux_Permutation st l :
    merge_sort_aux R st l  merge_stack_flatten st ++ l.
  Proof.
    revert st. induction l as [|?? IH]; simpl; intros.
    * by rewrite (right_id_L [] (++)), merge_stack_Permutation.
    * rewrite IH, merge_list_to_stack_Permutation; simpl.
      by rewrite Permutation_middle.
  Qed.

  Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
  Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
  Lemma merge_sort_Permutation l : merge_sort R l  l.
  Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
  Lemma StronglySorted_merge_sort `{!Transitive R} l :
    StronglySorted R (merge_sort R l).
  Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
End merge_sort_correct.

(** * Canonical pre and partial orders *)
(** We extend the canonical pre-order [⊆] to a partial order by defining setoid
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
310 311 312 313 314
Section preorder.
  Context `{SubsetEq A} `{!PreOrder ()}.

  Global Instance preorder_equiv: Equiv A := λ X Y, X  Y  Y  X.
  Instance preorder_equivalence: @Equivalence A ().
315 316
  Proof.
    split.
317 318 319
    * done.
    * by intros ?? [??].
    * by intros x y z [??] [??]; split; transitivity y.
320
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
321 322 323

  Global Instance: Proper (() ==> () ==> iff) ().
  Proof.
324 325 326 327
    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
328 329
  Qed.

330
  Lemma subset_spec X Y : X  Y  X  Y  X  Y.
331 332 333 334 335
  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
336

337 338
  Section leibniz.
    Context `{!LeibnizEquiv A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
339

340 341
    Lemma subset_spec_L X Y : X  Y  X  Y  X  Y.
    Proof. unfold_leibniz. apply subset_spec. Qed.
342 343 344 345 346 347 348 349 350
  End leibniz.

  Section dec.
    Context `{ X Y : A, Decision (X  Y)}.

    Global Instance preorder_equiv_dec_slow (X Y : A) :
      Decision (X  Y) | 100 := _.

    Lemma subseteq_inv X Y : X  Y  X  Y  X  Y.
351
    Proof. rewrite subset_spec. destruct (decide (X  Y)); tauto. Qed.
352
    Lemma not_subset_inv X Y : X  Y  X  Y  X  Y.
353
    Proof. rewrite subset_spec. destruct (decide (X  Y)); tauto. Qed.
354 355 356 357 358 359 360 361

    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.
362
End preorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
363

364
Typeclasses Opaque preorder_equiv.
365 366
Hint Extern 0 (@Equivalence _ ()) =>
  class_apply preorder_equivalence : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
367

368 369
(** * Partial orders *)
Section partialorder.
370
  Context `{SubsetEq A} `{!PartialOrder ()}.
371 372 373 374

  Global Instance: LeibnizEquiv A.
  Proof.
    split.
375
    * intros [??]. by apply (anti_symmetric ()).
376 377 378 379
    * intros. by subst.
  Qed.
End partialorder.

380 381
(** * Join semi lattices *)
(** General purpose theorems on join semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
382 383 384
Section bounded_join_sl.
  Context `{BoundedJoinSemiLattice A}.

385
  Hint Resolve subseteq_empty union_subseteq_l union_subseteq_r union_least.
Robbert Krebbers's avatar
Robbert Krebbers committed
386

387
  Lemma union_subseteq_l_alt x1 x2 y : x1  x2  x1  x2  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
388
  Proof. intros. transitivity x2; auto. Qed.
389
  Lemma union_subseteq_r_alt x1 x2 y : x1  x2  x1  y  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
390
  Proof. intros. transitivity x2; auto. Qed.
391
  Hint Resolve union_subseteq_l_alt union_subseteq_r_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
392

393
  Lemma union_preserving_l x y1 y2 : y1  y2  x  y1  x  y2.
394
  Proof. auto. Qed.
395
  Lemma union_preserving_r x1 x2 y : x1  x2  x1  y  x2  y.
396
  Proof. auto. Qed.
397
  Lemma union_preserving x1 x2 y1 y2 : x1  x2  y1  y2  x1  y1  x2  y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
  Proof. auto. Qed.
399

Robbert Krebbers's avatar
Robbert Krebbers committed
400
  Lemma union_empty x : x    x.
401
  Proof. by apply union_least. Qed.
402
  Lemma union_commutative_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
403
  Proof. auto. Qed.
404
  Lemma union_associative_1 x y z : (x  y)  z  x  (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
405
  Proof. auto. Qed.
406
  Lemma union_associative_2 x y z : x  (y  z)  (x  y)  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
407 408
  Proof. auto. Qed.

409
  Global Instance union_proper: Proper (() ==> () ==> ()) ().
410
  Proof.
411 412
    unfold equiv, preorder_equiv.
    split; apply union_preserving; simpl in *; tauto.
413
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
414 415 416 417 418 419 420
  Global Instance: Idempotent () ().
  Proof. split; eauto. Qed.
  Global Instance: LeftId ()  ().
  Proof. split; eauto. Qed.
  Global Instance: RightId ()  ().
  Proof. split; eauto. Qed.
  Global Instance: Commutative () ().
421
  Proof. split; apply union_commutative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
422
  Global Instance: Associative () ().
423
  Proof. split. apply union_associative_2. apply union_associative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426 427 428 429 430 431 432 433

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

435
  Global Instance union_list_proper: Proper (Forall2 () ==> ()) union_list.
436 437 438 439 440 441
  Proof.
    induction 1; simpl.
    * done.
    * by apply union_proper.
  Qed.

442 443 444 445 446 447 448 449 450 451 452 453
  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.
454
  Lemma union_list_reverse (Xs : list A) :  (reverse Xs)   Xs.
455 456 457 458 459
  Proof.
    induction Xs as [|X Xs IH]; simpl; [done |].
    by rewrite reverse_cons, union_list_app,
      union_list_singleton, (commutative _), IH.
  Qed.
460
  Lemma union_list_preserving (Xs Ys : list A) : Xs * Ys   Xs   Ys.
461 462
  Proof. induction 1; simpl; auto using union_preserving. Qed.

463 464 465 466 467 468 469
  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.
470
  Lemma empty_union_list Xs :  Xs    Forall ( ) Xs.
471 472 473 474 475 476
  Proof.
    split.
    * induction Xs; simpl; rewrite ?empty_union; intuition.
    * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
  Qed.

477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508
  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.
509 510
    Lemma empty_union_list_L Xs :  Xs =   Forall (= ) Xs.
    Proof. unfold_leibniz. apply empty_union_list. Qed.
511 512 513 514 515 516 517
  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.
518 519
    Lemma non_empty_union_list Xs :  Xs    Exists ( ) Xs.
    Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
520 521 522 523

    Context `{!LeibnizEquiv A}.
    Lemma non_empty_union_L X Y : X  Y    X    Y  .
    Proof. unfold_leibniz. apply non_empty_union. Qed.
524 525
    Lemma non_empty_union_list_L Xs :  Xs    Exists ( ) Xs.
    Proof. unfold_leibniz. apply non_empty_union_list. Qed.
526
  End dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528
End bounded_join_sl.

529 530
(** * Meet semi lattices *)
(** The dual of the above section, but now for meet semi lattices. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
531 532 533
Section meet_sl.
  Context `{MeetSemiLattice A}.

534
  Hint Resolve intersection_subseteq_l intersection_subseteq_r
535
    intersection_greatest.
Robbert Krebbers's avatar
Robbert Krebbers committed
536

537
  Lemma intersection_subseteq_l_alt x1 x2 y : x1  x2  x1  y  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
538
  Proof. intros. transitivity x1; auto. Qed.
539
  Lemma intersection_subseteq_r_alt x1 x2 y : x1  x2  y  x1  x2.
Robbert Krebbers's avatar
Robbert Krebbers committed
540
  Proof. intros. transitivity x1; auto. Qed.
541
  Hint Resolve intersection_subseteq_l_alt intersection_subseteq_r_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
542

543
  Lemma intersection_preserving_l x y1 y2 : y1  y2  x  y1  x  y2.
544
  Proof. auto. Qed.
545
  Lemma intersection_preserving_r x1 x2 y : x1  x2  x1  y  x2  y.
546 547
  Proof. auto. Qed.
  Lemma intersection_preserving x1 x2 y1 y2 :
548
    x1  x2  y1  y2  x1  y1  x2  y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
549
  Proof. auto. Qed.
550

551
  Lemma intersection_commutative_1 x y : x  y  y  x.
Robbert Krebbers's avatar
Robbert Krebbers committed
552
  Proof. auto. Qed.
553
  Lemma intersection_associative_1 x y z : (x  y)  z  x  (y  z).
Robbert Krebbers's avatar
Robbert Krebbers committed
554
  Proof. auto. Qed.
555
  Lemma intersection_associative_2 x y z : x  (y  z)  (x  y)  z.
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557 558
  Proof. auto. Qed.

  Global Instance: Proper (() ==> () ==> ()) ().
559 560
  Proof.
    unfold equiv, preorder_equiv. split;
561
      apply intersection_preserving; simpl in *; tauto.
562
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
563 564 565
  Global Instance: Idempotent () ().
  Proof. split; eauto. Qed.
  Global Instance: Commutative () ().
566
  Proof. split; apply intersection_commutative_1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
  Global Instance: Associative () ().
568 569 570
  Proof.
    split. apply intersection_associative_2. apply intersection_associative_1.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
571 572 573 574 575 576 577

  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.
578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595

  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
596
End meet_sl.
597 598 599 600 601 602 603 604

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

  Global Instance: LeftAbsorb ()  ().
  Proof.
    split.
605
    * by apply intersection_subseteq_l.
606 607 608 609
    * by apply subseteq_empty.
  Qed.
  Global Instance: RightAbsorb ()  ().
  Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657
  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.
658
End lower_bounded_lattice.