Library UniMath.OrderTheory.Prebilattice.Interlaced

Interlaced pre-bilattice Georgios V. Pitsiladis, Aug. 2024 -
In interlaced pre-bilattices, the two lattices are linked via monotonicity of the operators of each lattice with respect to the other lattice.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice.
Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Subtypes.
Require Import UniMath.Algebra.BinaryOperations.

Section definition .
  Definition interlacing {X : hSet} (op : binop X) (R : hrel X) :=
    ∏ x y z : X, R x y -> R (op x z) (op y z).

  Lemma isaprop_interlacing {X : hSet} (op : binop X) (R : hrel X) : isaprop (interlacing op R).
  Show proof.
    do 4 (use impred; intro).
    use propproperty.

  Definition is_interlaced {X : hSet} (b : prebilattice X) : UU :=
    interlacing (consensus b) (tle b)
                ×
                interlacing (gullibility b) (tle b)
                ×
                interlacing (meet b) (kle b)
                ×
                interlacing (join b) (kle b).

  Lemma isaprop_is_interlaced {X : hSet} {b : prebilattice X} : isaprop (is_interlaced b).
  Show proof.
    do 3 (try use (isapropdirprod)); use isaprop_interlacing.

  Definition interlaced_prebilattice (X : hSet) :=
    ∑ b : prebilattice X, is_interlaced b.

  Definition make_interlaced_prebilattice {X : hSet} {b : prebilattice X} (is : is_interlaced b) : interlaced_prebilattice X := b,,is.

  Definition interlaced_prebilattice_to_prebilattice {X : hSet} (b: interlaced_prebilattice X) : prebilattice X := pr1 b.
  Coercion interlaced_prebilattice_to_prebilattice : interlaced_prebilattice >-> prebilattice .
End definition.

Section equalities.
  Definition interlaced_prebilattice_eq {X : hSet} (b1 : interlaced_prebilattice X) (b2 : interlaced_prebilattice X) (m : meet b1 ~ meet b2) (j : join b1 ~ join b2) (c : consensus b1 ~ consensus b2) (g : gullibility b1 ~ gullibility b2): b1 = b2.
  Show proof.
    use total2_paths_f.
    - use (prebilattice_eq b1 b2 m j c g).
    - apply isaprop_is_interlaced.

  Definition interlaced_prebilattice_transportf {X1 X2 : hSet} (b1 : interlaced_prebilattice X1) (b2 : interlaced_prebilattice X2) (p : X1 = X2)
             (m : meet (transportf interlaced_prebilattice p b1) ~ meet b2)
             (j : join (transportf interlaced_prebilattice p b1) ~ join b2)
             (c : consensus (transportf interlaced_prebilattice p b1) ~ consensus b2)
             (g : gullibility (transportf interlaced_prebilattice p b1) ~ gullibility b2)
    : transportf interlaced_prebilattice p b1 = b2.
  Show proof.
    use total2_paths_f.
    - unfold interlaced_prebilattice.
      rewrite (pr1_transportf p b1).
      use prebilattice_transportf; [set (i := m) | set (i := j) | set (i := c) | set (i := g)];
        use (homotcomp _ i);
        induction p;
        use homotrefl.
    - apply isaprop_is_interlaced.
End equalities.

Section properties.
  Lemma interlacing_consensus_t {X : hSet} (b : interlaced_prebilattice X) : interlacing (consensus b) (tle b).
  Show proof.
