The Coq mailing list

[Conor McBride <conor AT cs.rhul.ac.uk>]

Hi Venanzio, hello all,

Venanzio Capretta wrote:
> I challenge you to do the same using the inductive Vector (or listn) 
> definition!

See attached Epigram file, which I offer as evidence of what's possible
with a bit more automation.

> I suggest a different solution to the problem. In my opinion the use of a
> dependent inductive definition for vectors is what causes the trouble. It
> is not necessary. Instead we should represent vectors are tuples, that is,
> as iterated products.
>
> Fixpoint Tuple (A:Set)(n:nat){struct n}: Set := 
> match n with
>  0 => unit
> | (S n') => (A*(Tuple A n'))%type
> end.

It depends on how you see the problem. If it's a question of manipulating
vectors, then yes, exploit the convenient relationship between the structure
of vectors and the structure of numbers (after all, a vector is a proof that
a number's S symbols can be given labels). Or go even further: define finite
sets (either inductively, or by iterated coproducts) and represent vectors
functionally: this makes all sorts of operations even easier (eg transpose),
at the cost of making vector equality extensional.

In my experience, inductive vectors are slightly easier to work with than
computed tuples because the typechecker can infer that Vcons makes vectors,
but it can only check that pairing makes vectors: you have to be a lot more
explicit about what you want. But apart from that, there isn't much
difference between the two.

But anyway, all of these tricks exploit the particular nature of vectors
to avoid the fact that dependent pattern matching is difficult. If you
want to work with a different type, eg expressions in simply typed lambda
calculus, you'll need to invent a different box of tricks to deal with that.
For that example, you can't just use the structure of types to compute the
structure of terms: they have totally different inductive structure. This is
good, because the combination of the two allows you to define the
normalization function structurally. But I digress...

> We should also remark, when using the libraries Eqdep and JMeg as suggested
> by Yves Bertot and Boris Yakobowski, that these contain axioms, so if you
> import them you are not using the pure type theory anymore. One more reason
> to do things differently.

Ultimately, if you have a universe (and can thus prove true-not-false etc)
dependent pattern matching as in Thierry Coquand's 1992 paper
is equivalent to Thomas Streicher's K axiom, of which JMeq is just a
convenient repackaging. What's more, JMeq supports an automated approach to
these dependent case analyses, which is why the attached Epigram file
elaborates successfully to a construction in a type theory rather like
CIC+JMeq. Those of you who have worries about K could replay the construction
with ordinary equality, using the proof of K-for-nat: a little more ad hoc,
but still automatable. What's so bad about K anyway?

Dependent pattern matching is currently difficult in Coq, but it doesn't
have to be that way. The question is what to do about it.

On conna\^it la chanson...

Conor

--
http://www.cs.rhul.ac.uk/~conor
------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
------------------------------------------------------------------------------
     ( n : Nat ;  X : * !                                         
data !------------------!                                         
     !   Vec n X : *    )                                         
                                                                  
                               ( X ;  n ;  x : X ;  xs : Vec n X !
where (-------------------! ;  !---------------------------------!
      ! vnil : Vec zero X )    !   vcons x xs : Vec (suc n) X    )
------------------------------------------------------------------------------
     (     n ;  x : X     !                
let  !--------------------!                
     ! vec _n x : Vec n X )                
                                           
     vec _ n x <= rec n                    
     { vec _ n x <= case n                 
       { vec _ zero x => vnil              
         vec _ (suc n) x => vcons x (vec x)
       }                                   
     }                                     
------------------------------------------------------------------------------
     ( fs : Vec n (S -> T) ;  ss : Vec n S !                         
let  !-------------------------------------!                         
     !        vapp fs ss : Vec n T         )                         
                                                                     
     vapp fs ss <= rec fs                                            
     { vapp fs ss <= case fs                                         
       { vapp vnil ss <= case ss                                     
         { vapp vnil vnil => vnil                                    
         }                                                           
         vapp (vcons f fs) ss <= case ss                             
         { vapp (vcons f fs) (vcons s ss) => vcons (f s) (vapp fs ss)
         }                                                           
       }                                                             
     }                                                               
------------------------------------------------------------------------------
     ( f : X -> X -> X ;  xs, ys : Vec n X ! 
let  !-------------------------------------! 
     !        vbo f xs ys : Vec n X        ) 
                                             
     vbo f xs ys => vapp (vapp (vec f) xs) ys
------------------------------------------------------------------------------
     (    xss : Vec m (Vec n X)     !                                    
let  !------------------------------!                                    
     ! vtrans xss : Vec n (Vec m X) )                                    
                                                                         
     vtrans xss <= rec xss                                               
     { vtrans xss <= case xss                                            
       { vtrans vnil => vec vnil                                         
         vtrans (vcons xs xss) => vapp (vapp (vec vcons) xs) (vtrans xss)
       }                                                                 
     }                                                                   
------------------------------------------------------------------------------
     ( X : * ;  n : Nat !                 
let  !------------------!                 
     !  Arity X n : *   )                 
                                          
     Arity X n <= rec n                   
     { Arity X n <= case n                
       { Arity X zero => X                
         Arity X (suc n) => X -> Arity X n
       }                                  
     }                                    
------------------------------------------------------------------------------
     ( f : Arity S n ;  ss : Vec n S !       
let  !-------------------------------!       
     !         vunc f ss : S         )       
                                             
     vunc f ss <= rec ss                     
     { vunc f ss <= case ss                  
       { vunc f vnil => f                    
         vunc f (vcons s ss) => vunc (f s) ss
       }                                     
     }                                       
------------------------------------------------------------------------------