Synthesize abbrev

Stream: new members

[jsodd]

I think I've probably asked a similar (but not quite) question before, but why things I define using abbrev do not work well with typeclass synthesis? An example would be

variable {n : Type} [Fintype n]
abbrev V := EuclideanSpace ℝ n
#synth Inner ℝ V
#synth Inner ℝ (EuclideanSpace ℝ n)

The second command works well, the first doesn't...

[jsodd]

Is this a bug/not yet implemented or I'm wrong to expect it to work and there is a deeper reason not to?

[Eric Wieser]

Where did n come from?

[jsodd]

Sorry, added to the post.

[Etienne Marion]

Here V is not a euclidean space, but a function which to a type n associates a euclidean space.

[Edward van de Meent]

indeed; this works : #synth Inner ℝ (V (n := n))

[jsodd]

I don't know the technical details, but okay. Still, you see what I wanted to do? Just give EuclideanSpace ℝ n a name in order to not rewrite it a hundred times.

[jsodd]

Edward van de Meent said:

indeed; this works : #synth Inner ℝ (V (n := n))

This is nice to know, but it's virtually of the same length as EuclideanSpace ℝ n, and I wanted to curtail the notation.

[Edward van de Meent]

you could use the following trick:

set_option hygiene false in
notation "V" => EuclideanSpace ℝ n

i would advise you to namespace this notation, as it is quite context-sensitive

[Edward van de Meent]

as well as prone to collision

[Edward van de Meent]

you could alternatively (and possibly preferably) make the argument n to V explicit like so:

variable (n) in
abbrev V := EuclideanSpace ℝ n

[Edward van de Meent]

this way, V n will refer to the type you intend

[jsodd]

What does hygiene false mean?

[Eric Wieser]

(and then #synth Inner ℝ (V n))

[Edward van de Meent]

jsodd said:

What does hygiene false mean?

the primary issue why your earlier attempt failed was that n is not some constant, but a free variable introduced in the context. (particularly an implicit free variable)

Lean warns against hiding a statement containing such a free variable behind notation, because it can cause an issue; the notation will still be made available even when a surrounding section ends, but the context may no longer contain the same n. Worse even: it may contain a different, entirely unrelated n!
In this sense the notation is "unhygienic", as it can be contaminated by switching contexts. Setting the hygiene option to false makes lean accept this unhygienic notation.

[jsodd]

So the problem is that Lean doesn't interpret n in abbrev V := ... as the n from variable {n : Type} [Fintype n]? Instead, n in abbrev V := ... is a free variable? I see how this can be problematic

[Edward van de Meent]

well... once you defined V as an abbrev, the n in it is no longer free but bound, but you seem to understand the issue.

[Edward van de Meent]

the n from variable {n : Type} [Fintype n] is free though.

[Kevin Buzzard]

variable n does not mean "make a new variable and call it n". It means "do nothing, but the next time someone mentions n in a statement, silently add a "for all n" at the beginning"

[Edward van de Meent]

lets add an asterisk* for the behaviour relating to theorem (and lemma in mathlib), but yes, that is usually effectively what happens