Zulip Chat Archive

Stream: new members

Topic: help with syntax

Vasily Ilin (Aug 30 2021 at 23:05):

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 (Aug 30 2021 at 23:07):

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

Kyle Miller (Aug 30 2021 at 23:08):

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 (Aug 31 2021 at 06:25):

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 (Sep 03 2021 at 06:36):

Another syntax question. Given state

n : mynat,
h : n + 1 = n

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
has type
  mynat : Type
but is expected to have type
  ?m_1 + ?m_2 = ?m_1 : Prop
n : mynat,
h : n + 1 = n

Johan Commelin (Sep 03 2021 at 06:39):

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 (Sep 03 2021 at 06:41):

This is the definition of 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 (Sep 03 2021 at 06:41):

the {} braces

Mario Carneiro (Sep 03 2021 at 06:41):

explicit arguments are written in ()

Vasily Ilin (Sep 03 2021 at 06:45):

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

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

Mario Carneiro (Sep 03 2021 at 06:46):

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 (Sep 03 2021 at 06:47):

(the @ syntax makes all arguments explicit)

Vasily Ilin (Sep 03 2021 at 18:02):

Hmm, this is pretty confusing but thank you!

Marcus Rossel (Sep 03 2021 at 18:54):

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

Chris B (Sep 03 2021 at 19:11):

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 (Sep 04 2021 at 06:36):

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

Last updated: Dec 20 2023 at 11:08 UTC