notation capturing type information

Stream: mathlib4

[Jireh Loreaux]

How can I capture type information for pieces involved in notation? For example, let's say I have some foo : Type → Type and some bar {β : Type} (α : Type) (b : β) (f : foo α) : β. For elaboration reasons in my actual example, α has to be explicit despite f. How can I create notation like this:

notation "my_bar_notation" (f : foo α) b => bar α b f

That is, I want to look at the type of f, see that it has type foo α for some α, and then use α in the definition of the notation.

[Jireh Loreaux]

Note, I know this is possible with metaprogramming, I'm just hoping we have a nice shortcut syntax that works for notation.

[Adam Topaz]

Can you just replace alpha with an underscore in the notation decl, or does that not elaborate properly?

[Jireh Loreaux]

I get an "expected =>" as soon as I put in the parentheses, but also, in my actual example, I have something more like foo : Type → Type → Type and I want (f : foo α α).

[Adam Topaz]

What I meant is something like this:

def foo : Type → Type := sorry
def bar {β : Type} (α  : Type) (b : β) (f : foo α) : β := sorry

notation "my_bar_notation" f b => bar _ b f

[Jireh Loreaux]

That causes the same elaboration problems as before because bar needs α to be explicit. For context, in my actual use case, bar α b is a bundled morphism between foo α and β. So when you write bar _ b f Lean can't seem to infer the hole.

To un- #xy, in #5750 I define:

class CFCCoreClass (R : Type _) {A : Type _} [CommSemiring R] [StarRing R] [TopologicalSpace R]
    [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A]
    [Algebra R A] (a : A) where
  toStarAlgHom : C(spectrum R a, R) →⋆ₐ[R] A
  hom_continuous : Continuous toStarAlgHom
  hom_map_X : toStarAlgHom (toContinuousMapOnAlgHom (spectrum R a) X) = a

def cfc₁ (R : Type _) {A : Type _} [CommSemiring R] [StarRing R] [TopologicalSpace R]
    [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A]
    [Algebra R A] (a : A) [CFCCoreClass R a] : C(spectrum R a, R) →⋆ₐ[R] A :=
  CFCCoreClass.toStarAlgHom

Here, if f : C(spectrum R a, R) then Lean needs R to be explicit in cfc₁ in order to elaborate cfc₁ R a f. But really, the type of f itself contains the R datum (and a too in fact), so it would be nice to just provide some notation so that Lean can look at that the type of f and fill in these values.

[Mario Carneiro]

can you give a MWE?

[Mario Carneiro]

(more precisely, does the foo/bar MWE above actually exhibit the issue you describe?)

[Adam Topaz]

Would the following solution work?

def foo : Type → Type → Type := sorry
def bar {β : Type} (α α' : Type) (b : β) (f : foo α α') : β := sorry
abbrev bar' {β : Type} (α : Type) (b : β) (f : foo α α) : β := bar α α b f

notation "my_bar_notation" f b => bar' _ b f

[Mario Carneiro]

there is also type_of% for getting the type of a value, although I can't tell if that is sufficient for your use case

[Jireh Loreaux]

I need to put kids to bed, but I'll come back to this in a bit.

[Jireh Loreaux]

@Mario Carneiro okay, I spent a bunch of time trying to minimize the problem. Here's what I came up with: docs#Module.Dual.instFunLikeDual breaks things

import Mathlib.Algebra.Module.LinearMap

-- these are the imports of `Mathlib.LinearAlgebra.Dual`
import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.LinearAlgebra.Projection
import Mathlib.LinearAlgebra.SesquilinearForm
import Mathlib.RingTheory.Finiteness
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic

section MyDual -- copied from `Mathlib.LinearAlgebra.Dual`

namespace Module

universe u v

variable (R : Type u) (M : Type v)
variable [CommSemiring R] [AddCommMonoid M] [Module R M]

@[reducible]
def Dual :=
  M →ₗ[R] R

-- this instance breaks `bar'` below.
instance : FunLike (Dual R M) M fun _ => R :=
  inferInstanceAs (FunLike (M →ₗ[R] R) M fun _ => R)

end Module

end MyDual

variable (R A : Type _) [Semiring R] [Semiring A] [Module R A]

def foo : R →* A := 1
def bar : R →ₗ[R] A := 0

variable {R}

def foo' : R →* A := 1
def bar' : R →ₗ[R] A := 0

