Dot notation shenanigans

Stream: lean4

[Andrew Yang]

def A := Unit
def B := A
def A.foo (b : B) : A := b
def A.bar (b : A) : A := b

variable (a : A)

#check A.foo a        -- works
#check a.foo          -- does not work
#check a.foo.bar      -- works
#check a.foo.foo      -- does not work
#check a.foo.foo.bar  -- works

Is there a reason why 3 and 5 works but 2 and 4 fails? 2 and 4 works if B is reducible, but I hope I can keep B as semireducible (for context, A is docs#AlgebraicGeometry.Scheme.Hom and B is docs#Quiver.Hom)

[Kyle Miller]

I'm surprised that 3 and 5 work.

[A.]

It seems that Lean treats a semireducible as irreducible if it appears in the penultimate position of the chain and as reducible otherwise. I don't think that can be right.

#check A.foo a        /- works because a is treated as reducible. -/
#check a.foo          /- does not work
  because a is in the penultimate position so is treated as irreducible. -/
#check a.foo.bar      /- works
  because a comes before the penultimate position so is treated as reducible,
  while a.foo already has the right type for bar. -/
#check a.foo.foo      /- does not work
  because although a comes before the penultimate position and is treated as reducible,
  a.foo is in the penultimate position so is treated as irreducible. -/
#check a.foo.foo.bar  /- works
  because a and a.foo come before the penultimate position so are treated as reducible,
  while a.foo.foo already has the right type for bar. -/

[A.]

I got burned earlier today by the difference between these two applications of Function.comp

import Mathlib.Data.Real.Basic
import Mathlib.Data.Matrix.Basic

variable {𝒩 : Type*} [Fintype 𝒩] (l : Matrix 𝒩 𝒩 ℝ)

#check l.vecMul.comp
#check (l.vecMul).comp

[Jon Eugster]

I only looked briefly at the source code, but I think I do get a feeling what's happening (see
Lean.Elab.App)

The relevant snippet seems to be this (line 1250-1256):

      if lvals.isEmpty then
        let fvarType ← inferType fvar
        let (args, namedArgs) ← addLValArg baseName fullName f args namedArgs fvarType
        elabAppArgs fvar namedArgs args expectedType? explicit ellipsis
      else
        let f ← elabAppArgs fvar #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
        loop f lvals

here, the list of dot notation things was split as lval::lvals further up in the code, so lval is foo and lvals is #[bar]. addLValArg is the function which throws the error in (3) and (5) (i.e. "no argument with type ...") and that one is only called for the last of these "projections". For all the ones before, it seems that rather there is some elaboration happening (in the else) statement, which I don't fully understand.

So I wouldn't be surprised if a.foo.bar is then essentially processed as (A.foo a).bar because the inner part got elaborated first.

[Andrew Yang]

What is the intended behaviour here? Can we make (2) and (4) work? Or is failing on (3) and (5) desired instead?

[Jon Eugster]

my first instinct was that (3) and (5) shouldn't be succeeding, but I don't know.

[Damiano Testa]

I think that the mechanism for making those work is to use abbrev (or @[reducible] def) instead of def, so I am also inclined to say that dot-notation should not see through defs.

[A.]

I think we see in the l.vecMul example above that permitting Lean to see through Matrix leads to a pretty crazy result.