From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.path.html | 346 ++++++++++++++++--------------
1 file changed, 187 insertions(+), 159 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.path.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.path.html b/docs/htmldoc/mathcomp.ssreflect.path.html
index 27e0fdf..39eba95 100644
--- a/docs/htmldoc/mathcomp.ssreflect.path.html
+++ b/docs/htmldoc/mathcomp.ssreflect.path.html
@@ -21,7 +21,6 @@
@@ -131,56 +130,56 @@
Section Paths.
-Variables (n0 : nat) (T : Type).
+Variables (n0 : nat) (T : Type).
Section Path.
-Variables (x0_cycle : T) (e : rel T).
+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.
+ 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 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 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))
+ 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.
+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 cycle_path p : cycle p = path (last x0_cycle p) p.
-Lemma rot_cycle p : cycle (rot n0 p) = cycle p.
+Lemma rot_cycle p : cycle (rot n0 p) = cycle p.
-Lemma rotr_cycle p : cycle (rotr 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_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 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 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.
+ path e (last x p) (rev (belast x p)) = path (fun z ⇒ e^~ z) x p.
End Paths.
@@ -191,68 +190,68 @@
Section EqPath.
-Variables (n0 : nat) (T : eqType) (x0_cycle : T) (e : rel T).
+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.
+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).
+ 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).
+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.
+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).
+Variant splitr x : seq T → Type :=
+ Splitr p1 p2 : splitr x (p1 ++ x :: p2).
-Lemma splitPr p x : x \in p → splitr x p.
+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'
+ | [::] ⇒ 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.
+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'
+ | [::] ⇒ 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.
+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.
+ 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.
+ 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_next p x : (next p x \in p) = (x \in p).
-Lemma mem_prev p x : (prev p x \in p) = (x \in p).
+Lemma mem_prev p x : (prev p x \in p) = (x \in p).
@@ -262,8 +261,8 @@
so that it can be used as a coercion target.
@@ -272,22 +271,22 @@
Projections, used for creating local lemmas.
@@ -298,72 +297,72 @@
-
Definition mem2 p x y :=
y \in drop (
index x p)
p.
+
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 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 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 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 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).
+
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.
+
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.
+
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).
+
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_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 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 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 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.
+
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).
+
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.
+
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 [::].
+
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) :
+
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).
+
Lemma shortenP x p :
path e x p → shorten_spec x p (
last x p) (
shorten x p).
End EqPath.
@@ -381,103 +380,103 @@
Variable T :
eqType.
-
Variable leT :
rel T.
+
Variable leT :
rel T.
-
Definition sorted s :=
if s is x :: s' then path leT x s' else true.
+
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_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.
+
{in s, ∀ y,
leT x y} → path leT x s = sorted s.
Section Transitive.
-
Hypothesis leT_tr :
transitive leT.
+
Hypothesis leT_tr :
transitive leT.
Lemma subseq_order_path x s1 s2 :
-
subseq s1 s2 → path leT x s2 → path leT x s1.
+
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 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 subseq_sorted s1 s2 :
subseq s1 s2 → sorted s2 → sorted s1.
-
Lemma sorted_filter a s :
sorted s → sorted (
filter a s).
+
Lemma sorted_filter a s :
sorted s → sorted (
filter a s).
-
Lemma sorted_uniq :
irreflexive leT → ∀ s,
sorted s → uniq 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 :
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.
+
Lemma eq_sorted_irr :
irreflexive leT →
+
∀ s1 s2,
sorted s1 → sorted s2 → s1 =i s2 → s1 = s2.
End Transitive.
-
Hypothesis leT_total :
total leT.
+
Hypothesis leT_total :
total leT.
Fixpoint merge s1 :=
-
if s1 is x1 :: s1' then
+
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
+
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.
+
else id.
Lemma merge_path x s1 s2 :
-
path leT x s1 → path leT x s2 → path leT x (
merge 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 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 perm_merge s1 s2 :
perm_eql (
merge s1 s2) (
s1 ++ s2).
-
Lemma mem_merge s1 s2 :
merge s1 s2 =i 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 size_merge s1 s2 :
size (
merge s1 s2)
= size (
s1 ++ s2).
-
Lemma merge_uniq s1 s2 :
uniq (
merge s1 s2)
= uniq (
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'
+ |
[::] :: 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.
+
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
+
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 [::].
+
Definition sort :=
merge_sort_rec [::].
Lemma sort_sorted s :
sorted (
sort s).
@@ -486,27 +485,27 @@
Lemma perm_sort s :
perm_eql (
sort s)
s.
-
Lemma mem_sort s :
sort s =i s.
+
Lemma mem_sort s :
sort s =i s.
-
Lemma size_sort s :
size (
sort s)
= size s.
+
Lemma size_sort s :
size (
sort s)
= size s.
-
Lemma sort_uniq s :
uniq (
sort s)
= uniq 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).
+
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 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 ltn_sorted_uniq_leq s :
sorted ltn s = uniq s && sorted leq s.
Lemma iota_sorted i n :
sorted leq (
iota i n).
@@ -533,29 +532,29 @@
Section Trajectory.
-
Variables (
T :
Type) (
f :
T → T).
+
Variables (
T :
Type) (
f :
T → T).
-
Fixpoint traject x n :=
if n is n'.+1 then x :: traject (
f x)
n' else [::].
+
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 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 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 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))
[::].
+
traject x n = iteri n (
fun i ⇒
rcons^~ (iter i f x))
[::].
-
Lemma size_traject x n :
size (
traject x n)
= n.
+
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.
+
Lemma nth_traject i n :
i < n → ∀ x,
nth x (
traject x n)
i = iter i f x.
End Trajectory.
@@ -564,33 +563,33 @@
Section EqTrajectory.
-
Variables (
T :
eqType) (
f :
T → T).
+
Variables (
T :
eqType) (
f :
T → T).
-
Lemma eq_fpath f' :
f =1 f' → fpath f =2 fpath f'.
+
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 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 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.
+
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).
+
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).
+
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.
+
Lemma looping_uniq x n :
uniq (
traject f x n.+1)
= ~~ looping x n.
End EqTrajectory.
@@ -601,34 +600,34 @@
Section UniqCycle.
-
Variables (
n0 :
nat) (
T :
eqType) (
e :
rel T) (
p :
seq T).
+
Variables (
n0 :
nat) (
T :
eqType) (
e :
rel T) (
p :
seq T).
Hypothesis Up :
uniq p.
-
Lemma prev_next :
cancel (
next p) (
prev p).
+
Lemma prev_next :
cancel (
next p) (
prev p).
-
Lemma next_prev :
cancel (
prev p) (
next 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_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_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 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 next_rot :
next (
rot n0 p)
=1 next p.
-
Lemma prev_rot :
prev (
rot n0 p)
=1 prev p.
+
Lemma prev_rot :
prev (
rot n0 p)
=1 prev p.
End UniqCycle.
@@ -637,16 +636,16 @@
Section UniqRotrCycle.
-
Variables (
n0 :
nat) (
T :
eqType) (
p :
seq T).
+
Variables (
n0 :
nat) (
T :
eqType) (
p :
seq T).
Hypothesis Up :
uniq p.
-
Lemma next_rotr :
next (
rotr n0 p)
=1 next p.
+
Lemma next_rotr :
next (
rotr n0 p)
=1 next p.
-
Lemma prev_rotr :
prev (
rotr n0 p)
=1 prev p.
+
Lemma prev_rotr :
prev (
rotr n0 p)
=1 prev p.
End UniqRotrCycle.
@@ -659,10 +658,10 @@
Implicit Type p :
seq T.
-
Lemma prev_rev p :
uniq p → prev (
rev p)
=1 next p.
+
Lemma prev_rev p :
uniq p → prev (
rev p)
=1 next p.
-
Lemma next_rev p :
uniq p → next (
rev p)
=1 prev p.
+
Lemma next_rev p :
uniq p → next (
rev p)
=1 prev p.
End UniqCycleRev.
@@ -671,16 +670,16 @@
Section MapPath.
-
Variables (
T T' :
Type) (
h :
T' → T) (
e :
rel T) (
e' :
rel T').
+
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'.
+
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'.
+
~~ has (
preim h b) (
belast x' p')
→
+
path e (
h x') (
map h p')
= path e' x' p'.
End MapPath.
@@ -689,25 +688,25 @@
Section MapEqPath.
-
Variables (
T T' :
eqType) (
h :
T' → T) (
e :
rel T) (
e' :
rel T').
+
Variables (
T T' :
eqType) (
h :
T' → T) (
e :
rel T) (
e' :
rel T').
-
Hypothesis Ih :
injective h.
+
Hypothesis Ih :
injective h.
-
Lemma mem2_map x' y' p' :
mem2 (
map h p') (
h x') (
h y')
= mem2 p' x' y'.
+
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 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).
+
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' :=
+
Definition fun_base (
T T' :
eqType) (
h :
T' → T)
f f' :=
rel_base h (
frel f) (
frel f').
@@ -721,26 +720,26 @@
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 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 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.
+
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 :
+
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.
+
uniq p → x \in p → y \in p → x != y → rot_to_arc_spec p x y.
End CycleArc.
@@ -748,6 +747,35 @@
+
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.
--
cgit v1.2.3