(Joint Center)Library MathComp.path

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

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 map_path. 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 cat_path equation can be used to split the path predicate after splitting the underlying sequence.

Set Implicit Arguments.

Section Paths.

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

Section Path.

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

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

Lemma cat_path x p1 p2 : path x (p1 ++ p2) = path x p1 && path (last x p1) p2.

Lemma rcons_path x p y : path x (rcons p y) = path x p && e (last x p) y.

Lemma pathP x p x0 :
  reflect ( i, i < size pe (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 p : cycle p = path (last x0_cycle p) p.

Lemma rot_cycle p : cycle (rot n0 p) = cycle p.

Lemma rotr_cycle p : cycle (rotr n0 p) = cycle p.

End Path.

Lemma eq_path e e' : e =2 e'path e =2 path e'.

Lemma eq_cycle e e' : e =2 e'cycle e =1 cycle e'.

Lemma sub_path e e' : subrel e e' x p, path e x ppath e' x p.

Lemma rev_path e x p :
  path e (last x p) (rev (belast x p)) = path (fun ze^~ 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).
Implicit Type p : seq T.

CoInductive split x : seq Tseq Tseq TType :=
  Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.

Lemma splitP p x (i := index x p) :
  x \in psplit x p (take i p) (drop i.+1 p).

CoInductive splitl x1 x : seq TType :=
  Splitl p1 p2 of last x1 p1 = x : splitl x1 x (p1 ++ p2).

Lemma splitPl x1 p x : x \in x1 :: psplitl x1 x p.

CoInductive splitr x : seq TType :=
  Splitr p1 p2 : splitr x (p1 ++ x :: p2).

Lemma splitPr p x : x \in psplitr x p.

Fixpoint next_at x y0 y 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'

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

Fixpoint prev_at x y0 y 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'

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

Lemma next_nth 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 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 p x : (next p x \in p) = (x \in p).

Lemma mem_prev p 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 p : ucycle pcycle e p.

Lemma ucycle_uniq p : ucycle puniq p.

Lemma next_cycle p x : cycle e px \in pe x (next p x).

Lemma prev_cycle p x : cycle e px \in pe (prev p x) x.

Lemma rot_ucycle p : ucycle (rot n0 p) = ucycle p.

Lemma rotr_ucycle p : ucycle (rotr n0 p) = ucycle p.

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

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

Lemma mem2l p x y : mem2 p x yx \in p.

Lemma mem2lf {p x y} : x \notin pmem2 p x y = false.

Lemma mem2r p x y : mem2 p x yy \in p.

Lemma mem2rf {p x y} : y \notin pmem2 p x y = false.

Lemma mem2_cat 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 p1 p3 x y p2 :
   mem2 (p1 ++ p3) x ymem2 (p1 ++ p2 ++ p3) x y.

Lemma mem2_splice1 p1 p3 x y z :
  mem2 (p1 ++ p3) x ymem2 (p1 ++ z :: p3) x y.

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

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

Lemma mem2l_cat {p1 p2 x} : x \notin p1mem2 (p1 ++ p2) x =1 mem2 p2 x.

Lemma mem2r_cat {p1 p2 x y} : y \notin p2mem2 (p1 ++ p2) x y = mem2 p1 x y.

Lemma mem2lr_splice {p1 p2 p3 x y} :
  x \notin p2y \notin p2mem2 (p1 ++ p2 ++ p3) x y = mem2 (p1 ++ p3) x y.

CoInductive split2r x y : seq TType :=
  Split2r p1 p2 of y \in x :: p2 : split2r x y (p1 ++ x :: p2).

Lemma splitP2r p x y : mem2 p x ysplit2r x y p.

Fixpoint shorten x 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 p : Tseq TType :=
   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 x p : path e x pshorten_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 x s : path leT x ssorted s.

Lemma path_min_sorted x s :
  {in s, y, leT x y}path leT x s = sorted s.

Section Transitive.

Hypothesis leT_tr : transitive leT.

Lemma subseq_order_path x s1 s2 :
  subseq s1 s2path leT x s2path leT x s1.

Lemma order_path_min x s : path leT x sall (leT x) s.

Lemma subseq_sorted s1 s2 : subseq s1 s2sorted s2sorted s1.

Lemma sorted_filter a s : sorted ssorted (filter a s).

Lemma sorted_uniq : irreflexive leT s, sorted suniq s.

Lemma eq_sorted : antisymmetric leT
   s1 s2, sorted s1sorted s2perm_eq s1 s2s1 = s2.

Lemma eq_sorted_irr : irreflexive leT
   s1 s2, sorted s1sorted s2s1 =i s2s1 = s2.

End Transitive.

Hypothesis leT_total : total leT.

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

Lemma merge_path x s1 s2 :
  path leT x s1path leT x s2path leT x (merge s1 s2).

Lemma merge_sorted s1 s2 : sorted s1sorted s2sorted (merge s1 s2).

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

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

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

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

Fixpoint merge_sort_push s1 ss :=
  match ss with
  | [::] :: ss' | [::] as ss's1 :: ss'
  | s2 :: ss'[::] :: merge_sort_push (merge s1 s2) ss'

Fixpoint merge_sort_pop s1 ss :=
  if ss is s2 :: ss' then merge_sort_pop (merge s1 s2) ss' else s1.

Fixpoint merge_sort_rec ss 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 sort_sorted s : sorted (sort s).

Lemma perm_sort s : perm_eql (sort s) s.

Lemma mem_sort s : sort s =i s.

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

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

Lemma perm_sortP : transitive leTantisymmetric leT
   s1 s2, reflect (sort s1 = sort s2) (perm_eq s1 s2).

End SortSeq.

Lemma rev_sorted (T : eqType) (leT : rel T) s :
  sorted leT (rev s) = sorted (fun y xleT x y) s.

Lemma ltn_sorted_uniq_leq s : sorted ltn s = uniq s && sorted leq s.

Lemma iota_sorted i n : sorted leq (iota i n).

Lemma iota_ltn_sorted i n : sorted ltn (iota i n).

Function trajectories.

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

Section Trajectory.

Variables (T : Type) (f : TT).

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

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

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

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

Lemma traject_iteri x n :
  traject x n = iteri n (fun ircons^~ (iter i f x)) [::].

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

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

End Trajectory.

Section EqTrajectory.

Variables (T : eqType) (f : TT).

Lemma eq_fpath f' : f =1 f'fpath f =2 fpath f'.

Lemma eq_fcycle f' : f =1 f'fcycle f =1 fcycle f'.

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

Lemma fpath_traject 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 x n :
  reflect ( m, iter m f x \in traject f x n) (looping x n).

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

Lemma looping_uniq 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 yx == prev p y) p.

Lemma cycle_from_next : ( x, x \in pe x (next p x)) → cycle e p.

Lemma cycle_from_prev : ( x, x \in pe (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.
Implicit Type p : seq T.

Lemma prev_rev p : uniq pprev (rev p) =1 next p.

Lemma next_rev p : uniq pnext (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) :=
   x' y', ~~ b (h x') → e (h x') (h y') = e' x' y'.

Lemma map_path b x' p' (Bb : 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 Ih : injective h.

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

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

Lemma prev_map p : uniq p 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.
Implicit Type p : seq T.

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

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

Lemma left_arc x y p1 p2 (p := x :: p1 ++ y :: p2) :
  uniq parc p x y = x :: p1.

Lemma right_arc x y p1 p2 (p := x :: p1 ++ y :: p2) :
  uniq parc p y x = y :: p2.

CoInductive rot_to_arc_spec p x y :=
    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 p x y :
  uniq px \in py \in px != yrot_to_arc_spec p x y.

End CycleArc.