# Library RelationAlgebra.prop

lattice operations

Canonical Structure Prop_lattice_ops: lattice.ops := {|

leq := impl;

weq := iff;

cup := or;

cap := and;

neg := not;

bot := False;

top := True

|}.

bounded distributive lattice laws
(we could get a Boolean lattice by assuming excluded middle)

#[export] Instance Prop_lattice_laws: lattice.laws (BDL+STR+CNV+DIV) Prop_lattice_ops.

Proof.

constructor; (try apply Build_PreOrder); simpl;

repeat intro; try discriminate; tauto.

Qed.

we could also equip Prop with a flat monoid structure, but this is
not useful in practice