Define function from ∀x, ∃y?

Stream: new members

[Chris M]

Suppose I have a theorem of the form:

constant P : X → Y → Prop
theorem existenceresult : ∀x:X, ∃y:Y, P x y := sorry

How can I define a function f: X → Y on the basis of existenceresult, such that ∀x:X, P x f(x)?
I've looked at the reference manual on the axiom of choice, but I can't actually see how to do this using Lean's choice.

[Kevin Buzzard]

You can use the choose tactic: https://leanprover-community.github.io/mathlib_docs/tactics.html#choose

[Chris M]

Is there a way to do it without tactics? (I a tactic is just a command for Lean to search for a proof that doesn't contain tactics, isn't it?)

[Kevin Buzzard]

There is, you can use classical.some to define the function, and classical.some_spec to prove it has the property you want.

[Kevin Buzzard]

What you posted doesn't make sense right now, you have a theorem, but its conclusion isn't a Proposition.

[Johan Commelin]

Also see classical.choice

[Chris M]

Yeah sorry, typo.

[Kevin Buzzard]

variables (X Y : Type) (P : X → Y → Prop) (hP : ∀x:X, ∃y:Y, P x y)

include P hP

noncomputable def f : X → Y := λ x, classical.some (hP x)

[Kevin Buzzard]

People around here get edgy about constants and axioms

[Chris M]

Oh, why is that ?

[Kevin Buzzard]

variables {X Y : Type} (P : X → Y → Prop) (hP : ∀x:X, ∃y:Y, P x y)

include P hP

noncomputable def f : X → Y := λ x, classical.some (hP x)

example : ∀ x : X, P x (f P hP x) := λ x, classical.some_spec (hP x)

[Kevin Buzzard]

Mathlib doesn't have any and we don't really see why we need any.

[Kevin Buzzard]

But note that I just had to write f P hP instead of f :-)

[Kevin Buzzard]

I think once someone told me that they were problematic in some other way, maybe something doesn't work very well with them, but I was a beginner at the time and probably didn't understand what they were talking about

[Chris M]

Why is f P hP x well formed? f takes an X but P : X \to Y \to Prop, and P can't take hP either right?

[Kevin Buzzard]

I changed the brackets round X and Y to be the squiggly "Lean will fill these in using unification" brackets

[Kevin Buzzard]

section

parameters (X Y : Type) (P : X → Y → Prop) (hP : ∀x:X, ∃y:Y, P x y)

noncomputable def f : X → Y := λ x, classical.some (hP x)

example : ∀ x : X, P x (f x) := λ x, classical.some_spec (hP x)

end

Here's another way which now looks beautiful

[Kevin Buzzard]

section

parameters (X Y : Type) (P : X → Y → Prop) (hP : ∀x:X, ∃y:Y, P x y)

noncomputable def f : X → Y := λ x, classical.some (hP x)

theorem foo : ∀ x : X, P x (f x) := λ x, classical.some_spec (hP x)

#check foo -- foo : ∀ (x : X), P x (f x)

end

#check foo
/-
foo : ∀ (X Y : Type) (P : X → Y → Prop) (hP : ∀ (x : X), ∃ (y : Y), P x y)
  (x : X), P x (f X Y P hP x)
-/

Inside the section the parameters are suppressed.

[Kevin Buzzard]

I think there's some kind of "real Lean programmers don't use constants" thing going on, and I don't really know why, but I try and stick to the general principle of no constants and no axioms

[Jannis Limperg]

constant is just another name for axiom, isn't it? So when you write constant P : ..., you're postulating the existence of such a P rather than stating a result about any such P (if they exist). The former is dangerous since you could postulate something that contradicts Lean's other axioms.

[Chris M]

The last couple of files make sense to me, thanks! I'm surprised though, after having just read about {} in the docs, that f P hP x works. I would have guessed that since X,Y are in {} brackets, but P and hP are not. I would have guessed that f X Y x would work, but it gives me "can't synthesize placeholder"

[Chris M]

@Jannis Limperg, is that different from assuming a variable that contradicts one of Lean's axioms?

[Kevin Buzzard]

You're talking about before I switched to parameters? {} means "just leave this out completely, I'll guess what it is".

[Kevin Buzzard]

So when Lean sees f P hP x it reads f _ _ P hP x and then has to guess what the missing things are, and this is easy: for things to typecheck, if you look at the type of P, the missing things must be X and Y

