Library prosa.classic.util.list
Require Export prosa.util.list.
Require Import prosa.classic.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about lists without duplicates. *)
Section UniqList.
Lemma idx_lt_rcons :
∀ {T: eqType} (l: seq T) i x0,
uniq l →
i < size l →
[seq x <- l | index x l < i.+1] =
rcons [seq x <- l | index x l < i] (nth x0 l i).
Lemma filter_idx_lt_take :
∀ {T: eqType} (l: seq T) i,
uniq l →
i < size l →
[seq x <- l | index x l < i] = take i l.
Lemma filter_idx_le_takeS :
∀ {T: eqType} (l: seq T) i,
uniq l →
i < size l →
[seq x <- l | index x l ≤ i] = take i.+1 l.
Lemma mapP2 (T: Type) (T': eqType) (s: seq T) (f: T → T') y:
reflect (exists2 x, List.In x s & y = f x) (y \in map f s).
End UniqList.
(* Additional lemmas about list zip. *)
Section Zip.
Lemma zipP {T: eqType} (x0: T) (P: _ → _ → bool) (X Y: seq T):
size X = size Y →
reflect (∀ i, i < size (zip X Y) → P (nth x0 X i) (nth x0 Y i))
(all (fun p ⇒ P (fst p) (snd p)) (zip X Y)).
Lemma mem_zip_exists :
∀ (T T': eqType) (x1: T) (x2: T') l1 l2 elem elem',
size l1 = size l2 →
(x1, x2) \in zip l1 l2 →
∃ idx,
idx < size l1 ∧
idx < size l2 ∧
x1 = nth elem l1 idx ∧
x2 = nth elem' l2 idx.
Lemma mem_zip :
∀ (T T': eqType) (x1: T) (x2: T') l1 l2,
size l1 = size l2 →
(x1, x2) \in zip l1 l2 →
x1 \in l1 ∧ x2 \in l2.
Lemma mem_zip_nseq_r :
∀ {T1 T2:eqType} (x: T1) (y: T2) n l,
size l = n →
((x, y) \in zip l (nseq n y)) = (x \in l).
Lemma mem_zip_nseq_l :
∀ {T1 T2:eqType} (x: T1) (y: T2) n l,
size l = n →
((x, y) \in zip (nseq n x) l) = (y \in l).
Lemma unzip1_pair:
∀ {T1 T2: eqType} (l: seq T1) (f: T1 → T2),
unzip1 [seq (x, f x) | x <- l] = l.
Lemma unzip2_pair:
∀ {T1 T2: eqType} (l: seq T1) (f: T1 → T2),
unzip2 [seq (f x, x) | x <- l] = l.
Lemma eq_unzip1:
∀ {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
size l1 = size l2 →
(∀ i, i < size l1 → (fst (nth x0 l1 i)) = (fst (nth x0 l2 i))) →
unzip1 l1 = unzip1 l2.
Lemma eq_unzip2:
∀ {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
size l1 = size l2 →
(∀ i, i < size l1 → (snd (nth x0 l1 i)) = (snd (nth x0 l2 i))) →
unzip2 l1 = unzip2 l2.
End Zip.
(* Restate nth_error function from Coq library. *)
Fixpoint nth_or_none {T: Type} (l: seq T) (n:nat) {struct n} : option T :=
match n, l with
| 0, x :: _ ⇒ Some x
| n.+1, _ :: l ⇒ nth_or_none l n
| _, _ ⇒ None
end.
(* Lemmas about nth. *)
Section Nth.
Context {T: eqType}.
Lemma nth_in_or_default:
∀ (l: seq T) x0 i,
(nth x0 l i) \in l ∨ (nth x0 l i) = x0.
Lemma nth_neq_default :
∀ (l: seq T) x0 i y,
nth x0 l i = y →
y ≠ x0 →
y \in l.
Lemma nth_or_none_mem :
∀ (l: seq T) n x, nth_or_none l n = Some x → x \in l.
Lemma nth_or_none_mem_exists :
∀ (l: seq T) x, x \in l → ∃ n, nth_or_none l n = Some x.
Lemma nth_or_none_size_none :
∀ (l: seq T) n,
nth_or_none l n = None ↔ n ≥ size l.
Lemma nth_or_none_size_some :
∀ (l: seq T) n x,
nth_or_none l n = Some x → n < size l.
Lemma nth_or_none_uniq :
∀ (l: seq T) i j x,
uniq l →
nth_or_none l i = Some x →
nth_or_none l j = Some x →
i = j.
Lemma nth_or_none_nth :
∀ (l: seq T) n x x0,
nth_or_none l n = Some x →
nth x0 l n = x.
End Nth.
Section PartialMap.
Lemma pmap_inj_in_uniq {T T': eqType} (s: seq T) (f: T → option T') :
{in s &, ssrfun.injective f} →
uniq s →
uniq (pmap f s).
Lemma pmap_inj_uniq {T T': eqType} (s: seq T) (f: T → option T') :
ssrfun.injective f →
uniq s →
uniq (pmap f s).
End PartialMap.
(* Define a set_nth that does not grow the vector. *)
Program Definition set_nth_if_exists {T: Type} (l: seq T) n y :=
if n < size l then
set_nth _ l n y
else l.
(* Define a function that replaces the first element that satisfies
some predicate with using a mapping function f. *)
Fixpoint replace_first {T: Type} P f (l: seq T) :=
if l is x0 :: l' then
if P x0 then
f x0 :: l'
else x0 :: replace_first P f l'
else [::].
(* Define a function that replaces the first element that satisfies
some predicate with a constant. *)
Definition replace_first_const {T: Type} P y (l: seq T) :=
replace_first P (fun x ⇒ y) l.
Definition set_pair_1nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
(fst p, y).
Definition set_pair_2nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
(fst p, y).
Section Replace.
Context {T: eqType}.
Lemma replace_first_size P f (l: seq T) :
size (replace_first P f l) = size l.
Lemma replace_first_cases {P} {f} {l: seq T} {x}:
x \in replace_first P f l →
x \in l ∨ (∃ y, x = f y ∧ P y ∧ y \in l).
Lemma replace_first_no_change {P} {f} {l: seq T} {x}:
x \in l →
~~ P x →
x \in replace_first P f l.
Lemma replace_first_idempotent {P} {f} {l: seq T} {x}:
x \in l →
f x = x →
x \in replace_first P f l.
Lemma replace_first_new :
∀ P f (l: seq T) x1 x2,
x1 \notin l →
x2 \notin l →
x1 \in replace_first P f l →
x2 \in replace_first P f l →
x1 = x2.
Lemma replace_first_previous P f {l: seq T} {x}:
x \in l →
(x \in replace_first P f l) ∨
(P x ∧ f x \in replace_first P f l).
Lemma replace_first_failed P f {l: seq T}:
(∀ x, x \in l → f x \notin replace_first P f l) →
(∀ x, x \in l → ~~ P x).
End Replace.
Definition pairs_to_function {T1: eqType} {T2: Type} y0 (l: seq (T1×T2)) :=
fun x ⇒ nth y0 (unzip2 l) (index x (unzip1 l)).
Section Pairs.
Lemma pairs_to_function_neq_default {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
pairs_to_function y0 l x = y →
y ≠ y0 →
(x,y) \in l.
Lemma pairs_to_function_mem {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
uniq (unzip1 l) →
(x,y) \in l →
pairs_to_function y0 l x = y.
End Pairs.
Section Order.
Context {T: eqType}.
Variable rel: T → T → bool.
Variable l: seq T.
Definition total_over_list :=
∀ x1 x2,
x1 \in l →
x2 \in l →
(rel x1 x2 ∨ rel x2 x1).
Definition antisymmetric_over_list :=
∀ x1 x2,
x1 \in l →
x2 \in l →
rel x1 x2 →
rel x2 x1 →
x1 = x2.
End Order.
(* In this section we prove some additional lemmas about sequences. *)
Section AdditionalLemmas.
(* First, we prove that x ∈ xs implies that xs can be split
into two parts such that xs = xsl ++ ::x ++ xsr. *)
Lemma in_cat:
∀ {X : eqType} (x : X) (xs : list X),
x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.
(* We define a local function max over lists using foldl and maxn. *)
Let max := foldl maxn 0.
(* We prove that max {x, xs} is equal to max {x, max xs}. *)
Lemma seq_max_cons: ∀ x xs, max (x :: xs) = maxn x (max xs).
(* We prove that for any two sequences xs and ys the fact that xs is a subsequence
of ys implies that the size of xs is at most the size of ys. *)
Lemma subseq_leq_size:
∀ {X : eqType} (xs ys: seq X),
uniq xs →
(∀ x, x \in xs → x \in ys) →
size xs ≤ size ys.
End AdditionalLemmas.
Require Import prosa.classic.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* Lemmas about lists without duplicates. *)
Section UniqList.
Lemma idx_lt_rcons :
∀ {T: eqType} (l: seq T) i x0,
uniq l →
i < size l →
[seq x <- l | index x l < i.+1] =
rcons [seq x <- l | index x l < i] (nth x0 l i).
Lemma filter_idx_lt_take :
∀ {T: eqType} (l: seq T) i,
uniq l →
i < size l →
[seq x <- l | index x l < i] = take i l.
Lemma filter_idx_le_takeS :
∀ {T: eqType} (l: seq T) i,
uniq l →
i < size l →
[seq x <- l | index x l ≤ i] = take i.+1 l.
Lemma mapP2 (T: Type) (T': eqType) (s: seq T) (f: T → T') y:
reflect (exists2 x, List.In x s & y = f x) (y \in map f s).
End UniqList.
(* Additional lemmas about list zip. *)
Section Zip.
Lemma zipP {T: eqType} (x0: T) (P: _ → _ → bool) (X Y: seq T):
size X = size Y →
reflect (∀ i, i < size (zip X Y) → P (nth x0 X i) (nth x0 Y i))
(all (fun p ⇒ P (fst p) (snd p)) (zip X Y)).
Lemma mem_zip_exists :
∀ (T T': eqType) (x1: T) (x2: T') l1 l2 elem elem',
size l1 = size l2 →
(x1, x2) \in zip l1 l2 →
∃ idx,
idx < size l1 ∧
idx < size l2 ∧
x1 = nth elem l1 idx ∧
x2 = nth elem' l2 idx.
Lemma mem_zip :
∀ (T T': eqType) (x1: T) (x2: T') l1 l2,
size l1 = size l2 →
(x1, x2) \in zip l1 l2 →
x1 \in l1 ∧ x2 \in l2.
Lemma mem_zip_nseq_r :
∀ {T1 T2:eqType} (x: T1) (y: T2) n l,
size l = n →
((x, y) \in zip l (nseq n y)) = (x \in l).
Lemma mem_zip_nseq_l :
∀ {T1 T2:eqType} (x: T1) (y: T2) n l,
size l = n →
((x, y) \in zip (nseq n x) l) = (y \in l).
Lemma unzip1_pair:
∀ {T1 T2: eqType} (l: seq T1) (f: T1 → T2),
unzip1 [seq (x, f x) | x <- l] = l.
Lemma unzip2_pair:
∀ {T1 T2: eqType} (l: seq T1) (f: T1 → T2),
unzip2 [seq (f x, x) | x <- l] = l.
Lemma eq_unzip1:
∀ {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
size l1 = size l2 →
(∀ i, i < size l1 → (fst (nth x0 l1 i)) = (fst (nth x0 l2 i))) →
unzip1 l1 = unzip1 l2.
Lemma eq_unzip2:
∀ {T1 T2: eqType} (l1 l2: seq (T1 × T2)) x0,
size l1 = size l2 →
(∀ i, i < size l1 → (snd (nth x0 l1 i)) = (snd (nth x0 l2 i))) →
unzip2 l1 = unzip2 l2.
End Zip.
(* Restate nth_error function from Coq library. *)
Fixpoint nth_or_none {T: Type} (l: seq T) (n:nat) {struct n} : option T :=
match n, l with
| 0, x :: _ ⇒ Some x
| n.+1, _ :: l ⇒ nth_or_none l n
| _, _ ⇒ None
end.
(* Lemmas about nth. *)
Section Nth.
Context {T: eqType}.
Lemma nth_in_or_default:
∀ (l: seq T) x0 i,
(nth x0 l i) \in l ∨ (nth x0 l i) = x0.
Lemma nth_neq_default :
∀ (l: seq T) x0 i y,
nth x0 l i = y →
y ≠ x0 →
y \in l.
Lemma nth_or_none_mem :
∀ (l: seq T) n x, nth_or_none l n = Some x → x \in l.
Lemma nth_or_none_mem_exists :
∀ (l: seq T) x, x \in l → ∃ n, nth_or_none l n = Some x.
Lemma nth_or_none_size_none :
∀ (l: seq T) n,
nth_or_none l n = None ↔ n ≥ size l.
Lemma nth_or_none_size_some :
∀ (l: seq T) n x,
nth_or_none l n = Some x → n < size l.
Lemma nth_or_none_uniq :
∀ (l: seq T) i j x,
uniq l →
nth_or_none l i = Some x →
nth_or_none l j = Some x →
i = j.
Lemma nth_or_none_nth :
∀ (l: seq T) n x x0,
nth_or_none l n = Some x →
nth x0 l n = x.
End Nth.
Section PartialMap.
Lemma pmap_inj_in_uniq {T T': eqType} (s: seq T) (f: T → option T') :
{in s &, ssrfun.injective f} →
uniq s →
uniq (pmap f s).
Lemma pmap_inj_uniq {T T': eqType} (s: seq T) (f: T → option T') :
ssrfun.injective f →
uniq s →
uniq (pmap f s).
End PartialMap.
(* Define a set_nth that does not grow the vector. *)
Program Definition set_nth_if_exists {T: Type} (l: seq T) n y :=
if n < size l then
set_nth _ l n y
else l.
(* Define a function that replaces the first element that satisfies
some predicate with using a mapping function f. *)
Fixpoint replace_first {T: Type} P f (l: seq T) :=
if l is x0 :: l' then
if P x0 then
f x0 :: l'
else x0 :: replace_first P f l'
else [::].
(* Define a function that replaces the first element that satisfies
some predicate with a constant. *)
Definition replace_first_const {T: Type} P y (l: seq T) :=
replace_first P (fun x ⇒ y) l.
Definition set_pair_1nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
(fst p, y).
Definition set_pair_2nd {T1: Type} {T2: Type} (y: T2) (p: T1 × T2) :=
(fst p, y).
Section Replace.
Context {T: eqType}.
Lemma replace_first_size P f (l: seq T) :
size (replace_first P f l) = size l.
Lemma replace_first_cases {P} {f} {l: seq T} {x}:
x \in replace_first P f l →
x \in l ∨ (∃ y, x = f y ∧ P y ∧ y \in l).
Lemma replace_first_no_change {P} {f} {l: seq T} {x}:
x \in l →
~~ P x →
x \in replace_first P f l.
Lemma replace_first_idempotent {P} {f} {l: seq T} {x}:
x \in l →
f x = x →
x \in replace_first P f l.
Lemma replace_first_new :
∀ P f (l: seq T) x1 x2,
x1 \notin l →
x2 \notin l →
x1 \in replace_first P f l →
x2 \in replace_first P f l →
x1 = x2.
Lemma replace_first_previous P f {l: seq T} {x}:
x \in l →
(x \in replace_first P f l) ∨
(P x ∧ f x \in replace_first P f l).
Lemma replace_first_failed P f {l: seq T}:
(∀ x, x \in l → f x \notin replace_first P f l) →
(∀ x, x \in l → ~~ P x).
End Replace.
Definition pairs_to_function {T1: eqType} {T2: Type} y0 (l: seq (T1×T2)) :=
fun x ⇒ nth y0 (unzip2 l) (index x (unzip1 l)).
Section Pairs.
Lemma pairs_to_function_neq_default {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
pairs_to_function y0 l x = y →
y ≠ y0 →
(x,y) \in l.
Lemma pairs_to_function_mem {T1: eqType} {T2: eqType} y0 (l: seq (T1×T2)) x y :
uniq (unzip1 l) →
(x,y) \in l →
pairs_to_function y0 l x = y.
End Pairs.
Section Order.
Context {T: eqType}.
Variable rel: T → T → bool.
Variable l: seq T.
Definition total_over_list :=
∀ x1 x2,
x1 \in l →
x2 \in l →
(rel x1 x2 ∨ rel x2 x1).
Definition antisymmetric_over_list :=
∀ x1 x2,
x1 \in l →
x2 \in l →
rel x1 x2 →
rel x2 x1 →
x1 = x2.
End Order.
(* In this section we prove some additional lemmas about sequences. *)
Section AdditionalLemmas.
(* First, we prove that x ∈ xs implies that xs can be split
into two parts such that xs = xsl ++ ::x ++ xsr. *)
Lemma in_cat:
∀ {X : eqType} (x : X) (xs : list X),
x \in xs → ∃ xsl xsr, xs = xsl ++ [::x] ++ xsr.
(* We define a local function max over lists using foldl and maxn. *)
Let max := foldl maxn 0.
(* We prove that max {x, xs} is equal to max {x, max xs}. *)
Lemma seq_max_cons: ∀ x xs, max (x :: xs) = maxn x (max xs).
(* We prove that for any two sequences xs and ys the fact that xs is a subsequence
of ys implies that the size of xs is at most the size of ys. *)
Lemma subseq_leq_size:
∀ {X : eqType} (xs ys: seq X),
uniq xs →
(∀ x, x \in xs → x \in ys) →
size xs ≤ size ys.
End AdditionalLemmas.