The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

Dear Coq'ers

I'm using an Inductive type like (greatly simplified...I have more cases)

Inductive XP :Set :=
    | void : XP
    | slash: XP -> XP -> XP
    | qualif: XP -> XQ -> XP
with XQ :Set :=
    | false : XQ
    | and : XQ -> XQ -> XQ  
    | leq : XP -> XP -> XQ
.

The default induction scheme is not adapted, and using 

Scheme IIP := Induction for XP Sort Prop with IIQ:=Induction for XQ Sort
Prop.

I get the right one (that's great, isn'it ?)

Print IIP.

 

(P:(XP->Prop); P0:(XQ->Prop))
 (P void)
 ->((x:XP)(P x)->(x0:XP)(P x0)->(P (slash x x0)))
   ->((x:XP)(P x)->(x0:XQ)(P0 x0)->(P (qualif x x0)))
     ->(P0 false)
       ->((x:XQ)(P0 x)->(P0 (not x)))
         ->((x:XQ)(P0 x)->(x0:XQ)(P0 x0)->(P0 (and x x0)))
           ->((x:XP)(P x)->(x0:XP)(P x0)->(P0 (leq x x0)))
             ->(x:XP)(P x)

 

Unfortunately, I need more: a double induction principle.

Based on Eduardo Gimenez 's example (c.f. tutorial on recursive types in
Coq) which is
applied on nat, I'm trying to generalize a similar double induction scheme
for my purpose,
starting from IIP above.

It is especially unclear to me how to quantify the predicates 
in mixed hypotheses, e.g. the ones derived from

(x:XP) (P x ) -> (x0:XQ) (P0 x0) -> (P
(qualif x  x0))

should it be 

(x,y:XP)  (P x y )-> (x0,y0:XQ)(P0 x0 y0) -> (P (qualif x  x0) y)
(x,y:XP)  (P x y )-> (x0,y0:XQ)(P0 x0 y0)
-> (P  x (qualif y  x0))


Any help or advice would be welcome. 

Jean-Yves

P.S: to coq designers: could such a scheme be automatically generated by
an extended 
SCHEME command ? does it make sense, as mutual recursive definition are far
from 
being rare in areas like prog. language modeling ?

--

Jean-Yves Vion-Dury   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) Jean-Yves.Vion-Dury AT inrialpes.fr	from France:   0 4 76 61 53 83 from abroad: +33 4 76 61 53 83
you may have a look at the Circus Transformation Language?	www.alphaAve.com