The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

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