refactor(order/complete_lattice): ditch `complete_semilattice_Inf` and `complete_semilattice_Sup` #14863

vihdzp · 2022-06-21T08:34:11Z

These typeclasses are made entirely redundant by complete_lattice. They were only used to define complete_lattice instances through complete_lattice_of_complete_semilattice_Inf and complete_lattice_of_complete_semilattice_Sup, but this can more directly be done with complete_lattice_of_Inf and complete_lattice_of_Sup.

Zulip

src/topology/metric_space/emetric_space.lean

YaelDillies · 2022-06-21T11:56:03Z

Note, we do not need to delete them to remove them from the typeclass hierarchy. You can consider them as alternative constructors and simply not give them any instance nor lemmas.

vihdzp · 2022-06-21T20:15:02Z

I do think it's best to remove them, so that nobody gets the wrong impression that these are useful standalone typeclasses. The complete_lattice_of_Inf and complete_lattice_of_Sup constructors pretty much retain all the convenience these typeclasses had.

src/measure_theory/measure/measure_space.lean

src/order/complete_lattice.lean

src/topology/algebra/group.lean

src/topology/algebra/ring.lean

src/topology/metric_space/emetric_space.lean

YaelDillies · 2022-06-22T22:33:12Z

Well no, because it uses is_glb instead of Inf_le, le_Inf, and you need to copy the resulting complete_lattice to fix definitional equalities.

vihdzp · 2022-06-22T23:45:57Z

is_glb (Inf s) is def-eq to Inf_le s \and le_Inf s. And you also needed to copy the resulting complete_lattice with the previous approach.

YaelDillies · 2022-06-22T23:50:27Z

Filling in p ∧ q is still more annoying than filling in p and q. So you can make it better by turning complete_semilattice_Inf into an actual constructor, which doesn't require copying.

vihdzp · 2022-06-23T04:16:32Z

If this is the problem, then I could just separate the hypotheses. But what's the point of even having the is_glb predicate if we consider working with the separate hypotheses simpler?

complete_semilattice_Inf is already a constructor. The only reason we copy it is to get nicer def-eqs.

vihdzp · 2022-06-23T05:46:54Z

Assuming there's situations where proving is_glb (Inf s) is easier than proving both fields Inf_le and le_Inf separately, we could merge them into a single field. If there's no such situations, then what purpose does that predicate serve?

urkud · 2022-06-27T21:08:51Z

These were added in #6797 by @semorrison. I wouldn't delete them without his approval.

As for is_glb vs Inf_le/le_Inf, I tried to refactor complete_lattice using is_glb_Inf/is_lub_Sup some time ago but failed to fix all errors. In many cases, the new proofs were shorter.

vihdzp · 2022-06-28T20:25:40Z

I would like to mention that Scott has been quite silent these past few weeks. I can wait, though I do plan to keep refactoring this and adjacent files, and might eventually cause trouble.

urkud · 2022-06-29T14:17:01Z

src/measure_theory/integral/lebesgue.lean

+    (set_lintegral_congr_fun hm
+      (ae_of_all _ (λ x, @max_eq_right ℝ≥0∞ _ _ _)))
+    (set_lintegral_congr_fun hm.compl
+      (ae_of_all _ (λ x (hx : ¬ _ ≤ _), max_eq_left (not_le.1 hx).le)))


Why did you need this change?

I have no idea, all I know is the code broke. To be fair, this was quite a nontrivial def-eq.

I hope that #15056 will fix this. I'll try to make it compile tonight.

Could you please merge master and see whether you still need this change?

urkud · 2022-06-29T14:18:59Z

src/measure_theory/measure/measure_space.lean

-
-  top := (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top),
+  bot_le := λ a s hs, bot_le,
+  top := (⊤ : outer_measure α).to_measure $ by { rw outer_measure.top_caratheodory, exact le_top },


I wonder why this no longer makes leanchecker fail.

src/measure_theory/measure/sub.lean

src/order/complete_lattice.lean

urkud · 2022-06-29T14:26:32Z

src/topology/algebra/group.lean

  ..group_topology.semilattice_inf,
-  ..complete_lattice_of_complete_semilattice_Inf _ }
+  ..group_topology.partial_order,
+  ..complete_lattice_of_Inf (group_topology α) $ λ S, ⟨


Can you use is_glb.of_image here?

I don't think so. These lemmas aren't def-eq even if they're very similar, because one is about all topological spaces, while the other is about all group topologies.

vihdzp · 2022-07-12T00:53:28Z

