# Zulip Chat Archive

## Stream: new members

### Topic: Dot notation

#### Christopher Hoskin (Mar 21 2021 at 09:51):

I can use the dot notation to reference lemmas about a specific natural number e.g. `3`

or a variable `n`

of type ℕ. However, the dot notation doesn't appear to work for referencing an additive group lemma for a variable of type α with the hypothesis `[add_group α] `

. Should I be surprised by this?

(As an aside, I seem to have to specifically cast `3`

as `ℕ`

rather than that being the default in this situation.)

```
import algebra.group.basic
universe u
variables {α : Type u}
#check (3:ℕ).one_mul
variable (n:ℕ)
#check n.eq_zero_or_pos
variables [add_group α] (c : α)
#check add_left_neg c
-- "invalid field notation, type is not of the form (C ...) where C is a constant"
#check c.add_left_neg
```

Christopher

#### Benjamin Davidson (Mar 21 2021 at 10:06):

I'm no expert but I'm pretty sure this is normal. Some lemmas are designed to work with dot notation; others aren't. `add_left_neg`

does not strike me as one of the ones that would work.

#### Kevin Buzzard (Mar 21 2021 at 11:05):

The way dot notation works is that if `a : foo x Y z`

then `a.bar`

means `foo.bar a`

. So n.succ works if n : nat because nat.succ exists. If you have alpha : Type then alpha.blah will not see any hypotheses on alpha like add_group, my guess is that it will just look for Type.blah .

#### Eric Wieser (Mar 21 2021 at 11:14):

It doesn't even look for that; from the error message "type is not of the form (C ...) where C is a constant". Here, `C`

is `α`

which is not a constant (unlike `nat`

or `foo`

which would be constants)

#### Christopher Hoskin (Mar 21 2021 at 17:05):

Yet something like this appears to work:

```
structure point (α : Type*) :=
mk :: (x : α) (y : α)
namespace point
def add (p q : point ℕ) := mk (p.x + q.x) (p.y + q.y)
lemma add_comm (p q : point ℕ) : p.add q = q.add p := sorry
end point
variables (r s : point ℕ)
#check r.add
#check r.add_comm s
```

(Based on an example of a `point`

structure in Section 9.1 of 'Theorem proving in lean' .

#### Eric Wieser (Mar 21 2021 at 17:07):

Yes, that works because 1) the type of `r`

is `point`

which is the prefix of `point.add`

, and 2) `point`

is a constant, not a variable

#### Bryan Gin-ge Chen (Mar 21 2021 at 17:13):

Dot notation also requires the parameter of type `point`

to be explicit (using round parentheses, not curly or square ones).

#### Bryan Gin-ge Chen (Mar 21 2021 at 17:15):

The key words are "first non-implicit argument" in the TPiL section you linked to above.

#### Christopher Hoskin (Mar 21 2021 at 17:37):

So, the group example can be made to work something like this:

```
import algebra.group.basic
universe u
variables {G : Type u} [group G]
namespace group
lemma mul_left_inv' (a: G) : a⁻¹ * a = 1 :=
group.mul_left_inv a
end group
constant g : group G
#check g.mul_left_inv'
variable h : G
#check group.mul_left_inv' h
```

My grasp of type theory is too weak to understand the distinction between `constant g : group G`

and `variable h : G`

here.

#### Eric Wieser (Mar 21 2021 at 17:44):

`constant`

is a distraction here, that would work just the same with `variable`

#### Christopher Hoskin (Mar 21 2021 at 17:47):

If I change it to `variable g : group G`

then `#check g.mul_left_inv'`

gives me:

```
failed to synthesize type class instance for
G : Type u,
_inst_1 g : group G
⊢ group (group G)
```

#### Eric Wieser (Mar 21 2021 at 17:53):

Oh, odd. Either way, you basically never want to use `constant`

, so while an interesting quirk this probably isn't going to be relevant to you

#### Kevin Buzzard (Mar 21 2021 at 18:19):

The (huge) difference between `g : group G`

and `h : G`

is that the first one means "g is a multiplication, an inverse, an identity, and proofs of three or more axioms" and the second one means "h is an element of the set G, or the type G, or however you want to think of it".

#### Christopher Hoskin (Mar 21 2021 at 18:37):

Thanks - I did wonder if that was the case, but I was surprised to see `group.mul_left_inv' g : g⁻¹ * g = 1`

in the Infoview for `#check g.mul_left_inv'`

- it seems to be accepting `g`

as an element of the group, rather than as the group axioms.

Last updated: Dec 20 2023 at 11:08 UTC