help with syntax

Stream: new members

[Vasily Ilin]

Hi. I am trying to prove theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=. After

intro h,
rw add_comm at h,
rw add_comm t b at h,

my state is

t a b : mynat,
h : a + t = b + t
⊢ a = b

I have the function add_right_cancel (a t b : mynat) : a + t = b + t → a = b. I would expect that have p := add_right_cancel(h), would work, because add_right_cancel takes in a proof of a+t=b+t and outputs a proof of a=b. But have p := add_right_cancel(h), actually errors. Instead, have p := add_right_cancel a t b, is correct. I do not understand why. Can anyone explain what is going on please?

[Adam Topaz]

The a b and t are explicit. Add some underscores before h

[Kyle Miller]

The three mynat variables to the left of the colon in add_right_cancel are the first three arguments. Like Adam said, you can get Lean to infer them for you using add_right_cancel _ _ _ h

[Marcus Rossel]

Or you can tell Lean to infer the arguments automatically by using curly braces in the definition of add_right_cancel:

theorem add_right_cancel {a t b : mynat} : a + t = b + t → a = b := ...

-- in your proof:
have p := add_right_cancel h -- a & t & b are inferred from the information contained in h

[Vasily Ilin]

Another syntax question. Given state

n : mynat,
h : n + 1 = n
⊢ false

why does have p := eq_zero_of_add_right_eq_self n 1 h, not work? it gives the error:

26:10: error:
type mismatch at application
  eq_zero_of_add_right_eq_self n
term
  n
has type
  mynat : Type
but is expected to have type
  ?m_1 + ?m_2 = ?m_1 : Prop
state:
n : mynat,
h : n + 1 = n
⊢ false

[Johan Commelin]

It looks like eq_zero_of_add_right_eq_self takes n and 1 as implicit arguments. So you only have to feed it h. It figures out n and 1 from the structure of h.

[Vasily Ilin]

This is the definition of eq_zero_of_add_right_eq_self:

eq_zero_of_add_right_eq_self
  {a b : mynat} : a + b = a → b = 0

How do I figure out that it does not actually take a and b as arguments?

[Mario Carneiro]

the {} braces

[Mario Carneiro]

explicit arguments are written in ()

[Vasily Ilin]

And what about {{}} braces? E.g.

add_left_eq_zero
  {{a b : mynat}} (H : a + b = 0) : b = 0

[Mario Carneiro]

those are strict implicit arguments, which means that they are not inserted if you use the lemma unapplied, but they are if you apply some argument coming after it (here H). So add_left_eq_zero means @add_left_eq_zero but add_left_eq_zero H means @add_left_eq_zero _ _ H

[Mario Carneiro]

(the @ syntax makes all arguments explicit)

[Vasily Ilin]

Hmm, this is pretty confusing but thank you!

[Marcus Rossel]

You can probably ignore the double braces. I think they no longer even exist in Lean 4.

[Chris B]

Marcus Rossel said:

You can probably ignore the double braces. I think they no longer even exist in Lean 4.

I do remember hearing that, but they work as of nightly 8-28, and they appear in the docs. https://github.com/leanprover/lean4/blob/master/doc/expressions.md#implicit-arguments

[Marcus Rossel]

Oh interesting, Leo talked about removing them at Lean Together. But I guess they're important enough not to.