Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Proof irrelevant Specif?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proof irrelevant Specif?


Chronological Thread 
  • 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










Archive powered by MHonArc 2.6.18.

Top of Page