Stream: Coq users

Topic: Proofs with forall and exists.


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC