Implicit proof (proposition) argument in partial function

Stream: general

[Jineon Baek]

I would like to define a partial function like the following.

import tactic.basic

def f (a b : ℕ) {h : a < b} : ℕ := a + b

example (a b : ℕ) (h : a < b) : f a b = f a b := sorry

So the function f is basically addition, but it is restricted so that the second argument is always greater than one.

I didn't want to put the hypothesis a < b every time I invoke the function f a b, so I made the hypothesis implicit.
But then the example line gives me the following (rather confusing for me) error.

don't know how to synthesize placeholder
context:
a b : ℕ,
h : a < b
⊢ a < b

To the best of my knowledge the value of h : a < b does not affect f a b h at all because all proofs of a proposition is considered equal in lean, and I believe it can be also shown by rfl. The seemingly obvious placeholder message makes me confused further. Your insight on why is it happening, and what can we do to make it work would be much appreciated here.

[Julian Berman]

I'm no expert, but I think from what I've seen, fundamentally the recommendation is to not try to define partial functions like that. Instead define a total function which returns garbage outside the range you care about, but when you prove things about your function, now you can include the hypothesis that the value is in the range where it makes sense.

E.g. in Lean you can indeed divide by zero, and get some garbage value, but no mathematically meaningful proof will do so (with the caveat that sometimes things indeed do do so because the garbage value sometimes conveniently simplifies proofs!)

[Kyle Miller]

Implicit arguments are solved for using unification. The "don't know how to synthesize placeholder" error means that there was nothing in the expression that led Lean to fill in a value for h using unification alone.

It's true that all proofs of propositions are equal to each other, but Lean won't try to synthesize a proof for you for implicit arguments.

You can tell Lean the name of a tactic to use, though, to try to synthesize a proof for optional arguments. For example, if you expect h to always be a local variable, you can use tactic.assumption.

import tactic.basic

def f (a b : ℕ) (h : a < b . tactic.assumption) : ℕ := a + b

example (a b : ℕ) (h : a < b) : f a b = f a b h := sorry
-- notice that we can still pass `h` ourselves if we want

Another choice is obviously to use the tidy tactic (or whatever it is that obviously is set to do).

[Junyan Xu]

I wonder if people have considered using d : Π (i j : ι) (h : c.rel i j . tactic.omega), self.X i ⟶ self.X j to define docs#homological_complex; what would be the advantage/disadvantage compared to the current approach? (tactic#omega is probably too powerful for this purpose.)

[Jineon Baek]

Thank you for all of your input. Both directions (not using partial function / using tactic synthesis) help practically. @Kyle Miller May I ask what is exactly meant for 'unification'? My guess is that it is a process of deriving what is equal to what from the assumption that two things are equal, like from f a 3 = f 4 bwe infer a=4 and 3=b. Also, I wonder if such tactic synthesis is also possible in lean4 - I'll defer this question to lean4 if needed.