Seems like this PR inadvertently undos @YaelDillies' refactor on upper_set, since the proof for upper_set.Icoi_le_Ioi (isn't this a typo?) no longer works, but flipping the ≤ to a ≥ fixes it. I have no idea what could have caused this, since I don't ever touch the upper_lower.lean file. Maybe @urkud's recent refactor interacts weirdly with this?

tweak

6d8ee4b

vihdzp added WIP Work in progress awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 21, 2022

eric-wieser requested a review from semorrison June 21, 2022 08:38

vihdzp added 7 commits June 21, 2022 03:50

tweak

7b56794

fix

b3dbc2a

remove private def

7bfdfcc

fix

a3e899b

remove redundant fields

9ba03b4

change defs to instances

83aab98

Weird

9775f4c

vihdzp commented Jun 21, 2022

View reviewed changes

src/topology/metric_space/emetric_space.lean Show resolved Hide resolved

vihdzp mentioned this pull request Jun 21, 2022

[Merged by Bors] - refactor(order/complete_lattice): Sup lemmas before Inf lemmas #14868

Closed

sup before inf

9a7f04d

fix instance

e9419ee

vihdzp added 3 commits June 21, 2022 16:21

fix

7fd71c9

Update nolints.txt

36f22b3

tweak

4cbb204

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 22, 2022

vihdzp removed the WIP Work in progress label Jun 22, 2022

linesthatinterlace reviewed Jun 22, 2022

View reviewed changes

urkud reviewed Jun 29, 2022

View reviewed changes

src/measure_theory/measure/sub.lean Outdated Show resolved Hide resolved

urkud reviewed Jun 29, 2022

View reviewed changes

src/order/complete_lattice.lean Show resolved Hide resolved

urkud reviewed Jun 29, 2022

View reviewed changes

vihdzp added 2 commits June 29, 2022 11:15

Update sub.lean

9d64cc4

Merge branch 'master' into conditional_refactor

fa4f804

Merge branch 'master' into conditional_refactor

9990559

vihdzp added help-wanted The author needs attention to resolve issues awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 13, 2022

vihdzp closed this Mar 30, 2023

YaelDillies deleted the conditional_refactor branch March 30, 2023 11:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor(order/complete_lattice): ditch `complete_semilattice_Inf` and `complete_semilattice_Sup` #14863

refactor(order/complete_lattice): ditch `complete_semilattice_Inf` and `complete_semilattice_Sup` #14863

vihdzp commented Jun 21, 2022 •

edited

YaelDillies commented Jun 21, 2022

vihdzp commented Jun 21, 2022

YaelDillies commented Jun 22, 2022

vihdzp commented Jun 22, 2022 •

edited

YaelDillies commented Jun 22, 2022

vihdzp commented Jun 23, 2022

vihdzp commented Jun 23, 2022

urkud commented Jun 27, 2022

vihdzp commented Jun 28, 2022

urkud Jun 29, 2022

vihdzp Jun 29, 2022

urkud Jul 1, 2022

urkud Jul 11, 2022

urkud Jun 29, 2022

urkud Jun 29, 2022

vihdzp Jun 29, 2022

vihdzp commented Jul 12, 2022 •

edited

refactor(order/complete_lattice): ditch complete_semilattice_Inf and complete_semilattice_Sup #14863

refactor(order/complete_lattice): ditch complete_semilattice_Inf and complete_semilattice_Sup #14863

Conversation

vihdzp commented Jun 21, 2022 • edited

YaelDillies commented Jun 21, 2022

vihdzp commented Jun 21, 2022

YaelDillies commented Jun 22, 2022

vihdzp commented Jun 22, 2022 • edited

YaelDillies commented Jun 22, 2022

vihdzp commented Jun 23, 2022

vihdzp commented Jun 23, 2022

urkud commented Jun 27, 2022

vihdzp commented Jun 28, 2022

urkud Jun 29, 2022

Choose a reason for hiding this comment

vihdzp Jun 29, 2022

Choose a reason for hiding this comment

urkud Jul 1, 2022

Choose a reason for hiding this comment

urkud Jul 11, 2022

Choose a reason for hiding this comment

urkud Jun 29, 2022

Choose a reason for hiding this comment

urkud Jun 29, 2022

Choose a reason for hiding this comment

vihdzp Jun 29, 2022

Choose a reason for hiding this comment

vihdzp commented Jul 12, 2022 • edited

refactor(order/complete_lattice): ditch `complete_semilattice_Inf` and `complete_semilattice_Sup` #14863

refactor(order/complete_lattice): ditch `complete_semilattice_Inf` and `complete_semilattice_Sup` #14863

vihdzp commented Jun 21, 2022 •

edited

vihdzp commented Jun 22, 2022 •

edited

vihdzp commented Jul 12, 2022 •

edited