Library RelationAlgebra.prop

prop: Propositions (Prop) as a bounded distributive lattice

Require Import lattice.

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