Module Prop.Boolean

The type property must form a partial order, and must be equipped with a least element bottom and with an equality test equal. The partial order must satisfy the ascending chain condition: every monotone sequence must eventually stabilize.

We do not require an ordering test leq or a join operation join.

bottom is the least property.

equal p q determines whether the properties p and q are equal. In the implementation of this test, it is permitted to assume that p <= q holds.

is_maximal p determines whether the property p is maximal with respect to the partial order. A conservative check suffices: it is always permitted for is_maximal p to be false. If is_maximal p is true, then p must have no strict upper bound. In particular, if properties form a lattice, then is_maximal p = true implies that p is the top element of the lattice.

leq p q determines whether p <= q holds.

join p q is the least upper bound of the properties p and q.

leq_join p q must compute the join of p and q. If the result is logically equal to q, then q itself must be returned. Thus, we have leq_join p q == q if and only if leq p q holds.