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
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.
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.
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
Last updated: Sep 28 2023 at 11:01 UTC