OrderLattice.v

From mathcomp Require Import all_ssreflect.
Require Import Bool.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Class poSet := PoSet {
  base : finType;
  le : rel base;
  refl : forall x, le x x;
  trans : forall x y z,le x y -> le y z -> le x z;
  antisym : forall x y,le x y /\ le y x -> x = y
}.


Infix "≺" := le(at level 40).

Coercion poSet_set (P : poSet) :=
  let: PoSet P' _ _ _ _ := P in P'.

Section defs.
  Variable T : poSet.

  Definition is_upb (B : {set T}) x :=
    forall y, y \in B -> y ≺ x.

  Definition is_lowb (B : {set T}) x :=
    forall y, y \in B -> x ≺ y.

  Definition is_sup (B : {set T}) x :=
    is_upb B x /\ forall y, is_upb B y -> x ≺ y.

  Definition is_inf (B : {set T}) x :=
    is_lowb B x /\ forall y, is_lowb B y -> y ≺ x.

  Section AB.
    Variable (A B : {set T}).

    Theorem sup_sub a b :
        is_sup A a -> is_sup B b -> A \subset B -> a ≺ b.
      Proof.
        rewrite /is_sup /is_upb => [[Ha1 Ha2] [Hb1 Hb2]] H.
        apply Ha2 => y Hy.
        apply Hb1.
        move /subsetP : H; apply; auto.
      Qed.

    Theorem inf_sub a b :
      is_inf A a -> is_inf B b -> A \subset B -> b ≺ a.
    Proof.
      rewrite /is_sup /is_upb => [[Ha1 Ha2] [Hb1 Hb2]] H.
      apply Ha2 => y Hy.
      apply Hb1.
      move /subsetP : H; apply; auto.
    Qed.
  End AB.

  Definition is_upb_ (B : {set T}) x :=
    [forall y, (y \in B) ==> y ≺ x].

  Definition is_lowb_ (B : {set T}) x :=
    [forall y, (y \in B) ==> x ≺ y].

  Definition is_sup_ (B : {set T}) x :=
    (is_upb_ B x) && [forall y, (is_upb_ B y) ==> x ≺ y].

  Definition is_inf_ (B : {set T}) x :=
    (is_lowb_ B x) && [forall y, (is_lowb_ B y) ==> y ≺ x].


End defs.

Class lattice := Lattice {
  carrier : poSet;
  meet : carrier -> carrier -> carrier;
  join : carrier -> carrier -> carrier;
  Hm : forall x y, is_inf [set x; y] (meet x y);
  Hj : forall x y, is_sup [set x; y] (join x y);
}.

Coercion lattice_set (P : lattice) :=
  let:  Lattice P' _ _ _ _ := P in (poSet_set P').


Section identities.
  Variable L : lattice.



  Lemma meet_le x y :
     meet x y = x <-> x ≺ y.
  Proof.
    move : (Hm x y).
    unfold is_inf, is_lowb => [[H1 H2]].
    split => H.
    {
      rewrite <- H.
      apply H1.
      apply /set2P; right; auto.
    }
    {
     apply antisym; split.
     -  apply H1. apply /set2P; left; auto.
     -  apply H2 => z.
        move /set2P; case => ->; auto.
        apply refl.
    }