.
    exact (pr12 b) .
  Lemma interlacing_gullibility_t {X : hSet} (b : interlaced_prebilattice X) : interlacing (gullibility b) (tle b).
  Show proof.
    exact (pr122 b) .
  Lemma interlacing_meet_k {X : hSet} (b : interlaced_prebilattice X) : interlacing (meet b) (kle b) .
  Show proof.
    exact (pr1 (pr2 (pr2 (pr2 b)))) .
  Lemma interlacing_join_k {X : hSet} (b : interlaced_prebilattice X) : interlacing (join b) (kle b) .
  Show proof.
    exact (pr2 (pr2 (pr2 (pr2 b)))) .

  Definition double_interlacing {X : hSet} {op : binop X} {R : hrel X} (i : interlacing op R) (a : istrans R) (c : iscomm op) {x y z w : X} (p : R x y) (q : R z w) : R (op x z) (op y w).
  Show proof.
    use (a (op x z) (op y z)).
    - use i. exact p.
    - rewrite (c y z), (c y w). use i . exact q.

  Lemma double_interlacing_gullibility_t {X : hSet} {b : interlaced_prebilattice X} {x y z w : X} (p : tle b x y) (q : tle b z w) : tle b (gullibility b x z) (gullibility b y w) .
  Show proof.
    exact (double_interlacing (interlacing_gullibility_t _) (istrans_Lle (tlattice _)) (iscomm_Lmax (klattice _)) p q) .
  Lemma double_interlacing_consensus_t {X : hSet} {b : interlaced_prebilattice X} {x y z w : X} (p : tle b x y) (q : tle b z w) : tle b (consensus b x z) (consensus b y w) .
  Show proof.
    exact (double_interlacing (interlacing_consensus_t _) (istrans_Lle (tlattice _)) (iscomm_Lmin (klattice _)) p q) .
  Lemma double_interlacing_meet_k {X : hSet} {b : interlaced_prebilattice X} {x y z w : X} (p : kle b x y) (q : kle b z w) : kle b (meet b x z) (meet b y w) .
  Show proof.
    exact (double_interlacing (interlacing_meet_k _) (istrans_Lle (klattice _)) (iscomm_Lmin (tlattice _)) p q).
  Lemma double_interlacing_join_k {X : hSet} {b : interlaced_prebilattice X} {x y z w : X} (p : kle b x y) (q : kle b z w) : kle b (join b x z) (join b y w) .
  Show proof.
    exact (double_interlacing (interlacing_join_k _) (istrans_Lle (klattice _)) (iscomm_Lmax (tlattice _)) p q).

  Lemma top_interlacing_gullibility_t {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : tle b x z) (q : tle b y z) : tle b (gullibility b x y) z.
  Show proof.
    rewrite <- (Lmax_id (klattice b) z).
    use (double_interlacing_gullibility_t p q).
  Lemma top_interlacing_consensus_t {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : tle b x z) (q : tle b y z) : tle b (consensus b x y) z.
  Show proof.
    rewrite <- (Lmin_id (klattice b) z).
    use (double_interlacing_consensus_t p q).
  Lemma top_interlacing_join_k {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : kle b x z) (q : kle b y z) : kle b (join b x y) z.
  Show proof.
    rewrite <- (Lmax_id (tlattice b) z).
    use (double_interlacing_join_k p q).
  Lemma top_interlacing_meet_k {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : kle b x z) (q : kle b y z) : kle b (meet b x y) z.
  Show proof.
    rewrite <- (Lmin_id (tlattice b) z).
    use (double_interlacing_meet_k p q).

  Lemma bottom_interlacing_join_k {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : kle b z x) (q : kle b z y) : kle b z (join b x y).
  Show proof.
    rewrite <- (Lmax_id (tlattice b) z).
    use (double_interlacing_join_k p q).
  Lemma bottom_interlacing_meet_k {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : kle b z x) (q : kle b z y) : kle b z (meet b x y).
  Show proof.
    rewrite <- (Lmin_id (tlattice b) z).
    use (double_interlacing_meet_k p q).
  Lemma bottom_interlacing_gullibility_t {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : tle b z x) (q : tle b z y) : tle b z (gullibility b x y).
  Show proof.
    rewrite <- (Lmax_id (klattice b) z).
    use (double_interlacing_gullibility_t p q).
  Lemma bottom_interlacing_consensus_t {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : tle b z x) (q : tle b z y) : tle b z (consensus b x y).
  Show proof.
    rewrite <- (Lmin_id (klattice b) z).
    use (double_interlacing_consensus_t p q).

  Lemma dual_prebilattice_is_interlaced {X : hSet} (b : interlaced_prebilattice X) : is_interlaced (dual_prebilattice b).
  Show proof.
    destruct b as [? [? [? [? ?]]]] . do 3 (try split); assumption .

  Lemma opp_prebilattice_is_interlaced {X : hSet} (b : interlaced_prebilattice X) : is_interlaced (opp_prebilattice b).
  Show proof.
    do 3 (try split); intros ? ? ? H;
    [set (i := (interlacing_gullibility_t b)) | set (i := interlacing_consensus_t b) | set (i := interlacing_join_k b) | set (i := interlacing_meet_k b)];
    use (Lmax_le_eq_l _ _ _ (i _ _ _ (Lmax_le_eq_l _ _ _ H))).

  Lemma t_opp_prebilattice_is_interlaced {X : hSet} (b : interlaced_prebilattice X) : is_interlaced (t_opp_prebilattice b).
  Show proof.
    do 3 (try split); intros ? ? ? H.
    - use (Lmax_le_eq_l _ _ _ (interlacing_consensus_t _ _ _ _ (Lmax_le_eq_l _ _ _ H))).
    - use (Lmax_le_eq_l _ _ _ (interlacing_gullibility_t _ _ _ _ (Lmax_le_eq_l _ _ _ H))).
    - use (interlacing_join_k _ _ _ _ H).
    - use (interlacing_meet_k _ _ _ _ H).

  Lemma k_opp_prebilattice_is_interlaced {X : hSet} (b : interlaced_prebilattice X) : is_interlaced (k_opp_prebilattice b).
  Show proof.
    destruct (t_opp_prebilattice_is_interlaced (make_interlaced_prebilattice (dual_prebilattice_is_interlaced b))) as [? [? [? ?]]].
    do 3 (try split); assumption.

  Lemma interlaced_leqt_leqk_leqkmeet {X : hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, tle b x r × kle b r y) -> kle b x (meet b y x).
  Show proof.
    intros ? x y [? [p1 p2]].
    set (w := (meet _ y x)); rewrite <- (Lmin_le_eq_r _ _ _ p1).
    use (interlacing_meet_k _ _ _ _ p2).

  Lemma interlaced_leqk_leqt_leqtconsensus {X:hSet}: ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, kle b x r × tle b r y) -> tle b x (consensus b y x).
  Show proof.
    intro b'.
    use (interlaced_leqt_leqk_leqkmeet (make_interlaced_prebilattice (dual_prebilattice_is_interlaced b'))).

  Lemma interlaced_leqk_geqt_geqtconsensus {X:hSet}: ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, kle b x r × tle b y r) -> tle b (consensus b y x) x.
  Show proof.
    intros ? x y [? [p1 p2]].
    set (w := (consensus _ y x)); rewrite <- (Lmin_le_eq_r _ _ _ p1).
    use (interlacing_consensus_t _ _ _ _ p2).

  Lemma interlaced_leqt_leqk_leqtconsensus {X : hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, tle b x r × kle b r y) -> tle b x (consensus b y x).
  Show proof.
    intros b' ? ? [? [p1 p2]].
    set (pp := interlaced_leqt_leqk_leqkmeet _ _ _ (_,,p1,,p2)).
    rewrite (iscomm_meet) in pp.
    use (interlaced_leqk_leqt_leqtconsensus _ _ _ (_,, pp,, Lmin_le_r (tlattice b') _ _)).

  Lemma interlaced_geqt_leqk_geqtconsensus {X : hSet} : ∏ (b : interlaced_prebilattice X) (x y : X), (∑ r : X, tle b r x × kle b r y) -> tle b (consensus b y x) x.
  Show proof.
    intros b x y [r [p1 p2]].
    assert (p1' : tle (make_interlaced_prebilattice (t_opp_prebilattice_is_interlaced b)) x r).
    {
      rewrite <- p1, iscomm_Lmin.
      use Lmax_absorb.
    }
    set (t := consensus b y x).
    assert (p : Lmax (tlattice b) t x = x).
    {
      rewrite iscomm_Lmax.
      exact (interlaced_leqt_leqk_leqtconsensus (make_interlaced_prebilattice (t_opp_prebilattice_is_interlaced b)) x y (r,,p1',,p2)).
    }
    rewrite <- p.
    use Lmin_absorb.

  Lemma interlaced_geqt_geqk_geqkjoin {X: hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, tle b r x × kle b y r) -> kle b (join b y x) x .
  Show proof.
    intros b' ? ? [? [p1 p2]].
    set (bop := make_interlaced_prebilattice (opp_prebilattice_is_interlaced b')).
    set (H := interlaced_leqt_leqk_leqkmeet bop _ _ (_,,(Lmax_le_eq_l _ _ _ p1),, (Lmax_le_eq_l _ _ _ p2))).
    use (Lmax_le_eq_l _ _ _ H).

  Lemma interlaced_leqk_leqt_leqkmeet {X : hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, kle b x r × tle b r y) -> kle b x (meet b y x) .
  Show proof.
.
    intro b'.
    use (interlaced_leqt_leqk_leqtconsensus (make_interlaced_prebilattice (dual_prebilattice_is_interlaced b'))).
End properties.