reversing a vector

[Pierre Casteran]

Hello,

  with vectors and vappend defined as in the Tutorial, I tried to define
vrev as follows :

     (     xs : Vec n X     !                        
let  !----------------------!                        
     ! vrev _n xs : Vec n X )                        
                                                     
     vrev _ n xs <= rec xs                          
     { vrev _ n xs <= case xs                        
       { vrev _ zero vnil => vnil                    
         vrev _ (suc n) (vcons x xs)                
           => vappend _ n (vrev _ n xs) (vcons x vnil)
       }                                            
     }    


The last clause was rejected, (I presume) because of the non-unification of
(suc n) with (plus n (suc zero)). Is that right ?
Is there a way to use some commutatitivy of plus (like using JMeq in
Coq) ?
Or any other way to define vrev ?

Cheers,
Pierre

[Pierre Casteran]

Sorry for the code presentation, too.
Perhaps it's better to attach a small piece of code :

>
> The last clause was rejected, (I presume) because of the
> non-unification of
> (suc n) with (plus n (suc zero)). Is that right ?
> Is there a way to use some commutatitivy of plus (like using JMeq in
> Coq) ? Or any other way to define vrev ?
>
> Cheers,
> Pierre
>
>
>

     (     xs : Vec n X     !                        
let  !----------------------!                        
     ! vrev _n xs : Vec n X )                        
                                                     
     vrev _ n xs <= rec xs                            
     { vrev _ n xs <= case xs                        
       { vrev _ zero vnil => vnil                    
         vrev _ (suc n) (vcons x xs)                  
           => vappend _ n (vrev _ n xs) (vcons x vnil)
       }                                              
     }                                

[Matthew Walton-2]

> > The last clause was rejected, (I presume) because of the
> > non-unification of
> > (suc n) with (plus n (suc zero)). Is that right ?
> > Is there a way to use some commutatitivy of plus (like using JMeq in
> > Coq) ? Or any other way to define vrev ?

You're correct.  In the vcons case, Epigram wants Vec (suc n) X but the
type of the vappend is Vec (plus n (suc zero)) X. Fortunately you can
prove that these two are equal:

     (    x : X     !
let  !--------------!
     ! rf x : x = x )
                     
     rf x => refl    
------------------------------------------------------------------------------
     ( f, g : S -> T ;  fg : f = g ;  x, y : S ;  xy : x = y !
let  !-------------------------------------------------------!
     !               ra fg xy : (f x) = (g y)                )
                                                             
     ra fg xy <= case fg                                      
     { ra refl fy <= case fy                                  
       { ra refl refl => refl                                
       }                                                      
     }                                                        
------------------------------------------------------------------------------
     (             n : Nat             !
let  !---------------------------------!
     ! q n : plus n (suc zero) = suc n )
                                       
     q n <= rec n                      
     { q n <= case n                    
       { q zero => refl                
         q (suc n) => ra (rf suc) (q n)
       }                                
     }                                  


Although it's no doubt better to give the proof a better name than 'q'.

Then wrap the proof up in another proof that makes it apply to vector
lengths:

     (          p : x = y          !
let  !-----------------------------!
     ! vecEq p : Vec x X = Vec y X )
                                   
     vecEq p <= case p              
     { vecEq refl => refl          
     }                              

And write a function that lets you use a proof of equality to do a type
coercion:

     (     p : S = T     !      
let  !-------------------!      
     ! coerce p : S -> T )      
                               
     coerce p <= case p        
     { coerce refl => lam x => x
     }                          


And then use this to make epigram accept vrev:

     (     xs : Vec n X     !                                  
let  !----------------------!                                  
     ! vrev _n xs : Vec n X )                                  
                                                               
     vrev _ n xs <= rec xs                                    
     { vrev _ n xs <= case xs                                  
       { vrev _ zero vnil => vnil                              
         vrev _ (suc n) (vcons x xs)                          
           => coerce (vecEq (q n)) (vappend xs (vcons x vnil))
       }                                                      
     }                                                        

It requires jumping through a few hoops, but it does work.