turn "exists and is unique" into a function

Stream: new members

[Pierre Guillot]

Hi!

I'm new to Lean, and also to Zulip (and I just accidentally deleted a draft of this message by messing with the "preview" button!), and this is my first question.

I've been wandering about how you would turn a statement of the form "for all x of type T, there exists y such that P x y, and this y is unique" into a function on T, without using the axiom of choice. I have absolutely nothing against using the axiom of choice, but this is for simplicity, and also, in ZF you wouldn't need it here: you would say that the set of (x,y) with P(x,y) forms the graph of a function, so well, you have a function.

Here is a concrete example, with the existence of a minimum for nonempty sets of integers. This will be an opportunity for me to ask other questions, and you can also help me with any oddities in the code (it does work, at least!) By the way, I have made no attempt at checking whether this was already in mathlib, this is for fun.

import data.nat.basic
import tactic

-- Definition of the minimum of a set of integers.
def is_minimum (A : set ℕ) (n : ℕ ) := n ∈ A ∧ ∀ a ∈ A, n ≤ a


/- We want to show that any nonempty set of integers has a minimum.
First we prove the following artificial version, allowing us to use
induction. -/
lemma min_exists' (A : set ℕ) (n:ℕ) (h : ∃ k:ℕ , k ∈ A ∧ k ≤ n) :
    ∃ m : ℕ, is_minimum A m
:= begin
---- By induction on n.
induction n with n IH,
---- Case n=0. First show k=0.
cases h with k hk,
have hzero : k=0, from nat.eq_zero_of_le_zero hk.2,
-- and then 0 is the minimum of course
use 0,
simp [is_minimum],
rw ← hzero,
exact hk.1,
---- Inductive step.
-- two cases according as k can actually be found ≤ n
by_cases alt : ∃ k' : ℕ , k' ∈ A ∧ k' ≤ n,
-- in the first case, k' ≤ n, just use inductive hypothesis
cases alt with k' hk',
have hyp_for_IH : ∃ x : ℕ, x ∈ A ∧ x ≤ n, --indeed, with x = k'.
use k', exact hk',
-- now conclude in this case:
exact IH hyp_for_IH,
-- remains to treat the alternative case, and first prove
-- that this is just k = n+1.
cases h with k hk, -- show that k ≤ n leads to contradiction
have kgtn : k > n, by_contradiction absurd_h,
have klen := le_of_not_gt absurd_h,
apply alt, use k, exact ⟨ hk.1, klen ⟩, -- OK so k > n
have kgesuccn := nat.succ_le_of_lt kgtn,
have ksuccn : k = n.succ, by linarith, -- good, k=n+1.
-- Now n+1 is the minimum of A.
use k,
simp [is_minimum], split, exact hk.1,
intro a,
by_contradiction absurd_h, apply alt, use a,
push_neg at absurd_h,
split, exact absurd_h.1,
apply nat.le_of_lt_succ,
rw ← ksuccn,
exact absurd_h.2,
end

-- Every nonempty set of integers has a minimum:
theorem min_exists (A : set ℕ) {n : ℕ} (h : n ∈ A):
    ∃m : ℕ, is_minimum A m
:= begin
have : ∃k : ℕ, k ∈ A ∧ k ≤ n,
use n,
exact ⟨ h, le_refl n⟩,
-- so we may just use the lemma:
exact min_exists' A n this,
end

-- How to turn this into a function?
noncomputable def the_minimum_of (A : set ℕ) {n : ℕ} (h : n ∈ A): ℕ :=
    classical.some (min_exists A h)

So my questions are :

1. (Mostly) Can you change the very end, and avoid the axiom of choice?
2. I don't really know how to do my imports. On this example, it seems that if I dont use import data.nat.basic then I cannot use... the "use" keyword! how weird! Any comment? And tactic is for linarith at least, which makes more sense.
3. I thought Lean would understand (h : ∃ k ∈ A, k ≤ n) instead of my h in the lemma, but surprisingly, it doesn't work (try it, it's hard to describe... sorry...)

Thanks for reading!
Pierre

[Pierre Guillot]

PS I did not bother including a proof that the minimum is unique, sorry!

[Eric Rodriguez]

I think you need the axiom of choice in Lean

[Heather Macbeth]

@Pierre Guillot Welcome! Looks like you've come a long way all by yourself :)

[Heather Macbeth]

Pierre Guillot said:

2. I don't really know how to do my imports. On this example, it seems that if I dont use import data.nat.basic then I cannot use... the "use" keyword! how weird! Any comment? And tactic is for linarith at least, which makes more sense.

Here's where use is defined: docs#tactic.interactive.use. So indeed it's not in Lean core. Maybe it's enough to import the file where that is defined,

import tactic.interactive

[Heather Macbeth]

