The Coq mailing list

[Vincent Aravantinos <vincent.aravantinos AT yahoo.fr>]

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