The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Fred,

Fred Smith 
<fsmith1024 AT gmail.com>
 writes:

> 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:

In the line of Robert's reply, you may be interested in math-comp
subTypes, which provide extensive support for "irrelevant" sigma types,
as long as the property can be encoded as a bool. Thus, you can do:

Definition coord := { x | 0 < x <= 3 }.

and Coq will recognized coord automatically as a Subtype.

> Now I would like to prove:
>
>   Lemma coord_all_wish:
>     forall c:coord, c=c1 \/ c=c2 \/ c=c3.

I took the freedom to rewrite the lemma a bit:

Definition c1 : coord := exist _ 1 erefl.
Definition c2 : coord := exist _ 2 erefl.
Definition c3 : coord := exist _ 3 erefl.

Lemma coordP (c : coord) : c \in [:: c1; c2; c3].
Proof.
by rewrite -(mem_map val_inj); case: c => n /=; do 4!case: n => [//|n].
Qed.

Best regards,
Emilio

ps: I've put the code online in case you'd like to play with it (Chrome 
required)
    https://x80.org/collacoq/zebulayugu.coq