Zulip Chat Archive

Stream: new members

Topic: Dot notation


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 .

view this post on Zulip 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)

view this post on Zulip 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' .

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Mar 21 2021 at 17:44):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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