The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

From a practical point of view, it is easy to prove that your 
definitions are equivalent. I don't know if that
is the kind of answer you expect.

Regards,
Pierre


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.

Hint Constructors in_subset in_subset'.

Lemma L1 : forall n, in_subset n -> in_subset' n.
Proof.
destruct 1.
assert (x=1 \/ x=2 \/ x = 3 \/ x=4 \/ x=5).
Require Import Omega.
omega.
decompose [or] H0 .
rewrite H1;auto.
rewrite H2;auto.
 rewrite H1;auto.
 rewrite H2;auto.
 rewrite H2;auto.
Qed.

Lemma L2 :  forall n, in_subset' n -> in_subset n.
Proof.
intros n Hn;case Hn;auto with arith.
Qed.

Marko Malikoviæ a écrit :
> 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?
>
> Thank you very much and greetings,
>
> Marko Malikoviæ
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>