The Coq mailing list

[jean-francois.monin AT imag.fr]

Hi,

This works:

Fixpoint lift [T:def] : deftwo
  := Cases T of
         base => basetwo
       | (lister L) => (listertwo (map lift L))
     end.



Nadeem Abdul Hamid a ecrit :
 > Hi all,
 > 
 > I have two inductive definitions which are very similar and want to 
 > convert a term of one to the other. But, the mutually recursive fixpoint 
 > doesn't work. I even tried unfolding the definition of "lift" below as 
 > mentioned in previous posts to the Coq list but it still doesn't seem to 
 > work?
 > 
 > 
 > Require PolyList.
 > 
 > Inductive def : Set
 >   := base : def
 >   |  lister : (list def) -> def.
 > 
 > Inductive deftwo : Set
 >   := basetwo : deftwo
 >   |  listertwo : (list deftwo) -> deftwo
 >   |  othertwo: deftwo.
 > 
 > Fixpoint lift [T:def] : deftwo
 >   := Cases T of
 >          base => basetwo
 >        | (lister L) => (listertwo (liftL L))
 >      end
 > with liftL [L:(list def)] : (list deftwo)
 >   := Cases L of
 >         nil => (nil ?)
 >       | (cons a L') => (cons (lift a) (liftL L'))
 >      end
 > .
 > 
 > 
 > This doesn't seem to work either:
 > 
 > Fixpoint liftL [L:(list def)] : (list deftwo)
 >   := Cases L of
 >         nil => (nil ?)
 >       | (cons a L') =>
 >           let lift = (Fix lift {lift [T:def] : (deftwo) :=
 >                      Cases T of
 >               base => basetwo
 >              | (lister L'') => (listertwo (liftL L''))
 >              end })
 >           in (cons (lift a) (liftL L'))
 >      end
 > .
 > 
 > 
 > Any suggestions? Thanks in advance,
 > 
 > --- nadeem
 > 
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/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

-- 
Jean-François Monin           http://www-verimag.imag.fr/~monin/
VERIMAG - Centre Equation     tel (+33 | 0) 4 56 52 03 72
2, av. de Vignate             fax (+33 | 0) 4 56 52 03 44 
F-38610 GIERES