application at variables

Stream: new members

[Horatiu Cheval]

How can I apply terms to variables in defs (or create variables defined respectively to other variables, so to say), in the following sense?

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare variables for some of its arguments
variables {X : Type} (a₀ : X)
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type `ℕ → α`
def x := seq a₀

#check x
-- but it still has type ?M_1 → ℕ → ?M_1

[Kevin Buzzard]

That's because a variable is not actually a variable in the sense that it's defined once and for all, for the rest of the file -- a variable is just a trick whereby in your definition of x Lean thinks "crumbs -- what is a_0? Oh -- I see the user declared it as a variable, so I'll just stick "for all a_0 : X" in that def -- oh crumbs -- what is X? Oh that's a variable too, so I'll just stick "for all {X : Type}" in as well"

[Kevin Buzzard]

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare constants for some of its arguments
constants {X : Type} (a₀ : X)
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type `ℕ → α`
noncomputable def x := seq a₀

#check x -- x : ℕ → X

Note that there are no constants in mathlib -- you can easily prove false statements if you start throwing constants around. If you actually know what you want a_0 to be, then let it be that, and if you don't, then actually you might want it as a variable in Lean's sense.

[Kevin Buzzard]

If you really don't want variables then this is safer than using constants:

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare sorried definitions for some of its arguments
def X : Type := sorry
def a₀ : X := sorry
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type `ℕ → α`
def x := seq a₀

#check x -- x : ℕ → X

This time Lean emits a warning saying that you cheated, so proofs of false are known not to be trusted.

[Horatiu Cheval]

Thanks for the insight on how variables work! I knew defining constants is not recommended, plus it doesn't seem to represent the intention. Essentially, I defined some sorts of recursive sequences, having the initial value as argument, and then I wanted to have an initial point and a sequences starting at that point as variables, to reduce verbosity.

def seq : ∀ {α : Type} (a : α), ℕ → α := sorry

variables {X : Type} (a₀ : X)

local notation `x` := seq a₀

#check x

I guess this works best, but reserving the token x didn't seem the best idea.

[Eric Wieser]

parameters {X : Type} {a₀ : X} may work for you too