coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marko Malikovi� <marko AT ffri.hr>
- To: roconnor AT theorem.ca
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Subset of natural numbers
- Date: Wed, 5 Sep 2007 10:00:30 +0200 (CEST)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Thank you also,
but I need just to inductive "build up" subgoals like this:
Coq < Inductive in_subset : nat -> Prop :=
Coq < | C1 : in_subset 1
Coq < | C2 : in_subset 2
Coq < | C3 : in_subset 3
Coq < | C4 : in_subset 4
Coq < | C5 : in_subset 5.
in_subset is defined
in_subset_ind is defined
Coq <
Coq < Goal forall x:nat, in_subset x -> x<6.
1 subgoal
============================
forall x : nat, in_subset x -> x < 6
Unnamed_thm < intros x H;induction H.
5 subgoals
============================
1 < 6
subgoal 2 is:
2 < 6
subgoal 3 is:
3 < 6
subgoal 4 is:
4 < 6
subgoal 5 is:
5 < 6
With "normally" definition I obtain subgoals which need more required
tactics.
Greetings,
Marko Malikoviæ
roconnor AT theorem.ca
reèe:
> 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.''
>
- [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.