Introducing Arbitrary Variables in Proofs

Stream: general

[Strategist _]

In a lot of math proofs, it's pretty standard and useful technique to introduce an arbitrary variable, argue in terms of that specific variable, then use the fact that it was arbitrary to generalize the argument to an entire set. It's not too hard to do that when the variable is defined in the theorem statement with a "forall", but sometimes it's useful to do it in proofs as an intermediate step, where the variable that's introduced wasn't a part of the final proof statement.

I've figured out that I can use let x : A := Classical.arbitrary x to get an arbitrary x of type A in a proof. Once I do that though, I find it's hard to perform usual operations you would do after introducing arbitrary variables.

Right now for example, I'm trying to construct a function using a value constructed from an arbitrary variable. As a minimal working example, in the code

import Mathlib

example : ∃ (f : ℕ → ℝ), f 1 = 0 := by
    let n : ℕ := Classical.arbitrary ℕ
    let real_value : ℝ := (n : ℝ) - 1
    sorry

I would love to somehow take real_value, which is a real number defined in terms of the arbitrary natural number n, and define a function f which returns the value of real_value for each n. (Obviously I could accomplish this much more simply by defining the function and computing the real_value in terms of the function argument, but this gives an idea for the kind of thing I'm trying to do).

Is there some way in Lean 4 to construct a function from an arbitrary variable like that? If manipulations like that are impossible, what's the use case for arbitrary variables, and is there some way to introduce and interact with arbitrary values like we do in math proofs?

[Jz Pan]

I think what you want is let f (n : ℕ) : ℝ := n - 1, or let f : ℕ → ℝ := fun n => n - 1. It means that "define a function from ℕ to ℝ which maps n to n - 1". The Classical.arbitrary ℕ means choose a random element in ℕ. It is not what you want.

[Ruben Van de Velde]

Or do you mean you want to turn "for all x, there exists a y" into a function that maps x to y? In that case, there's the choose tactic

[Patrick Massot]

I think we need concrete examples of your “pretty standard and useful technique” to help you. I strongly suspect there are better way to do those proofs, but maybe we’ll still find something useful to say.

[Patrick Massot]

We can already point out something that can be very confusing for beginners: Lean is much more suitable for explaining proofs than searching for proofs. What you describe sounds a lot like proof search exploration.

[Kevin Buzzard]

Right: if you want to "let x be arbitrary" that is typically because you are in the middle of deciding what you want to do. Once you've decided (e.g. you've decided that it will be helpful that x^2>=0 for x arbitrary) it is that that point that you can write the next line of Lean, which would be have helpful_thing : \forall x, x^2>=0 and then Lean will ask you to prove that too. But you can't write the line of Lean code until you've decided exactly what you're doing with this arbitrary x, i.e. you've gone from the "search" phase to the "explain" phase.

[Christian Merten]

Well you can write have not_so_helpful_thing (x : Sometype) : True which I do sometimes to explore what I can do.

[suhr]

You can also do:

have foo (x: Real) := by
    -- have: Whatever := whatever
    exact ()

Same idea.

[Robert Maxton]

As a side note, it sounds like your "standard technique is", I think, pretty much a statement of function extensionality -- some statement about functions is true iff it is true when evaluated at an arbitrary x. Where it isn't, it should be instead equivalent to using generalize to replace some subexpression with an arbitrary value.

[Strategist _]

Yeah that was the "simpler" method I was talking about, defining the output in terms of the function argument. That could work for specific situations, but there are other situations where I might want to do something other than define a function using the arbitrary variable. Thanks for the response though!

[Strategist _]

Ruben Van de Velde said:

Or do you mean you want to turn "for all x, there exists a y" into a function that maps x to y? In that case, there's the choose tactic

Sort of that, but I was hoping without an explicit "for all x, there exists a y" proposition, just using the arbitrary variable directly. I guess I could use a have statement to prove that type of statement though.

[Strategist _]

Patrick Massot said:

I think we need concrete examples of your “pretty standard and useful technique” to help you. I strongly suspect there are better way to do those proofs, but maybe we’ll still find something useful to say.

Ok, as one example, in the textbook "Partial Differential Equations" by Evans, during a proof of the existence of certain PDEs, they introduce an arbitrary natural number N
Screenshot 2025-04-08 at 2.23.36 PM.png.

They use this to construct a function that depends on that N, and then they use the fact that if you allow N to vary over all natural numbers, the functions constructed form a dense subset of the space of interest. This is the sort of thing I'm after.

[Strategist _]

Patrick Massot said:

We can already point out something that can be very confusing for beginners: Lean is much more suitable for explaining proofs than searching for proofs. What you describe sounds a lot like proof search exploration.

I'm actually just trying to reproduce some Evans PDE proofs in Lean, so I'm not exactly searching for proofs. It just seems like the proofs in standard math textbooks use a pretty different "language" than Lean does. I guess I'm searching for a convenient way to translate proofs, rather than searching for the proofs themselves.

[Strategist _]

Christian Merten said:

Well you can write have not_so_helpful_thing (x : Sometype) : True which I do sometimes to explore what I can do.

Sounds interesting. And does that let you treat the x as arbitrary somehow?

[Strategist _]

Robert Maxton said:

As a side note, it sounds like your "standard technique is", I think, pretty much a statement of function extensionality -- some statement about functions is true iff it is true when evaluated at an arbitrary x. Where it isn't, it should be instead equivalent to using generalize to replace some subexpression with an arbitrary value.

Interesting. I'll have to look into generalize a bit more.

