Running tactics during instance synthesis

Stream: lean4

[Aymeric Fromherz]

Hi! I'm trying to define a typeclass instance where one of the arguments should be resolved by tactic during synthesis. After some help from others on the new members stream, we have the following minimal example:

class foo (n : Nat) where
  x : Nat

instance foo_insts (n : Nat) (p : n = n := by rfl) : foo n where
  x := n

#check foo_insts 1 -- ok
#check foo.x 1 -- failed to synthesize instance

Is this code supposed to work in Lean 4? If not, is there a workaround to allow the synthesis of instance arguments through tactics? Thanks in advance!

[Kyle Miller]

For context, an application is using simp to automatically satisfy a subtype property:

abbrev isPos (x:Int) := x > 0

def pos : Type := { x : Int // isPos x}

instance posOfNat (n:Nat) (p: isPos n := by simp) : OfNat pos n where
  ofNat := ⟨ Int.ofNat n, p ⟩

example := posOfNat 1 -- ok
example : pos := 1 -- failed to synthesize instance OfNat pos 1

[Henrik Böving]

The issue is not with proofs per se here but due to default arguments:

class Foo (n : Nat) where
  x : Nat
  y : Nat

instance {n : Nat} (y : Nat := 1) : Foo n where
  x := n
  y := y

set_option trace.Meta.synthInstance true in
#check Foo.x (1 : Nat) -- failed to synthesize instance

also fails with:

[Meta.synthInstance] ❌ Foo 1
  [Meta.synthInstance] new goal Foo 1
    [Meta.synthInstance.instances] #[@instFoo]
  [Meta.synthInstance] ✅ apply @instFoo to Foo 1
    [Meta.synthInstance.tryResolve] ✅ Foo 1 ≟ Foo 1
    [Meta.synthInstance] skip answer containing metavariables instFoo ?m.53

so it seems that if we want to support this we need general support for default arguments in type class synthesis

[Tom]

Somewhat unrelated, is there any documentation on what exactly abbrev can do? I've seen it in simple type assignments but here it's used as an abbreviation of a function.
What's the difference between it and an inline function?
Is it just a macro that expands to the exact expression on the left? I can't do "go to definition" on it in VSCode.

[Henrik Böving]

abbrev is essentially equivalent to

abbrev X := y
==
@[reducible]
def X := y

which is relevant for instance search because it will look through reducible definitions so what we for example often do in the compiler and elaborator is

abbrev MyMonadM := ReaderT Context StateReftT State BaseMonadM

and since we are using abbrev here instance search automagically finds the monad instance.

[Tom]

And what are the exact remantics of reducible? I’ve not found that in the docs either.

[James Gallicchio]

I believe it mainly determines which definitions get unfolded during typeclass resolution

[Henrik Böving]

In theory any elaborator can do whatever it wants based on reducability of a function, it might for example also be relevant for certain tactics. But by far the most common use case is type classes.

[Tom]

So take the trivial recursive example of Nat addition.

I could use it as a normal computation but to eg use it in a proof/prop would I need to mark it as reducible?

[Henrik Böving]

No not at all you can do proofs about any lean program (although using partial limits this ability drastically but that's another story I can go into if you want) However it might be that there are certain tactics that operate in a special way on reducible vs non reducible definitions. I have no example at hand though, all of the ones I know don't really care afaik.

[Tom]

Thanks, Henrik