The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Hi,

This kind of problem is usually solved by finding the right 
generalization of your goal.

In your case, probably somethink like
   forall x, P x -> x=C1 ->  ....
(be sure that what you want to prove is true by induction)
then use an induction on P.
then use discriminate in order to get rid of the useless cases (this is 
what inversion does except it uses pattern-matching, not induction.

If the same pattern occurs several times, it may be useful to derive 
once for all a specialized elimination lemma that will look like

forall Q, Q C1 D1 -> (forall d, Q C1 d -> Q C1 (D2 d))
   -> forall y:P C1, Q C1 y

then the tactic elim using gives you a way to apply this lemma in each 
particular cases.

Hope it helps, if not you should send the complete example.

Christine Paulin

Vincent Aravantinos a écrit :
> Hi,
>
> I am a beginner in coq and I can't manage to prove a certain goal;
> I'll try to get a minimal example out of my problem.
>
> Say I have an inductive set S:
>
> Inductive S : Set := C1 | C2 | C3 | ...
>
> and an inductive predicate P over S:
>
> Inductive P : S -> Prop :=
> |D1 : P C1
> |D2 : P C1 -> P C1
> |D3 : ... -> P C2 (or P C3 or P C4, ... anything but C1)
> |... : ... -> P C2 (idem)
>
> My goal has the form:
>
> ... P C1 ...
>
> To prove it, I need (first) an inversion on (P C1) in order to get
> rid of cases D3,D4,... I can now focus on cases D1 and D2.
>
> But it appears that I need now an induction on (P C1). The problem
> is that the induction tactic will only destruct P, not (P C1).
> This leads me to have to prove my goal over D3,D4,... ie. I lose
> the benefit of my previous inversion.
>
> It seems I should do both at once: inversion AND induction.
>
> Is that right ? (Is my example understandable ?)
> How can I deal with this ?
>
>
> Thanks in advance,
> Vincent Aravantinos
>
> --------------------------------------------------------
> 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