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.
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 ⇨ ⊥))
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: May 13 2021 at 17:42 UTC