## 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 : α)

-- "invalid field notation, type is not of the form (C ...) where C is a constant"


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)

end point

variables (r s : point ℕ)



(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: May 15 2021 at 23:13 UTC