example (f : R) : foo R A f = foo R A f := rfl -- works
example (f : R) : foo' A f =  foo R A f := rfl -- works

example (f : R) : bar R A f = bar R A f := rfl -- works
example (f : R) : bar' A f =  bar R A f := sorry

[Mario Carneiro]

the instance is very strange, you can prove it using inferInstance alone because Dual is reducible

[Mario Carneiro]

but there also seems to be a bug here, adding the bad instance shouldn't prevent the real one from being found

[Jireh Loreaux]

Yeah, it's a bit weird because adding

@[reducible] def SynHom (α : Type u) (β : Type v) [Monoid α] [Monoid β] := α →* β

instance notBad [Monoid α] [Monoid β] : FunLike (SynHom α β) α fun _ => β := inferInstance

doesn't break foo'.

[Jireh Loreaux]

Also, I think there may lie lurking other instances of this bug. Disabling that FunLike instance locally doesn't fix the elaboration problems for my StarAlgHom case.

[Jireh Loreaux]

Out of my depth here, but could the problem be that something uses a whnfR where it should be using whnfI?

[Jireh Loreaux]

Can we have a linter that catches whenever an instance is declared but it could have been filled with inferInstance?

[Matthew Ballard]

inferInstanceAs would be nice too but probably very hard

[Alex J. Best]

Don't we sometimes add these short circuit instances on purpose though? Such a linter would be easy to write but I'm not sure if there would be too many false positives?

[Scott Morrison]

We do have lots of short circuit instances, but it would be great if they were documented, and a linter would help with this.

[Scott Morrison]

Also, the linter could check for and allow := inferInstance as the definition.

[Jireh Loreaux]

I have no experience writing a linter, but since Alex says it's easy, maybe I'll have a go at writing it. Which existing linter might be a good one to read and learn from?

[Alex J. Best]

It might be easiest to start from scratch. The most similar in spirit is one of the simp linters, the one that says "simp can prove this", we really want a version that says "inferInstance" can prove this, docs#Std.Tactic.Lint.simpNF. But the simp linter is quite a bit more complicated than we need here.

I think you just need to check if the declaration is a def or a theorem, and check that it is an instance, and if so get the type, make a new MVarId representing a term of that type and call introsN to get a new metavariable representing the goal of the typeclass in the context of the hypotheses, then try to apply the term inferInstance (docs#Lean.MVarId.apply, making sure you are in the withContext of that MVarId) and see that you get no goals left (i.e. apply returns an empty list).

I have to run now, but will happily say more detail later if that is helpful.

[Jireh Loreaux]

Thanks for the outline! I'll give it a try.

[Kyle Miller]

@Jireh Loreaux In case it helps, here's a command that can tell you if an instance is superfluous:

import Lean

open Lean Meta Elab

elab "#is_superfluous " id:ident : command => withoutModifyingEnv <| Command.runTermElabM fun _ => do
  let name ← resolveGlobalConstNoOverloadWithInfo id

  let some decl := (← getEnv).find? name | throwError "(internal error) no such declaration"
  let type := decl.type
  unless (← isClass? type).isSome do throwError "{name} does not give a class instance"
  modifyEnv Meta.instanceExtension.pushScope
  try
    let s ← (instanceExtension.getState (← getEnv)).erase name
    modifyEnv fun env => instanceExtension.modifyState env fun _ => s
    let inst? ← trySynthInstance type
    if let .some inst := inst? then
      logWarning m!"{name} is superfluous. Independently provided by{indentD inst}"
    else
      logInfo m!"{name} is not superfluous"
  finally
    modifyEnv Meta.instanceExtension.popScope

#is_superfluous instAddNat
-- instAddNat is not superfluous

instance myGreatInstance : Add Nat := inferInstance

#is_superfluous myGreatInstance
-- myGreatInstance is superfluous. Independently provided by instAddNat

instance anotherGreatInstance (x y : Nat) : Decidable (x = y) := inferInstance

#is_superfluous anotherGreatInstance
/-
anotherGreatInstance is superfluous. Independently provided by
  fun x y ↦ instDecidableEqNat x y
-/

[Kyle Miller]

The key is (1) temporarily removing the instance under question and (2) using trySynthInstance on the type of the declaration (which is able to handle foralls, so no need use introN, and it's basically the core to inferInstance)