heyting_algebra

Stream: general

[christopher andrew upshaw]

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]

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]

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

[christopher andrew upshaw]

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]

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]

Could you try to fix your #backticks christopher?