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.                                                                  

Import Prenex Implicits.

Section Paths.

Variables (n0 : nat) (T : Type).

Section Path.

Variables (x0_cycle : T) (e : rel T).

Fixpoint path x (p : seq T) {struct p} :=
  if p is y :: p' then e x y && path y p' else true.

Lemma path_cat : forall x p1 p2,
  path x (p1 ++ p2) = path x p1 && path (last x p1) p2.

Lemma path_rcons : forall x p y,
  path x (rcons p y) = path x p && e (last x p) y.

Lemma pathP : forall x p x0,
  reflect (forall i, i < size p -> e (nth x0 (x :: p) i) (nth x0 p i))
          (path x p).

Definition cycle p := if p is x :: p' then path x (rcons p' x) else true.

Lemma cycle_path : forall p, cycle p = path (last x0_cycle p) p.

Lemma cycle_rot : forall p, cycle (rot n0 p) = cycle p.

Lemma cycle_rotr : forall p, cycle (rotr n0 p) = cycle p.

End Path.

Lemma eq_path : forall e e', e =2 e' -> path e =2 path e'.

Lemma sub_path : forall e e', subrel e e' ->
  forall x p, path e x p -> path e' x p.

Lemma path_rev : forall e x p,
  path e (last x p) (rev (belast x p)) = path (fun z y => e y z) x p.

End Paths.

Implicit Arguments pathP [T e x p].

Section EqPath.

Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T).

CoInductive split x : seq T -> seq T -> seq T -> Type :=
  Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.

Lemma splitP : forall (p : seq T) x, x \in p ->
   let i := index x p in split x p (take i p) (drop i.+1 p).

CoInductive splitl (x1 x : T) : seq T -> Type :=
  Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2).

Lemma splitPl : forall x1 p x, x \in x1 :: p -> splitl x1 x p.

CoInductive splitr x : seq T -> Type :=
  Splitr p1 p2 : splitr x (p1 ++ x :: p2).

Lemma splitPr : forall (p : seq T) x, x \in p -> splitr x p.

Fixpoint next_at (x y0 y : T) (p : seq T) {struct p} :=
  match p with
  | [::] => if x == y then y0 else x
  | y' :: p' => if x == y then y' else next_at x y0 y' p'
  end.

Definition next p x := if p is y :: p' then next_at x y y p' else x.

Fixpoint prev_at (x y0 y : T) (p : seq T) {struct p} :=
  match p with
  | [::] => if x == y0 then y else x
  | y' :: p' => if x == y' then y else prev_at x y0 y' p'
  end.

Definition prev p x := if p is y :: p' then prev_at x y y p' else x.

Lemma next_nth : forall p x,
  next p x = if x \in p then
               if p is y :: p' then nth y p' (index x p) else x
             else x.

Lemma prev_nth : forall p x,
  prev p x = if x \in p then
               if p is y :: p' then nth y p (index x p') else x
             else x.

Lemma mem_next : forall (p : seq T) x, (next p x \in p) = (x \in p).

Lemma mem_prev : forall (p : seq T) x, (prev p x \in p) = (x \in p).

ucycleb is the boolean predicate, but ucycle is defined as a Prop 
 so that it can be used as a coercion target. 
Definition ucycleb p := cycle e p && uniq p.
Definition ucycle p : Prop := cycle e p && uniq p.

Projections, used for creating local lemmas. 
Lemma ucycle_cycle : forall p, ucycle p -> cycle e p.

Lemma ucycle_uniq : forall p, ucycle p -> uniq p.

Lemma next_cycle : forall p x, cycle e p -> x \in p -> e x (next p x).

Lemma prev_cycle : forall p x, cycle e p -> x \in p -> e (prev p x) x.

Lemma ucycle_rot : forall p, ucycle (rot n0 p) = ucycle p.

Lemma ucycle_rotr : forall p, ucycle (rotr n0 p) = ucycle p.

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

Definition mem2 (p : seq T) x y := y \in drop (index x p) p.

Lemma mem2l : forall p x y, mem2 p x y -> x \in p.

Lemma mem2lf : forall (p : seq T) x,
  (x \in p) = false -> forall y, mem2 p x y = false.

Lemma mem2r : forall p x y, mem2 p x y -> y \in p.

Lemma mem2rf : forall (p : seq T) y,
  (y \in p) = false -> forall x, mem2 p x y = false.

Lemma mem2_cat : forall p1 p2 x y,
  mem2 (p1 ++ p2) x y = mem2 p1 x y || mem2 p2 x y || (x \in p1) && (y \in p2).

Lemma mem2_splice : forall p1 p3 x y p2,
  mem2 (p1 ++ p3) x y -> mem2 (p1 ++ p2 ++ p3) x y.

Lemma mem2_splice1 : forall p1 p3 x y z,
  mem2 (p1 ++ p3) x y -> mem2 (p1 ++ z :: p3) x y.

Lemma mem2_cons : forall x p y,
  mem2 (x :: p) y =1 if x == y then predU1 x (mem p) : pred T else mem2 p y.

Lemma mem2_last : forall y0 p x,
  mem2 (y0 :: p) x (last y0 p) = (x \in y0 :: p).

