Library paths

   The basic theory of paths over an eqType; this file is essentially a    
 complement to seq.v. Paths are non-empty sequences that obey a progression 
 relation. They are passed around in three parts: the head and tail of the  
 sequence, and a proof of (boolean) predicate asserting the progression.    
 This "exploded" view is rarely embarrassing, as the first two parameters   
 are usually inferred from the type of the third; on the contrary, it saves 
 the hassle of constantly constructing and destructing a dependent record.  
    We define similarly cycles, for which we allow the empty sequence,      
 which represents a non-rooted empty cycle; by contrast, the "empty" path   
 from a point x is the one-item sequence containing only x.                 
   We allow duplicates; uniqueness, if desired (as is the case for several  
 geometric constructions), must be asserted separately. We do provide       
 shorthand, but only for cycles, because the equational properties of       
 "path" and "uniq" are unfortunately  incompatible (esp. wrt "cat").        
    We define notations for the common cases of function paths, where the   
 progress relation is actually a function. In detail:                       
   path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we     
                 e x_i x_{i+1} for all i < n. The path x :: p starts at x   
                 and ends at last x p.                                      
  fpath f x p == x :: p is an f-path, where f is a function, i.e., p is of  
                 the form [:: f x; f (f x); ...]. This is just a notation   
                 for path (frel f) x p.                                     
   sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p  
                 is an e-path (this is oten used with e = leq or ltn).      
    cycle e c == c is an e-cycle: either c = [::], or c = x :: p with       
                 x :: (rcons p x) an e-path.                                
   fcycle f c == c is an f-cycle, for a function f.                         
 traject f x n == the f-path of size n starting at x                        
              := [:: x; f x; ...; iter n.-1 f x]                            
 looping f x n == the f-paths of size greater than n starting at x loop     
                 back, or, equivalently, traject f x n contains all         
                 iterates of f at x.                                        
 merge e s1 s2 == the e-sorted merge of sequences s1 and s2: this is always 
                 a permutation of s1 ++ s2, and is e-sorted when s1 and s2  
                 are and e is total.                                        
     sort e s == a permutation of the sequence s, that is e-sorted when e   
                 is total (computed by a merge sort with the merge function 
                 above).                                                    
   mem2 s x y == x, then y occur in the sequence (path) s; this is          
                 non-strict: mem2 s x x = (x \in s).                        
     next c x == the successor of the first occurrence of x in the sequence 
                 c (viewed as a cycle), or x if x \notin c.                 
     prev c x == the predecessor of the first occurrence of x in the        
                 sequence c (viewed as a cycle), or x if x \notin c.        
    arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting  
                 at the first occurrence of x in c, and ending just before  
                 the next ocurrence of y (in cycle order); arc c x y        
                 returns an unspecified sub-arc of c if x and y do not both 
                 occur in c.                                                
  ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) 
 ufcycle f c <-> c is a simple f-cycle, for a function f.                   
  shorten x p == the tail a duplicate-free subpath of x :: p with the same  
                 endpoints (x and last x p), obtained by removing all loops 
                 from x :: p.                                               
 rel_base e e' h b <-> the function h is a functor from relation e to       
                 relation e', EXCEPT at points whose image under h satisfy  
                 the "base" predicate b:                                    
                    e' (h x) (h y) = e x y UNLESS b (h x) holds             
                 This is the statement of the side condition of the path    
                 functorial mapping lemma path_map.                         
 fun_base f f' h b <-> the function h is a functor from function f to f',   
                 except at the preimage of predicate b under h.             
 We also provide three segmenting dependently-typed lemmas (splitP, splitPl 
 and splitPr) whose elimination split a path x0 :: p at an internal point x 
 as follows:                                                                
  - splitP applies when x \in p; it replaces p with (rcons p1 x ++ p2), so  
    that x appears explicitly at the end of the left part. The elimination  
    of splitP will also simultaneously replace take (index x p) with p1 and 
    drop (index x p).+1 p with p2.                                          
  - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and     
    simulaneously generates an equation x = last x0 p.                      
  - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x  
    appears explicitly at the start of the right part.                      
 The parts p1 and p2 are computed using index/take/drop in all cases, but   
 only splitP attemps to subsitute the explicit values. The substitution of  
 p can be deferred using the dependent equation generation feature of       
 ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates    
 the equation p = p1 ++ p2 instead of performing the substitution outright. 
   Similarly, eliminating the loop removal lemma shortenP simultaneously    
 replaces shorten e x p with a fresh constant p', and last x p with         
 last x p'.                                                                 
   Note that although all "path" functions actually operate on the          
 underlying sequence, we provide a series of lemmas that define their       
 interaction with thepath and cycle predicates, e.g., the path_cat equation 
 can be used to split the path predicate after splitting the underlying     
 sequence.                                                                  

ucycleb is the boolean predicate, but ucycle is defined as a Prop 
 so that it can be used as a coercion target. 

Projections, used for creating local lemmas. 

The "appears no later" partial preorder defined by a path. 

Ordered paths and sorting. 

Function trajectories.