# Library mathcomp.ssreflect.path

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

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 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 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 p path 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 T seq T seq T Type :=
Split p1 p2 : split x (rcons p1 x ++ p2) p1 p2.

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

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

Lemma splitPl 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 p x : x \in p splitr 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'
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 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 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 p cycle e p.

Lemma ucycle_uniq p : ucycle p uniq p.

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

Lemma prev_cycle p x : cycle e p x \in p e (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 y x \in p.

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

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

Lemma mem2rf {p x y} : y \notin p mem2 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 y mem2 (p1 ++ p2 ++ p3) x y.

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

Lemma mem2_cons x p y z :
mem2 (x :: p) y z = (if x == y then z \in x :: p else mem2 p y z).

Lemma mem2_seq1 x y z : mem2 [:: x] y z = (y == x) && (z == x).

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

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

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

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

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

Lemma splitP2r p x y : mem2 p x y split2r 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 : 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 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 x s : path leT x s sorted 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 s2 path leT x s2 path leT x s1.

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

Lemma subseq_sorted s1 s2 : subseq s1 s2 sorted s2 sorted s1.

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

Lemma sorted_uniq : irreflexive leT s, sorted s uniq s.

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

Lemma eq_sorted_irr : irreflexive leT
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 :=
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 merge_path x s1 s2 :
path leT x s1 path leT x s2 path leT x (merge s1 s2).

Lemma merge_sorted s1 s2 : sorted s1 sorted s2 sorted (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'
end.

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 leT antisymmetric 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 : T T).

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 : T T).

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 p e x (next p x)) cycle e p.

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

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

Lemma next_rev p : 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) :=
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 p arc p x y = x :: p1.

Lemma right_arc x y p1 p2 (p := x :: p1 ++ y :: p2) :
uniq p arc 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 p x \in p y \in p x != y rot_to_arc_spec p x y.

End CycleArc.