The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

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