CompleteBooleanAlgebra from CompleteDistribLattice

Stream: mathlib4

[Floris van Doorn]

How do I turn a complete distributive lattice into a complete Boolean algebra?
A year ago this was easy: just define compl and prove inf_compl_le_bot and top_le_sup_compl.

Since @Yaël Dillies's refactor of complete distributive lattices this is now much harder.
Either I use CompleteDistribLattice.ofMinimalAxioms. This means that compl instance already exists, and I have to prove that an unfriendly definition is the same as the definition I want.
and now I have two goals sdiff_eq and himp_eq involving two operations that I don't care about and they're not rfl anymore.
Or I use the constructor for CompleteDistribLattice and I have to give the operations himp and sdiff that I don't care about, and then I have to prove lemmas about (and having defined them in terms of complements does not make these properties entirely trivial).
Why don't these fields have default values?

[Floris van Doorn]

For reference, this was all I had to do a year ago: https://github.com/fpvandoorn/LeanCourse23/blob/master/LeanCourse/Lectures/Lecture11.lean#L478-L498

[Yaël Dillies]

This is for the same reason as to why we are slowly moving away from default values altogether: they are very prone to invisibly creating diamonds

[Yaël Dillies]

For people reading: docs#CompleteBooleanAlgebra, docs#CompleteDistribLattice

[Floris van Doorn]

I disagree with the objective to make beginners suffer so that we maybe avoid a diamond.

[Yaël Dillies]

Sorry, I don't understand what you are complaining about anymore

Floris van Doorn said:

now I have two goals sdiff_eq and himp_eq involving two operations that I don't care about and they're not rfl anymore.

Why are they not rfl? Can you provide a MWE?

[Yaël Dillies]

The usual way to fill in those "not default but morally default" arguments is to do

  sdiff_eq _ _ := rfl
  himp_eq _ _ := rfl

What I understand from your message is that this doesn't work. I am surprised!

[Floris van Doorn]

Not quite minimal:

import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Analysis.Calculus.Deriv.Pow

noncomputable section
open BigOperators Function Set Real Filter Classical Topology TopologicalSpace

/- The goal of the following exercise is to prove that
the regular open sets in a topological space form a complete boolean algebra.
`U ⊔ V` is given by `interior (closure (U ∪ V))`.
`U ⊓ V` is given by `U ∩ V`. -/


variable {X : Type*} [TopologicalSpace X]

variable (X) in
structure RegularOpens where
  carrier : Set X
  isOpen : IsOpen carrier
  regular' : interior (closure carrier) = carrier

namespace RegularOpens

/- We write some lemmas so that we can easily reason about regular open sets. -/
variable {U V : RegularOpens X}

instance : SetLike (RegularOpens X) X where
  coe := RegularOpens.carrier
  coe_injective' := fun ⟨_, _, _⟩ ⟨_, _, _⟩ _ => by congr

theorem le_def {U V : RegularOpens X} : U ≤ V ↔ (U : Set X) ⊆ (V : Set X) := by simp
@[simp] theorem regular {U : RegularOpens X} : interior (closure (U : Set X)) = U := U.regular'

@[simp] theorem carrier_eq_coe (U : RegularOpens X) : U.1 = ↑U := rfl

@[ext] theorem ext (h : (U : Set X) = V) : U = V :=
  SetLike.coe_injective h


/- First we want a complete lattice structure on the regular open sets.
We can obtain this from a so-called `GaloisCoinsertion` with the closed sets.
This is a pair of maps
* `l : RegularOpens X → Closeds X`
* `r : Closeds X → RegularOpens X`
with the properties that
* for any `U : RegularOpens X` and `C : Closeds X` we have `l U ≤ C ↔ U ≤ r U`
* `r ∘ l = id`
If you know category theory, this is an *adjunction* between orders
(or more precisely, a coreflection).
-/

