Dot notation

Stream: new members

[Christopher Hoskin]

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]

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]

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]

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]

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]

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]

Dot notation also requires the parameter of type point to be explicit (using round parentheses, not curly or square ones).

[Bryan Gin-ge Chen]

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

[Christopher Hoskin]

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]

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

[Christopher Hoskin]

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]

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]

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]

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.