Library choice

This file contains the definitions of:                                    
  - choiceType : interface for type with choice operator                   
  - countType : interface for countable type                               
 In addition to the lemmas relevant to these definitions, this file also   
 contains definitions of Canonical Structure of choiceType for nat and     
 subtype / option type / seq type / sigma type of a choice type. It also   
 contains definitions of Canonical Structure of countType for nat, bool    
 and subtype / option type / seq type / sigma type of a countable type and 
 sum and prod types of two countable types.                                

Technical definitions about coding and decoding of  list. This results are
 useful for the definition of Canonical Structure of choice and countable  
 types. 

Goedel-style one-to-one encoding of seq T into T, for T := nat    
 and T := seq (seq T0). Note that there is no such encoding in     
 general for T := seq T0, since seq void ~ unit while              
 seq (seq void) ~ nat.                                             

The code for [:: n1; ...; nk] has binary representation           
     1 0 ... 0 1 ... 1 0 ... 0 1 0 ... 0                           
       <----->         <----->   <----->                           
        nk 0s           n2 0s     n1 0s                            

Auxiliary functions that pad s2 : seq (seq T) with leading [::], 
 compute the padding, and strip it.                               
 To encode a sequence we flatten its contents and prepend padding 
 whose length encodes (via Nat.code) the shape of the sequence.   
 More precisely code for a sequence s3 with shape sh == shape s3  
 and contents sc == flatten s3 is:                                
  - pad (Nat.code sh) [::]        if sc = [::]                    
  - pad (Nat.code sh) (strip sc)  if sc has padding               
  - pad (Nat.code (behead sh)) sc if sc != [::] has no padding    
 The omitted padding/shape can be readily reconstructed; it is    
 obviously necessary to delete the padding to avoid confusion     
 with the shape encoding; beheading the shape makes the encoding  
 one-to-one (otherwise, the contents following the padding could  
 never exceed the capacity of the shape encoded by the padding.   

Miscellaneous encodings: option T -c-> seq T, T -c-> seq (seq T),          
 T1 * T2 -c-> {i : T2 & T1}, and T1 + T2 -c-> option T1 * option T2.        
   We use these encodings to propagate canonical structures through these   
 type constructors so that ultimately all Choice and Countable derive from  
 the (trivial) Countable structure on nat. The peculiar order of the        
 encoding of the product type T1 * T2 is due to the fact that we want it to 
 compose with  {i : T & T_ i} -c-> seq I, which is the only encoding we     
 have for sigT, and is only defined when T_ i : countType (hence, it will   
 only appear later in this file). This limitation means we have to assume   
 that one of T1 or T2 in T1 * T2 / T1 + T2 is a countType, even if we only  
 need a choiceType; it seemed somewhat more natural to take T1 : countType. 

Structures for Types with a choice function, and for Types with   
 countably many elements. The two concepts are closely linked: we  
 indeed make Countable a subclass of Choice, as countable choice   
 is valid in CiC. This apparent redundancy is needed to ensure the 
 consistency of the Canonical Structure inference, as the          
 canonical Choice for a given type may differ from the countable   
 choice for its canonical Countable structure, e.g., for options.  
 Nevertheless for most standard datatype constructors, including   
 sums and pairs, Choice can only be satisfied constructively via   
 countability, so in practice we build most Choice and Countable   
 structures simultaneously.                                        
   For T : choiceType and P : pred T, we have actually two choice  
 functions:                                                        
    xchoose : (exists x, P x) -> T                                 
    choose : pred T -> T -> T                                      
   We always have P (xchoose exP), while P (choose P x0) only if   
 P x0 holds. Both xchoose and choose are extensional in P and do   
 not depend on the witness exP or x0 (provided P x0). Note that    
 xchoose is slightly more powerful, but less convenient to use.    
 The Choice structure actually contains an xchoose function for    
 seq (seq T), as this allows us to derive a Choice structure for   
 seq T (and thus for iter n seq T for any n).                      
   For T : countType we have two functions:                        
    pickle : T -> nat, and unpickle : nat -> option T              
 The two functions provide an effective embedding of T in nat: we  
 have pcancel pickle unpickle, i.e., unpickle \o pickle =1 some.   
 The names of the generic functions underline the correspondence   
 with the notion of "Serializable" types in programming languages. 
 Note that unpickle needs to be a partial function to account for  
 a possibly empty T (e.g., T = {x | P x}). We derive a pickle_inv  
 function that is an exact inverse to pickle, i.e., we have both   
 pcancel pickle pickle_inv, and ocancel pickle_inv pickle.         
   Finally, we need to provide a join class to let type inference  
 unify subType and countType class constraints, as we can have     
 a countable subType of an uncountable choiceType (the problem     
 did not arise earlier with eqType or choiceType because in        
 in practice the base type of an Equality/Choice subType is always 
 an Equality/Choice Type).                                         

Construct class_of T directly from an encoding seq (seq T) c-> nat.  
 This is used to build a Choice base class for Countable types.       

Canonical Structure of choiceType 

This assumes that T has both countType and subType structures. 

The remaining Canonical Structures for standard datatypes. 

To encode {i : I | T_ i} into a type that inherits the Choice or    
 Countable structure of I, we need T_ i to be a countType, in which  
 case we get an encoding {i : I | T_ i} c-> seq I.