[Strategist _]

Thanks for all the comments everyone!

[Kevin Buzzard]

Strategist _ said:

Patrick Massot said:

I think we need concrete examples of your “pretty standard and useful technique” to help you. I strongly suspect there are better way to do those proofs, but maybe we’ll still find something useful to say.

Ok, as one example, in the textbook "Partial Differential Equations" by Evans, during a proof of the existence of certain PDEs, they introduce an arbitrary natural number N
Screenshot 2025-04-08 at 2.23.36 PM.png.

They use this to construct a function that depends on that N, and then they use the fact that if you allow N to vary over all natural numbers, the functions constructed form a dense subset of the space of interest. This is the sort of thing I'm after.

So this is "have eqn29: \forall N, \forall v : (C^1 function), \forall d : Fin N -> (smooth functions), v = sum_{k=1}^N ... => \forall m >= N, integral from 0 to T ... = integral from 0 to T of ... := by intro everything, multiply (16) by d^k, sum and then integrate" in Lean.

[Kevin Buzzard]

The claim (29) is a new claim which you're pulling out of a hat so this is a have statement, and then everything before (29) in the para is either the statement or the proof of this new claim. Once you have stated eqn29 you start the new proof with by and then after the intro you have the N which you seek.

[Kevin Buzzard]

However rather than having intermediate haves in a proof, you might consider factoring these arguments out as sublemmas which can be proved and named beforehand; Lean would rather have two shorter proofs than one long one, because lean can get sluggish with very long proofs. If you take a look at files in mathlib they are often mostly comprised of many short proofs of easy things rather than a few very long ones and nothing else.

[Kevin Buzzard]

In particular let me stress that in contrast to the way it is written, you cannot be formally "fixing an integer N" because if N were fixed (e.g. N=37, that's a fixed integer) then you would not be able to vary it in the argument just before (31). Informally this is the way we write, but what we mean is not "for an arbitrary fixed N which the reader can choose", we mean "for all N".

[Strategist _]

Kevin Buzzard said:

In particular let me stress that in contrast to the way it is written, you cannot be formally "fixing an integer N" because if N were fixed (e.g. N=37, that's a fixed integer) then you would not be able to vary it in the argument just before (31). Informally this is the way we write, but what we mean is not "for an arbitrary fixed N which the reader can choose", we mean "for all N".

Yeah ok, that makes sense. Thanks.

Do you know what the actual use case for Classical.arbitrary and Nonempty.some would be then, if not introducing a weird alternate version of a forall statement?

[Aaron Liu]

They can be used to provide junk values when there's no other obvious choice.

[Aaron Liu]

For example, docs#Function.invFun

[Thomas Murrills]

I would actually support changing the name of Classical.arbitrary, especially since it lends itself easily to being used the wrong way by a mathematician who, understandably, would like to transcribe the sentence "let x be an arbitrary..." and might reach for let x := Classical.arbitrary ... after searching for "arbitrary".

I think forall free variable introduction (in one way or another) is the nearly-exclusive way mathematicians use the word "arbitrary"; I would even go so far as to say that most mathematicians probably do not even usually come in contact with global choice! "There is a fixed, canonical, globally-chosen element for every type" is not a thing mathematicians intuitively believe, and while it is "arbitrarily chosen" at the foundational level, this isn't really the level at which mathematicians work.

[Kevin Buzzard]

Yeah I'm not sure mathematicians want to use Classical.arbitrary. This is just a strong version of the axiom of choice. The way lean does the axiom of choice is that it has a function where you feed it a set (or more precisely a type) plus a proof that the set isn't empty and the function returns you an element of that set, and you're unable to prove anything about the element other than the fact that it's in the set. So asking "when do you use Classical.arbitrary " is a bit like asking "when do you use the axiom of choice".

[Patrick Massot]

Strategist _ said:

Ok, as one example, in the textbook "Partial Differential Equations" by Evans, during a proof of the existence of certain PDEs, they introduce an arbitrary natural number N

That’s another difference between ordinary maths writing and Lean. In Lean you announce what you will prove before proving it. We don’t suddenly start a different story arc without a warning. As Kevin explained, you can use the have tactic or, better, write more lemmas. It is expected that switching to this style takes some time. Something very productive you can do is to formalize this proof and then ask for help to make it idiomatic Lean. This will work if you don’t need to add to much preparatory material. Otherwise choose a different first target.

[Alok Singh]

Patrick Massot said:

Strategist _ said:

Ok, as one example, in the textbook "Partial Differential Equations" by Evans, during a proof of the existence of certain PDEs, they introduce an arbitrary natural number N

That’s another difference between ordinary maths writing and Lean. In Lean you announce what you will prove before proving it. We don’t suddenly start a different story arc without a warning. As Kevin explained, you can use the have tactic or, better, write more lemmas. It is expected that switching to this style takes some time. Something very productive you can do is to formalize this proof and then ask for help to make it idiomatic Lean. This will work if you don’t need to add to much preparatory material. Otherwise choose a different first target.

How _could_ you start a different arc suddenly? Are there affordances for it?

[Johan Commelin]

You have to announce where your arc is going:

"Here is a story about how some dwarves, a wizard and a hobbit go on an adventure to reclaim a treasure from a dragon."

Not:

"In a hole in the ground there lived a hobbit."

So I think the key difference is: in Lean you can change arcs, but not "suddenly".

[Jz Pan]

"We have a story about how some dwarves, a wizard and a hobbit go on an adventure to reclaim a treasure from a dragon."