lean#1910 (dot notation with coercions) has been fixed

Stream: mathlib4

[Kim Morrison]

lean#1910 has been fixed. Would anyone be interested in going through the 26 appearances of the URL https://github.com/leanprover/lean4/issues/1910 in Mathlib and taking advantage of dot notation again, and removing the porting notes?

[Edward van de Meent]

i'll take a look

[Edward van de Meent]

Kim Morrison said:

and taking advantage of dot notation again

there are hundreds of occurences of Additive.toAdd (and mul version) to be changed.... and that's just one porting note...

[Edward van de Meent]

seems like a right place to split PRs...
PR at #19369 for the Additive and Multiplicative changes, please take a look to decide if this is appropriately sized or if the PR should be split up more...

[Edward van de Meent]

btw, it looks like there is some defeq abuse at around Order.succ_toMul?

[Junyan Xu]

One that I often encounter is docs#Subalgebra.toSubmodule

[Junyan Xu]

Is there a PR making dot notation work for docs#LinearMap.range etc.? Currently the middle example in #11036 to lean#1910, but it seems to be a different problem since no coercion is going on ...

[Edward van de Meent]

part of the issue there is also that the definition is more general than just linear maps...

[Kyle Miller]

There's a proposal to make dot notation first look for an argument named self rather than an argument whose type matches. That would work here for LinearMap itself, right?

[Edward van de Meent]

if you want g.ker to work, lean would need to recognise that the f:F argument to LinearMap.Ker is the intended place for g to fit, somehow... i think naming the argument self would work in that case, yes.

[Edward van de Meent]

could you link the proposal?

[Edward van de Meent]

you might still need to use the LinearMap.ker g notation when g is an AlgHom, so it still wouldn't be 'optimal'

[Kyle Miller]

lean4#1629 has the self proposal, and lean4#5482 has a proposal for adding to the list of namespaces that dot notation searches through. That second one also has a link to another proposal.

[Edward van de Meent]

Edward van de Meent said:

btw, it looks like there is some defeq abuse at around Order.succ_toMul?

PR fixing this at #19379

[Edward van de Meent]

2nd PR removing porting notes at #19380

[Edward van de Meent]

there are a bunch of porting notes in relation to this issue which claim that @[pp_nodot] has no effect on a declaration since it can't be used with dot notation anyway. However, the following example suggests that this still has no effect, as the pretty printer doesn't print these with dot notation anway... the following example shows this using docs#SymAlg.unsym as an example

import Mathlib.Algebra.Symmetrized

variable {α : Type*} (a:αˢʸᵐ)

#help attr pp_nodot -- [pp_nodot]: mark declaration to never be pretty printed using field notation

#check SymAlg.unsym -- this declaration has the @[pp_nodot] attribute in mathlib

-- as expected, no dot notation used here...
#check a.unsym -- SymAlg.unsym a : α

-- let's define it again, without the attribute
def SymAlg.unsym' := (@SymAlg.sym α).symm

-- doesn't use dot notation anyway
#check a.unsym' -- SymAlg.unsym' a : α

attribute [pp_nodot] SymAlg.unsym'

-- no change at all.
#check a.unsym' -- SymAlg.unsym' a : α

[Edward van de Meent]

what should happen with these porting notes?

[Edward van de Meent]

to be clear, these porting notes related to the pp_nodot attribute can be found near SymAlg.unsym (here), Real.nnabs (here), and NNReal.sqrt (here)

[Kyle Miller]

At some point I'm hoping the pretty printer can print these with dot notation, but yeah, it does not support it yet so pp_nodot does not yet have an effect.

[Edward van de Meent]

For the LinearMap.ker (and friends) related porting notes, i will replace the link to lean4#1910 with a link to lean4#1629

[Edward van de Meent]

Edward van de Meent said:

For the LinearMap.ker (and friends) related porting notes, i will replace the link to lean4#1910 with a link to lean4#1629

PR at #19381

[Edward van de Meent]

Kyle Miller said:

At some point I'm hoping the pretty printer can print these with dot notation, but yeah, it does not support it yet so pp_nodot does not yet have an effect.

alright, but what should happen to the porting notes which wrongly accuse lean4#1910 of causing this?

[Edward van de Meent]

(these are the only porting notes that arent covered by a PR yet)

[Kyle Miller]

It'd be a help if you made a new Lean issue that tracks pretty printing of the CoeFun dot notation :-)

[Edward van de Meent]

i haven't made issues for lean4 repo yet, is there some guide for best practices?

[Kyle Miller]

Maybe you could start by copying the lean4#1910 issue and then adjusting it to say "now dot notation works, but pretty printing doesn't".

