The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hi,

Yes, it is the answer,

Thank you very much and greetings,

Marko Malikoviæ

Pierre Casteran reèe:
> 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
>>
>
> --------------------------------------------------------
> 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
>