+ +

Library mathcomp.ssreflect.path

+ +

+(* (c) Copyright 2006-2016 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 z ⇒ e ^~ z) x p.
+ +
+End Paths.
+ +
+ +
+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 x ⇒ leT 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 i ⇒ rcons ^~ (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.
+ +
+ +
+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 : (∀ 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.
+ +
+ +
+