More problems with placeholder context

Stream: new members

[Bolton Bailey]

After seeing the comments on my post here yesterday, I took the advice of Reid Barton and eliminated constant from my file. I then experienced another problem where it was impossible to succinctly express what I want and I don't understand why the program is unable to synthesize placeholder

import data.polynomial.basic

noncomputable theory

universes u

variables {F : Type u}
variables [field F]

def my_poly : polynomial F := polynomial.X

variables {f11 f12 f13 f21 f22 f23 : F}

def p1 : polynomial F := (f11 * f12 * f13) • my_poly
def p2 : polynomial F := (f21 * f22 * f23) • my_poly

lemma my_prop : (f11 = f21) -> (f12 = f22) -> (f13 = f23) -> (p1 = p2)
:= sorry

Here the program complains about p2. It works fine if I replace with (@p1 F _ f21 f22 f23) = (@p2 F _ f11 f12 f13) but this is very verbose and I don't want to have to write all this out every time p1 or p2 occurs in my longer lemmas. It seems like this is exactly the problem implicit arguments are meant to help with. I don't understand why the type checker is confused about the implicit arguments to p2. If I run #check p2 I get

p2 : Π {F : Type u} [_inst_1 : field F] {f21 f22 f23 : F}, polynomial F

Which suggests to me that it knows the arguments should be F, _inst_1, f21, f22, f23. So what's the problem?

[Kevin Buzzard]

p2 also has type Π {A : Type u} [B : field A] {C D E : A}, polynomial A.

[Kevin Buzzard]

Those two types are alpha equivalent and hence syntactically equal. Lean doesn't have a clue which inputs to use.

[Kevin Buzzard]

{} means "use the type of the things around me to figure me out". Lean doesn't have enough information to solve the jigsaw puzzle.

[Kevin Buzzard]

p2 says "if you give me a field F and three elements, I'll produce a polynomial. Oh, you put all the inputs in {}s so I am expected to figure them out by looking at the types of stuff. Wait -- I don't even know the type of p1. I give in."

[Bolton Bailey]

Ok, that's a very helpful perspective, thank you. It still seems to me that, since f21 f22 f23 are the F type variables (or perhaps I should say the names of the F type variables) that are used in the definition of p2 itself, it should be possible for the program to guess that I want those same variable (names) to be the variable (names) that p2 is called with whenever it appears without explicit arguments. Is there a way to command the compiler to look to synthesize placeholders from the variables that appeared in the definition?

[Yakov Pechersky]

This is what parameter is for, for a section, as far as I understand. But you can't ensure that a name is always used in the same way. One of the replacement rules is that names are replaceable (is that beta reduction? I don't remember). What would you expect would happen if two terms were provided that have the same name?

[Bolton Bailey]

@Yakov Pechersky Yep, this parameters keyword thing is exactly what I was looking for and works perfectly - thanks for your help

import data.polynomial.basic

noncomputable theory

section

universes u

parameter {F : Type u}
parameter [field F]

def my_poly : polynomial F := polynomial.X


parameters {f11 f12 f13 f21 f22 f23 : F}

def p1 : polynomial F := (f11 * f12 * f13) • my_poly
def p2 : polynomial F := (f21 * f22 * f23) • my_poly

#check p2

lemma my_prop : (f11 = f21) -> (f12 = f22) -> (f13 = f23) -> p1 = p2
:= sorry

end

[Mario Carneiro]

Yakov Pechersky said:

This is what parameter is for, for a section, as far as I understand. But you can't ensure that a name is always used in the same way. One of the replacement rules is that names are replaceable (is that beta reduction? I don't remember). What would you expect would happen if two terms were provided that have the same name?

The word you are looking for is alpha renaming