[Kevin Buzzard]

The risk of using a constant is that you might be able to prove false outright. With a variable you can't, you can only prove "forall (something), false".

[Kevin Buzzard]

and if you can't actually feed in an example of the something, which you can't if Lean is consistent, then you can't prove false.

[Chris M]

yeah, but since P and hP are NOT in {} but in (), I would guess that f would implicitly take the type f: {X Y :Type} \to (X\to Y), so that P and hP can't be arguments.

[Chris M]

Oh that makes sense.

[Chris M]

Ok tomorrow I'll look at how to do it with classical.choice. Going to bed now, thanks a lot for the help!

[Jannis Limperg]

Chris M said:

Jannis Limperg, is that different from assuming a variable that contradicts one of Lean's axioms?

Yes! Consider this example:

section

variable FALSE : false

lemma everything_is_true {α : Prop} : α := false.rec _ FALSE

end

#check everything_is_true
-- `everything_is_true` says: Under the assumption that we have something of
-- type `false`, we can prove anything.

lemma zero_eq_one : 0 = 1 :=
begin
  apply everything_is_true,
  -- To apply everything_is_true, we need to exhibit something of type `false`,
  -- but thankfully there's no such thing.
  sorry
end


constant FALSE : false

lemma everything_is_true' {α : Prop} : α := false.rec _ FALSE
-- `everything_is_true'` says: we can prove anything, no extra assumptions
-- needed. So now we're inconsistent.

lemma zero_eq_one' : 0 = 1 :=
begin
  apply everything_is_true'
end

[Kenny Lau]

Kevin Buzzard said:

People around here get edgy about constants and axioms

Kevin Buzzard said:

I think once someone told me that they were problematic in some other way, maybe something doesn't work very well with them, but I was a beginner at the time and probably didn't understand what they were talking about

Kevin Buzzard said:

I think there's some kind of "real Lean programmers don't use constants" thing going on, and I don't really know why, but I try and stick to the general principle of no constants and no axioms

Variables can be substituted. If you prove that "for any variable G, a group structure on G induces a semigroup structure on G", then you can use this "theorem" to deduce a semigroup structure on units \Z; but if you have a constant G, a constant group structure on G, and a theorem that G has a semigroup structure, then you're in effect introducing to the world of Lean a new constant G that exists per fiat, and you cannot substitute it with units \Z

[Chris M]

Is it actually possible to define a function from ∀x, ∃y using classical.choice, instead of classical.some? I haven't heard of the some axiom in math, so it must be Lean-specific, and in math one would use choice for this.

[Andrew Ashworth]

choice is a derived theorem from some more fundamental axioms assumed in Lean's classical library

[Andrew Ashworth]

theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
  ∃ (f : Π x, β x), ∀ x, r x (f x) :=
⟨_, λ x, some_spec (h x)⟩

[Andrew Ashworth]

er, I mean, the axiom of choice you are familiar with is derived from classical.choice. classical.some is similarly

[Andrew Ashworth]

if I remember correctly, old versions of Lean didn't even use classical.choice, it was all derived from

[Andrew Ashworth]

