## Stream: general

### Topic: heyting_algebra

#### christopher andrew upshaw (Dec 20 2020 at 08:21):

So because heyting_algebras define complement in terms of implication, but the current boolean algebra is defined in terms of complement, everywhere we provide an instance of boolean_algebra has to change with my current refactor. Is there some way to avoid this?

#### Mario Carneiro (Dec 20 2020 at 09:37):

a heyting algebra has a complement field too, but it adds the constraint that the complement is equal to the definition using implication

#### Mario Carneiro (Dec 20 2020 at 09:38):

Take a look at the way lt is written in the definition of src#preorder

#### christopher andrew upshaw (Dec 20 2020 at 20:17):

I think I am already doing that, but it still means that the definition of boolean changes enough that instances do longer work.
From
lean
class boolean_algebra α extends bounded_distrib_lattice α, has_compl α, has_sdiff α :=
(inf_compl_le_bot : ∀x:α, x ⊓ xᶜ ≤ ⊥)
(top_le_sup_compl : ∀x:α, ⊤ ≤ x ⊔ xᶜ)
(sdiff_eq : ∀x y:α, x \ y = x ⊓ yᶜ)

to
lean
class heyting_algebra α extends bounded_distrib_lattice α, has_compl α, has_internal_imp α :=
(imp_adjoint : ∀ x y z : α, x ⊓ y ≤ z ↔ x ≤ y ⇨ z)
(compl_eq : ∀ x : α, xᶜ = (x ⇨ ⊥))


and

class boolean_algebra α extends heyting_algebra α, has_sdiff α :=
(top_le_sup_compl : ∀x:α, ⊤ ≤ x ⊔ xᶜ)
(sdiff_eq : ∀x y:α, x \ y = x ⊓ yᶜ)


So under the old scheme all you needed was the complement and sdiff, but now you need to define the implication and imp_adjoint. (Which seems harder to prove sometimes.) I am very much open to suggestions about how this should be structured.

#### Chris Hughes (Dec 22 2020 at 15:13):

You should probably keep implication as part of the definition of boolean_algebra, but provide a new constructor for people to construct a boolean_algebra with only the sdiff and complement fields the same way as before.

#### Eric Wieser (Dec 22 2020 at 15:14):

Could you try to fix your #backticks christopher?

Last updated: Dec 20 2023 at 11:08 UTC