The Coq mailing list

[David Nowak <David.Nowak AT irisa.fr>]

Bonjour,

J'aurai besoin d'un petit coup de pouce pour une démonstration qui me
résiste. J'ai défini un prédicat inductif sur les flux d'entiers :

     Inductive ZeroPrefix : nat->(Stream nat)->(Stream nat)->Prop :=
       another_zero : (n:nat)(x,y:(Stream nat))
         (ZeroPrefix n x y)->(ZeroPrefix n (cons O x) y)
     | end_zero : (n:nat)(x:(Stream nat))
         (ZeroPrefix n (cons n x) x).

(ZeroPrefix n x y) signifiant que le flux x est de la forme O...O.n.y.

Ne pouvant substituer une égalité extensionnelle entre deux flux, je
cherche à montrer le cas de substitution particulier qui m'intéresse. 

     Goal (n:nat)(x,x',y:(Stream nat))
       (ZeroPrefix n x y)->(EqSt ? x x')->(ZeroPrefix n x' y).

Je ne peux utiliser ni Cofix, ni Induction et l'élimination de
l'hypothèse inductive ne donne pas grand chose.

Merci de votre aide.

-- 
David

mél   : 
David.Nowak AT irisa.fr
ouèbe : http://www.mygale.org/~nowak/