About proving the existence of specific function.

[jaewooklee93]

Every time I encountered the goal looks like

exists (f: nat -> nat), P f.

I felt somewhat tired. If I was so lucky that I could define a simple and concrete Fixpoint function, I could easily clear the goal with something like this.

Coq > exists (fun n => if ble_nat n m then 1 else 0).

However, in many cases, it is quite difficult to make such a concrete definition, even though I believe that such function should exist. For example, even if I am successful in proving this,

forall (x: nat), exists (y: nat), P x y.

I don't know how to derive the following.

exists (f: nat -> nat), forall (x: nat), P x (f x).

I think if this is a course in mathematics, I can freely derive the existence of such function from the above assumption. Well, of course, there is one subtle point. Since I didn't prove the uniqueness of y for each x, a function f satisfying that condition is not unique and we have to make a choice among possibilities. So I believe that this is related to the axiom of countable choice, and I'm curious about whether we can use such principle in Coq or not. Or, is there any good trick to prove the existence of function?

Addition: When I thought about it a little more, I realized that we don't need to use axiom of choice here, since nat is well-ordered. There is a canonical choice of f, which has a value of f x to be the smallest possible y for each x. Yet, I don't know how to express this idea in Coq.

[gilhur]

If you are a constructivist, you have to define such a function directly, which makes your life hard. Since I am not a constructivist in order to make my life easier, I can freely assume classical axioms and axiom of choice, etc. If you download the coq source and look at the directory "theories/Logic/", you can find many interesting classical axioms and lemmas.

For instance, I do the following.

Require Import IndefiniteDescription. Check functional_choice.

[jaewooklee93]

That's exactly what I look for! Thank you. Now I feel like I can utilize almost every proof technique I used in paper mathematics.

Jaewook Lee

[jaewooklee93]

When I wrote this issue, I thought that I could prove this theorem without using AC or excluded middle

Theorem well_ordering_principle: forall P,
(exists n, P n) ->
exists n, (P n) /\ (forall m, P m -> n <= m).
Proof.

However, now I realized that I cannot. Because, in order to compute the smallest natural number satisfying P, I have to know how I can decide whether P n or ~ P n for each n.

Suppose that well_ordering_principle has a constructive proof, then if I choose P as P 0 := Riemann Hypothesis is True. P 1 := True.

Since this predicate P satisfies the condition (exists n=1, P n), I must be able to decide whether the smallest natural number satisfying P is 0 or 1. But if I can do it, I am at least able to prove or disprove Riemann Hypothesis.

Thus, I think I have no way to avoid using excluded middle in this case.