The Coq mailing list

[Nathanaël Courant <nathanael.courant AT ens.fr>]

Hi all,

I have a complicated inductive proposition:

Inductive red: X -> Prop :=
| case_1 : ...
...
| case_N : ...


I also have some proposition P : X -> Prop.
I have goals of the form:

forall x, red x -> P x -> Q x.

which I prove by induction on red x. I can prove that if red x and P x, 
then P y is true for all y appearing as recursive calls to red in the 
constructor of red x.

However, each time I want to prove such a result, I have to prove P is 
true for each of the recursive calls, and I want to avoid such code 
duplication.



One possibility would be to create a custom induction principle, but 
since red is very complicated, this would amount to duplicate a lot of 
code, which I would rather avoid.



Another possibility I tried was to switch to open recursion:

Inductive red_ (rec : X -> Prop) : X -> Prop :=
...
Inductive red := red_intro : forall x, red_ red x -> red x.

Then I proved:

forall H x, red_ (fun x => red x /\ H x) x -> P x ->
            red_ (fun x => red x /\ H x /\ P x) x

and

forall x, red_ (fun x => red x /\ P x /\ Q x) x -> Q x

which, combined, allow to prove forall x, red x -> P x -> Q x, and the 
deduplication of the work is done thanks to the first proof, which does 
not depend on Q.


This works well on that simple case, however, the case I have is a bit 
more complicated: P is not of type X -> Prop, but of type X -> A -> 
Prop, for some other type A.

I still have that if red x and P x a are true, then P y b are true for 
all y appearing as recursive calls to red in the constructor of red x 
(i.e. as calls to rec in red_ rec x), but it is for some b that depends 
on the recursive call and the constructor used.
Thus, I can still prove the same thing as in the open recursion case, 
but with the proposition (fun x => exists a, P x a). However, I want to 
be able to use the correct value of a for the recursive calls in the 
second part of the proof when I want to prove Q, and I can't, because it 
is hidden away by the exists, since I have to prove:

forall x, red_ (fun x => red x /\ (exists a, P x a) /\ Q x) x -> Q x.



Finally, I tried to create a function to extract the values of a needed 
from the constructor used to prove red x, but I'm getting a universe 
inconsistency, since red is a Prop.



Does anyone have an idea about how to extend recursion schemes for 
induction propositions, while proving some property is preserved as 
above, without getting a lot of code duplication in the way?


Thanks,
Nathanaël