- -

Library mathcomp.ssreflect.path

- -

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

- -

- 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.
- -
-Variant 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).
- -
-Variant 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.
- -
-Variant 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.
- -
-Variant 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 [::].
- -
-Variant 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.
- -
-Variant 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.
- -
- -
-Section Monotonicity.
- -
-Variables (T : eqType) (r : rel T).
- -
-Hypothesis r_trans : transitive r.
- -
-Lemma sorted_lt_nth x0 (s : seq T) : sorted r s →
-  {in [pred n | n < size s ] &, {homo nth x0 s : i j / i < j >-> r i j }}.
- -
-Lemma ltn_index (s : seq T) : sorted r s →
-  {in s &, ∀ x y, index x s < index y s → r x y }.
- -
-Hypothesis r_refl : reflexive r.
- -
-Lemma sorted_le_nth x0 (s : seq T) : sorted r s →
-  {in [pred n | n < size s ] &, {homo nth x0 s : i j / i ≤ j >-> r i j }}.
- -
-Lemma leq_index (s : seq T) : sorted r s →
-  {in s &, ∀ x y, index x s ≤ index y s → r x y }.
- -
-End Monotonicity.
-