/- The closure of a regular open set. Of course mathlib knows that the closure of a set is closed.
(the `simps` attribute will automatically generate the simp-lemma for you that
`(U.cl : Set X) = closure (U : Set X)`
-/
@[simps]
def cl (U : RegularOpens X) : Closeds X :=
  ⟨closure U, isClosed_closure⟩

/- The interior of a closed set. You will have to prove yourself that it is regular open. -/
@[simps]
def _root_.TopologicalSpace.Closeds.int (C : Closeds X) : RegularOpens X :=
  ⟨interior C, sorry, sorry⟩

/- Now let's show the relation between these two operations. -/
lemma cl_le_iff {U : RegularOpens X} {C : Closeds X} :
    U.cl ≤ C ↔ U ≤ C.int := by
  sorry

@[simp] lemma cl_int : U.cl.int = U := by
  ext1
  exact U.regular

/- This gives us a GaloisCoinsertion. -/

def gi : GaloisCoinsertion cl (fun C : Closeds X ↦ C.int) where
  gc U C := cl_le_iff
  u_l_le U := by simp
  choice C hC := C.int
  choice_eq C hC := rfl

/- It is now a general theorem that we can lift the complete lattice structure from `Closeds X`
to `RegularOpens X`. The lemmas below give the definitions of the lattice operations. -/

instance completeLattice : CompleteLattice (RegularOpens X) :=
  GaloisCoinsertion.liftCompleteLattice gi

@[simp] lemma coe_inf {U V : RegularOpens X} : ↑(U ⊓ V) = (U : Set X) ∩ V := by
  have : U ⊓ V = (U.cl ⊓ V.cl).int := rfl
  simp [this]

@[simp] lemma coe_sup {U V : RegularOpens X} : ↑(U ⊔ V) = interior (closure ((U : Set X) ∪ V)) := by
  have : U ⊔ V = (U.cl ⊔ V.cl).int := rfl
  simp [this]

@[simp] lemma coe_top : ((⊤ : RegularOpens X) : Set X) = univ := by
  have : (⊤ : RegularOpens X) = (⊤ : Closeds X).int := rfl
  simp [this]

@[simp] lemma coe_bot : ((⊥ : RegularOpens X) : Set X) = ∅ := by
  have : (⊥ : RegularOpens X) = (⊥ : Closeds X).int := rfl
  simp [this]

@[simp] lemma coe_sInf {U : Set (RegularOpens X)} :
    ((sInf U : RegularOpens X) : Set X) =
    interior (⋂₀ ((fun u : RegularOpens X ↦ closure u) '' U)) := by
  have : sInf U = (sInf (cl '' U)).int := rfl
  simp [this]

@[simp] lemma coe_sSup {U : Set (RegularOpens X)} :
    ((sSup U : RegularOpens X) : Set X) =
    interior (closure (⋃₀ ((fun u : RegularOpens X ↦ closure u) '' U))) := by
  have : sSup U = (sSup (cl '' U)).int := rfl
  simp [this]

/- We still have to prove that this gives a distributive lattice.
Warning: these are hard. -/
instance completeDistribLattice : CompleteDistribLattice (RegularOpens X) :=
  CompleteDistribLattice.ofMinimalAxioms
  { completeLattice with
    inf_sSup_le_iSup_inf := by sorry
    iInf_sup_le_sup_sInf := by sorry
    }

-- this now creates diamonds
-- instance : HasCompl (RegularOpens X) where
--   compl U := Closeds.int ⟨(U : Set X)ᶜ, U.isOpen.isClosed_compl⟩

@[simp]
lemma coe_compl (U : RegularOpens X) : ↑Uᶜ = interior (U : Set X)ᶜ := by
  sorry -- I guess I have to prove this now

instance : CompleteBooleanAlgebra (RegularOpens X) where
  __ := inferInstanceAs (CompleteDistribLattice (RegularOpens X))
  -- { inferInstanceAs (CompleteDistribLattice (RegularOpens X)) with
  inf_compl_le_bot := by simp
  top_le_sup_compl := by
    intro U
    rw [le_def]
    simp
    rw [← Set.univ_subset_iff]
    have : (U : Set X) ∪ Uᶜ ⊆ closure U ∪ Uᶜ
    · gcongr; apply subset_closure
    refine Subset.trans ?_ this
    simp
  le_sup_inf := by exact?
  sdiff_eq := fun x y ↦ rfl -- error
  himp_eq := fun x y ↦ rfl -- error

[Yaël Dillies]

That is unexpected :frown: I have a hunch that this is coming from a Lean change to how metavariables in where/{} notation are handled. Could you bisect on the Lean version?

[Yaël Dillies]

(I would offer to do it but my wrist is still painful and I need to prepare two talks...)

[Floris van Doorn]

I am unable to do that myself.

[Floris van Doorn]

So what is the intended way to give a complete Boolean algebra from a complete lattice? I want to prove
inf_sSup_le_iSup_inf/iInf_sup_le_sup_sInf/inf_compl_le_bot/top_le_sup_compl and nothing else.

[Floris van Doorn]

Note that my example above does not do this, because it also requires me to show that an inconveniently defined complement is equal to my complement. I want to provide the complement myself.

[Floris van Doorn]

Yaël Dillies said:

That is unexpected :frown: I have a hunch that this is coming from a Lean change to how metavariables in where/{} notation are handled. Could you bisect on the Lean version?

Why do you even expect himp_eq to be rfl when it's defined by this line?

[Yaël Dillies]

Ah wait, you are using ofMinimalAxioms!

[Yaël Dillies]

Sorry, I had completely missed that somehow. If you want to define your own compl, you shouldn't use it

[Yaël Dillies]

I am more and more confused. I now think this doesn't anything have to do with my refactor, except for the fact that it incidentally reordered some parents in the order hierarchy

[Floris van Doorn]

I think if you actually read my questions, that I nowhere have a problem that could be caused by reordering parents, and I do have problems with

• CompleteDistribLattice counterintuitively providing a HasCompl instance
• If I want to define a CompleteDistribLattice with my own HasCompl instance, I have to prove things that I don't want to prove.

[Floris van Doorn]

I guess I can do what I want mostly by just ignoring CompleteDistribLattice. Do you agree that we should add the following to Mathlib, to conveniently allow what I want?

import Mathlib.Order.CompleteBooleanAlgebra

structure CompleteBooleanAlgebra.MinimalAxioms (α : Type*) extends
    CompleteDistribLattice.MinimalAxioms α, HasCompl α where
  inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
  top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ

abbrev CompleteBooleanAlgebra.ofMinimalAxioms {α : Type*}
    (h : CompleteBooleanAlgebra.MinimalAxioms α) : CompleteBooleanAlgebra α where
      __ := h
      le_sup_inf x y z :=
        let z := CompleteDistribLattice.ofMinimalAxioms h.toMinimalAxioms
        le_sup_inf

[Eric Wieser]

The issue here is:

This sets a ⇨ b := sSup {c | c ⊓ a ≤ b}, aᶜ := a ⇨ ⊥, a \ b := sInf {c | a ≤ b ⊔ c} and
￢a := ⊤ \ a. -/

in the docs for docs#CompleteDistribLattice.ofMinimalAxioms

[Eric Wieser]

Generally, the ofMinimalAxioms constructors pick bad defeqs that probably don't compose very well across "joins" in the hierarchy

[Eric Wieser]

I think in particular the axioms are too minimal for your use-case, since you wanted to write

instance : HasCompl (RegularOpens X) where