## Stream: Coq users

### Topic: Proofs with forall and exists.

#### walker (Apr 29 2022 at 07:09):

In some complicated proof, I end up trying to prove the following theorem, but I don't know how to do it:

``````Theorem exists_forall: forall (T: Type), exists (v: T), forall (d: T), d = v.
``````

The challenge is that the `exists (v: T)` appear before the `forall (d: T)` part so eexists does not work.
Edit: I was able to prove it throught contradition in some of the other assuptions but I still wonder if this statement as it is:
A- is correct.
B- is provable

#### Patrick Nicodemus (Apr 29 2022 at 07:19):

If a type T is empty, then it will be impossible to construct some v : T, unless Coq's whole logic is inconsistent.
There is an empty type built into the standard library, so this should be a counterexample.

#### walker (Apr 29 2022 at 07:22):

Well, that is actually true, but we can simplify the problem as follows:

``````Theorem exists_forall:  exists (v: nat), forall (d: nat), d = v.
``````

This feels correct but it doesn't look provable because we need v to be equal to d, but d is not yet introduced.

#### James Wood (Apr 29 2022 at 07:25):

It says that there is one natural number that all other natural numbers are equal to. This is only going to hold of one-inhabitant (up to propositional equality) types like `unit`.

Last updated: Sep 28 2023 at 11:01 UTC