Module orders

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.
Require Import SetoidList.
Require Export base decidable tactics list.

Pre-orders

We extend a pre-order to a partial order by defining equality as λ X Y, XYYX. We prove that this indeed gives rise to a setoid.
Section preorder.
  Context `{SubsetEq A} `{!PreOrder (⊆)}.

  Global Instance preorder_equiv: Equiv A := λ X Y, XYYX.
  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.


  Global Instance preorder_subset: Subset A := λ X Y, XYYX.
  Lemma subset_spec X Y : XYXYYX.
  Proof. done. Qed.

  Lemma subset_subseteq X Y : XYXY.
  Proof. by intros [? _]. Qed.
  Lemma subset_trans_l X Y Z : XYYZXZ.
  Proof.
    intros [? Hxy] ?. split.
    * by transitivity Y.
    * contradict Hxy. by transitivity Z.
  Qed.

  Lemma subset_trans_r X Y Z : XYYZXZ.
  Proof.
    intros ? [? Hyz]. split.
    * by transitivity Y.
    * contradict Hyz. by transitivity X.
  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.

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

  Lemma subseteq_inv X Y : XYXYXY.
  Proof.
    destruct (decide (YX)).
    * by right.
    * by left.
  Qed.

End preorder.

Typeclasses Opaque preorder_equiv.
Hint Extern 0 (@Equivalence _ (≡)) =>
  class_apply preorder_equivalence : typeclass_instances.

Join semi lattices

General purpose theorems on join semi lattices.
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 : x1x2x1x2y.
  Proof. intros. transitivity x2; auto. Qed.
  Lemma union_compat_r x1 x2 y : x1x2x1yx2.
  Proof. intros. transitivity x2; auto. Qed.
  Hint Resolve union_compat_l union_compat_r.

  Lemma union_compat x1 x2 y1 y2 : x1x2y1y2x1y1x2y2.
  Proof. auto. Qed.
  Lemma union_empty x : x ∪ ∅ ⊆ x.
  Proof. by apply union_least. Qed.
  Lemma union_comm x y : xyyx.
  Proof. auto. Qed.
  Lemma union_assoc_1 x y z : (xy) ∪ zx ∪ (yz).
  Proof. auto. Qed.
  Lemma union_assoc_2 x y z : x ∪ (yz) ⊆ (xy) ∪ z.
  Proof. auto. Qed.

  Global Instance union_proper: 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 : XYXYY.
  Proof. repeat split; eauto. intros E. rewrite <-E. auto. Qed.
  Lemma subseteq_union_1 X Y : XYXYY.
  Proof. apply subseteq_union. Qed.
  Lemma subseteq_union_2 X Y : XYYXY.
  Proof. apply subseteq_union. Qed.

  Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅.
  Proof. split; eauto. Qed.

  Global Instance: Proper (eqlistA (≡) ==> (≡)) union_list.
  Proof.
    induction 1; simpl.
    * done.
    * by apply union_proper.
  Qed.


  Lemma empty_union X Y : XY ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
  Proof.
    split.
    * intros E. split; apply equiv_empty;
        by transitivity (XY); [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 (XY)}.
  Lemma non_empty_union X Y : XY ≢ ∅ → 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.
End bounded_join_sl.

Meet semi lattices

The dual of the above section, but now for meet semi lattices.
Section meet_sl.
  Context `{MeetSemiLattice A}.

  Hint Resolve subseteq_intersection_l subseteq_intersection_r
    intersection_greatest.

  Lemma intersection_compat_l x1 x2 y : x1x2x1yx2.
  Proof. intros. transitivity x1; auto. Qed.
  Lemma intersection_compat_r x1 x2 y : x1x2yx1x2.
  Proof. intros. transitivity x1; auto. Qed.
  Hint Resolve intersection_compat_l intersection_compat_r.

  Lemma intersection_compat x1 x2 y1 y2 :
    x1x2y1y2x1y1x2y2.
  Proof. auto. Qed.
  Lemma intersection_comm x y : xyyx.
  Proof. auto. Qed.
  Lemma intersection_assoc_1 x y z : (xy) ∩ zx ∩ (yz).
  Proof. auto. Qed.
  Lemma intersection_assoc_2 x y z : x ∩ (yz) ⊆ (xy) ∩ 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 : XYXYX.
  Proof. repeat split; eauto. intros E. rewrite <-E. auto. Qed.
  Lemma subseteq_intersection_1 X Y : XYXYX.
  Proof. apply subseteq_intersection. Qed.
  Lemma subseteq_intersection_2 X Y : XYXXY.
  Proof. apply subseteq_intersection. Qed.
End meet_sl.

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.