Updating preimage_val to use ↓∩ notation

Stream: mathlib4

[Richard Osborn]

With the new notation defined in Mathlib.Data.Set.Subset for preimage_val, would people be interested in converting the existing theorems in Mathlib to use this notation? A simple loogle search shows at least 49 theorems that reference Subtype.val ⁻¹', but do not use the ↓∩ notation. Personally, I think the new notation is much clearer and would happily submit a PR.

[Eric Wieser]

Can you explain how you're using loogle to conclude that these theorems do not use the new notation (in the source code)?

[Eric Wieser]

Note I find 44 theorems if I search for things which _do_ use that notation!

[Richard Osborn]

As far as I can tell when grepping Mathlib, Data.Set.Subset is the only file that actually uses the notation. So, I just ignored the loogle results from that file.

[Richard Osborn]

I demonstrated potential changes in #12418. Would be interested in hearing if anyone thinks this is a downgrade.

[Eric Wieser]

Perhaps it's worth noting that Subtype.val ⁻¹' is more general than ↓∩, since the former works on subtypes but the latter only on sets

[Richard Osborn]

Yea, I realized that when Topology.Algebra.StarSubalgebra failed to compile. Should I change the definition of ↓∩ to work with subtypes? I can look into it tonight or tomorrow.

[Kyle Miller]

The ↓∩ notation was intentionally designed for sets, to make sure it elaborates in a predictable way with s ↓∩ t having type Set s.

If generalizing it doesn't mean needing to introduce type ascriptions, then that might be ok.

[Kyle Miller]

What goes wrong in Topology.Algebra.StarSubalgebra?

[Jireh Loreaux]

Topology.Algebra.StarSubalgebra is not fully battle-tested (i.e., not that much depends on it). It's possible there are issues that need fixing.

[Richard Osborn]

The error was a convert within docs#StarSubalgebra.closedEmbedding_inclusion that was unable to unify.

application type mismatch
  (range_subtype_map id ?m.7619).symm
argument
  range_subtype_map id ?m.7619
has type
  range (Subtype.map id ?m.7619) = {x | ?m.7613 x} ↓∩ id '' {x | ?m.7612 x} : Prop
but is expected to have type
  range (Subtype.map id ?m.7619) = ?m.7627 : Prop

The fix isn't very difficult, but it does point out that the notation isn't as powerful as just Subtype.val ⁻¹'.

--- a/Mathlib/Topology/Algebra/StarSubalgebra.lean
+++ b/Mathlib/Topology/Algebra/StarSubalgebra.lean
@@ -52,10 +52,8 @@ theorem closedEmbedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤
   { embedding_inclusion h with
     isClosed_range := isClosed_induced_iff.2
       ⟨S₁, hS₁, by
-          convert (Set.range_subtype_map id _).symm
-          · rw [Set.image_id]; rfl
-          · intro _ h'
-            apply h h' ⟩ }
+        convert (Set.range_subtype_map id (fun _ a ↦ h a)).symm
+        rw [Set.image_id]; rfl ⟩ }
 #align star_subalgebra.closed_embedding_inclusion StarSubalgebra.closedEmbedding_inclusion

[Richard Osborn]

In #12418, I went ahead and changed the rest of mathlib, but limited to cases where the left-hand of ↓∩ is a Set.
While changing things, I noticed that image_restrict and volume_preimage_coe flip the order of the sets in the type signature. Should this be changed?
Also, the naming conventions are fairly inconsistent between preimage_val, preimage_coe,preimage_subtype_coe, coe_preimage, etc... I assume one of these should be favored? Should image_preimage_coe be deprecated as it's a duplicate of image_preimage_val?

[Eric Wieser]

A PR that deprecates the coe lemmas in favor of the val lemmas (and does nothing else; no notation changes yet) sounds like a good idea to me

[Richard Osborn]

Is the current mathlib policy to replace coe with the actual function name?

[Eric Wieser]

I think so, but that might be worth a dedicated thread

[Eric Wieser]

The argument is that coe doesn't exist in the final statement

[Richard Osborn]

btw, #12418 had a curl failure. Is it possible to re-run the CI? It seems to build successfully on my machine.
Nevermind. I figured out how to re-run it.

[Ruben Van de Velde]

Looks like you did

[Yaël Dillies]

Richard Osborn said:

Is the current mathlib policy to replace coe with the actual function name?

Personally I replace it with (↑)

[Ruben Van de Velde]

That doesn't work in the name

[Eric Wieser]

A literal coe should never appear in theorem statements

[Richard Osborn]

Eric Wieser said:

A PR that deprecates the coe lemmas in favor of the val lemmas (and does nothing else; no notation changes yet) sounds like a good idea to me

I did a quick search and replace in #12465 and noticed that even if (↑) expands as a Subtype.val, its type won't necessarily match what Subtype.val itself would expand to (not sure if I am using the correct terminology). Is this the sort of behavior you are trying to avoid with wanting to deprecate coe lemmas? Does anyone know lean well enough to know when to use (↑) vs Subtype.val, and if so, could it be explained to us mortals? :sweat_smile:

[Eric Wieser]

Here's an example of that:

import Mathlib

set_option pp.explicit true

variable (s : Set ℕ) (m : AddSubmonoid ℕ)
#check (Subtype.val ⁻¹' s : Set m)
#check ((↑) ⁻¹' s : Set m)

[Eric Wieser]

I think problably:

• The lemmas should be written with (↑) where possible
• The lemmas should be named with val, since this is ultimately what gets elaborated

[Eric Wieser]

The actual type difference here is largely irrelevant, and having two copies of every lemma that appear the same in the docs (and in practice) is just confusing.

[Richard Osborn]

Ok, so when I changed docs#TopologicalSpace.Opens.openEmbedding' to use (↑), the type of openEmbedding' changed. I explain the change in slightly more detail in #12465. Would this be considered an improvement? I was hoping to do these changes without changing the types of things, but this seems incredibly difficult to do without a tool like leaff.