Prop as `canonically_ordered_monoid`

Stream: Is there code for X?

[Junyan Xu]

Do we have something like this? Of course it's non-standard to use + to denote or, but that's better than *.

instance Prop.canonically_ordered_add_monoid : canonically_ordered_add_monoid Prop :=
{ add := (∨),
  add_assoc := λ a b _, propext (or_assoc a b),
  zero := false,
  zero_add := λ a, propext (false_or a),
  add_zero := λ a, propext (or_false a),
  add_comm := λ a b, propext (or_comm a b),
  bot := false,
  bot_le := λ _, false.elim,
  add_le_add_left := λ _ _ h _, or.imp_right h,
  exists_add_of_le := λ _ b h, ⟨b, propext (or_iff_right_of_imp h).symm⟩,
  le_self_add := λ _ _, or.inl,
.. Prop.partial_order }

#print axioms Prop.canonically_ordered_add_monoid /- propext -/

instance set.canonically_ordered_add_monoid {α} : canonically_ordered_add_monoid (set α) :=
{ add := (∪), le := (⊆), lt := (⊂), /- could be omitted but these are better syntactically -/
.. pi.canonically_ordered_add_monoid }

[Junyan Xu]

Since it doesn't use any classical axioms I expect that it generalizes to Heyting algebras; with classical axioms it becomes a linear order. I'm investigating what conditions would be required for has_ordered_sub.

[Yaël Dillies]

Maybe you want docs#boolean_algebra.to_boolean_ring?

[Yaël Dillies]

We also have docs#generalized_boolean_algebra.to_non_unital_comm_ring and probably could get a few weaker versions now that docs#heyting_algebra is a thing.

[Junyan Xu]

addition in boolean_ring is xor, IIRC.

[Yaël Dillies]

Right, then it looks more like docs#set_semiring.canonically_ordered_comm_semiring

[Junyan Xu]

Oh great, docs#set_semiring is the alias for set that I'm looking for.

[Junyan Xu]

Thanks!

[Junyan Xu]

The multiplication in docs#set_semiring is actually pointwise multiplication coming from a monoid structure on α, while the addition and order don't depend on the monoid structure. I think we should single out the canonically_ordered_add_monoid structure, but then set_semiring would be a misnomer.

In fact there is another way to put a semiring structure on set α, with multiplication given by intersection. However it doesn't satisfy the no zero-divisor condition eq_zero_or_eq_zero_of_mul_eq_zero since the intersection of two nonempty sets can be empty if they're disjoint, so it's not a canonically_ordered_comm_semiring, unless α is a subsingleton and we're in the classical setting. See the following for Prop, i.e. the special case α := unit:

instance Prop.canonically_ordered_comm_semiring : canonically_ordered_comm_semiring Prop :=
{ mul := (∧),
  left_distrib := λ _ _ _, propext and_or_distrib_left,
  right_distrib := λ _ _ _, propext or_and_distrib_right,
  zero_mul := λ a, propext (false_and a),
  mul_zero := λ a, propext (and_false a),
  mul_assoc := λ a b _, propext (and_assoc a b),
  one := true,
  one_mul := λ a, propext (true_and a),
  mul_one := λ a, propext (and_true a),
  mul_comm := λ a b, propext (and_comm a b),
  eq_zero_or_eq_zero_of_mul_eq_zero := sorry, /- classically true -/
.. Prop.canonically_ordered_add_monoid }

[Junyan Xu]

And I've also realized that has_ordered_sub corresponds to the co-Heyting condition:

instance : has_sub Prop := { sub := λ a b, a ∧ ¬ b }
/- classically satisfies `has_ordered_sub`; in a co-Heyting algebra we should define
  `sub := (\)` and then the condition `a \ b ≤ c ↔ a ≤ b ⊔ c` is exactly `has_ordered_sub`. -/

[Junyan Xu]

I realized that semilattice_sup + order_bot is sufficient to obtain a canonically_ordered_add_monoid:

def semilattice_sup.to_canonically_ordered_add_monoid {α} [sls : semilattice_sup α]
  [ob : order_bot α] : canonically_ordered_add_monoid α :=
{ add := (⊔),
  add_assoc := λ _ _ _, sup_assoc,
  zero := (⊥),
  zero_add := λ _, bot_sup_eq,
  add_zero := λ _, sup_bot_eq,
  add_comm := λ _ _, sup_comm,
  add_le_add_left := λ _ _, sup_le_sup_left,
  exists_add_of_le := λ _ b h, ⟨b, (sup_eq_right.2 h).symm⟩,
  le_self_add := λ _ _, le_sup_left,
.. sls, .. ob }

I also found Prop.distrib_lattice unnecessarily invokes classical axioms, so I opened #16497 to remove it.

[Yaël Dillies]

We could make a general as_canonical_order where we inherit those instances, and then redefine set_semiring as as_canonical_order (set α)