Automatically synthesize a fact in instance argument

Stream: new members

[Aymeric Fromherz]

Hi! I've recently been going through the Lean 4 tutorial, and trying to experiment a bit with it.
In particular, I have (a slightly more complicated version of) the following code, where I'm trying to use refinement types:

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

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

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

def test : pos :=  ⟨ 1, by simp [isPos] ⟩

Ideally, I'd like to write test as simply def test : pos := 1, and let the ofNat pos n typeclass instance automatically introduce the coercion. However, in the current state, Lean does not seem to be able to synthesize the isPos argument automatically.
Is there a way to tell Lean 4 to always try to apply the simplifier during synthesis for this specific argument?

Thanks!

[Tomas Skrivan]

You can apply simplifier to synthesize an argument like this:

abbrev isPos (x:Int) := x > 0  -- marked it as abbrev for simp to see through it

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 ⟩

but it this case it is not doing what you are after, not sure why.

[Tomas Skrivan]

When you call the instance explicitly, it works:

#check posOfNat 1
#check posOfNat 10
#check_failure posOfNat 0

[Aymeric Fromherz]

Thanks for the answer! the := by simp syntax was what I was looking for. However, this indeed does not seem to interact well with instance synthesis. Could it be that the by simp is executed prior to resolving n?

[Tomas Skrivan]

In that case calling the instance directly would not work too, no?

[Aymeric Fromherz]

Mmh, possibly, but I do not know enough about how Lean 4 solves metavariables. The difference i see is that, when calling the instance directly, there is no metavariable for n, while if Lean is trying to solve isPos ?m_n by simp before ?m_n is resolved, this could lead to issues

[Tomas Skrivan]

Could be, I do not understand these things too much either.

[Kyle Miller]

My guess is that instance search doesn't attempt running the tactic for (p: isPos n := by simp).

Another 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

[Kyle Miller]

Maybe it's worth asking on #lean4 about this and whether @Tomas Skrivan's version is expected to work.

[Aymeric Fromherz]

Did Lean 3 use to handle this? Thanks for the advice, will do