Commit 2023-12-20 15:10 a4a7700f

refactor: Closure predicate for ClosureOperator (#9153) This PR is the result of two years and a half of pondering. The only way we ever define closure operators is by having a pre-existing "closedness" predicate and defining the closure of an element x as the infimum of all closed y ≥ x (assuming we're in a complete lattice). In particular, the emphasis is not on the preorder of closed elements, but on the closedness predicate. Morally, this is because a closure operator is the same as a Galois connection to the preorder of closed elements, but without mentioning the preorder of closed elements. That means that if we cared about the preorder of closed elements, we would not have wanted a closure operator in the first place, but a Galois connection. All this said, here's what this PR does

• Add an IsClosed predicate to ClosureOperator. This redundant field is here to fix definitional equalities.
• Remove the set closeds. This is mostly replaced by the predicate, except in the map toCloseds, so we...
• ... Introduce an abbrev Closeds for the order of closed elements
• Rename toClosed to toCloseds to match.
• Rename the constructor mk₃ to the more sexy ofPred. This is virtually the only useful constructor. Maybe it should even be taken as the definition, but I haven't gone that far.
• Rename the old ofPred to ofCompletePred. ofCompletePred is a specialisation of ofPred to the case where we are in a complete lattice.
• Remove a bunch of lemmas that are junk now that the definitional equality for IsClosed can be controlled.
• Golf existing uses of ClosureOperator. The diff here, I think, truly demonstrates that this PR is a step forward. I am not extending the refactor to LowerAdjoint because:
• I am still not sure we want LowerAdjoint to even exist
• The rationale of preferring the closedness predicate over the preorder of closed elements is less strong here.
• I am lazy. It is however easy to do the same refactor if wanted.