walker (Apr 29 2022 at 07:09): 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: Oct 13 2024 at 01:02 UTC