# boolean: Booleans as a lattice, and as a monoid

Require Import monoid prop sups.

# Booleans as a lattice

Canonical Structure bool_lattice_ops: lattice.ops := {|
leq := le_bool;
weq := eq;
cup := orb;
cap := andb;
neg := negb;
bot := false;
top := true
|}.

is_true is a bounded distributive lattice homomorphism from bool to Prop. (Actually a Boolean lattice homomorphism, but we don't need it here.)
#[export] Instance mm_bool_Prop: morphism BDL is_true.
Proof.
constructor; simpl.
now auto.
intros ? ?. now rewrite eq_bool_iff.
intros _ [|] [|]; firstorder.
intros _ [|] [|]; firstorder.
intros _. easy.
tauto.
intros _ [|]. firstorder auto with bool. easy.
Qed.

we get most lattice laws by the faithful embedding into Prop
#[export] Instance bool_lattice_laws: lattice.laws (BL+STR+CNV+DIV) bool_lattice_ops.
Proof.
assert(H: lattice.laws BDL bool_lattice_ops).
apply (laws_of_injective_morphism is_true mm_bool_Prop).
auto.
intros x y. apply eq_bool_iff.
constructor; try apply H; (try now left); intros _ [|]; reflexivity.
Qed.

simple characterisation of finite sups and infs in bool

Lemma is_true_sup I J (f: I bool): \sup_(i\in J) f i ( i, List.In i J f i).
Proof.
unfold is_true. induction J; simpl. firstorder; discriminate.
rewrite Bool.orb_true_iff. firstorder congruence.
Qed.

Lemma is_true_inf I J (f: I bool): \inf_(i\in J) f i ( i, List.In i J f i).
Proof.
unfold is_true. induction J; simpl. firstorder.
rewrite Bool.andb_true_iff. firstorder congruence.
Qed.

# Boolean as a (flat) monoid

this is useful:
• to construct boolean matrices,
• to consider regex.epsilon as a functor)
this monoid is flat: this is a one object category. We use the following singleton type to avoid confusion with the singleton types of other flat structures
CoInductive bool_unit := bool_tt.

note that the trivial type information is simply ignored
Canonical Structure bool_ops: monoid.ops := {|
ob := bool_unit;
mor n m := bool_lattice_ops;
dot n m p := andb;
one n := true;
itr n x := x;
str n x := true;
cnv n m x := x;
ldv n m p x y := !x y;
rdv n m p x y := !x y
|}.

shorthand for bool, when a morphism is expected
Notation bool' := (bool_ops bool_tt bool_tt).

we actually have all laws on bool
#[export] Instance bool_laws: laws (BL+STR+CNV+DIV) bool_ops.
Proof.
constructor; (try now left);repeat right; intros.
apply bool_lattice_laws.
apply capA.
apply captx.
apply weq_leq. simpl. apply capC.
reflexivity.
now intros ? ? ?.
reflexivity.
all: try setoid_rewrite <- le_bool_spec.
all: try case x; try case y; try case z; reflexivity.
Qed.

# properties of the ofbool injection

Section ofbool.

Open Scope bool_scope.
Implicit Types a b c: bool.
Context {X: ops} {l} {L: laws l X} {n: ob X}.
Notation ofbool := (@ofbool X n).

Lemma andb_dot `{BOT l} a b: ofbool (a&&b) ofbool a ofbool b.
Proof.
symmetry. case a. apply dot1x.
apply antisym. now apply weq_leq, dot0x. apply leq_bx.
Qed.

Lemma orb_pls `{CUP+BOT l} a b: ofbool (a||b) ofbool a + ofbool b.
Proof. symmetry. case a; simpl. case b; simpl; lattice. lattice. Qed.

#[export] Instance ofbool_leq `{BOT l}: Proper (leq ==> leq) ofbool.
Proof. intros [|] b E; simpl. now rewrite E. apply leq_bx. Qed.

Lemma dot_ofboolx `{BOT l} b (x: X n n): ofbool bx xofbool b.
Proof. case b; simpl. now rewrite dot1x, dotx1. now rewrite dot0x, dotx0. Qed.

End ofbool.

is_true is also monotone
#[export] Instance is_true_leq: Proper (leq ==> leq) is_true.
Proof. intros [|] b E; simpl. now rewrite E. discriminate. Qed.