About automatic insertion of variable as parameter.

Stream: general

[Hyunwoo Lee]

I often use the variable inside the section. And if you define something after declaration of variable, the variables are automatically inserted as parameter for such definition.

def test_fun (x : T × T × T) := true

section A
variable {T : Type} (x y z : T)

def t : T × T × T := (x,y,z)
#check t -- t has type {T : Type} → T → T → T → T × T × T
#check_failure test_fun t
#check test_fun (t x y z)

end A

I fully understand that it must work in this way if I use t outside the section A. But why I always need to add additional parameter even in the same section? I want to use t as (x,y,z).

In the other proof assistant like Rocq, it is possible to use t as type T in the same section it's defined. The parameters are automatically filled as definition without any hint from the context. I expect the similar behavior in Lean.

Is there other method to make it work as what I expect?

Here's the list of possible answer I find and the reason why it's not enough.

1. Making the variable implicit => It doesn't allow me to use t as (x,y,z). It just make type of t as {T : Type} → {x y z : T} → T × T × T, which makes the situation worse. Parameters couldn't be infereed in the most of case.
2. Using Notation instead of definition => I think it's not a good idea in the sense of engineering. It make the code difficult to maintain or develop further.

[Kim Morrison]

Hyunwoo Lee said:

1. I think it's not a good idea in the sense of engineering. It make the code difficult to maintain or develop further.

Essentially, we have decided in Lean that providing something like Rocq's parameters would also fall under this category.

[Thomas Murrills]

Would a top-level let (like variable) be a good idea for this sort of thing? It seems that this would fit with Lean’s approach to variable management (i.e. it fundamentally works by modifying the context, and, like variable, could be reverted in each actual definition to produce a self-contained type/term at the end of the day).

(I’m not familiar with Rocq’s parameters, so I don’t know if this would be essentially the same thing or not.)

[Snir Broshi]

#new members > Is it possible to have genuine abbreviations?