Lemma mem2l_cat : forall (p1 : seq T) x, (x \in p1) = false ->
  forall p2, mem2 (p1 ++ p2) x =1 mem2 p2 x.

Lemma mem2r_cat : forall (p2 : seq T) y, (y \in p2) = false ->
   forall p1 x, mem2 (p1 ++ p2) x y = mem2 p1 x y.

Lemma mem2lr_splice : forall (p2 : seq T) x y,
    (x \in p2) = false -> (y \in p2) = false ->
  forall p1 p3, mem2 (p1 ++ p2 ++ p3) x y = mem2 (p1 ++ p3) x y.

CoInductive split2r (x y : T) : seq T -> Type :=
  Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2).

Lemma splitP2r : forall p x y, mem2 p x y -> split2r x y p.

Fixpoint shorten x (p : seq T) {struct p} :=
  if p is y :: p' then
    if x \in p then shorten x p' else y :: shorten y p'
  else [::].

CoInductive shorten_spec (x : T) (p : seq T) : T -> seq T -> Type :=
   ShortenSpec p' of path e x p' & uniq (x :: p') & subpred (mem p') (mem p) :
     shorten_spec x p (last x p') p'.

Lemma shortenP : forall x p, path e x p ->
   shorten_spec x p (last x p) (shorten x p).

End EqPath.

Ordered paths and sorting. 

Section SortSeq.

Variable T : eqType.
Variable leT : rel T.

Definition sorted s := if s is x :: s' then path leT x s' else true.

Lemma path_sorted : forall x s, path leT x s -> sorted s.

Lemma path_min_sorted : forall x s,
  (forall y, leT x y) -> path leT x s = sorted s.

Section Transitive.

Hypothesis leT_tr : transitive leT.

Lemma order_path_min : forall x s, path leT x s -> all (leT x) s.

Lemma sorted_filter : forall a s, sorted s -> sorted (filter a s).

Lemma sorted_uniq : irreflexive leT -> forall s, sorted s -> uniq s.

Lemma eq_sorted : antisymmetric leT -> forall s1 s2,
   sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.

Lemma eq_sorted_irr : irreflexive leT -> forall s1 s2,
  sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2.

End Transitive.

Hypothesis leT_total : total leT.

Fixpoint merge s1 :=
  if s1 is x1 :: s1' then
    let fix merge_s1 (s2 : seq T) :=
      if s2 is x2 :: s2' then
        if leT x2 x1 then x2 :: merge_s1 s2' else x1 :: merge s1' s2
      else s1 in
    merge_s1
  else id.

Lemma path_merge : forall x s1 s2,
  path leT x s1 -> path leT x s2 -> path leT x (merge s1 s2).

Lemma sorted_merge : forall s1 s2,
  sorted s1 -> sorted s2 -> sorted (merge s1 s2).

Lemma perm_merge : forall s1 s2, perm_eql (merge s1 s2) (s1 ++ s2).

Lemma mem_merge : forall s1 s2, merge s1 s2 =i s1 ++ s2.

Lemma size_merge : forall s1 s2, size (merge s1 s2) = size (s1 ++ s2).

Lemma merge_uniq : forall s1 s2, uniq (merge s1 s2) = uniq (s1 ++ s2).

Fixpoint merge_sort_push (s1 : seq T) (ss : seq (seq T)) {struct ss} :=
  match ss with
  | [::] :: ss' | [::] as ss' => s1 :: ss'
  | s2 :: ss' => [::] :: merge_sort_push (merge s1 s2) ss'
  end.

Fixpoint merge_sort_pop (s1 : seq T) (ss : seq (seq T)) {struct ss} :=
  if ss is s2 :: ss' then merge_sort_pop (merge s1 s2) ss' else s1.

Fixpoint merge_sort_rec (ss : seq (seq T)) (s : seq T) {struct s} :=
  if s is [:: x1, x2 & s'] then
    let s1 := if leT x1 x2 then [:: x1; x2] else [:: x2; x1] in
    merge_sort_rec (merge_sort_push s1 ss) s'
  else merge_sort_pop s ss.

Definition sort := merge_sort_rec [::].

Lemma sorted_sort : forall s, sorted (sort s).

Lemma perm_sort : forall s, perm_eql (sort s) s.

Lemma mem_sort : forall s, sort s =i s.

Lemma size_sort : forall s, size (sort s) = size s.

Lemma sort_uniq : forall s, uniq (sort s) = uniq s.

Lemma perm_sortP : transitive leT -> antisymmetric leT ->
  forall s1 s2, reflect (sort s1 = sort s2) (perm_eq s1 s2).

End SortSeq.

Lemma sorted_rev : forall (T : eqType) (leT : rel T) s,
  sorted leT (rev s) = sorted (fun y x => leT x y) s.

Lemma sorted_ltn_uniq_leq : forall s, sorted ltn s = uniq s && sorted leq s.

Lemma sorted_iota : forall i n, sorted leq (iota i n).

Lemma sorted_ltn_iota : forall i n, sorted ltn (iota i n).

Function trajectories. 

Notation fpath f := (path (frel f)).
Notation fcycle f := (cycle (frel f)).
Notation ufcycle f := (ucycle (frel f)).


Section Trajectory.

Variables (T : Type) (f : T -> T).

Fixpoint traject x (n : nat) {struct n} :=
  if n is n'.+1 then x :: traject (f x) n' else [::].

Lemma trajectS : forall x n, traject x n.+1 = x :: traject (f x) n.

Lemma trajectSr : forall x n, traject x n.+1 = rcons (traject x n) (iter n f x).

Lemma last_traject : forall x n, last x (traject (f x) n) = iter n f x.

Lemma traject_iteri : forall x n,
  traject x n = iteri n (fun i => rcons^~ (iter i f x)) [::].

Lemma size_traject : forall x n, size (traject x n) = n.

Lemma nth_traject : forall i n, i < n ->
  forall x, nth x (traject x n) i = iter i f x.

End Trajectory.

Section EqTrajectory.

Variables (T : eqType) (f : T -> T).

Lemma fpathP : forall x p,
  reflect (exists n, p = traject f (f x) n) (fpath f x p).

Lemma fpath_traject : forall x n, fpath f x (traject f (f x) n).

Definition looping x n := iter n f x \in traject f x n.

Lemma loopingP : forall x n,
  reflect (forall m, iter m f x \in traject f x n) (looping x n).

Lemma trajectP : forall x n y,
  reflect (exists2 i, i < n & y = iter i f x) (y \in traject f x n).

Lemma looping_uniq : forall x n, uniq (traject f x n.+1) = ~~ looping x n.

End EqTrajectory.

Implicit Arguments fpathP [T f x p].
Implicit Arguments loopingP [T f x n].
Implicit Arguments trajectP [T f x n y].

Section UniqCycle.

Variables (n0 : nat) (T : eqType) (e : rel T) (p : seq T).

Hypothesis Up : uniq p.

Lemma prev_next : cancel (next p) (prev p).

Lemma next_prev : cancel (prev p) (next p).

Lemma cycle_next : fcycle (next p) p.

Lemma cycle_prev : cycle (fun x y => x == prev p y) p.

Lemma cycle_from_next : (forall x, x \in p -> e x (next p x)) -> cycle e p.

Lemma cycle_from_prev : (forall x, x \in p -> e (prev p x) x) -> cycle e p.

Lemma next_rot : next (rot n0 p) =1 next p.

Lemma prev_rot : prev (rot n0 p) =1 prev p.

End UniqCycle.

Section UniqRotrCycle.

Variables (n0 : nat) (T : eqType) (p : seq T).

Hypothesis Up : uniq p.

Lemma next_rotr : next (rotr n0 p) =1 next p.

Lemma prev_rotr : prev (rotr n0 p) =1 prev p.

End UniqRotrCycle.

Section UniqCycleRev.

Variable T : eqType.

Lemma prev_rev : forall p : seq T, uniq p -> prev (rev p) =1 next p.

Lemma next_rev : forall p : seq T, uniq p -> next (rev p) =1 prev p.

End UniqCycleRev.

Section MapPath.

Variables (T T' : Type) (h : T' -> T) (e : rel T) (e' : rel T').

Definition rel_base (b : pred T) :=
  forall x' y', ~~ b (h x') -> e (h x') (h y') = e' x' y'.

Lemma path_map : forall b x' p', rel_base b ->
    ~~ has (preim h b) (belast x' p') ->
  path e (h x') (map h p') = path e' x' p'.

End MapPath.

Section MapEqPath.

Variables (T T' : eqType) (h : T' -> T) (e : rel T) (e' : rel T').

Hypothesis Hh : injective h.

Lemma mem2_map : forall x' y' p',
  mem2 (map h p') (h x') (h y') = mem2 p' x' y'.

Lemma next_map : forall p, uniq p ->
  forall x, next (map h p) (h x) = h (next p x).

Lemma prev_map : forall p, uniq p ->
  forall x, prev (map h p) (h x) = h (prev p x).

End MapEqPath.

Definition fun_base (T T' : eqType) (h : T' -> T) f f' :=
  rel_base h (frel f) (frel f').

Section CycleArc.

Variable T : eqType.

Definition arc (p : seq T) x y :=
  let px := rot (index x p) p in take (index y px) px.

Lemma arc_rot : forall i p, uniq p -> {in p, arc (rot i p) =2 arc p}.

Lemma left_arc : forall x y p1 p2,
  let p := x :: p1 ++ y :: p2 in uniq p -> arc p x y = x :: p1.

Lemma right_arc : forall x y p1 p2,
  let p := x :: p1 ++ y :: p2 in uniq p -> arc p y x = y :: p2.

CoInductive rot_to_arc_spec (p : seq T) (x y : T) : Type :=
    RotToArcSpec i p1 p2 of x :: p1 = arc p x y
                          & y :: p2 = arc p y x
                          & rot i p = x :: p1 ++ y :: p2 :
    rot_to_arc_spec p x y.

Lemma rot_to_arc : forall p x y,
  uniq p -> x \in p -> y \in p -> x != y -> rot_to_arc_spec p x y.

End CycleArc.