The Coq mailing list

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

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.''
>