Library UniMath.OrderTheory.Prebilattice.Distributive
Interlaced pre-bilattice Georgios V. Pitsiladis, Aug. 2024 -
Distributive pre-bilattices are generalisations of distributive lattices.
Every distributive pre-bilattice is also interlaced.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice.
Require Import UniMath.OrderTheory.Prebilattice.Interlaced.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.OrderTheory.Lattice.Distributive.
Section Def.
Definition is_distributive_prebilattice {X : hSet} (b : prebilattice X) :=
isldistr (gullibility b) (consensus b)
× isldistr (join b) (meet b)
× isldistr (consensus b) (meet b)
× isldistr (meet b) (consensus b)
× isldistr (consensus b) (join b)
× isldistr (join b) (consensus b)
× isldistr (gullibility b) (meet b)
× isldistr (meet b) (gullibility b)
× isldistr (gullibility b) (join b)
× isldistr (join b) (gullibility b)
.
Lemma isaprop_is_distributive {X : hSet} {b : prebilattice X} : isaprop (is_distributive_prebilattice b).
Show proof.
Definition distributive_prebilattice (X : hSet) :=
∑ b : prebilattice X, is_distributive_prebilattice b.
Definition distributive_prebilattices_to_prebilattices {X : hSet} (b : distributive_prebilattice X) : prebilattice X := pr1 b.
Coercion distributive_prebilattices_to_prebilattices : distributive_prebilattice >-> prebilattice .
Definition make_distributive_prebilattice {X : hSet} {b : prebilattice X} (is : is_distributive_prebilattice b) : distributive_prebilattice X := b,,is .
End Def.
Section Properties.
Lemma is_distributive_klattice {X : hSet} (b : distributive_prebilattice X) : is_distributive (klattice b).
Show proof.
Lemma is_distributive_tlattice {X : hSet} (b : distributive_prebilattice X) : is_distributive (tlattice b).
Show proof.
Lemma ldistr_gullibility_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (gullibility b) (consensus b).
Show proof.
Lemma ldistr_consensus_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (gullibility b) .
Show proof.
Lemma rdistr_gullibility_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (consensus b) .
Show proof.
Lemma rdistr_consensus_gullibility {X : hSet} (b : distributive_prebilattice X): isrdistr (consensus b) (gullibility b) .
Show proof.
Lemma ldistr_join_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (meet b) .
Show proof.
Lemma ldistr_meet_join {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (join b) .
Show proof.
Lemma rdistr_meet_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (join b) .
Show proof.
Lemma rdistr_join_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (meet b) .
Show proof.
Lemma ldistr_consensus_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (meet b) .
Show proof.
Lemma rdistr_consensus_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (consensus b) (meet b) .
Show proof.
Lemma ldistr_meet_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (consensus b) .
Show proof.
Lemma rdistr_meet_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (consensus b) .
Show proof.
Lemma ldistr_consensus_join {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (join b) .
Show proof.
Lemma rdistr_consensus_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (consensus b) (join b) .
Show proof.
Lemma ldistr_join_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (consensus b) .
Show proof.
Lemma rdistr_join_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (consensus b) .
Show proof.
Lemma ldistr_gullibility_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (gullibility b) (meet b) .
Show proof.
Lemma rdistr_gullibility_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (meet b) .
Show proof.
Lemma ldistr_meet_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (gullibility b) .
Show proof.
Lemma rdistr_meet_gullibility {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (gullibility b) .
Show proof.
Show proof.
Lemma rdistr_gullibility_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (join b) .
Show proof.
Lemma ldistr_join_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (gullibility b) .
Show proof.
Lemma rdistr_join_gullibility {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (gullibility b) .
Show proof.
Proposition distributive_prebilattices_are_interlaced_prebilattices {X : hSet} (b : distributive_prebilattice X) : is_interlaced b .
Show proof.
Definition distributive_prebilattices_to_interlaced_prebilattices {X : hSet} (b : distributive_prebilattice X) : interlaced_prebilattice X :=
make_interlaced_prebilattice (distributive_prebilattices_are_interlaced_prebilattices b).
Coercion distributive_prebilattices_to_interlaced_prebilattices : distributive_prebilattice >-> interlaced_prebilattice .
End Properties.
Require Import UniMath.OrderTheory.Prebilattice.Interlaced.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.OrderTheory.Lattice.Distributive.
Section Def.
Definition is_distributive_prebilattice {X : hSet} (b : prebilattice X) :=
isldistr (gullibility b) (consensus b)
× isldistr (join b) (meet b)
× isldistr (consensus b) (meet b)
× isldistr (meet b) (consensus b)
× isldistr (consensus b) (join b)
× isldistr (join b) (consensus b)
× isldistr (gullibility b) (meet b)
× isldistr (meet b) (gullibility b)
× isldistr (gullibility b) (join b)
× isldistr (join b) (gullibility b)
.
Lemma isaprop_is_distributive {X : hSet} {b : prebilattice X} : isaprop (is_distributive_prebilattice b).
Show proof.
Definition distributive_prebilattice (X : hSet) :=
∑ b : prebilattice X, is_distributive_prebilattice b.
Definition distributive_prebilattices_to_prebilattices {X : hSet} (b : distributive_prebilattice X) : prebilattice X := pr1 b.
Coercion distributive_prebilattices_to_prebilattices : distributive_prebilattice >-> prebilattice .
Definition make_distributive_prebilattice {X : hSet} {b : prebilattice X} (is : is_distributive_prebilattice b) : distributive_prebilattice X := b,,is .
End Def.
Section Properties.
Lemma is_distributive_klattice {X : hSet} (b : distributive_prebilattice X) : is_distributive (klattice b).
Show proof.
Lemma is_distributive_tlattice {X : hSet} (b : distributive_prebilattice X) : is_distributive (tlattice b).
Show proof.
Lemma ldistr_gullibility_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (gullibility b) (consensus b).
Show proof.
Lemma ldistr_consensus_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (gullibility b) .
Show proof.
Lemma rdistr_gullibility_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (consensus b) .
Show proof.
Lemma rdistr_consensus_gullibility {X : hSet} (b : distributive_prebilattice X): isrdistr (consensus b) (gullibility b) .
Show proof.
Lemma ldistr_join_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (meet b) .
Show proof.
Lemma ldistr_meet_join {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (join b) .
Show proof.
Lemma rdistr_meet_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (join b) .
Show proof.
Lemma rdistr_join_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (meet b) .
Show proof.
Lemma ldistr_consensus_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (meet b) .
Show proof.
Lemma rdistr_consensus_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (consensus b) (meet b) .
Show proof.
Lemma ldistr_meet_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (consensus b) .
Show proof.
Lemma rdistr_meet_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (consensus b) .
Show proof.
Lemma ldistr_consensus_join {X : hSet} (b : distributive_prebilattice X) : isldistr (consensus b) (join b) .
Show proof.
Lemma rdistr_consensus_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (consensus b) (join b) .
Show proof.
Lemma ldistr_join_consensus {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (consensus b) .
Show proof.
Lemma rdistr_join_consensus {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (consensus b) .
Show proof.
Lemma ldistr_gullibility_meet {X : hSet} (b : distributive_prebilattice X) : isldistr (gullibility b) (meet b) .
Show proof.
Lemma rdistr_gullibility_meet {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (meet b) .
Show proof.
Lemma ldistr_meet_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (meet b) (gullibility b) .
Show proof.
Lemma rdistr_meet_gullibility {X : hSet} (b : distributive_prebilattice X) : isrdistr (meet b) (gullibility b) .
Show proof.
exact (weqldistrrdistr (meet b) (gullibility b) (iscomm_gullibility b) (ldistr_meet_gullibility b)) .
Lemma ldistr_gullibility_join {X : hSet} (b : distributive_prebilattice X) : isldistr (gullibility b) (join b) .Show proof.
Lemma rdistr_gullibility_join {X : hSet} (b : distributive_prebilattice X) : isrdistr (gullibility b) (join b) .
Show proof.
Lemma ldistr_join_gullibility {X : hSet} (b : distributive_prebilattice X) : isldistr (join b) (gullibility b) .
Show proof.
Lemma rdistr_join_gullibility {X : hSet} (b : distributive_prebilattice X) : isrdistr (join b) (gullibility b) .
Show proof.
exact (weqldistrrdistr (join b) (gullibility b) (iscomm_gullibility b) (ldistr_join_gullibility b)) .
Proposition distributive_prebilattices_are_interlaced_prebilattices {X : hSet} (b : distributive_prebilattice X) : is_interlaced b .
Show proof.
do 3 (try split); intros x y z H.
- rewrite (iscomm_consensus _ x z), (iscomm_consensus _ y z).
set(d := ldistr_meet_consensus b x y z). unfold meet in d. cbn.
rewrite <- d, H. reflexivity.
- rewrite (iscomm_gullibility _ x z), (iscomm_gullibility _ y z).
set (d := ldistr_meet_gullibility b x y z). unfold meet in d. cbn.
rewrite <- d, H; reflexivity.
- rewrite (iscomm_meet _ x z), (iscomm_meet _ y z).
set (d := (ldistr_consensus_meet b x y z)). unfold consensus in d. cbn.
rewrite <- d , H; reflexivity.
- rewrite (iscomm_join _ x z), (iscomm_join _ y z).
set (d := ldistr_consensus_join b x y z). unfold consensus in d. cbn.
rewrite <- d, H; reflexivity .
- rewrite (iscomm_consensus _ x z), (iscomm_consensus _ y z).
set(d := ldistr_meet_consensus b x y z). unfold meet in d. cbn.
rewrite <- d, H. reflexivity.
- rewrite (iscomm_gullibility _ x z), (iscomm_gullibility _ y z).
set (d := ldistr_meet_gullibility b x y z). unfold meet in d. cbn.
rewrite <- d, H; reflexivity.
- rewrite (iscomm_meet _ x z), (iscomm_meet _ y z).
set (d := (ldistr_consensus_meet b x y z)). unfold consensus in d. cbn.
rewrite <- d , H; reflexivity.
- rewrite (iscomm_join _ x z), (iscomm_join _ y z).
set (d := ldistr_consensus_join b x y z). unfold consensus in d. cbn.
rewrite <- d, H; reflexivity .
Definition distributive_prebilattices_to_interlaced_prebilattices {X : hSet} (b : distributive_prebilattice X) : interlaced_prebilattice X :=
make_interlaced_prebilattice (distributive_prebilattices_are_interlaced_prebilattices b).
Coercion distributive_prebilattices_to_interlaced_prebilattices : distributive_prebilattice >-> interlaced_prebilattice .
End Properties.