Library paths

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
The basic theory of paths over an eqType; this 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 (boolean) predicate asserting the progression.    
This is rarely embarrassing, as the first two are usually         
implicit parameters inferred from the predicate, and it saves the 
hassle of constantly constructing and destructing a dependent     
record.                                                           
   We define similarly cycles, but in this case we allow the      
empty sequence (which is a non-rooted empty cycle; by contrast,   
the empty path from 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 for cycles only, 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. We also       
define additional traversal/surgery operations, many of which     
could have been in seq.v, but are here because they only really   
are useful for sequences considered as paths :                    
 - directed surgery : splitPl, splitP, splitPr are dependent      
   predicates whose elimination splits a path x0:p at one of its  
   elements (say x). The three variants differ as follows:        
     - splitPl applies when x is in x0::p, generates two paths p1 
       and p2, along with the equation x = (last x0 p), and       
       replaces p with (p1 ++ p2) in the goal (the patterned      
       Elim can be used to select occurrences and generate an     
       equation p = (p1 ++ p2).                                   
     - splitP applies when x is in p, and replaces p with         
       (rcons p1 x ++ p2), where x appears explicitly at the end  
       of the left part.                                          
     - splitPr similarly replaces p with (p1 ++ x :: p2), where x 
       appears explicitly at the right of the split, when x       
       actually occurs in p.                                      
   The parts p1 and p2 are computed using index/take/drop. The    
   splitP variant (but not the others) attempts to replace the    
   explicit expressions for p1 and p2 by p1 and p2, respectively. 
   This is moderately useful, but allows for defining other       
   splitting lemmas with conclusions of the form (split x p p1 p2)
   with other expressions for p1 and p2 that might be known to    
   occur.                                                         
 - function trajectories: traject, and  looping predicates.       
 - cycle surgery : arc extracts the sub-arc between two points    
   (including the first, excluding the second). (arc p x y) is    
   thus only meaningful if x and y are different points in p.     
 - cycle traversal : next, prev                                   
 - path order: mem2 checks whether two points belong to a path    
   and appear in order (i.e., (mem2 p x y) checks that y appears  
   after an occurrence of x in p). This predicate is a crucial    
   part of the definition of the abstract Jordan property.        
 - sorting: sorted checks whether a sequence is sorted wrt a      
   transitive relation; sorted e (x :: p) expands to path e x p,  
   and sort sorts a sequence recursively, using a "merge" function
   to interleave sorted sublists.                                 
 - loop removal : shorten returns a shorter, duplicate-free path  
   with the same endpoints as its argument. The related shortenP  
   dependent predicate simultaneously substitutes a new path p',  
   for (shorten e x p), (last x p') for (last x p), and generates 
   predicates asserting that p' is a duplicate-free subpath of p. 
Although these functions operate on the underlying sequences, we  
provide a series of lemmas that define their interaction with the 
path 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 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.

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.

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_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))
  (at level 10, f at level 8) : seq_scope.

Notation "'fcycle' f" := (cycle (frel f))
  (at level 10, f at level 8) : seq_scope.

Notation "'ufcycle' f" := (ucycle (frel f))
  (at level 10, f at level 8) : seq_scope.


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 size_traject : forall x n, size (traject x n) = n.

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

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. Qed.

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

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.