Pierre Guillot said:

3. I thought Lean would understand (h : ∃ k ∈ A, k ≤ n) instead of my h in the lemma, but surprisingly, it doesn't work (try it, it's hard to describe... sorry...)

Indeed, h : ∃ k ∈ A, k ≤ n and ∃ k:ℕ , k ∈ A ∧ k ≤ n are slightly different things. The former is shorthand for ∃ k : ℕ, ∃ H : k ∈ A, k ≤ n. So when you do cases h with k hk on the first version you get a natural k and a hypothesis hk : ∃ H : k ∈ A, k ≤ n, whereas when you run it on the second version you get a natural k and a hypothesis hk : k ∈ A ∧ k ≤ n.

To extract out the second piece, k ≤ n, you would use hk.some_spec for the first one, whereas hk.2 (as you did) for the second one.

[Mario Carneiro]

actually you can use hk.snd for the first one, using docs#Exists.snd

[Heather Macbeth]

But not hk.2 :)

[Heather Macbeth]

And regarding your first question, I'm not sure, but my general impression is that in Lean's axiomatics the "axiom of choice" is not exactly the same as the one you'd use in ZFC.

[Eric Wieser]

For this particular case where the function is to a natural, I imagine you can use docs#nat.find

[Anatole Dedecker]

The fact that you can define functions that way in ZFC is a consequence of the fact that a function is literally a set of pairs which satisfies this existence and uniqueness property. But this is not the case in Lean, and you always have to use choice if you want to extract data from an existential, even if you can prove uniqueness (slight caveat : subsingleton elimination)

[Eric Wieser]

You don't need choice if the codomain is finite docs#fintype.choose

[Anatole Dedecker]

But that is because of the computable nature of docs#fintype, right ? I think we couldn't do that with docs#finite for example

[Matt Diamond]

if you define your set as a finset instead of a set, you can use docs#finset.choose

[Matt Diamond]

also, you can use docs#set.nonempty and docs#finset.nonempty to represent non-emptiness

[Kevin Buzzard]

@Pierre Guillot the example which shows that Lean's axiom of choice is not the same as the set theory one is that if in lean you have a proof of "there exists a unique x such that..." then you still need the type theory axiom of choice to get x. Mathematics in lean gets divides up into two "universes" -- the stuff in Prop (theorem statements and proofs) and the stuff in Type (definitions like the real numbers or $\pi$ or the definition of a group structure) and the axiom of choice is basically the way to get from the Prop universe to the Type universe. For example to show the product of nonempty types is nonempty you start with a proof that each of the factors are nonempty, apply Lean's AC to get a term in each factor, and then take the product of these terms.

[Eric Wieser]

That's a bit misleading, docs#prod.nonempty doesn't need or use AC

[Eric Wieser]

Precisely because there is no need to get to the type universe in that example

[Pierre Guillot]

Thanks everyone for your answers!

It's fascinating that the axiom of choice plays a different role in type theory/Lean compared to ZF. I was already happy to use it in ZF, and in Lean it appears even more compelling.

An extra question for anyone reading: I have used by_cases, but did not have to specify that I was going to use the Law of the Excluded Middle, so I guess this happened automatically? and then somewhere there's a flag that the proof is classical? (I don't worry about using the LEM either, I'm just curious).

Other things:

@Heather Macbeth : thanks to you I have found that, when you have (h : ∃k ∈ A, k ≤ n) (for example), then rcases h with ⟨k, h1, h2 ⟩ worked really well.

@Eric Wieser : thanks for pointing out nat.find. It looks like it will only work when k ∈ Ais "decidable" (not that I really understand what this means precisely).

Oh and should I mark this question as answered? how do I do that?

[Eric Wieser]

and then somewhere there's a flag that the proof is classical?

Yes, you can use #print axioms my_lemma to see that flag

[Eric Wieser]

It looks like it will only work when k ∈ Ais "decidable" (not that I really understand what this means precisely).

It means that there is an algorithm to decide whether k is in the set A. If A is the set of rationals within the reals, then there is no such algorithm for all k.

[Pierre Guillot]

and then somewhere there's a flag that the proof is classical?

Yes, you can use #print axioms my_lemma to see that flag

Interesting, for the lemma I get "propext, classical.choice, quot.sound". The LEM is seen as a consequence of AC, somehow?

[Eric Wieser]

Yes, docs#classical.em is proved in terms of docs#classical.choice

[Eric Wieser]

https://github.com/leanprover-community/lean/blob/22b09be35ef66aece11e6e8f5d114f42b064259b/library/init/classical.lean#L25-L70

[Pierre Guillot]

Thanks! I am amazed by the efficiency of the community in answering questions!

[Ruben Van de Velde]

Huh, I didn't realize the proof of EM was so involved