orders.v 3.99 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 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
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 ().
  Proof. split. firstorder. firstorder. intros x y z; split; transitivity y; firstorder. Qed.

  Global Instance: Proper (() ==> () ==> iff) ().
  Proof.
    unfold equiv, preorder_equiv. intros x1 y1 ? x2 y2 ?. split; intro.
     transitivity x1. tauto. transitivity x2; tauto.
    transitivity y1. tauto. transitivity y2; tauto.
  Qed.
End preorder.

Hint Extern 0 (@Equivalence _ ()) => class_apply preorder_equivalence : typeclass_instances.

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 (() ==> () ==> ()) ().
  Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed.
  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}.

  Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest.

  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 (() ==> () ==> ()) ().
  Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed.
  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.