In the end, I'm very likely going to be stuck with implementing the feature, and I know what it's about, but still it needs to be logged somewhere to make sure it happens. (I'd do it myself, but I don't have time for the next few hours at least.)

[Edward van de Meent]

lean4#6178

[Edward van de Meent]

putting the relevant PRs in a row:
#19369 removes porting notes for Additive.toMul and Multiplicative.toAdd

[Edward van de Meent]

• #19379 removes defeq abuse for docs#Order.succ_toMul and friends

[Edward van de Meent]

#19380 removes porting notes for OrderHom.lfp, OrderHom.gfp, and OrderHom.dual

[Edward van de Meent]

#19381 changes adaptation notes regarding LinearMap.range and friends to refer to lean4#1629 , since that is an issue that would actually solve the problem these notes are about

[Edward van de Meent]

#19385 changes adaptation notes regarding use of pp_nodot to refer to lean4#6178 , since that is the newly blocking issue for the purpose of these notes.

[Edward van de Meent]

at the end of the day, a whole 4 porting notes are removed by these PRs (of the 26 which mentioned the issue) :melting_face:

[Joseph Myers]

There's a case I've seen (outside of mathlib, don't know if it appears anywhere in mathlib, and don't have a reduced test case) where dot notation with bundled functions (specifically, when a hypothesis calls a bundled function and dot notation is used on that hypothesis) still doesn't work even after the fix for lean#1910.

A representative example is at https://github.com/jsm28/AperiodicMonotilesLean/blob/a20bb761aee7263a613d4853662ca368f26321ef/AM/Mathlib/Combinatorics/Tiling/Periodic.lean#L156 - if I change FiniteDistinctIntersections.finiteDistinctIntersectionsOn {x} hf to hf.finiteDistinctIntersectionsOn {x}, it no longer works; Lean is apparently looking for Discrete.TileSetFunction.toFun.finiteDistinctIntersectionsOn when I'd like it to look for Discrete.TileSet.FiniteDistinctIntersections.finiteDistinctIntersectionsOn given that hf is calling Discrete.TileSet.FiniteDistinctIntersections.

[Kyle Miller]

I'd be interested in a reduced test case

[Joseph Myers]

Reduced test case, not depending on mathlib, where I'd like dot notation to work but it doesn't:

structure MyStruct (ι : Type) where
  d : ι → Nat

structure MyFun where
  toFun : {ι : Type} → MyStruct ι → Prop

instance : CoeFun MyFun (fun _ ↦ {ι : Type} → MyStruct ι → Prop) where
  coe := MyFun.toFun

namespace MyStruct

def IsZero : MyFun where
  toFun := fun s ↦ ∀ i, s.d i = 0

def IsConst : MyFun where
  toFun := fun s ↦ ∀ i j, s.d i = s.d j

theorem IsZero.isConst {ι : Type} {s : MyStruct ι} (h : s.IsZero) : s.IsConst := by
  intro i j
  rw [h i, h j]

example {ι : Type} {s : MyStruct ι} (h : s.IsZero) : s.IsConst :=
  h.isConst

/-
23:2:
invalid field 'isConst', the environment does not contain 'MyFun.toFun.isConst'
  h
has type
  IsZero.toFun s
23:2:
invalid field notation, type is not of the form (C ...) where C is a constant
  h
has type
  ∀ (i : ι), s.d i = 0
-/

end MyStruct

[Violeta Hernández]

#19237 addresses (among other things) an instance of this

[Violeta Hernández]

#19417 doesn't directly address a porting note but it does amend a more recent decision that was made based on the lack of dot notation

[Kyle Miller]

Thanks for minimizing @Joseph Myers. Here's my understanding of the issue:

• s.IsZero is short for IsZero.toFun s due to the fix to lean4#1910, so at least that works.
• Recall that this type is @MyStruct.MyFun.toFun MyStruct.IsZero ι s in full.
• Writing h.isConst, it takes the head constant MyStruct.MyFun.toFun and looks for something named isConst in that namespace. There is no MyStruct.MyFun.toFun.isConst, so dot notation fails.

We don't have any mechanism to reverse a CoeFun, at least not yet, so there's no way for dot notation to deduce that it should be looking in the MyStruct.IsZero namespace. Even if it did, it would have to figure out that it shouldn't be looking for a MyStruct.MyFun.toFun argument — it would have to reverse the CoeFun on s itself too.

I'm not sure if we will ever support this ('this' being reversing coercions to resolve dot notations), sorry Joseph.

I do have a workaround for you, which is to move IsZero.isConst or at least give it an alias. This works:

alias MyFun.toFun.isConst := MyStruct.IsZero.isConst

example {ι : Type} {s : MyStruct ι} (h : s.IsZero) : s.IsConst :=
  h.isConst