axiom strong_indefinite_description {a : Type u} (p : a → Prop) (h : nonempty a) : { x : a // (∃ y : a, p y) → p x}

[Andrew Ashworth]

then at some point it got simplified because it was confusing people

[Chris M]

My first impression is that the problem with this is that we don't actually strictly speaking know that strong_indefinite_description is not stronger than choice? If we want to rigorously know that the classical axioms actually correspond to the classical axioms, then we should build classical from the same axioms that are used in mathematics?

[Andrew Ashworth]

what is mathematics?

[Andrew Ashworth]

ZFC set theory?

[Andrew Ashworth]

but Lean's foundations are in the type theory, specifically the calculus of inductive constructions

[Andrew Ashworth]

applying the axiom of choice as defined in set theory

[Andrew Ashworth]

doesn't really make much sense

[Chris M]

I see

[Mario Carneiro]

In lean, it is easy to prove that classical.choice and strong_indefinite_description are equivalent in strength

[Mario Carneiro]

(actually the proof that strong_indefinite_description follows from choice is not entirely obvious since it requires Diaconescu's proof of EM first)

[Mario Carneiro]

As for whether they are equivalent to the axiom known as the "axiom of choice" in ZFC, this depends on some details of the foundational setup

[Mario Carneiro]

lean's choice is actually closer to Hilbert's epsilon operator, or a variant of AC called "global choice", because it posits a single class function that chooses elements simultaneously from every nonempty set

[Mario Carneiro]

The usual formulation of AC in ZFC puts the function that does the choosing behind an existential

[Mario Carneiro]

However, it is well known that this is a conservative extension; the general process is known as Skolemization

[Mario Carneiro]

In lean you actually can't prove classical.choice from the theorem axiom_of_choice mentioned above because of this

[Kevin Buzzard]

Chris M said:

Is it actually possible to define a function from ∀x, ∃y using classical.choice, instead of classical.some? I haven't heard of the some axiom in math, so it must be Lean-specific, and in math one would use choice for this.

@Chris M here are two interesting uses of some in Lean. For the first one, consider the proof that if $X\to Y$ is a surjection then there's an injection $Y\to X$ which is a one-sided inverse. In Lean this construction is immediate using some -- you pick y : Y and then observe that we have a non-empty type of x : X to choose from and use some to pick one. In ZFC you would use choice for this. Here choice and some seem to be about the same.

For the second one, consider the proof that if $X\to Y$ is a bijection then there's a bijection $Y\to X$ which is a two-sided inverse. In Lean this construction is also made using some because even though we have a proof that the preimage contains exactly one term, the assertion has type Prop, whereas we need to move into the Type universe if we actually want the element. This whole some business can be thought of as a method of getting from Lean's proof-irrelevant Prop universe to the universe Type where data is remembered. The way Prop is modelled internally in Lean is that you can make a proof that the pre-image has exactly one element, but because this is in Prop the statement is just recorded by Lean as being proved, there is no information in the system as to what that element is and in particular there is no way of extracting it. This is a foundational issue where set theory and type theory seem to me to differ. Here when people talk about choice they often just mean the ability to move from Prop to Type. some is somehow the basic example of this.

[Chris M]

very interesting. I am actually surprised though that Prop doesn't record that data, i.e. that propositional extentionality is used as an axiom. To put it a different way, I'm surprised that Choice is considered a classical notion. It seems to me that, according to the constructivist notion of $\exists$, we only prove it once we have an example. Hence as soon as we've proven it, we do in fact have aconstructed example somewhere. Hence, shouldn't we be able to choose that example, without leaving constructivist logic? This argument basically makes me think that $\exists$ should just be a tuple like $\Sigma$, i.e. that $\exists$ should just be syntactic sugar for, but otherwise identical to, $\Sigma$, and that propositional extentionality shouldn't hold. I'm curious where people disagree with my view.

[Mario Carneiro]

This is the approach taken in more hardcore constructivist foundations like HoTT. There, there is no difference between Prop and Type

[Mario Carneiro]

although propositional extensionality still holds in HoTT, for a different reason

[Mario Carneiro]

In HoTT there is a version of choice that is trivial, and then there is another version that is equivalent to the mathematician's axiom of choice, which requires inserting propositional truncations to make the exists have this "forgetting" behavior

[Mario Carneiro]

In lean, the reason we care about having Prop around is so that we can forget about witnesses

[Mario Carneiro]

This has to do with the semantics behind VM computation and "proof erasure"

[Mario Carneiro]

proofs are generally not good for computation so it is nice to be able to forget about them in programs. Reflecting this back into the logic entails that proofs have to be irrelevant, and exists cannot record the witness that proved it

[Mario Carneiro]

If you want a proof relevant version of exists, you can use \Sigma, but it is a conscious decision you have to make. This gives you a little extra bit of expressive power

[Chris M]

Mario Carneiro said:

proofs are generally not good for computation so it is nice to be able to forget about them in programs. Reflecting this back into the logic entails that proofs have to be irrelevant, and exists cannot record the witness that proved it

What do you mean by "proofs are generally not good for computation"? In what sense?

[Andrew Ashworth]

They represent pieces of code that have to be evaluated when the code is run; it can lead to large amounts of overhead and inefficiency

[Mario Carneiro]

If I have a vector of length 5, say [1,2,3,4,5], and want to turn it into a vector of length 3 + 2, I can do so by applying a theorem that says that 3 + 2 = 5. But there is no need to evaluate this proof (which boils down to refl 5) to get the resulting vector, because in memory the resulting vector has the exact same representation [1,2,3,4,5] so it is a no-op in the computer

[Mario Carneiro]

If equality is proof irrelevant, then this "cast" operation is always a no-op, and the computer can just skip the proof, even though it was provided and may very well be computable

[Mario Carneiro]

Here the proof is being used to ensure that the program does not go wrong, but it is not needed for the program to actually get to the end result

[Chris M]

My impression is that a proof NEVER has to be evaluated. So it seems to me that if Lean just has a general rule that says "never evaluate proofs", then there is no danger of inefficiency. I might have some kind of misconception though.

[Reid Barton]

What's your notion of "proof", then, for which they never have to be evaluated?
It sounds like you are suggesting that \exists effectively shouldn't exist; but its purpose is precisely to be usable in this "proof" context.

[Chris M]

My notion of proof is basically, it's a program that could in principle be evaluated, but we are not actually interested in doing so, we are only interested in type checking it to see if it's correct. Once we know it's correct, we know the theorem is true, and that's all there is to it. No need to actually run the proof. Is that wrong?

[Kevin Buzzard]

I'm not an expert in this area, but it sounds to me like this is right. Proofs are typechecked and then instantly forgotten

[Reid Barton]

Okay but if you want to extract a function from "∀x, ∃y", then you are actually interested in evaluating the "proof" after all, right?

[Reid Barton]

I mean, if you want to be able to evaluate the function, you'd better be able to figure out what y was used to construct the existential and that means evaluating the term of type ∃y, ... (we can call it a proof or not).

[Reid Barton]

So, in Lean, we do have some things called "proofs" that are never evaluated, namely terms whose type is a proposition, and ∃y, P y is a proposition. That means that from h : ∀x, ∃y, P ythere is no way to extract the data of "the y for a given x" (or any other data for that matter) and so you need a nonconstructive axiom if you want to obtain a function. Other systems make different choices.

[Chris M]

Reid Barton said:

Okay but if you want to extract a function from "∀x, ∃y", then you are actually interested in evaluating the "proof" after all, right?

Well, it seems to me that I want to extract a function but again not actually evaluate that function. I just want to use it to construct further proofs, all of which won't ever be evaluated.

[Reid Barton]

Then that's precisely what choice is for

[Reid Barton]

But if we're saying "we know that there exists such a function, but we have no access to the function", then I don't see how it could be called constructive

[Kevin Buzzard]

Chris M said:

Well, it seems to me that I want to extract a function but again not actually evaluate that function. I just want to use it to construct further proofs, all of which won't ever be evaluated.

import tactic

example (X : Type) (P : X → Prop) (h : ∃ x : X, P x) :
  ∃ x : X, P x ∧ P x :=
begin
  cases h with x hx, -- x is out!
/-
1 goal
X : Type,
P : X → Prop,
x : X,
hx : P x
⊢ ∃ (x : X), P x ∧ P x
-/
  use x,
  tauto,
end

[Kevin Buzzard]

You can get to the existential witness without choice if your goal is a proposition.

[Kevin Buzzard]

import tactic

example (X : Type) (P : X → Prop) (h : ∃ x : X, P x) :
  { x : X | P x ∧ P x} :=
begin
  cases h with x hx,
/-
induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
-/
  sorry
end

but not if your goal is data.

[Sebastien Gouezel]

I was surprised to see how well Lean can compute, so I just wanted to share this with you. In #2398, I introduce compositions of an integer, i.e., ways to decompose n as a sum of positive integers, as

structure composition (n : ℕ) :=
(blocks_pnat : list ℕ+)
(blocks_pnat_sum : (blocks_pnat.map (λ n : ℕ+, (n : ℕ))).sum = n)

In the course of the file, I register an explicit equiv between composition n and fin (n-1), to get that the cardinality of composition n is 2^(n-1). After this, Lean can check numerical stuff on compositions! For instance, if you want to check the number of compositions of 9 with length 4 in which the first term is 2, you can ask

#eval fintype.card {s : composition 9 // ∃ (h : s.length = 4),
  (list.nth_le s.blocks 3 (by { rw [composition.blocks_length, h], norm_num })) = 2}

It works, and answers 15 (I didn't check this is the right answer, but I hope we can trust Lean :). What surprises me is that there is a proof in the definition of the set, needed to show that the set makes sense, but this is not a problem at all for the computation.