coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fred Smith <fsmith1024 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Proof irrelevant Specif?
- Date: Fri, 27 May 2016 19:24:11 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fsmith1024 AT gmail.com; spf=Pass smtp.mailfrom=fsmith1024 AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f49.google.com
- Ironport-phdr: 9a23:mMzZqxVUniHb9mOd/ninwq+Wx+nV8LGtZVwlr6E/grcLSJyIuqrYZheDt8tkgFKBZ4jH8fUM07OQ6PCxHzBRqs/c+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8yVP1QD3Wf1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDvABFD0D+6RDmXt+lvDD/t/Z9gXHAYeX5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=
Hi all,
I wanted to define a small range of numbers and thought this would be a clean solution:
Definition coord := { x | x>0 /\ x <= 3}.
Then I can define the 3 valid coordinates:
Definition c1 : coord := coord1.
refine (exist _ 1 _).
lia.
Defined.
Definition c2 : coord.
refine (exist _ 2 _).
lia.
Defined.
Definition c3 : coord.
refine (exist _ 3 _).
lia.
Defined.
Now I would like to prove:
Lemma coord_all_wish:
forall c:coord, c=c1 \/ c=c2 \/ c=c3.
Of course this statement is not true, because there are an infinite number of proofs that c1 satisfies the specification. What I really mean is proj1_sig c = proj1_sig c1, ...
I was originally viewing this coord type as morally equivalent to the inductive type c1 | c2 | c3 but with the added benefit that I could make 3 a parameter n and the design would scale. Now, I see that using this design makes "forall" arguments about coordinates quite painful because it precludes direct case analysis.
In summary I would like a type parametrized by n that when n is known has n distinguishable inhabitants.
Is Fin.t the answer to this question? Or does everything magically evaporate if I am willing to invoke proof irrelevance? Or is there some magic encoding I haven't thought of?
Thanks for any help.
-Fred
- [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Robbert Krebbers, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Emilio Jesús Gallego Arias, 05/28/2016
- Re: [Coq-Club] Proof irrelevant Specif?, Fred Smith, 05/28/2016
Archive powered by MHonArc 2.6.18.