The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 5 Sep 2007, Marko Malikovi? wrote:

> Greetings,
>
> I need to work with small subset of natural numbers, from 1 to 5.
> Normally, I can define it in this way:
>
> Inductive in_subset : nat -> Prop := in_subset_def : forall x : nat,
> 1<=x<=5 -> in_subset x.
>
> But, for my needs is more appropriate to have definition like this:
>
> Inductive in_subset : nat -> Prop :=
> | C1 : in_subset 1
> | C2 : in_subset 2
> | C3 : in_subset 3
> | C4 : in_subset 4
> | C5 : in_subset 5.
>
> Is something theoretically (from view of Cic) wrong with this kind of
> definitions?

There is nothing wrong with your second definition, (although personally, 
inductive families always bother me a bit).  However I should point out 
that you can have the best of both worlds.

Your second definition produces the inductive principle:

forall P : nat -> Prop,
       P 1 -> P 2 -> P 3 -> P 4 -> P 5 -> forall n : nat, in_subset n -> P n.

You can write this theorem for your first definition without much 
difficulty.

Lemma in_subset_ind' : forall P : nat -> Prop,
       P 1 -> P 2 -> P 3 -> P 4 -> P 5 -> forall n : nat, in_subset n -> P n.
Proof.
intros P P1 P2 P3 P4 P5 n H.
destruct H as [[|[|[|[|[|[|n]]]]]] [H0 H1]];
 solve [assumption|elimtype False; omega].
Qed.

Then this new inductive priciple can be used on demand using the
`` elim H using in_subset_ind' ''
(or `` induction H using in_subset_ind' '' if you had a truely inductive 
definition).

Goal forall n, in_subset n -> in_subset (6-n).
intros n H.
elim H using in_subset_ind';
simpl; repeat constructor.
Qed.

You can write your own pseduo-constructors.

Definition c1 : in_subset 1.
repeat constructor.
Qed.

Definition c2 : in_subset 2.
repeat constructor.
Qed.

...

The result is that you can use your old definition on almost all the same 
ways you would use your new definition.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''