Qed.

  Lemma join_le x y :
    join x y = x <-> y ≺ x.
  Proof.
    move : (Hj x y).
    unfold is_sup, is_upb => [[H1 H2]].
    split => H.
    {
      rewrite <- H.
      apply H1.
      apply /set2P; right; auto.
    }
    {
      apply antisym; split.
      - apply H2 => z.
        move /set2P; case => ->; auto.
        apply refl.
      - apply H1. apply /set2P; left; auto.
    }
  Qed.

  Lemma meet_join x y :
    meet x (join x y) = x.
  Proof.
    apply meet_le.
    move : (Hj x y) => [H1 H2].
    apply H1.
    apply /set2P; left; auto.
  Qed.


  Lemma join_meet x y :
    join x (meet x y) = x.
  Proof.
    apply join_le.
    move : (Hm x y) => [H _].
    apply H.
    apply /set2P; left; auto.
  Qed.

  Lemma meetR  x :
    meet x x = x.
  Proof.
    apply meet_le. apply refl.
  Qed.

  Lemma meetA x y z :
    meet x (meet y z) = meet (meet x y) z.
  Proof.
    move : (Hm x (meet y z)) => [H1x_yz H2x_yz].
    move : (Hm y z) => [H1yz H2yz].
    move : (Hm (meet x y) z) => [H1xy_z H2xy_z].
    move : (Hm x y) => [H1xy H2xy].
    remember (meet x (meet y z)) as x_yz.
    remember (meet (meet x y) z) as xy_z.
    apply antisym; split.
    -
      have Hyz : x_yz ≺ meet y z. {
        apply H1x_yz. apply /set2P; right; auto.
      }
      have Hx : x_yz ≺ x. {
        apply H1x_yz; apply /set2P; left; auto.
      }
      have Hy : x_yz ≺ y. {
        apply trans with (meet y z); auto.
        apply H1yz. apply /set2P.
        left; auto.
      }
      have Hz : x_yz ≺ z. {
        apply trans with (meet y z); auto.
        apply H1yz. apply /set2P.
        right; auto.
      }
      apply H2xy_z => a.
      unfold is_lowb.
      move /set2P; case => ->; auto.
      apply H2xy => b.
      move /set2P; case => ->; auto.
    - have Hyz : xy_z ≺ meet x y. {
        apply H1xy_z. apply /set2P; left; auto.
      }
      have Hx : xy_z ≺ z. {
        apply H1xy_z; apply /set2P; right; auto.
      }
      have Hy : xy_z ≺ x. {
        apply trans with (meet x y); auto.
        apply H1xy. apply /set2P.
        left; auto.
      }
      have Hz : xy_z ≺ y. {
        apply trans with (meet x y); auto.
        apply H1xy. apply /set2P.
        right; auto.
      }
      apply H2x_yz => a.
      move /set2P; case => ->; auto.
      apply H2yz => b.
      move /set2P; case => ->; auto.
  Qed.

  Lemma meetC x y :
    meet x y = meet y x.
  Proof.
    apply antisym; split.
    - move : (Hm x y) => [H1 _].
      move : (Hm y x) => [_ H2].
      apply H2 => a.
      move /set2P;case => ->;
      apply H1; apply /set2P; [right|left]; auto.
    - move : (Hm y x) => [H1 _].
      move : (Hm x y) => [_ H2].
      apply H2 => a.
      move /set2P;case => ->;
      apply H1; apply /set2P; [right|left]; auto.
  Qed.

  Lemma joinR x :
    join x x = x.
  Proof.
    apply join_le. apply refl.
  Qed.

  Lemma joinA x y z :
    join x (join y z) = join (join x y) z.
  Proof.
    move : (Hj x (join y z)) => [H1x_yz H2x_yz].
    move : (Hj y z) => [H1yz H2yz].
    move : (Hj (join x y) z) => [H1xy_z H2xy_z].
    move : (Hj x y) => [H1xy H2xy].
    remember (join x (join y z)) as x_yz.
    remember (join (join x y) z) as xy_z.
    apply antisym; split.
    - have Hyz : join x y ≺ xy_z. {
        apply H1xy_z. apply /set2P; left; auto.
      }
      have Hx : z ≺ xy_z. {
        apply H1xy_z; apply /set2P; right; auto.
      }
      have Hy : x ≺ xy_z. {
        apply trans with (join x y); auto.
        apply H1xy. apply /set2P.
        left; auto.
      }
      have Hz : y ≺ xy_z. {
        apply trans with (join x y); auto.
        apply H1xy. apply /set2P.
        right; auto.
      }
      apply H2x_yz => a.
      move /set2P; case => ->; auto.
      apply H2yz => b.
      move /set2P; case => ->; auto.
    -
      have Hyz : join y z ≺ x_yz. {
        apply H1x_yz. apply /set2P; right; auto.
      }
      have Hx : x ≺ x_yz. {
        apply H1x_yz; apply /set2P; left; auto.
      }
      have Hy : y ≺ x_yz. {
        apply trans with (join y z); auto.
        apply H1yz. apply /set2P.
        left; auto.
      }
      have Hz : z ≺ x_yz. {
        apply trans with (join y z); auto.
        apply H1yz. apply /set2P.
        right; auto.
      }
      apply H2xy_z => a.
      unfold is_lowb.
      move /set2P; case => ->; auto.
      apply H2xy => b.
      move /set2P; case => ->; auto.
  Qed.

  Lemma joinC x y :
    join x y = join y x.
  Proof.
    apply antisym; split.
    - move : (Hj y x) => [H1 _].
      move : (Hj x y) => [_ H2].
      apply H2 => a.
      move /set2P;case => ->;
      apply H1; apply /set2P; [right|left]; auto.
    - move : (Hj x y) => [H1 _].
      move : (Hj y x) => [_ H2].
      apply H2 => a.
      move /set2P;case => ->;
      apply H1; apply /set2P; [right|left]; auto.
  Qed.
End identities.