coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marko Malikovi� <marko AT ffri.hr>
- To: pierre.casteran AT labri.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Subset of natural numbers
- Date: Wed, 5 Sep 2007 09:38:57 +0200 (CEST)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
>
- [Coq-Club] Subset of natural numbers, Marko Malikoviæ
- Re: [Coq-Club] Subset of natural numbers,
Pierre Casteran
- Re: [Coq-Club] Subset of natural numbers, Marko Malikoviæ
- Re: [Coq-Club] Subset of natural numbers,
roconnor
- Re: [Coq-Club] Subset of natural numbers,
Marko Malikoviæ
- Re: [Coq-Club] Subset of natural numbers, roconnor
- Re: [Coq-Club] Subset of natural numbers,
Marko Malikoviæ
- Re: [Coq-Club] Subset of natural numbers,
Pierre Casteran
Archive powered by MhonArc 2.6.16.