# 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
⊢ 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 (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`

:

```
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.

```
add_left_eq_zero
{{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