Skip to content

Instantly share code, notes, and snippets.

@Agnishom

Agnishom/AwesomeListLemmas.v

Last active April 26, 2024 14:20
Show Gist options
  • Save Agnishom/d686ef345d7c7b408362e1d2c9c64581 to your computer and use it in GitHub Desktop.
Save Agnishom/d686ef345d7c7b408362e1d2c9c64581 to your computer and use it in GitHub Desktop.
Download ZIP
Awesome List Lemmas
Raw
AwesomeListLemmas.v
(*
Some lemmas that can be used in conjunction with those in Coq.Lists.List
See https://coq.inria.fr/library/Coq.Lists.List.html
*)
Require Import Lia.
Require Import Coq.Lists.List.
Require Import Coq.Arith.Wf_nat.
Require Import Arith.
Import ListNotations.
(* In *)
Lemma In_singleton_refl {X : Type} : forall (x : X),
In x [x].
Proof.
intros. left. auto.
Qed.
Lemma In_singleton {X : Type} : forall (x y : X),
In x [y] <-> x = y.
Proof.
intros. split; intros.
- destruct H; auto. destruct H.
- subst. left. auto.
Qed.
(* nilb *)
Definition nilb {A : Type} (l : list A) : bool :=
match l with
| [] => true
| _ => false
end.
Lemma nilb_true {A : Type} : forall (l : list A),
nilb l = true <-> l = [].
Proof.
intros. destruct l; split; intros; auto; discriminate.
Qed.
Lemma nilb_false {A : Type} : forall (l : list A),
nilb l = false <-> l <> [].
Proof.
intros l. split.
- intros Hnilb Hl.
subst l. simpl in Hnilb. discriminate.
- intros Hl.
destruct l; [ contradiction | auto].
Qed.
(* firstn / skipn / nth_error / map / combine *)
Lemma skipn_skipn {B : Type}: forall n m (l : list B),
skipn n (skipn m l) = skipn (n + m) l.
Proof.
intros n m l. generalize dependent n. generalize dependent l.
induction m as [|m' IHm'].
- simpl. intros. replace (n + 0) with n by lia. reflexivity.
- intros l n. destruct l as [|h t].
+ simpl. repeat rewrite skipn_nil. reflexivity.
+ simpl. destruct n as [|n'].
* reflexivity.
* rewrite IHm'. simpl plus.
replace (n' + S m') with (S (n' + m')) by lia.
reflexivity.
Qed.
Lemma nth_error_skipn {X} : forall (xs : list X) i d,
nth_error xs (i + d) = nth_error (skipn d xs) i.
Proof.
intros.
rewrite <- firstn_skipn with (n := d) (l := xs) at 1.
assert (d < length xs \/ d >= length xs) as Hxs by lia.
destruct Hxs.
- rewrite nth_error_app2.
+ rewrite firstn_length.
f_equal. lia.
+ rewrite firstn_length.
lia.
- rewrite firstn_all2 by lia.
rewrite skipn_all2 by lia.
rewrite app_nil_r.
replace (nth_error (@nil X) i) with (@None X)
by now destruct i.
replace (nth_error xs (i + d)) with (@None X).
auto.
symmetry. apply nth_error_None. lia.
Qed.
Lemma nth_error_firstn {X : Type} (l : list X) : forall d i,
i < d
-> nth_error (firstn d l) i = nth_error l i.
Proof.
intros d i Hdi.
assert (d <= length l \/ d > length l) as [Hdl | Hdl] by lia.
+ rewrite <- firstn_skipn with (l := l) (n := d) at 2.
rewrite nth_error_app1. auto.
rewrite firstn_length. lia.
+ now rewrite firstn_all2 by lia.
Qed.
Lemma firstn_In {X : Type} : forall (l : list X) n,
forall x, In x (firstn n l) -> In x l.
Proof.
intros.
rewrite <- (firstn_skipn n l) at 1.
apply in_or_app. auto.
Qed.
Lemma skipn_In {X : Type} : forall (l : list X) n,
forall x, In x (skipn n l) -> In x l.
Proof.
intros.
rewrite <- (firstn_skipn n l) at 1.
apply in_or_app. auto.
Qed.
Lemma hd_error_skipn {X : Type} (l : list X) : forall i,
hd_error (skipn i l) = nth_error l i.
Proof.
intro i.
generalize dependent l. induction i.
- intro. rewrite skipn_O. destruct l; auto.
- intro. destruct l; auto.
simpl. auto.
Qed.
Lemma hd_error_snoc_snoc {X : Type} (l : list X) (x1 x2 : X) :
hd_error ((l ++ [x1]) ++ [x2]) = hd_error (l ++ [x1]).
Proof.
destruct l; auto.
Qed.
Lemma hd_error_nth_error {X : Type} (l : list X) :
hd_error l = nth_error l 0.
Proof.
destruct l; auto.
Qed.
Lemma nth_error_rev {X : Type} (l : list X) (n : nat) :
n < length l ->
nth_error (rev l) n = nth_error l (length l - S n).
Proof.
destruct l.
- simpl. destruct n; reflexivity.
- intros. remember (x :: l) as l'.
rewrite nth_error_nth' with (d := x).
rewrite nth_error_nth' with (d := x).
f_equal. apply rev_nth.
auto. lia. auto.
rewrite rev_length. auto.
Qed.
Lemma nth_error_Some_ex {X : Type} (l : list X) (n : nat) :
n < length l <->
exists x, nth_error l n = Some x.
Proof.
split.
- intros. destruct (nth_error l n) eqn:Hnth.
+ exists x. auto.
+ apply nth_error_None in Hnth. lia.
- intros [x Hnth]. apply nth_error_Some. congruence.
Qed.
Lemma skipn_succ_nth_error {X : Type} (l : list X) (n : nat) :
forall x,
nth_error l n = Some x ->
skipn n l = x :: skipn (S n) l.
Proof.
intros.
replace l with (firstn n l ++ skipn n l) at 1 by now rewrite firstn_skipn.
destruct (skipn n l) eqn:Hskipn.
1 : { specialize (hd_error_skipn l n) as Hhd.
rewrite Hskipn in Hhd. simpl in Hhd. congruence. }
specialize (hd_error_skipn l n) as Hhd.
rewrite Hskipn in Hhd. simpl in Hhd.
replace x0 with x in * by congruence.
clear Hhd.
rewrite skipn_app.
rewrite skipn_firstn_comm.
rewrite firstn_length.
assert (n < length l).
{ rewrite nth_error_Some_ex. now exists x. }
replace (min n (length l)) with n by lia.
replace (n - n) with 0 by lia.
simpl firstn.
rewrite skipn_O. simpl app.
f_equal.
replace (S n) with (1 + n) by lia.
rewrite <- skipn_skipn.
rewrite Hskipn.
reflexivity.
Qed.
Lemma firstn_eq {X : Type} (l1 l2 : list X) (n1 n2 : nat) :
firstn n1 l1 = firstn n2 l2
-> (n1 < length l1 /\ n2 < length l2 /\ n1 = n2)
\/ (n1 >= length l1 /\ length l1 <= length l2 /\ n2 <= n1)
\/ (n2 >= length l2 /\ length l2 <= length l1 /\ n1 <= n2).
Proof.
intros.
assert (n1 < length l1 \/ n1 >= length l1) as [Hn1 | Hn1] by lia.
- assert (n2 < length l2 \/ n2 >= length l2) as [Hn2 | Hn2] by lia.
+ left. split; [| split]; auto.
apply f_equal with (f := @length X) in H.
repeat rewrite firstn_length in H. lia.
+ rewrite -> firstn_all2 with (n := n2) in H by assumption.
apply f_equal with (f := @length X) in H.
rewrite firstn_length in H. lia.
- assert (length l1 <= length l2 \/ length l1 > length l2) as [Hl1 | Hl1] by lia.
+ rewrite -> firstn_all2 with (n := n1) in H by assumption.
apply f_equal with (f := @length X) in H.
rewrite firstn_length in H. lia.
+ right. left. split; [| split]; auto.
* apply f_equal with (f := @length X) in H.
repeat rewrite firstn_length in H. lia.
* rewrite -> firstn_all2 with (n := n1) in H by assumption.
apply f_equal with (f := @length X) in H.
rewrite firstn_length in H. lia.
Qed.
Lemma skipn_eq {X : Type} (l1 l2 : list X) (n1 n2 : nat) :
skipn n1 l1 = skipn n2 l2
-> (n1 < length l1 /\ n2 < length l2 /\ length l1 - n1 = length l2 - n2)
\/ (n1 >= length l1 /\ n2 >= length l2)
.
Proof.
intros Hskipn.
assert (n1 < length l1 \/ n1 >= length l1) as [Hn1 | Hn1] by lia.
- assert (n2 < length l2 \/ n2 >= length l2) as [Hn2 | Hn2] by lia.
+ left. split; [| split]; auto.
apply f_equal with (f := @length X) in Hskipn.
repeat rewrite skipn_length in Hskipn. lia.
+ rewrite -> skipn_all2 with (n := n2) in Hskipn by assumption.
apply f_equal with (f := @length X) in Hskipn.
rewrite skipn_length in Hskipn. simpl in Hskipn.
lia.
- right.
apply f_equal with (f := @length X) in Hskipn.
repeat rewrite skipn_length in Hskipn. simpl in Hskipn.
lia.
Qed.
Lemma firstn_eq_slice {X : Type} (l1 l2 : list X) (n n' : nat) :
firstn n l1 = firstn n l2
-> n' <= n
-> firstn n' l1 = firstn n' l2.
Proof.
intros Hf Hn.
assert (n >= length l1 \/ n < length l1) as [Hn1 | Hn1] by lia;
assert (n >= length l2 \/ n < length l2) as [Hn2 | Hn2] by lia.
1, 2: rewrite -> firstn_all2 with (l := l1) in Hf by assumption.
3: rewrite -> firstn_all2 with (l := l2) in Hf by assumption.
+ rewrite -> firstn_all2 with (n := n) in Hf by lia. congruence.
+ subst l1. rewrite firstn_firstn. rewrite Nat.min_l by lia. auto.
+ subst l2. rewrite firstn_firstn. rewrite Nat.min_l by lia. auto.
+ apply f_equal with (f := firstn n') in Hf.
repeat rewrite -> firstn_firstn in Hf.
now replace (min n' n) with n' in Hf by lia.
Qed.
Lemma skipn_eq_slice {X : Type} (l1 l2 : list X) (n n' : nat) :
skipn n l1 = skipn n l2
-> n' >= n
-> skipn n' l1 = skipn n' l2.
Proof.
intros Hf Hn.
assert (n >= length l1 \/ n < length l1) as [Hn1 | Hn1] by lia;
assert (n >= length l2 \/ n < length l2) as [Hn2 | Hn2] by lia.
1, 2: rewrite -> skipn_all2 by lia.
3: rewrite -> skipn_all2 with (l := l2) by lia.
+ now rewrite -> skipn_all2 with (n := n') by lia.
+ rewrite skipn_all2 in Hf by lia.
apply f_equal with (f := @length X) in Hf.
rewrite skipn_length in Hf. simpl in Hf.
now rewrite skipn_all2 by lia.
+ rewrite skipn_all2 with (l := l2) in Hf by lia.
apply f_equal with (f := @length X) in Hf.
rewrite skipn_length in Hf. simpl in Hf.
now rewrite skipn_all2 by lia.
+ apply f_equal with (f := skipn (n' - n)) in Hf.
repeat rewrite -> skipn_skipn in Hf.
now replace (n' - n + n) with n' in Hf by lia.
Qed.
Lemma app_inv_head_length {X : Type} (l1 l2 l1' l2' : list X) :
l1 ++ l2 = l1' ++ l2'
-> length l1 = length l1'
-> l1 = l1' /\ l2 = l2'.
Proof.
intros.
enough (l1 = l1'). {
subst l1'. apply app_inv_head in H. auto.
}
apply f_equal with (f := @firstn X (length l1)) in H.
repeat rewrite -> firstn_app in H.
replace (length l1 - length l1) with 0 in H by lia.
replace (length l1 - length l1') with 0 in H by lia.
repeat rewrite firstn_O in H. repeat rewrite app_nil_r in H.
rewrite firstn_all in H. rewrite firstn_all2 in H by lia.
auto.
Qed.
Lemma app_inv_tail_length {X : Type} (l1 l2 l1' l2' : list X) :
l1 ++ l2 = l1' ++ l2'
-> length l2 = length l2'
-> l1 = l1' /\ l2 = l2'.
Proof.
intros.
apply f_equal with (f := @rev X) in H.
repeat rewrite rev_app_distr in H.
assert (length (rev l2) = length (rev l2')) as Hlen. {
now repeat rewrite rev_length.
}
apply app_inv_head_length in H. 2 : { auto. }
destruct H.
apply f_equal with (f := @rev X) in H. repeat rewrite rev_involutive in H.
apply f_equal with (f := @rev X) in H1. repeat rewrite rev_involutive in H1.
auto.
Qed.
Lemma skipn_tl {X : Type} (l : list X) :
skipn 1 l = tl l.
Proof.
destruct l; auto.
Qed.
Lemma map_id {X} : forall (xs : list X),
map id xs = xs.
Proof.
induction xs; auto.
simpl. rewrite IHxs. auto.
Qed.
Inductive Forall2 {A B} (P : A -> B -> Prop) : list A -> list B -> Prop :=
| Forall2_nil : Forall2 P [] []
| Forall2_cons : forall x y xs ys,
P x y -> Forall2 P xs ys -> Forall2 P (x :: xs) (y :: ys).
Lemma Forall2_refl {X} (P : X -> X -> Prop) : forall xs,
(forall x, In x xs -> P x x) -> Forall2 P xs xs.
Proof.
intros xs H.
induction xs.
- constructor.
- constructor.
+ apply H. now left.
+ apply IHxs. intros x Hin. apply H. now right.
Qed.
Lemma combine_map {X Y M N} : forall (f : X -> M) (g : Y -> N) xs ys,
combine (map f xs) (map g ys) = map (fun '(x, y) => (f x, g y)) (combine xs ys).
Proof.
induction xs.
- auto.
- intros. destruct ys.
+ simpl. auto.
+ simpl. rewrite IHxs. auto.
Qed.
Lemma combine_app {X Y} : forall (xs1 xs2 : list X) (ys1 ys2 : list Y),
length xs1 = length ys1
-> combine (xs1 ++ xs2) (ys1 ++ ys2) = combine xs1 ys1 ++ combine xs2 ys2.
Proof.
intros.
revert ys1 H.
induction xs1.
- intros. destruct ys1. auto. simpl in H. discriminate.
- intros. destruct ys1. simpl in H. discriminate.
simpl. rewrite IHxs1. auto.
simpl in H. inversion H. auto.
Qed.
Lemma combine_rev {X Y} : forall (xs : list X) (ys : list Y),
length xs = length ys
-> combine (rev xs) (rev ys) = rev (combine xs ys).
Proof.
intros.
revert ys H.
induction xs.
- intros. destruct ys. auto. simpl in H. discriminate.
- intros. destruct ys. simpl in H. discriminate.
simpl. simpl in H. inversion H.
rewrite combine_app. simpl. rewrite IHxs. auto.
auto.
repeat rewrite rev_length. auto.
Qed.
Lemma Forall2_length {X Y} (P : X -> Y -> Prop) (xs : list X) (ys : list Y) :
Forall2 P xs ys -> length xs = length ys.
Proof.
intros H. induction H; simpl; auto.
Qed.
Lemma Forall2_In_combine {X Y} (P : X -> Y -> Prop) (xs : list X) (ys : list Y) :
Forall2 P xs ys -> forall x y, In (x, y) (combine xs ys) -> P x y.
Proof.
intros H.
induction H.
- intros. contradiction.
- intros xx yy Hin. destruct Hin.
+ inversion H1. subst. auto.
+ apply IHForall2. auto.
Qed.
Lemma In_combine_Forall2 {X Y} (P : X -> Y -> Prop) (xs : list X) (ys : list Y) :
length xs = length ys
-> (forall x y, In (x, y) (combine xs ys) -> P x y)
-> Forall2 P xs ys.
Proof.
remember (length xs) as n.
revert xs ys Heqn.
induction n.
- intros. destruct xs; destruct ys; auto.
2, 3, 4 : simpl in Heqn, H; discriminate.
constructor.
- intros. destruct xs; destruct ys; simpl in Heqn; try discriminate.
simpl in H. inversion Heqn. inversion H.
specialize (IHn xs ys H2 H3).
constructor.
+ apply H0. simpl. auto.
+ apply IHn. intros. apply H0. simpl. auto.
Qed.
Lemma Forall2_In_combine_iff {X Y} (P : X -> Y -> Prop) : forall (xs : list X) (ys : list Y),
Forall2 P xs ys <->
(length xs = length ys /\
(forall x y, In (x, y) (combine xs ys) -> P x y)).
Proof.
intros. split.
- intros H. split.
+ apply Forall2_length in H. auto.
+ intros. eapply Forall2_In_combine in H; eauto.
- intros [Hlen H]. apply In_combine_Forall2; auto.
Qed.
Lemma Forall2_hd {X Y} (P : X -> Y -> Prop) : forall x y xs ys,
Forall2 P (x :: xs) (y :: ys) -> P x y.
Proof.
intros. inversion H; subst. auto.
Qed.
Lemma Forall2_uncons {X Y} (P : X -> Y -> Prop) : forall x y xs ys,
Forall2 P (x :: xs) (y :: ys) -> Forall2 P xs ys.
Proof.
intros. inversion H; subst. auto.
Qed.
Lemma Forall2_app {X Y} (P : X -> Y -> Prop) : forall xs1 xs2 ys1 ys2,
Forall2 P xs1 ys1 -> Forall2 P xs2 ys2 -> Forall2 P (xs1 ++ xs2) (ys1 ++ ys2).
Proof.
intros xs1 xs2 ys1 ys2 H1.
revert xs2 ys2.
induction H1; intros xs2 ys2 H2.
- simpl. auto.
- simpl. constructor; auto.
Qed.
Lemma Forall2_snoc {X Y} (P : X -> Y -> Prop) : forall xs ys x y,
Forall2 P xs ys -> P x y -> Forall2 P (xs ++ [x]) (ys ++ [y]).
Proof.
intros xs ys x y H1 H2.
apply Forall2_app; auto.
constructor.
- assumption.
- constructor.
Qed.
Lemma Forall2_flip {X Y} (P : X -> Y -> Prop) : forall xs ys,
Forall2 P xs ys -> Forall2 (fun y x => P x y) ys xs.
Proof.
intros; induction H; constructor; auto.
Qed.
Lemma Forall2_map {X1 X2 Y1 Y2} (P : X1 -> Y1 -> Prop) (Q : X2 -> Y2 -> Prop)
(f : X1 -> X2) (g : Y1 -> Y2) :
(forall x y, P x y -> Q (f x) (g y)) ->
forall xs ys, Forall2 P xs ys -> Forall2 Q (map f xs) (map g ys).
Proof.
intros.
induction H0.
- constructor.
- simpl. constructor; auto.
Qed.
Lemma Forall2_Forall_and {X Y} (P : X -> Y -> Prop) (Q : X -> Prop) : forall xs ys,
Forall2 P xs ys
-> Forall Q xs
-> Forall2 (fun x y => P x y /\ Q x) xs ys.
Proof.
induction xs.
- intros. inversion H. constructor.
- intros. inversion H; subst. constructor.
+ inversion H0; inversion H; auto.
+ apply IHxs; inversion H0; auto.
Qed.
Lemma Forall2_Forall_and' {X Y} (P : X -> Y -> Prop) (Q : Y -> Prop) : forall xs ys,
Forall2 P xs ys
-> Forall Q ys
-> Forall2 (fun x y => P x y /\ Q y) xs ys.
Proof.
induction xs.
- intros. inversion H. constructor.
- intros. inversion H; subst. constructor.
+ inversion H0; inversion H; auto.
+ apply IHxs; inversion H0; auto.
Qed.
Lemma Forall2_In_l {X Y} (P : X -> Y -> Prop) : forall xs ys x,
Forall2 P xs ys
-> In x xs
-> exists y, In y ys /\ P x y.
Proof.
intros.
induction H.
- contradiction.
- destruct H0.
+ subst. exists y. split; [ left | ]; auto.
+ specialize (IHForall2 H0). destruct IHForall2 as [y' [Hin HP]].
exists y'. split; [ right | ]; auto.
Qed.
Lemma Forall2_In_r {X Y} (P : X -> Y -> Prop) : forall xs ys y,
Forall2 P xs ys
-> In y ys
-> exists x, In x xs /\ P x y.
Proof.
intros.
induction H.
- contradiction.
- destruct H0.
+ subst. exists x. split; [ left | ]; auto.
+ specialize (IHForall2 H0). destruct IHForall2 as [x' [Hin HP]].
exists x'. split; [ right | ]; auto.
Qed.
Lemma map_repeat {X Y : Type} (f : X -> Y) (x : X) n :
map f (repeat x n) = repeat (f x) n.
Proof.
induction n; auto.
simpl. rewrite IHn. auto.
Qed.
Lemma concat_repeat_nil {X : Type} : forall n,
concat (repeat (@nil X) n) = [].
Proof.
induction n; auto.
Qed.
Lemma repeat_iff {X : Type} (x : X) l:
l = repeat x (length l) <-> (forall y, In y l -> y = x).
Proof.
split.
- intros. rewrite H in H0.
apply repeat_spec in H0. auto.
- intros. apply Forall_eq_repeat.
apply Forall_forall. firstorder.
Qed.
Lemma map_ext_combine {X Y Z} (f : X -> Z) (g : Y -> Z) :
forall xs ys,
length xs = length ys
-> (forall x y, In (x, y) (combine xs ys) -> f x = g y)
-> map f xs = map g ys.
Proof.
intros xs ys Hlen Hext.
induction xs as [|x xs IHxs] in ys, Hlen, Hext |- *.
- destruct ys; auto. simpl in Hlen. discriminate.
- destruct ys as [|y ys]; auto. simpl in Hlen. discriminate.
simpl. f_equal.
+ specialize (Hext x y) as Hext'.
apply Hext'. now left.
+ apply IHxs. simpl in Hlen. lia.
intros x' y' Hin. apply Hext. now right.
Qed.
Lemma nth_error_combine {X Y} : forall (xs : list X) (ys : list Y),
forall i, nth_error (combine xs ys) i =
match nth_error xs i, nth_error ys i with
| Some x, Some y => Some (x, y)
| _, _ => None
end.
Proof.
induction xs as [|x xs IHxs].
- intros ys i. simpl. destruct i; auto.
- intros ys [|i].
+ destruct ys; auto.
+ destruct ys.
* simpl. destruct (nth_error xs i); auto.
* simpl. apply IHxs.
Qed.
Lemma nth_error_combine_Some {X Y} :
forall (xs : list X) (ys : list Y) x y i,
nth_error xs i = Some x
-> nth_error ys i = Some y
-> nth_error (combine xs ys) i = Some (x, y).
Proof.
intros xs ys x y i Hx Hy.
rewrite nth_error_combine.
rewrite Hx, Hy. auto.
Qed.
Lemma nth_error_In_combine {X Y} : forall (xs : list X) (ys : list Y) x y,
In (x, y) (combine xs ys) <->
(exists i,
nth_error xs i = Some x /\ nth_error ys i = Some y).
Proof.
split; intros.
- apply In_nth_error in H. destruct H as [i Hi].
rewrite nth_error_combine in Hi.
destruct (nth_error xs i) eqn:Hx; destruct (nth_error ys i) eqn:Hy; try discriminate.
inversion Hi; subst. clear Hi. eauto.
- destruct H as [i [Hx Hy]].
pose proof (nth_error_combine_Some xs ys x y i Hx Hy) as Hxy.
now apply nth_error_In in Hxy.
Qed.
(* zipWith *)
Definition zipWith {X Y Z} (f : X -> Y -> Z) (xs : list X) (ys : list Y) : list Z :=
map (fun '(x, y) => f x y) (combine xs ys).
Lemma zipWith_length {X Y Z} : forall (f : X -> Y -> Z) xs ys,
length (zipWith f xs ys) = min (length xs) (length ys).
Proof.
intros. unfold zipWith.
now rewrite map_length, combine_length.
Qed.
Lemma zipWith_In {X Y Z} : forall (P : X -> Prop) (Q : Y -> Prop) (R : Z -> Prop) (f : X -> Y -> Z) xs ys,
(forall x, In x xs -> P x)
-> (forall y, In y ys -> Q y)
-> (forall x y, P x -> Q y -> R (f x y))
-> forall z, In z (zipWith f xs ys) -> R z.
Proof.
intros P Q R f.
induction xs; intros ys Hxs Hys Hf z Hz.
- simpl in Hz. inversion Hz.
- simpl in Hz. destruct ys.
+ inversion Hz.
+ destruct Hz.
* subst. apply Hf.
apply Hxs. now left.
apply Hys. now left.
* rewrite in_map_iff in H.
destruct H as [[xx yy] [H1 H2]].
subst. apply Hf.
apply Hxs. right.
now apply in_combine_l in H2.
apply Hys. right.
now apply in_combine_r in H2.
Qed.
Lemma nth_error_zipWith {X Y Z} : forall (f : X -> Y -> Z) xs ys n,
nth_error (zipWith f xs ys) n =
match nth_error xs n, nth_error ys n with
| Some x, Some y => Some (f x y)
| _, _ => None
end.
Proof.
intros f. induction xs.
- intros ys n.
assert (zipWith f [] ys = []). {
unfold zipWith. destruct ys; auto.
}
rewrite H.
remember (nth_error [] n) as nz.
assert (nz = None). {
subst. destruct n; auto.
}
remember (nth_error (@nil X) n) as nx.
assert (nx = None). {
subst. destruct n; auto.
}
rewrite H0, H1. auto.
- intros. destruct n.
+ simpl. destruct ys.
* auto.
* simpl. auto.
+ destruct ys.
* simpl. destruct (nth_error xs n); auto.
* simpl.
rewrite <- IHxs.
auto.
Qed.
Lemma zipWith_cons {X Y Z} : forall (f : X -> Y -> Z) x xs y ys,
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys.
Proof.
auto.
Qed.
Lemma zipWith_repeat_l {X Y Z} : forall n (f : X -> Y -> Z) x ys,
n >= length ys
-> zipWith f (repeat x n) ys = map (f x) ys.
Proof.
induction n.
- intros. simpl. destruct ys; [auto | simpl in H; lia].
- intros. destruct ys.
+ simpl. auto.
+ simpl. rewrite zipWith_cons.
rewrite IHn. auto.
simpl in H. lia.
Qed.
Lemma zipWith_repeat_r {X Y Z} : forall n (f : X -> Y -> Z) xs y,
n >= length xs
-> zipWith f xs (repeat y n) = map (fun x => f x y) xs.
Proof.
induction n.
- intros. simpl. destruct xs; [auto | simpl in H; lia].
- intros. destruct xs.
+ simpl. auto.
+ simpl. rewrite zipWith_cons.
rewrite IHn. auto.
simpl in H. lia.
Qed.
Lemma zipWith_firstn_l {X Y Z} : forall (f : X -> Y -> Z) xs ys,
zipWith f xs ys = zipWith f xs (firstn (length xs) ys).
Proof.
unfold zipWith. intros. rewrite combine_firstn_l. auto.
Qed.
Lemma zipWith_firstn_r {X Y Z} : forall (f : X -> Y -> Z) xs ys,
zipWith f xs ys = zipWith f (firstn (length ys) xs) ys.
Proof.
unfold zipWith. intros. rewrite combine_firstn_r. auto.
Qed.
Lemma zipWith_firstn {X Y Z} : forall (f : X -> Y -> Z) xs ys,
zipWith f xs ys =
let n := (min (length xs) (length ys)) in
zipWith f (firstn n xs) (firstn n ys).
Proof.
intros.
assert (length xs <= length ys \/ length xs > length ys) as [H | H] by lia.
- replace (min (length xs) (length ys)) with (length xs) by lia.
simpl.
assert (zipWith f xs ys = zipWith f xs (firstn (length xs) ys)) as H1.
{ apply zipWith_firstn_l. }
assert (zipWith f xs (firstn (length xs) ys) =
zipWith f (firstn (length xs) xs) (firstn (length xs) ys)) as H3.
{ f_equal. now rewrite firstn_all. }
congruence.
- replace (min (length xs) (length ys)) with (length ys) by lia.
simpl.
assert (zipWith f xs ys = zipWith f (firstn (length ys) xs) ys) as H1.
{ apply zipWith_firstn_r. }
assert (zipWith f (firstn (length ys) xs) ys =
zipWith f (firstn (length ys) xs) (firstn (length ys) ys)) as H3.
{ f_equal. now rewrite firstn_all. }
congruence.
Qed.
Lemma zipWith_map { M N X Y Z }: forall (f : M -> N -> Z) (g : X -> M) (h : Y -> N) (xs : list X) (ys : list Y),
zipWith f (map g xs) (map h ys) = map (fun '(x, y) => f (g x) (h y)) (combine xs ys).
Proof.
intros. unfold zipWith.
rewrite combine_map. rewrite map_map.
apply map_ext. intros. destruct a. auto.
Qed.
Lemma zipWith_assoc {X}: forall (f : X -> X -> X) xs ys zs,
(forall x y z, f x (f y z) = f (f x y) z)
-> zipWith f xs (zipWith f ys zs) = zipWith f (zipWith f xs ys) zs.
Proof.
intros f xs.
remember (length xs) as len.
generalize dependent xs.
induction len.
- intros. destruct xs. auto. simpl in Heqlen. discriminate.
- intros. destruct xs.
+ auto.
+ destruct ys.
* auto.
* destruct zs.
-- auto.
-- simpl. repeat rewrite zipWith_cons.
rewrite H. rewrite IHlen.
++ auto.
++ simpl in Heqlen. inversion Heqlen. auto.
++ apply H.
Qed.
Lemma zipWith_ext { X Y Z M N } : forall (f : X -> Y -> Z) (g : M -> N -> Z) xs ys ms ns,
(forall x y m n, In ((x, y), (m, n)) (combine (combine xs ys) (combine ms ns)) -> f x y = g m n)
-> length xs = length ms
-> length ys = length ns
-> zipWith f xs ys = zipWith g ms ns.
Proof.
intros f g xs.
remember (length xs) as len.
generalize dependent xs.
induction len.
- intros. destruct xs. destruct ms. auto.
simpl in H0. discriminate. simpl in H0. discriminate.
- intros. destruct xs. {
simpl in Heqlen. discriminate.
} destruct ms. {
simpl in Heqlen. discriminate.
} destruct ys. {
simpl in H1. simpl in H0.
destruct ns. auto. simpl in H1. discriminate.
} destruct ns. {
simpl in H1. discriminate.
}
rewrite zipWith_cons. rewrite zipWith_cons.
simpl in H. f_equal.
+ apply H. auto.
+ apply IHlen.
1 : { simpl in Heqlen. inversion Heqlen. auto. }
3 : { simpl in H1. inversion H1. auto. }
2 : { simpl in H. firstorder. }
firstorder.
Qed.
Lemma zipWith_cons_singleton {X} : forall (xs : list X) (xss : list (list X)),
zipWith cons xs xss = zipWith (@app X) (map (fun x => [x]) xs) xss.
Proof.
intros.
apply zipWith_ext.
2 : { now rewrite map_length. }
2 : { auto. }
revert xss.
induction xs.
- intros. simpl in H. tauto.
- intros. destruct xss.
+ simpl in H. tauto.
+ simpl in H. destruct H.
* inversion H. auto.
* eapply IHxs. eauto.
Qed.
Lemma zipWith_rev {X Y Z} : forall (f : X -> Y -> Z) xs ys,
length xs = length ys
-> zipWith f (rev xs) (rev ys) = rev (zipWith f xs ys).
Proof.
intros. unfold zipWith.
rewrite combine_rev by assumption.
apply map_rev.
Qed.
Lemma zipWith_map2 {X Y Z W : Type} (f : X -> Y -> Z) (g : Z -> W) (xs : list X) (ys : list Y) :
map g (zipWith f xs ys) = zipWith (fun x y => g (f x y)) xs ys.
Proof.
unfold zipWith at 2.
replace (map (fun '(x, y) => g (f x y)) (combine xs ys))
with (map g (map (fun '(x, y) => f x y) (combine xs ys))). 2: {
rewrite map_map. apply map_ext_in. intros [x y]. auto.
}
auto.
Qed.
Lemma zipWith_ext_id_l {X Y : Type} (f : X -> Y -> X) (xs : list X) (ys : list Y) :
(forall x y, In (x, y) (combine xs ys) -> f x y = x)
-> length xs <= length ys
-> zipWith f xs ys = xs.
Proof.
remember (length xs) as len.
generalize dependent xs.
generalize dependent ys.
induction len.
- intros. destruct xs; destruct ys; auto.
simpl in Heqlen. discriminate.
simpl in H0. discriminate.
- intros. destruct xs; destruct ys; auto.
+ simpl in H0. lia.
+ simpl in H. rewrite zipWith_cons.
f_equal.
* specialize (H x y). auto.
* apply IHlen.
simpl in Heqlen. lia.
intros. apply H. auto.
simpl in H0. lia.
Qed.
Lemma zipWith_ext_id_r {X Y : Type} (f : X -> Y -> Y) (xs : list X) (ys : list Y) :
(forall x y, In (x, y) (combine xs ys) -> f x y = y)
-> length xs >= length ys
-> zipWith f xs ys = ys.
Proof.
remember (length xs) as len.
generalize dependent xs.
generalize dependent ys.
induction len.
- intros. destruct xs; destruct ys; auto.
simpl in H0. lia.
simpl in H0. discriminate.
- intros. destruct xs; destruct ys; auto.
+ simpl in H0. discriminate.
+ simpl in H. rewrite zipWith_cons.
f_equal.
* specialize (H x y). auto.
* apply IHlen.
simpl in Heqlen. lia.
intros. apply H. auto.
simpl in H0. lia.
Qed.
(* transpose *)
Fixpoint transpose {X : Type} (len : nat) (tapes : list (list X)) : list (list X) :=
match tapes with
| [] => repeat [] len
| t :: ts => zipWith cons t (transpose len ts)
end.
Lemma transpose_length {X : Type} : forall len (tapes : list (list X)),
(forall t,
In t tapes -> length t >= len)
-> length (transpose len tapes) = len.
Proof.
intros len tapes. revert len.
induction tapes; intros len Hlen.
- simpl. now rewrite repeat_length.
- simpl. rewrite zipWith_length.
rewrite IHtapes.
+ simpl in Hlen. specialize (Hlen a).
assert (length a >= len) by auto.
lia.
+ intros t Ht. apply Hlen. now right.
Qed.
Lemma transpose_inner_length {X : Type}: forall len (tapes : list (list X)),
forall u,
In u (transpose len tapes)
-> length u = length tapes.
Proof.
intros len tapes. revert len.
induction tapes; intros len u Hu.
- simpl in *. apply repeat_spec in Hu.
subst. auto.
- simpl in *.
unfold zipWith in Hu.
rewrite in_map_iff in Hu.
destruct Hu as [[u1 us] [Hu Hus]].
apply in_combine_r in Hus.
subst. simpl. f_equal.
firstorder.
Qed.
Lemma transpose_inner_length_eq {X : Type} : forall len (tapes : list (list X)),
forall u v,
In u (transpose len tapes)
-> In v (transpose len tapes)
-> length u = length v.
Proof.
intros.
apply transpose_inner_length in H.
apply transpose_inner_length in H0.
congruence.
Qed.
Lemma transpose_app {X : Type} : forall len (tapes1 tapes2 : list (list X)),
(forall t, In t tapes1 -> length t >= len)
-> (forall t, In t tapes2 -> length t >= len)
-> transpose len (tapes1 ++ tapes2) =
zipWith (@app X) (transpose len tapes1) (transpose len tapes2).
Proof.
intros len tapes1 tapes2 Ht1 Ht2.
induction tapes1.
- simpl.
rewrite zipWith_repeat_l.
rewrite <- map_id with (xs := transpose _ _) at 1.
apply map_ext. auto.
rewrite transpose_length. auto. auto.
- simpl. rewrite IHtapes1.
+ rewrite zipWith_cons_singleton.
rewrite zipWith_cons_singleton.
rewrite zipWith_assoc by apply app_assoc.
auto.
+ simpl in Ht1. firstorder.
Qed.
Lemma transpose_singleton {X : Type} : forall (t : list X),
transpose (length t) [t] = map (fun x => [x]) t.
Proof.
intros. unfold transpose.
now rewrite zipWith_repeat_r by lia.
Qed.
Lemma transpose_rev_aux {X : Type} : forall (xss : list (list X)) (l : list X),
(forall t u, In t xss -> In u xss -> length t = length u)
-> zipWith (@app X) (map (@rev X) xss) (map (fun x => [x]) l)
= map (@rev X) (zipWith (@app X) (map (fun x => [x]) l) xss).
Proof.
induction xss as [ | xs xss].
- intros. simpl.
destruct l.
+ auto.
+ simpl. unfold zipWith. auto.
- intros. destruct l.
+ simpl. unfold zipWith. auto.
+ simpl map at 1 2. rewrite zipWith_cons.
simpl map at 3. f_equal.
rewrite IHxss. auto.
simpl in H. firstorder.
Qed.
Lemma transpose_rev {X : Type} : forall len (tapes : list (list X)),
(forall t, In t tapes -> length t = len)
-> transpose len (rev tapes) = map (@rev X) (transpose len tapes).
Proof.
intros len tapes Hlen.
induction tapes.
- simpl. rewrite <- map_id with (xs := repeat [] len) at 1.
apply map_ext_in. intros.
apply repeat_spec in H. subst. auto.
- simpl. simpl in Hlen.
assert (length a = len) as Ha. {
apply Hlen. auto.
}
rewrite transpose_app.
rewrite IHtapes.
rewrite zipWith_cons_singleton.
rewrite <- Ha.
rewrite transpose_singleton.
rewrite transpose_rev_aux. auto.
+ apply transpose_inner_length_eq.
+ auto.
+ intros. rewrite <- in_rev in H.
enough (length t = len) by lia. auto.
+ simpl. intros.
enough (length t = len) by lia. firstorder.
Qed.
Lemma transpose_zipWith_cons {X : Type} : forall len (mat : list (list X)) t,
(forall u, In u mat -> length u >= len)
-> length t = length mat
-> transpose (S len) (zipWith cons t mat) = t :: transpose len mat.
Proof.
intros len mat. revert len. induction mat as [ | t1 mat1 IHmat].
- intros. simpl. destruct t; auto. simpl in H0. discriminate.
- intros. simpl. destruct t.
+ simpl in H0. discriminate.
+ rewrite zipWith_cons.
simpl transpose. rewrite IHmat.
* now rewrite zipWith_cons.
* simpl in H. firstorder.
* simpl in H0. now inversion H0.
Qed.
Lemma transpose_involutive {X : Type} : forall len (tapes : list (list X)),
(forall t, In t tapes -> length t = len)
-> transpose (length tapes) (transpose len tapes) = tapes.
Proof.
intros len tapes. revert len.
induction tapes as [ | t tapes1 IHtapes].
- simpl. intros.
destruct len; auto.
- intros. simpl. rewrite transpose_zipWith_cons.
+ rewrite IHtapes. auto.
simpl in H. firstorder.
+ simpl in H. intros.
enough (length u = length tapes1) by lia.
apply transpose_inner_length with (len := len).
auto.
+ rewrite transpose_length.
* simpl in H. apply H. auto.
* simpl in H. intros.
enough (length t0 = len) by lia.
apply H. auto.
Qed.
Lemma transpose_rev2 {X : Type} : forall len (tapes : list (list X)),
(forall t, In t tapes -> length t = len)
-> rev (transpose len tapes) = transpose len (map (@rev X) tapes).
Proof.
intros len tapes Hlen.
pose proof (@transpose_rev X (length tapes) (transpose len tapes)).
assert (forall t, In t (transpose len tapes) -> length t = length tapes) as Hlen2. {
intros; now apply transpose_inner_length in H0.
}
specialize (H Hlen2).
rewrite transpose_involutive in H.
apply (f_equal (fun x => transpose len x)) in H.
replace len with (length (rev (transpose len tapes))) in H at 1. 2 :{
rewrite rev_length. rewrite transpose_length. auto.
intros. enough (length t = len) by lia. auto.
}
rewrite transpose_involutive in H. auto.
- intros. rewrite <- in_rev in H0.
now apply transpose_inner_length with (len := len).
- auto.
(* (1) from transpose_rev: transpose (rev tapes) = map rev (transpose tapes)
(2) plugin (tapes := transpose tapes):
transpose (rev (transpose tapes))
= map rev (transpose (transpose tapes))
= map rev tapes
(3) apply transpose to both sides.
*)
Qed.
Lemma transpose_firstn {X : Type} : forall len (tapes : list (list X)) n,
(forall t, In t tapes -> length t >= len)
-> transpose len (firstn n tapes) = map (firstn n) (transpose len tapes).
Proof.
intros len tapes n Hlen.
assert (n > length tapes \/ n <= length tapes) as [Hn | Hn] by lia. {
rewrite firstn_all2 by lia.
rewrite map_ext_in with (g := id).
now rewrite map_id.
intros. simpl.
rewrite firstn_all2.
auto. apply transpose_inner_length in H. lia.
}
rewrite <- firstn_skipn with (l := tapes) (n := n) at 2.
rewrite transpose_app. rewrite zipWith_map2.
rewrite zipWith_ext_id_l. auto.
- intros. rewrite firstn_app.
enough (n = length x). {
rewrite H0.
replace (length x - length x) with 0 by lia.
rewrite firstn_O. rewrite firstn_all. apply app_nil_r.
}
apply in_combine_l in H.
apply transpose_inner_length in H.
rewrite firstn_length in H.
lia.
- repeat rewrite transpose_length. auto.
* intros. apply skipn_In in H. auto.
* intros. apply firstn_In in H. auto.
- intros. apply firstn_In in H. auto.
- intros. apply skipn_In in H. auto.
Qed.
Lemma transpose_skipn {X : Type} : forall len (tapes : list (list X)) n,
(forall t, In t tapes -> length t >= len)
-> transpose len (skipn n tapes) = map (skipn n) (transpose len tapes).
Proof.
intros len tapes n Hlen.
assert (n > length tapes \/ n <= length tapes) as [Hn | Hn] by lia. {
rewrite skipn_all2 by lia.
simpl. revert Hn.
induction tapes.
- simpl. rewrite map_repeat. destruct n; auto.
- simpl. intros. rewrite zipWith_map2. unfold zipWith.
rewrite map_ext_in with (g := (fun x => [])). 2 : {
intros. destruct a0.
pose proof H as H0.
apply in_combine_l in H.
apply in_combine_r in H0.
apply skipn_all2.
simpl. apply transpose_inner_length in H0.
lia.
}
assert (length (combine a (transpose len tapes)) = len). {
rewrite combine_length. simpl in Hlen.
rewrite transpose_length. specialize (Hlen a ltac:(auto)). lia.
auto.
}
remember (map _ (combine _ _)) as rhs.
assert (rhs = repeat [] (length rhs)). {
rewrite repeat_iff. subst rhs. intros.
apply in_map_iff in H0. destruct H0 as [? [? ?]].
auto.
}
rewrite Heqrhs in H0 at 2. rewrite map_length in H0.
rewrite H in H0. auto.
}
rewrite <- firstn_skipn with (l := tapes) (n := n) at 2.
rewrite transpose_app. rewrite zipWith_map2.
rewrite zipWith_ext_id_r. auto.
- intros. rewrite skipn_app.
enough (n = length x). {
rewrite H0.
replace (length x - length x) with 0 by lia.
rewrite skipn_O. rewrite skipn_all. auto.
}
apply in_combine_l in H.
apply transpose_inner_length in H.
rewrite firstn_length in H.
lia.
- repeat rewrite transpose_length. auto.
* intros. apply skipn_In in H. auto.
* intros. apply firstn_In in H. auto.
- intros. apply firstn_In in H. auto.
- intros. apply skipn_In in H. auto.
Qed.
Lemma skipn_zipWith_cons {X : Type} (xs : list X) (xss : list (list X)) :
length xs >= length xss
-> map (skipn 1) (zipWith cons xs xss) = xss.
Proof.
generalize dependent xs.
induction xss; intros.
- destruct xs; auto.
- destruct xs.
+ simpl in H. lia.
+ rewrite zipWith_cons.
rewrite map_cons.
simpl skipn at 1.
f_equal. apply IHxss.
simpl in H. lia.
Qed.
(* augmentVString *)
Definition augmentVString {X : Type} (vstring : list (list X)) (tape : list X) : list (list X) :=
zipWith (@app X) vstring (map (fun x => [x]) tape).
Lemma augmentVString_length {X : Type} : forall (vstring : list (list X)) (tape : list X),
length tape >= length vstring
-> length (augmentVString vstring tape) = length vstring.
Proof.
intros. unfold augmentVString.
rewrite zipWith_length. rewrite map_length.
lia.
Qed.
Lemma augmentVString_inner_length {X : Type} : forall (vstring : list (list X)) (tape : list X) i,
i < length vstring
-> forall val, nth_error (augmentVString vstring tape) i = Some val
-> exists val', nth_error vstring i = Some val' /\ length val = S (length val').
Proof.
intros.
unfold augmentVString in H0.
rewrite nth_error_zipWith in H0.
destruct (nth_error vstring i) eqn:Heq; try discriminate.
destruct (nth_error (map (fun x : X => [x]) tape) i) eqn:Heq2; try discriminate.
inversion H0.
exists l. split; [auto | ].
rewrite app_length. enough (length l0 = 1) by lia.
rewrite nth_error_map in Heq2.
unfold option_map in Heq2.
destruct (nth_error tape i); try discriminate.
inversion Heq2. auto.
Qed.
Lemma augmentVString_inner_length_eq {X : Type} : forall (vstring : list (list X)) (tape : list X),
length tape >= length vstring
-> (forall u v, In u vstring -> In v vstring -> length u = length v)
-> (forall u v, In u (augmentVString vstring tape) -> In v (augmentVString vstring tape) -> length u = length v).
Proof.
intros.
apply In_nth_error in H1, H2.
destruct H1 as [i1 Hi1], H2 as [i2 Hi2].
assert (i1 < length vstring). {
rewrite <- augmentVString_length with (tape := tape) by auto.
apply nth_error_Some. congruence.
}
assert (i2 < length vstring). {
rewrite <- augmentVString_length with (tape := tape) by auto.
apply nth_error_Some. congruence.
}
apply augmentVString_inner_length in Hi1; [ | auto].
apply augmentVString_inner_length in Hi2; [ | auto].
destruct Hi1 as [u1 [Hu1 Hu1len]].
destruct Hi2 as [u2 [Hu2 Hu2len]].
rewrite Hu1len, Hu2len. f_equal.
apply nth_error_In in Hu1.
apply nth_error_In in Hu2.
apply H0; auto.
Qed.
Lemma augmentVString_transpose {X : Type} : forall (vstring : list (list X)) (tape : list X) len,
(forall val, In val vstring -> length val = len)
-> length tape = length vstring
-> transpose (length tape) (transpose len vstring ++ [tape]) = augmentVString vstring tape.
Proof.
intros.
rewrite transpose_app. 2 : {
intros. apply transpose_inner_length in H1.
lia.
} 2 : {
simpl. firstorder. subst. auto.
}
rewrite transpose_singleton.
rewrite H0.
rewrite transpose_involutive by assumption.
unfold augmentVString.
reflexivity.
Qed.
Lemma augmentVString_transpose_1 {X : Type} : forall (vstring : list (list X)) (tape : list X) len,
(forall val, In val vstring -> length val = len)
-> length tape = length vstring
-> transpose (S len) (augmentVString vstring tape) = transpose len vstring ++ [tape].
Proof.
intros.
rewrite <- augmentVString_transpose with (len := len) by auto.
assert (S len = length (transpose len vstring ++ [tape])) as Hlen. {
rewrite app_length. rewrite transpose_length. simpl. lia.
intros t Hx. apply H in Hx. lia.
}
rewrite Hlen. rewrite transpose_involutive. auto.
intros. apply in_app_iff in H1. destruct H1.
- apply transpose_inner_length in H1. congruence.
- simpl in H1. firstorder. congruence.
Qed.
(* ij_error *)
Definition ij_error {X : Type} (i j : nat) (l : list (list X)) : option X :=
match nth_error l i with
| Some l' => nth_error l' j
| None => None
end.
Lemma ij_error_remove_rows {X : Type} (i j d : nat) (l : list (list X)) :
ij_error (i + d) j l = ij_error i j (skipn d l).
Proof.
unfold ij_error.
rewrite nth_error_skipn.
auto.
Qed.
Lemma ij_error_remove_cols {X : Type} (i j d : nat) (l : list (list X)) :
ij_error i (j + d) l = ij_error i j (map (skipn d) l).
Proof.
unfold ij_error.
remember (nth_error l i) as row_i.
destruct row_i.
2 : {
symmetry in Heqrow_i.
rewrite nth_error_None in Heqrow_i.
assert (nth_error (map (skipn d) l) i = None). {
rewrite nth_error_None.
now rewrite map_length.
}
rewrite H. auto.
}
assert (length l > i) as Hlen. {
symmetry in Heqrow_i.
assert (nth_error l i <> None) by congruence.
rewrite nth_error_Some in H.
lia.
}
remember (nth_error (map (skipn d) l) i) as row_i'.
destruct row_i'.
2 : {
symmetry in Heqrow_i'.
rewrite nth_error_None in Heqrow_i'.
rewrite map_length in Heqrow_i'. lia.
}
rewrite nth_error_map in Heqrow_i'.
rewrite <- Heqrow_i in Heqrow_i'. simpl in Heqrow_i'.
inversion Heqrow_i'. subst.
now rewrite nth_error_skipn.
Qed.
Lemma transpose_spec_0 {X : Type} : forall (xs : list X) (xss : list (list X)) i,
length xss = length xs
-> nth_error xs i = ij_error i 0 (zipWith cons xs xss).
Proof.
induction xs.
- intros. simpl. destruct i; auto.
- intros xss. destruct i.
+ intros. simpl. unfold ij_error.
destruct xss.
* simpl in H. lia.
* simpl. auto.
+ intros. simpl. unfold ij_error.
destruct xss.
* simpl in H. lia.
* rewrite zipWith_cons.
simpl nth_error.
rewrite IHxs with (xss := xss).
auto. simpl in H. lia.
Qed.
Lemma transpose_spec {X : Type} : forall len (tapes : list (list X)),
(forall t,
In t tapes -> length t = len)
-> forall i j,
ij_error i j tapes = ij_error j i (transpose len tapes).
Proof.
induction tapes as [|l tapes IHt]; simpl; intros H.
- (* when the matrix is empty *)
intros i j.
destruct i.
+ unfold ij_error at 1. simpl.
unfold ij_error.
assert (j < len \/ j >= len) by lia.
destruct H0.
++ rewrite nth_error_repeat by apply H0.
auto.
++ assert (nth_error (repeat (@nil X) len) j = None). {
rewrite nth_error_None by lia.
rewrite repeat_length.
auto.
}
rewrite H1. auto.
+ unfold ij_error at 1. simpl.
unfold ij_error.
assert (j < len \/ j >= len) by lia.
destruct H0.
++ rewrite nth_error_repeat by apply H0.
auto.
++ assert (nth_error (repeat (@nil X) len) j = None). {
rewrite nth_error_None by lia.
rewrite repeat_length.
auto.
}
rewrite H1. auto.
- destruct i.
+ (* ij_error 0 j and ij_error j 0 *)
intros j.
unfold ij_error at 1. simpl.
apply transpose_spec_0.
rewrite transpose_length.
symmetry. apply H. auto.
intros. enough (length t = len) by lia.
apply H. auto.
+ (* ij_error (S i) j and ij_error j (S i *)
replace (S i) with (i + 1) by lia. intros.
rewrite ij_error_remove_cols.
rewrite ij_error_remove_rows.
simpl skipn at 1.
rewrite IHt.
rewrite skipn_zipWith_cons. auto.
* rewrite transpose_length.
enough (length l = len) by lia.
apply H. auto.
intros.
enough (length t = len) by lia.
apply H. auto.
* intros.
enough (length t = len) by lia.
apply H. auto.
Qed.
(* select *)
Fixpoint select {X} (selector : list nat) (selectee : list X) : option (list X) :=
match selector with
| [] => Some []
| n :: ns =>
match nth_error selectee n with
| Some x =>
match select ns selectee with
| Some xs => Some (x :: xs)
| None => None
end
| None => None
end
end.
Lemma select_app_Some {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
forall result1 result2,
select selector1 selectee = Some result1 ->
select selector2 selectee = Some result2 ->
select (selector1 ++ selector2) selectee = Some (result1 ++ result2).
Proof.
revert selector2.
induction selector1.
- intros. simpl in *. inversion H. subst. simpl. assumption.
- intros. simpl in *. destruct (nth_error selectee a) eqn:E.
+ destruct (select selector1 selectee) eqn:E2.
* inversion H. subst. simpl.
rewrite IHselector1 with (selector2 := selector2) (result1 := l) (result2 := result2); auto.
* inversion H.
+ inversion H.
Qed.
Lemma select_app_None_r {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
select selector2 selectee = None ->
select (selector1 ++ selector2) selectee = None.
Proof.
revert selector2.
induction selector1.
+ intros. rewrite app_nil_l. assumption.
+ intros. simpl.
apply IHselector1 in H.
rewrite H. destruct (nth_error selectee a); auto.
Qed.
Lemma select_defined {X : Type} : forall (selector : list nat) (selectee : list X),
(forall n, In n selector -> n < length selectee) <->
exists result, select selector selectee = Some result.
Proof.
split.
{ induction selector.
- intros. exists []. auto.
- intros.
simpl in H.
assert (a < length selectee) by (apply H; left; auto).
assert (forall n, In n selector -> n < length selectee)
by (intros; apply H; right; auto).
clear H.
specialize (IHselector H1).
destruct IHselector as [result IH].
pose proof (nth_error_Some_ex selectee a).
rewrite H in H0. destruct H0 as [x H0].
exists (x :: result).
simpl. rewrite H0. rewrite IH. auto.
}
{ intros. destruct H as [result H].
generalize dependent selectee.
revert result.
induction selector.
- simpl in H0. contradiction.
- intros. simpl in *. destruct H0.
+ subst. destruct (nth_error selectee n) eqn:E.
* apply nth_error_Some. congruence.
* congruence.
+ destruct (nth_error selectee a) eqn:E;
destruct (select selector selectee) eqn:E2; try congruence.
apply IHselector with (result := l); auto.
}
Qed.
Lemma select_app_None_l {X : Type} (selector1 selector2 : list nat) (selectee : list X) :
select selector1 selectee = None ->
select (selector1 ++ selector2) selectee = None.
Proof.
intros.
destruct (select (selector1 ++ selector2) selectee) eqn:E1.
2 : auto.
assert (exists result, select (selector1 ++ selector2) selectee = Some result)
by now exists l.
rewrite <- select_defined in H0.
setoid_rewrite in_app_iff in H0.
assert (forall n, In n selector1 -> n < length selectee) as H1. {
intros. apply H0. left. auto.
}
apply select_defined in H1 as [result1 H1].
congruence.
Qed.
Lemma select_length {X : Type} : forall (selector : list nat) (selectee : list X) result,
select selector selectee = Some result ->
length selector = length result.
Proof.
induction selector.
- intros. simpl in *. inversion H. auto.
- intros. simpl in *. destruct (nth_error selectee a) eqn:E.
+ destruct (select selector selectee) eqn:E2.
* inversion H. subst. simpl. f_equal.
now apply IHselector with (selectee := selectee).
* inversion H.
+ inversion H.
Qed.
(* collectSome *)
Definition collectSome {X} (l : list (option X)) : list X :=
flat_map (fun x => match x with Some x => [x] | None => [] end) l.
Lemma collectSome_app {X} : forall (l1 l2 : list (option X)),
collectSome (l1 ++ l2) = collectSome l1 ++ collectSome l2.
Proof.
intros. unfold collectSome.
rewrite flat_map_app. auto.
Qed.
Lemma collectSome_cons {X} : forall (l : list (option X)) (x : option X),
collectSome (x :: l) =
match x with Some x => x :: collectSome l | None => collectSome l end.
Proof.
intros. unfold collectSome.
simpl. destruct x; auto.
Qed.
Lemma collectSome_length {X} : forall (l : list (option X)),
(forall x, In x l -> x <> None)
-> length (collectSome l) = length l.
Proof.
intros.
induction l.
- auto.
- simpl. destruct a eqn:E.
+ simpl. f_equal. apply IHl.
intros. apply H. now right.
+ specialize (H None). simpl in H.
firstorder.
Qed.
Lemma collectSome_length_le {X} : forall (l : list (option X)),
length (collectSome l) <= length l.
Proof.
intros. unfold collectSome.
induction l.
- simpl. lia.
- simpl. destruct a; simpl; lia.
Qed.
Lemma collectSome_In {X} : forall (l : list (option X)) x,
In x (collectSome l)
<-> In (Some x) l.
Proof.
intros.
split.
- intros. induction l.
+ simpl in H. tauto.
+ rewrite collectSome_cons in H.
destruct a eqn:E.
* simpl in H. destruct H.
** subst. constructor. auto.
** right. apply IHl. auto.
* right. apply IHl. auto.
- intros. induction l.
+ simpl. tauto.
+ rewrite collectSome_cons.
destruct a eqn:E.
* simpl. destruct H.
** inversion H. auto.
** right. apply IHl. auto.
* apply IHl. destruct H.
** inversion H.
** auto.
Qed.
(* maximum *)
Definition maximum (l : list nat) : nat :=
fold_right max 0 l.
Lemma maximum_app (l1 l2 : list nat) :
maximum (l1 ++ l2) = max (maximum l1) (maximum l2).
Proof.
induction l1.
- auto.
- simpl. rewrite IHl1. lia.
Qed.
Lemma maximum_In (l : list nat) :
forall x, In x l -> x <= maximum l.
Proof.
induction l.
- intros. simpl in *. tauto.
- intros. simpl in *. destruct H.
+ subst. lia.
+ specialize (IHl x H). lia.
Qed.
(* unsnoc *)
Fixpoint unsnoc {X : Type} (l : list X) : option (list X * X) :=
match l with
| [] => None
| x :: l' => match unsnoc l' with
| None => Some ([], x)
| Some (l'', x') => Some (x :: l'', x')
end
end.
Lemma last_inversion {A : Type} : forall (x y : A) xs ys,
xs ++ [x] = ys ++ [y] -> xs = ys /\ x = y.
Proof.
intros. apply (f_equal (@rev A)) in H.
repeat rewrite (rev_app_distr) in H.
simpl in H. inversion H. apply (f_equal (@rev A)) in H2.
repeat rewrite rev_involutive in H2.
auto.
Qed.
Lemma unsnoc_spec {X : Type} : forall (l : list X) (l' : list X),
(forall x, unsnoc l = Some (l', x) <-> l = l' ++ [x])
/\ (unsnoc l = None <-> l = []).
Proof.
induction l.
- simpl. intros. repeat split. try discriminate.
intros. destruct l'; discriminate.
- destruct (unsnoc l) eqn:E.
+ destruct p as [l1 x1].
intros. split.
* intros. simpl. rewrite E.
specialize (IHl l1).
destruct IHl as [IHl1 IHl2].
specialize (IHl1 x1).
assert (l = l1 ++ [x1]) as H. {
apply IHl1. auto.
}
rewrite H.
split. intros.
** inversion H0. auto.
** intros.
replace (a :: l1 ++ [x1]) with ((a :: l1) ++ [x1]) in H0 by auto.
apply last_inversion in H0. destruct H0. subst. auto.
* intros. split; [ | discriminate].
simpl. rewrite E. intros. inversion H.
+ simpl.
assert (l = []) as H. {
specialize (IHl []) as [IHl1 IHl2].
apply IHl2. auto.
}
subst l. simpl.
repeat split; try discriminate.
* intros. inversion H. subst. reflexivity.
* intros.
replace ([a]) with ([] ++ [a]) in H by auto.
apply last_inversion in H. destruct H. subst. auto.
Qed.
Lemma unsnoc_Some {X : Type} : forall (l : list X) (l' : list X) (x : X),
(unsnoc l = Some (l', x) <-> l = l' ++ [x]).
Proof.
intros. apply unsnoc_spec.
Qed.
Lemma unsnoc_None {X : Type} : forall (l : list X),
(unsnoc l = None <-> l = []).
Proof.
intros. apply unsnoc_spec. exact [].
Qed.
Lemma unsnoc_Some_ex_ne {X : Type} : forall (l : list X),
l <> [] -> exists l' x, unsnoc l = Some (l', x).
Proof.
intros. destruct (unsnoc l) eqn:E.
- destruct p as [l' x]. exists l', x. auto.
- rewrite unsnoc_None in E. congruence.
Qed.
Lemma unsonc_Some_ex {X : Type} : forall (x : X) (l : list X),
exists l' y, unsnoc (x :: l) = Some (l', y).
Proof.
intros. pose proof (unsnoc_Some_ex_ne (x :: l)) as H.
specialize (H ltac:(discriminate)).
auto.
Qed.
Lemma unsnoc_length {X : Type} : forall (l : list X) (l' : list X) (x : X),
unsnoc l = Some (l', x) -> length l = S (length l').
Proof.
intros. apply unsnoc_Some in H. subst.
rewrite app_length. simpl. lia.
Qed.
Definition last_error {X : Type} (l : list X) : option X :=
match unsnoc l with
| Some (_, x) => Some x
| None => None
end.
Lemma last_error_Some {X : Type} : forall (l : list X) (x : X),
last_error l = Some x <-> exists l', l = l' ++ [x].
Proof.
intros. unfold last_error.
destruct (unsnoc l) eqn:E.
- destruct p as [l' x'].
rewrite unsnoc_Some in E. subst.
split; intros.
+ inversion H. exists l'. auto.
+ destruct H as [l'' H].
apply last_inversion in H. destruct H.
subst. auto.
- split.
+ intros. discriminate.
+ intros. destruct H as [l'' H]. subst.
rewrite unsnoc_None in E.
destruct l''; discriminate.
Qed.
Lemma last_error_snoc {X : Type} : forall (x : X) (l : list X),
last_error (l ++ [x]) = Some x.
Proof.
intros. rewrite last_error_Some.
exists l. auto.
Qed.
Lemma last_error_None {X : Type} : forall (l : list X),
last_error l = None <-> l = [].
Proof.
intros l.
destruct (unsnoc l) as [[l' x ]| ] eqn:El.
- rewrite unsnoc_Some in El. split.
+ intros. subst l. rewrite last_error_snoc in H.
discriminate.
+ intros. subst.
apply f_equal with (f := @length X) in H.
rewrite app_length in H. simpl in H. lia.
- rewrite unsnoc_None in El. split
+ intros. subst l. auto.
+ intros. subst. auto.
Qed.
Lemma last_error_cons_cons {X : Type} : forall (x y : X) (l : list X),
last_error (x :: y :: l) = last_error (y :: l).
Proof.
intros. unfold last_error.
simpl.
destruct (unsnoc l) eqn:E.
- destruct p. auto.
- auto.
Qed.
Lemma last_error_nth_error {X : Type} : forall (l : list X),
last_error l = nth_error l (length l - 1).
Proof.
intros. unfold last_error.
destruct (unsnoc l) eqn:E.
- destruct p. rewrite unsnoc_Some in E. rewrite E.
rewrite nth_error_app2. rewrite app_length. simpl.
replace (length l0 + 1 - 1 - length l0) with 0 by lia.
auto.
rewrite app_length. simpl. lia.
- rewrite unsnoc_None in E. subst. auto.
Qed.
(* filter *)
Lemma filter_index : forall {X : Type} (l : list X) (f : X -> bool) (x : X) (i : nat),
nth_error (filter f l) i = Some x
-> exists j,
nth_error l j = Some x
/\ i <= j.
Proof.
induction l.
{ intros. simpl in H. destruct i; inversion H. }
intros; simpl in H.
destruct (f a) eqn:Hfa.
- intros.
destruct i.
+ simpl in H. inversion H. subst a. clear H.
exists 0. split; [reflexivity | lia].
+ simpl in H.
destruct (IHl f x i H) as [j [Hj Hij]].
exists (S j). split; [assumption | lia].
- intros.
destruct (IHl f x i H) as [j [Hj Hij]].
exists (S j). split; [assumption | lia].
Qed.
Lemma filter_order {X : Type} (l : list X) (f : X -> bool):
forall x y i j,
i < j
-> nth_error (filter f l) i = Some x
-> nth_error (filter f l) j = Some y
-> exists i' j',
i' < j'
/\ nth_error l i' = Some x
/\ nth_error l j' = Some y.
Proof.
induction l.
{ intros. simpl in H0. destruct i; inversion H0. }
destruct (f a) eqn:Hfa.
- intros.
pose proof (filter_index (a :: l) _ _ _ H0) as [i' [Hi' Hii']].
pose proof (filter_index (a :: l) _ _ _ H1) as [j' [Hj' Hjj']].
simpl in H0, H1. rewrite Hfa in H0, H1.
destruct i.
+ destruct j; [lia | ].
simpl in H0. inversion H0. subst a. clear H0.
simpl in H1. exists 0.
destruct j'; [lia | ].
exists (S j'). repeat split. lia. assumption.
+ destruct j; [lia | ].
simpl in H0, H1.
destruct (IHl x y i j ltac:(lia) H0 H1) as [i'' [j'' [Hij [Hi'' Hj'']]]].
exists (S i''). exists (S j''). repeat split.
lia. assumption. assumption.
- intros.
simpl in H0, H1. rewrite Hfa in H0, H1.
destruct (IHl x y i j ltac:(lia) H0 H1) as [i'' [j'' [Hij [Hi'' Hj'']]]].
exists (S i''). exists (S j''). repeat split.
lia. assumption. assumption.
Qed.
(* list_2_ind *)
Fixpoint list_2_ind {A : Type} (P : list A -> Prop)
(I0 : P [])
(I1 : forall x, P [x])
(I2 : forall x y l, P l -> P (x :: y :: l)) (l : list A) : P l :=
match l with
| [] => I0
| [x] => I1 x
| x :: y :: l => I2 x y l (list_2_ind P I0 I1 I2 l)
end.
Lemma rev_list_2_ind {A : Type} (P : list A -> Prop) :
P []
-> (forall x, P [x])
-> (forall x y l, P l -> P (l ++ [x; y]))
-> forall l, P l.
Proof.
intros I0 I1 I2 l.
remember (rev l) as l'.
generalize dependent l.
induction l' using list_2_ind; intros.
- rewrite <- rev_involutive.
rewrite <- Heql'.
apply I0.
- rewrite <- rev_involutive.
rewrite <- Heql'.
apply I1.
- rewrite <- rev_involutive.
rewrite <- Heql'.
simpl. rewrite <- app_assoc.
simpl.
apply I2.
apply IHl'.
auto using rev_involutive.
Qed.
(* InConsecutive *)
Fixpoint InConsecutive {X : Type} (x1 x2 : X) (l : list X) : Prop :=
match l with
| [] => False
| x :: l => match l with
| [] => False
| y :: l' => x = x1 /\ y = x2 \/ InConsecutive x1 x2 l
end
end.
Lemma in_consecutive_nil {X : Type} : forall (x1 x2 : X),
~ InConsecutive x1 x2 [].
Proof. auto. Qed.
Lemma in_consecutive_singleton {X : Type} : forall (x1 x2 x : X),
~ InConsecutive x1 x2 [x].
Proof. auto. Qed.
Lemma in_consecutive_begin {X : Type} : forall (x1 x2 : X) (l : list X),
InConsecutive x1 x2 (x1 :: x2 :: l).
Proof. intros. simpl. auto. Qed.
Lemma in_consecutive_begin_iff {X : Type} : forall (x1 x2 a1 a2: X) (l : list X),
InConsecutive x1 x2 (a1 :: a2 :: l) <-> x1 = a1 /\ x2 = a2 \/ InConsecutive x1 x2 (a2 :: l).
Proof.
split; simpl InConsecutive in *; intros; firstorder.
Qed.
Lemma in_consecutive_cons {X : Type} : forall (x1 x2 x : X) (l : list X),
InConsecutive x1 x2 l -> InConsecutive x1 x2 (x :: l).
Proof.
intros.
simpl. destruct l.
- now apply in_consecutive_nil in H.
- auto.
Qed.
Lemma in_consecutive_end {X : Type} : forall (x1 x2 : X) (l : list X),
InConsecutive x1 x2 (l ++ [x1; x2]).
Proof.
induction l.
- simpl. auto.
- simpl app. apply in_consecutive_cons. apply IHl.
Qed.
Lemma in_consecutive_end_iff {X : Type} : forall (x1 x2 a1 a2: X) (l : list X),
InConsecutive x1 x2 (l ++ [a1; a2])
<-> InConsecutive x1 x2 (l ++ [a1])
\/ x1 = a1 /\ x2 = a2.
Proof.
induction l.
- simpl. firstorder.
- destruct l.
+ simpl. firstorder.
+ simpl app.
rewrite in_consecutive_begin_iff.
rewrite IHl. rewrite in_consecutive_begin_iff.
simpl app. tauto.
Qed.
Lemma in_consecutive_In {X : Type} : forall (x1 x2 : X) (l : list X),
InConsecutive x1 x2 l -> In x1 l /\ In x2 l.
Proof.
intros. induction l.
- simpl in H. contradiction.
- simpl in H. destruct l.
+ simpl in H. contradiction.
+ destruct H as [[H1 H2] | H3].
* subst. split; simpl; auto.
* apply IHl in H3. destruct H3. split; simpl; auto.
Qed.
Lemma in_consecutive_app {X : Type} : forall (x1 x2 a1 a2: X) (l1 l2 : list X),
InConsecutive x1 x2 (l1 ++ a1 :: a2 :: l2)
<-> InConsecutive x1 x2 (l1 ++ [a1])
\/ InConsecutive x1 x2 (a2 :: l2)
\/ x1 = a1 /\ x2 = a2.
Proof.
intros.
revert l1 x1 x2 a1 a2.
induction l2.
- intros. rewrite in_consecutive_end_iff.
simpl. tauto.
- intros.
replace (l1 ++ a1 :: a2 :: a :: l2)
with ((l1 ++ [a1]) ++ a2 :: a :: l2)
by now rewrite <- app_assoc.
rewrite IHl2.
rewrite <- app_assoc. simpl app.
rewrite in_consecutive_end_iff.
rewrite in_consecutive_begin_iff.
tauto.
Qed.
Lemma in_consecutive_app_2 {X : Type} : forall (x1 x2 a1 a2 a: X) (l1 l2 : list X),
InConsecutive x1 x2 ((l1 ++ [a1]) ++ [a] ++ (a2 :: l2))
<-> InConsecutive x1 x2 (l1 ++ [a1])
\/ InConsecutive x1 x2 (a2 :: l2)
\/ x1 = a1 /\ x2 = a
\/ x1 = a /\ x2 = a2.
Proof.
intros. simpl app.
rewrite in_consecutive_app.
rewrite <- app_assoc. simpl app.
rewrite in_consecutive_end_iff.
tauto.
Qed.
Lemma in_consecutive_rev {X : Type} : forall (x1 x2 : X) (l : list X),
InConsecutive x1 x2 (rev l) <-> InConsecutive x2 x1 l.
Proof.
induction l.
- simpl. tauto.
- destruct l.
+ simpl. tauto.
+ simpl rev. rewrite <- app_assoc.
simpl app.
rewrite in_consecutive_end_iff.
replace (rev l ++ [x]) with (rev (x :: l)) by auto.
rewrite IHl.
rewrite in_consecutive_begin_iff.
tauto.
Qed.
Lemma in_consecutive_map {X Y : Type} : forall (x1 x2 : X) (f : X -> Y) (l : list X),
InConsecutive x1 x2 l -> InConsecutive (f x1) (f x2) (map f l).
Proof.
intros. induction l.
- simpl in H. contradiction.
- simpl in H. destruct l.
+ simpl in H. contradiction.
+ destruct H as [[H1 H2] | H3].
* subst. simpl. left. split; auto.
* simpl. right. apply IHl. auto.
Qed.
Lemma in_consecutive_map_iff {X Y : Type} : forall (y1 y2 : Y) (f : X -> Y) (l : list X),
InConsecutive y1 y2 (map f l) <-> exists x1 x2, InConsecutive x1 x2 l /\ y1 = f x1 /\ y2 = f x2.
Proof.
intros. split; intros.
- induction l.
+ simpl in H. contradiction.
+ simpl in H. destruct l.
* simpl in H. contradiction.
* destruct H as [[H1 H2] | H3].
-- subst. exists a, x. simpl. split; auto.
-- apply IHl in H3. destruct H3 as [x1 [x2 [H3 [H4 H5]]]].
exists x1, x2. simpl. split; auto.
- destruct H as [x1 [x2 [H1 [H2 H3]]]].
subst. apply in_consecutive_map. auto.
Qed.
Lemma nth_error_in_consecutive {X : Type} : forall (x1 x2 : X) (l : list X) i,
nth_error l i = Some x1
-> nth_error l (S i) = Some x2
-> InConsecutive x1 x2 l.
Proof.
intros.
destruct (nth_error_split l i H) as [l1 [l2 [Hl Ll1]]].
rewrite Hl in H0.
rewrite nth_error_app2 in H0 by lia.
replace (S i - length l1) with 1 in H0 by lia.
rewrite nth_error_cons in H0.
destruct l2; simpl in H0. { discriminate. }
inversion H0. subst x.
rewrite Hl.
apply in_consecutive_app.
auto.
Qed.
Lemma in_consecutive_nth_error {X : Type} : forall (l : list X) x1 x2,
InConsecutive x1 x2 l
-> exists i, nth_error l i = Some x1 /\ nth_error l (S i) = Some x2.
Proof.
induction l using list_2_ind.
- intros. apply in_consecutive_nil in H. contradiction.
- intros. apply in_consecutive_singleton in H. contradiction.
- intros. simpl in H. destruct H as [[H1 H2] | H].
* subst. exists 0. simpl. auto.
* destruct l; [ contradiction | ].
destruct H as [[H1 H2] | H].
-- subst. exists 1. simpl. auto.
-- apply IHl in H. destruct H as [i [H1 H2]].
exists (2 + i). simpl in H2 |- *. auto.
Qed.
(* is_prefix_of *)
Definition is_prefix_of {A : Type} (w1 w2 : list A) : Prop :=
exists w, w1 ++ w = w2.
Notation "w1 ⊑ w2" := (is_prefix_of w1 w2) (at level 70).
Lemma prefix_refl {A : Type} : forall (w : list A), w ⊑ w.
Proof.
intros. exists [].
autorewrite with list.
reflexivity.
Qed.
Lemma prefix_trans {A : Type} : forall (w1 w2 w3 : list A),
w1 ⊑ w2
-> w2 ⊑ w3
-> w1 ⊑ w3.
Proof.
intros.
destruct H as [w4 Hw4].
destruct H0 as [w5 Hw5].
exists (w4 ++ w5).
rewrite app_assoc.
rewrite Hw4, Hw5.
reflexivity.
Qed.
Lemma prefix_app {A : Type} : forall (w1 w2 w3 : list A),
w1 ⊑ w2
-> w1 ⊑ w2 ++ w3.
Proof.
intros.
destruct H as [w4 Hw4].
exists (w4 ++ w3).
rewrite app_assoc. rewrite Hw4.
reflexivity.
Qed.
Lemma prefix_antisym {A : Type} : forall (w1 w2 : list A),
w1 ⊑ w2
-> w2 ⊑ w1
-> w1 = w2.
Proof.
intros.
destruct H as [w3 Hw3].
destruct H0 as [w4 Hw4].
rewrite <- Hw3 in Hw4.
rewrite <- app_assoc in Hw4.
replace w1 with (w1 ++ []) in Hw4 at 2 by now rewrite app_nil_r.
apply app_inv_head in Hw4.
destruct w3; destruct w4; inversion Hw4.
rewrite app_nil_r in Hw3.
apply Hw3.
Qed.
Lemma prefix_firstn {A : Type} : forall (w : list A) (n : nat),
firstn n w ⊑ w.
Proof.
intros.
exists (skipn n w).
rewrite firstn_skipn.
reflexivity.
Qed.
Lemma prefix_eq_length {A : Type} (x1 x2 w : list A) :
x1 ⊑ w
-> x2 ⊑ w
-> length x1 = length x2
-> x1 = x2.
Proof.
intros.
unfold is_prefix_of in *.
remember (length x1) as n.
revert Heqn.
revert H H0 H1.
revert x1 x2 w.
induction n.
- intros.
assert (x1 = []) by now apply length_zero_iff_nil.
assert (x2 = []) by now apply length_zero_iff_nil.
subst. reflexivity.
- intros.
destruct x1; [ inversion Heqn | ].
destruct x2; [ inversion H1 | ].
destruct H as [w1 Hw1].
destruct H0 as [w2 Hw2].
simpl in Hw1, Hw2.
assert (a = a0).
{ rewrite <- Hw1 in Hw2. now inversion Hw2. }
subst a0.
f_equal.
destruct w.
{ inversion Hw1. }
assert (a = a0) by now inversion Hw1.
subst a0.
specialize (IHn x1 x2 w).
assert (exists w0, x1 ++ w0 = w).
{ exists w1. now inversion Hw1. }
assert (exists w0, x2 ++ w0 = w).
{ exists w2. now inversion Hw2. }
simpl in H1, Heqn.
exact (IHn H H0 ltac:(lia) ltac:(lia)).
Qed.
Lemma prefix_firstn_iff {A : Type} (x w : list A) :
x ⊑ w
<-> x = firstn (length x) w.
Proof.
split. {
intros.
pose proof (prefix_firstn w (length x)).
assert (length x <= length w).
{ destruct H as [w' Hw'].
rewrite <- Hw'. rewrite app_length.
lia.
}
pose proof (firstn_length (length x) w).
exact (prefix_eq_length x (firstn (length x) w) w H H0 ltac:(lia)).
} {
intros. rewrite H. apply prefix_firstn.
}
Qed.
Lemma prefix_comparable {A : Type} : forall (x1 x2 w : list A),
x1 ⊑ w
-> x2 ⊑ w
-> x1 ⊑ x2 \/ x2 ⊑ x1.
Proof.
setoid_rewrite prefix_firstn_iff.
intros x1 x2 w Hx1 Hx2.
assert (length x1 <= length w). {
rewrite Hx1.
rewrite firstn_length.
lia.
}
assert (length x2 <= length w). {
rewrite Hx2.
rewrite firstn_length.
lia.
}
destruct (Nat.le_gt_cases (length x1) (length x2)).
- left.
rewrite Hx1. rewrite Hx2.
rewrite firstn_firstn. rewrite firstn_length.
f_equal. lia.
- right.
rewrite Hx1. rewrite Hx2.
rewrite firstn_firstn. rewrite firstn_length.
f_equal. lia.
Qed.
Lemma prefix_left_app {A : Type} : forall (x1 x2 w : list A),
x1 ⊑ x2
-> w ++ x1 ⊑ w ++ x2.
Proof.
unfold is_prefix_of.
intros x1 x2 w [w' Hw'].
exists w'.
rewrite <- app_assoc.
rewrite Hw'.
reflexivity.
Qed.
(* is_suffix_of *)
Definition is_suffix_of {A : Type} (w1 w2 : list A) : Prop :=
exists w, w ++ w1 = w2.
Lemma is_suffix_is_prefix_rev {A : Type} : forall (w1 w2 : list A),
is_suffix_of w1 w2 <-> is_prefix_of (rev w1) (rev w2).
Proof.
unfold is_suffix_of, is_prefix_of.
split; intros.
- destruct H as [w Hw].
exists (rev w).
rewrite <- rev_app_distr.
now rewrite Hw.
- destruct H as [w Hw].
exists (rev w).
replace w with (rev (rev w)) in Hw by now rewrite rev_involutive.
rewrite <- rev_app_distr in Hw.
assert ( rev (rev (rev w ++ w1)) = rev (rev w2) ) by now rewrite Hw.
repeat rewrite rev_involutive in H.
assumption.
Qed.
Lemma suffix_refl {A : Type} : forall (w : list A), is_suffix_of w w.
Proof.
intros. exists [].
autorewrite with list.
reflexivity.
Qed.
Lemma suffix_trans {A : Type} : forall (w1 w2 w3 : list A),
is_suffix_of w1 w2
-> is_suffix_of w2 w3
-> is_suffix_of w1 w3.
Proof.
intros.
rewrite is_suffix_is_prefix_rev in *.
eapply prefix_trans; eauto.
Qed.
Lemma suffix_app {A : Type} : forall (w1 w2 w : list A),
is_suffix_of w1 w2
-> is_suffix_of w1 (w ++ w2).
Proof.
intros.
rewrite is_suffix_is_prefix_rev in *.
rewrite rev_app_distr.
eapply prefix_app; eauto.
Qed.
Lemma suffix_antisym {A : Type} : forall (w1 w2 : list A),
is_suffix_of w1 w2
-> is_suffix_of w2 w1
-> w1 = w2.
Proof.
intros.
rewrite is_suffix_is_prefix_rev in *.
assert (rev w1 = rev w2) by now eapply prefix_antisym; eauto.
assert (rev (rev w1) = rev (rev w2)) by now rewrite H1.
repeat rewrite rev_involutive in H2.
assumption.
Qed.
Lemma suffix_firstn {A : Type} : forall (w : list A) (n : nat),
is_suffix_of (skipn n w) w.
Proof.
intros.
unfold is_suffix_of.
exists (firstn n w).
now rewrite firstn_skipn.
Qed.
Lemma suffix_eq_length {A : Type} (x1 x2 w : list A) :
is_suffix_of x1 w
-> is_suffix_of x2 w
-> length x1 = length x2
-> x1 = x2.
Proof.
intros.
rewrite is_suffix_is_prefix_rev in *.
assert (rev x1 = rev x2). {
eapply prefix_eq_length; eauto.
now repeat rewrite rev_length.
}
assert (rev (rev x1) = rev (rev x2)) by now rewrite H2.
now repeat rewrite rev_involutive in H3.
Qed.
Lemma suffix_skipn_iff {A : Type} (x w : list A) :
is_suffix_of x w
<-> x = skipn (length w - length x) w.
Proof.
split.
- intros.
assert (length w >= length x) as Hl. {
destruct H as [w' Hw'].
rewrite <- Hw'.
rewrite app_length.
lia.
}
rewrite is_suffix_is_prefix_rev in H.
rewrite prefix_firstn_iff in H.
remember (rev w) as w'.
rewrite rev_length in H.
replace (length x) with (length w - (length w - length x)) in H by lia.
assert (rev (rev x) = rev (firstn (length w - (length w - length x)) w')) by now rewrite H.
assert ((length w) = (length w')).
{ rewrite Heqw'. now rewrite rev_length. }
rewrite H1 in H0 at 1.
rewrite <- skipn_rev in H0.
subst w'.
now repeat rewrite rev_involutive in H0.
- intros. rewrite H.
apply suffix_firstn.
Qed.
Lemma suffix_comparable {A : Type} : forall (x1 x2 w : list A),
is_suffix_of x1 w
-> is_suffix_of x2 w
-> is_suffix_of x1 x2 \/ is_suffix_of x2 x1.
Proof.
intros.
repeat rewrite is_suffix_is_prefix_rev in *.
eapply prefix_comparable; eauto.
Qed.
Lemma suffix_right_app {A : Type} : forall (x1 x2 w : list A),
is_suffix_of x1 x2
-> is_suffix_of (x1 ++ w) (x2 ++ w).
Proof.
intros.
rewrite is_suffix_is_prefix_rev in *.
repeat rewrite rev_app_distr.
apply prefix_left_app; auto.
Qed.
(* is_infix_of *)
Definition is_infix_of {A : Type} (w ww : list A) : Prop :=
exists w1 w2, w1 ++ w ++ w2 = ww.
Lemma infix_refl {A : Type} : forall (w : list A), is_infix_of w w.
Proof.
exists [], [].
rewrite app_nil_r.
auto.
Qed.
Lemma infix_trans {A : Type} : forall (w1 w2 w3 : list A),
is_infix_of w1 w2
-> is_infix_of w2 w3
-> is_infix_of w1 w3.
Proof.
intros.
destruct H as [w11 [w12 H1]].
destruct H0 as [w21 [w22 H2]].
rewrite <- H1 in H2.
exists (w21 ++ w11), (w12 ++ w22).
rewrite <- !app_assoc in H2.
rewrite <- !app_assoc.
assumption.
Qed.
Lemma infix_antisym {A : Type} : forall (w1 w2 : list A),
is_infix_of w1 w2
-> is_infix_of w2 w1
-> w1 = w2.
Proof.
intros.
destruct H as [w11 [w12 H1]].
destruct H0 as [w21 [w22 H2]].
rewrite <- H1 in H2.
rewrite <- !app_assoc in H2.
apply f_equal with (f := @length A) in H2.
rewrite !app_length in H2.
assert (length w21 = 0) by lia.
assert (length w11 = 0) by lia.
assert (length w12 = 0) by lia.
assert (length w22 = 0) by lia.
assert (w11 = []) by now apply length_zero_iff_nil.
assert (w12 = []) by now apply length_zero_iff_nil.
subst. simpl. now rewrite app_nil_r.
Qed.
Lemma infix_firstn_skipn {A : Type} : forall (w : list A) (n m : nat),
is_infix_of (firstn m (skipn n w)) w.
Proof.
intros.
exists (firstn n w), (skipn (n + m) w).
pose proof (firstn_skipn n w).
pose proof (firstn_skipn m (skipn n w)).
rewrite skipn_skipn in H0.
replace (m + n) with (n + m) in H0 by lia.
congruence.
Qed.
Lemma infix_skipn_firstn {A : Type} : forall (w : list A) (n m : nat),
is_infix_of (skipn n (firstn m w)) w.
Proof.
intros.
pose proof (firstn_skipn m w).
pose proof (firstn_skipn n (firstn m w)).
rewrite firstn_firstn in H0.
remember (min n m) as k.
exists (firstn k w), (skipn m w).
rewrite <- H0 in H. now rewrite app_assoc.
Qed.
Lemma infix_skipn_firstn_bw {A : Type} (w ww : list A) :
is_infix_of w ww
-> exists m, skipn m (firstn (m + length w) ww) = w.
Proof.
intros.
destruct H as [w1 [w2 H]].
exists (length w1).
subst ww.
rewrite app_assoc.
rewrite <- app_length.
rewrite firstn_app.
rewrite firstn_all.
replace (length (w1 ++ w) - length (w1 ++ w)) with 0 by lia.
simpl. rewrite app_nil_r.
rewrite skipn_app.
rewrite skipn_all.
replace (length w1 - length w1) with 0 by lia.
auto.
Qed.
Lemma infix_firstn_skipn_bw {A : Type} (w ww : list A) :
is_infix_of w ww
-> exists m, firstn (length w) (skipn m ww) = w.
Proof.
intros.
destruct H as [w1 [w2 H]].
exists (length w1).
subst ww.
rewrite skipn_app.
rewrite skipn_all. simpl.
replace (length w1 - length w1) with 0 by lia.
simpl.
rewrite firstn_app. rewrite firstn_all.
replace (length w - length w) with 0 by lia.
simpl. now rewrite app_nil_r.
Qed.
Lemma infix_app_r {A : Type} : forall (w wr ww : list A),
is_infix_of w ww
-> is_infix_of w (ww ++ wr).
Proof.
intros.
destruct H as [w1 [w2 H]].
exists w1, (w2 ++ wr).
rewrite <- H.
now rewrite !app_assoc.
Qed.
Lemma infix_app_l {A : Type} : forall (w wl ww : list A),
is_infix_of w ww
-> is_infix_of w (wl ++ ww).
Proof.
intros.
destruct H as [w1 [w2 H]].
exists (wl ++ w1), w2.
rewrite <- H.
now rewrite !app_assoc.
Qed.
Lemma infix_nil {A : Type} : forall (w : list A),
is_infix_of [] w.
Proof.
intros.
exists [], w.
auto.
Qed.
Lemma infix_nil_inv {A : Type} : forall (w : list A),
is_infix_of w [] -> w = [].
Proof.
intros.
destruct H as [w1 [w2 H]].
assert (HH := H).
apply f_equal with (f := @length A) in H.
rewrite !app_length in H. simpl in H.
assert (length w1 = 0) by lia.
assert (length w2 = 0) by lia.
apply length_zero_iff_nil in H0, H1.
subst. now rewrite app_nil_r in HH.
Qed.
Lemma infix_uncons {A : Type} : forall (w1 w2 : list A) (a : A),
is_infix_of (a :: w1) w2
-> is_infix_of w1 w2.
Proof.
intros.
destruct H as [w11 [w12 H]].
exists (w11 ++ [a]), w12.
rewrite <- H.
now rewrite <- app_assoc.
Qed.
Lemma infix_unsnoc {A : Type} : forall (w1 w2 : list A) (a : A),
is_infix_of (w1 ++ [a]) w2
-> is_infix_of w1 w2.
Proof.
intros.
destruct H as [w11 [w12 H]].
exists w11, (a::w12).
rewrite <- H.
now rewrite <- app_assoc.
Qed.
Lemma infix_tl {A : Type} : forall (w1 w2 : list A) (a : A),
is_infix_of w1 w2
-> is_infix_of (tl w1) w2.
Proof.
destruct w1.
- intros. apply infix_nil.
- intros. apply infix_uncons in H.
simpl. auto.
Qed.
Lemma infix_unapp_l {A : Type} : forall (w1 w2 w3 : list A),
is_infix_of (w1 ++ w2) w3
-> is_infix_of w2 w3.
Proof.
intros.
destruct H as [w11 [w12 H]].
exists (w11 ++ w1), w12.
now rewrite <- H, !app_assoc.
Qed.
Lemma infix_unapp_r {A : Type} : forall (w1 w2 w3 : list A),
is_infix_of (w1 ++ w2) w3
-> is_infix_of w1 w3.
Proof.
intros.
destruct H as [w11 [w12 H]].
exists w11, (w2 ++ w12).
now rewrite <- H, !app_assoc.
Qed.
Lemma infix_cons_In {A : Type} : forall (w1 w2 : list A) (a : A),
is_infix_of (a :: w1) w2
-> In a w2.
Proof.
intros.
destruct H as [w11 [w12 H]].
rewrite <- H.
rewrite !in_app_iff.
right; left; left; auto.
Qed.
Lemma infix_snoc_In {A : Type} : forall (w1 w2 : list A) (a : A),
is_infix_of (w1 ++ [a]) w2
-> In a w2.
Proof.
intros.
destruct H as [w11 [w12 H]].
rewrite <- H.
rewrite !in_app_iff.
right; left; right; apply In_singleton_refl.
Qed.
(* is_first_member *)
Definition is_first_member {X : Type} (x : X) (l : list X) (P : X -> Prop) : Prop :=
exists i,
nth_error l i = Some x
/\ P x
/\ forall j y,
j < i
-> nth_error l j = Some y
-> ~ P y.
Lemma is_first_member_unique {X : Type} (x y : X) (l : list X) (P : X -> Prop) :
is_first_member x l P
-> is_first_member y l P
-> x = y.
Proof.
unfold is_first_member.
intros Hx Hy.
destruct Hx as [i [Hxi [HxP Hx]]].
destruct Hy as [j [Hyi [HyP Hy]]].
destruct (Nat.lt_trichotomy i j) as [Hij | [Hij | Hij]].
- specialize (Hy _ _ Hij Hxi). contradiction.
- congruence.
- specialize (Hx _ _ Hij Hyi). contradiction.
Qed.
Lemma is_first_member_exists {X : Type} (l : list X) (P : X -> Prop) (decP : forall x, {P x} + {~ P x}) :
forall x,
In x l
-> P x
-> exists x', is_first_member x' l P.
Proof.
induction l. {
intros x Hin Hx.
inversion Hin. }
{ intros x Hin Hx.
destruct (decP a) as [Ha | Ha].
- exists a. exists 0. simpl. repeat split; try assumption.
intros. inversion H.
- assert (In x l /\ P x).
{ simpl in Hin.
destruct Hin as [Hin | Hin].
- subst. contradiction.
- split; assumption.
}
specialize (IHl x ltac:(tauto) ltac:(tauto)).
destruct IHl as [x' [i [Hxi [Hx'P Hx']]]].
exists x'. exists (S i). simpl.
repeat split; try assumption.
intros j y Hji Hyj.
destruct j.
+ simpl in Hyj. inversion Hyj.
subst. assumption.
+ simpl in Hyj. eapply Hx'.
2 : eauto.
lia.
}
Qed.
Lemma is_first_member_cons {X : Type} (x1 x2 : X) (l : list X) (P : X -> Prop) :
is_first_member x1 (x2 :: l) P
<-> (x1 = x2 /\ P x1
\/ (~ P x2 /\ is_first_member x1 l P)).
Proof.
unfold is_first_member.
split; intros.
- destruct H as [i [Hxi [HxP Hx]]].
destruct i.
+ simpl in Hxi. inversion Hxi. subst. auto.
+ simpl in Hxi.
right. split.
* eapply Hx. apply Nat.lt_0_succ.
reflexivity.
* exists i. repeat split; try assumption.
intros. apply Hx with (j := S j). lia. auto.
- destruct H as [[Hx1 Hx1P] | Hx1].
+ subst. exists 0. simpl. repeat split; try assumption.
intros. inversion H.
+ destruct Hx1 as [Hx2P Hx1].
destruct Hx1 as [i [Hxi [Hx1P Hx1]]].
exists (S i). simpl. repeat split; try assumption.
intros. destruct j.
* simpl in H0. inversion H0. subst. assumption.
* simpl in H0. apply Hx1 with (j := j). lia. assumption.
Qed.
Lemma find_some_first_member {X : Type} (l : list X) (pred : X -> bool) :
forall x,
find pred l = Some x
<-> is_first_member x l (fun x => pred x = true).
Proof.
induction l; intros.
- simpl. unfold is_first_member. split.
+ discriminate.
+ intros [i [H _]]. destruct i; inversion H.
- rewrite is_first_member_cons. simpl.
rewrite <- IHl.
destruct (pred a) eqn:Ha.
+ split; intros.
* inversion H. subst.
auto.
* destruct H as [[Hx1 Hx1P] | Hx1].
subst. auto.
destruct Hx1 as [Hx2P Hx1].
congruence.
+ firstorder. subst. congruence.
Qed.
Lemma find_none_first_member {X : Type} (l : list X) (pred : X -> bool) :
find pred l = None
<-> forall x, ~ is_first_member x l (fun x => pred x = true).
Proof.
split.
- intros Hnone x Hx.
rewrite <- find_some_first_member in Hx.
congruence.
- intros.
destruct (find pred l) eqn:Hfind; [ | auto].
rewrite find_some_first_member in Hfind.
firstorder.
Qed.
Lemma first_member_split {X : Type} (l : list X) (P : X -> Prop) :
forall x,
is_first_member x l P
<-> exists l1 l2,
l = l1 ++ x :: l2
/\ (forall y, In y l1 -> ~ P y)
/\ P x.
Proof.
intros x. split.
{ intros Hx.
destruct Hx as [i [Hxi [HxP Hx]]].
destruct i.
{ destruct l.
- simpl in Hxi. discriminate.
- simpl in Hxi. inversion Hxi. subst x0.
exists [], l. simpl.
split; [reflexivity | split; [ | assumption]].
intros. contradiction.
}
exists (firstn (S i) l), (skipn (S (S i)) l).
split; [ | split]. 3 : assumption.
- rewrite <- firstn_skipn with (n := S i) (l := l) at 1.
f_equal. apply skipn_succ_nth_error. apply Hxi.
- intros y Hy.
apply In_nth_error in Hy.
destruct Hy as [j Hj].
pose proof (nth_error_Some l (S i)) as Xi.
pose proof (nth_error_Some (firstn (S i) l) j) as Xj.
rewrite firstn_length in Xj.
assert (nth_error l (S i) <> None) by (congruence).
assert (nth_error (firstn (S i) l) j <> None) by (congruence).
rewrite Xi in H. rewrite Xj in H0.
rewrite nth_error_firstn in Hj by lia.
eapply Hx. 2 : apply Hj. lia.
}
{ intros [l1 [l2 [Hl [Hl1 Hl2]]]].
exists (length l1).
split; [ | split]. 2 : assumption.
- rewrite Hl. rewrite nth_error_app2 by auto.
replace (length l1 - length l1) with 0 by lia.
auto.
- intros j y Hj HHj.
apply Hl1.
rewrite Hl in HHj.
rewrite nth_error_app1 in HHj by apply Hj.
apply nth_error_In in HHj.
apply HHj.
}
Qed.
Lemma first_member_dec {X : Type} (P : X -> Prop) (decP : forall x, {P x} + {~ P x}) :
forall l,
{ forall x, In x l -> ~ P x}
+ { exists x, is_first_member x l P }.
Proof.
induction l.
- left. intros. inversion H.
- destruct (decP a) as [Ha | Ha].
+ right. apply is_first_member_exists with (x := a); auto.
left. auto.
+ destruct IHl as [IHl | IHl].
* left. intros x Hin.
destruct Hin.
++ now subst.
++ auto.
* right. destruct IHl as [x Hx].
exists x. apply is_first_member_cons. auto.
Qed.
(* window_agree *)
Definition window_agree {A : Type} (start delta : nat) (w1 w2 : list A) :=
forall i, i < delta -> nth_error w1 (start + i) = nth_error w2 (start + i).
Definition window_agree_2 {A : Type} (start1 start2 delta : nat) (w1 w2 : list A) :=
forall i, i < delta -> nth_error w1 (start1 + i) = nth_error w2 (start2 + i).
Lemma window_agree_symm {A : Type} : forall (start delta : nat) (w1 w2 : list A),
window_agree start delta w1 w2
-> window_agree start delta w2 w1.
Proof.
unfold window_agree.
intros. firstorder.
Qed.
Lemma window_agree_2_comm {A : Type} : forall (start1 start2 delta : nat) (w1 w2 : list A),
window_agree_2 start1 start2 delta w1 w2
-> window_agree_2 start2 start1 delta w2 w1.
Proof.
unfold window_agree_2.
intros. firstorder.
Qed.
Lemma window_agree_agree_2 {A : Type} : forall (start delta : nat) (w1 w2 : list A),
window_agree start delta w1 w2
-> window_agree_2 start start delta w1 w2.
Proof.
unfold window_agree_2, window_agree.
intros. auto.
Qed.
Lemma window_agree_2_agree {A : Type} : forall (start1 start2 delta : nat) (w1 w2 : list A),
start2 >= start1
-> window_agree_2 start1 start2 delta w1 w2
-> window_agree start1 delta w1 (skipn (start2 - start1) w2).
Proof.
unfold window_agree_2, window_agree.
intros.
rewrite <- nth_error_skipn.
replace (start1 + i + (start2 - start1)) with (start2 + i) by lia.
now apply H0.
Qed.
(* when the first window contains the second window, then the second window agrees automatically *)
Lemma window_agree_smaller {A : Type} : forall (start delta : nat) (w1 w2 : list A),
window_agree start delta w1 w2
-> forall start' delta',
start' >= start
-> start' + delta' <= start + delta
-> window_agree start' delta' w1 w2.
Proof.
intros.
intros i' Hi'.
replace (start' + i') with (start + (i' + (start' - start))) by lia.
apply H. lia.
Qed.
Lemma window_agree_2_smaller {A : Type} : forall (start1 start2 delta : nat) (w1 w2 : list A),
window_agree_2 start1 start2 delta w1 w2
-> forall d' delta',
start1 + d' + delta' <= start1 + delta
-> start2 + d' + delta' <= start2 + delta
-> window_agree_2 (start1 + d') (start2 + d') delta' w1 w2.
Proof.
intros.
intros i' Hi'.
replace (start1 + d' + i') with (start1 + (i' + d')) by lia.
replace (start2 + d' + i') with (start2 + (i' + d')) by lia.
apply H. lia.
Qed.
Lemma window_agree_firstn {A : Type} (w : list A) (n : nat) :
window_agree 0 n w (firstn n w).
Proof.
intros.
intros i Hi.
simpl.
now rewrite nth_error_firstn by assumption.
Qed.
Lemma window_agree_2_skipn {A : Type} (w : list A) (n : nat) :
window_agree_2 n 0 (length w - n) w (skipn n w).
Proof.
intros.
intros i Hi.
simpl. replace (n + i) with (i + n) by lia.
now rewrite nth_error_skipn.
Qed.
(* seq *)
Lemma seq_nth_error : forall start len i,
i < len
-> nth_error (seq start len) i = Some (start + i).
Proof.
intros start len i.
revert start len.
induction i; intros.
- destruct len; [lia | ].
simpl. auto.
- destruct len; [lia | ].
simpl.
specialize (IHi (S start) len ltac:(lia)).
rewrite IHi. f_equal. lia.
Qed.
(* altr / last_Some / opt_enum / find_largest_true *)
Definition altl {X : Type} (a b : option X) : option X :=
match a with
| None => b
| _ => a
end.
Definition altr {X : Type} (a b : option X) : option X :=
match b with
| None => a
| _ => b
end.
Notation "a <<|> b" := (altl a b) (at level 50).
Notation "a <|>> b" := (altr a b) (at level 50).
Lemma altl_None_r {X} : forall (a : option X),
a <<|> None = a.
Proof.
intros. unfold altl. destruct a; auto.
Qed.
Lemma altr_None_l {X} : forall (a : option X),
None <|>> a = a.
Proof.
intros. unfold altr. destruct a; auto.
Qed.
Lemma altl_None_inv {X} : forall (a b : option X),
a <<|> b = None
-> a = None /\ b = None.
Proof.
intros; destruct a; destruct b; inversion H; auto.
Qed.
Lemma altr_None_inv {X} : forall (a b : option X),
a <|>> b = None
-> a = None /\ b = None.
Proof.
intros; destruct a; destruct b; inversion H; auto.
Qed.
Lemma altl_assoc {X} : forall (a b c : option X),
a <<|> (b <<|> c) = (a <<|> b) <<|> c.
Proof.
intros. unfold altl. destruct a, b, c; auto.
Qed.
Lemma altr_assoc {X} : forall (a b c : option X),
a <|>> (b <|>> c) = (a <|>> b) <|>> c.
Proof.
intros. unfold altr. destruct a, b, c; auto.
Qed.
Definition first_Some {X} (l : list (option X)) : option X :=
fold_right altl None l .
Definition last_Some {X} (l : list (option X)) : option X :=
fold_right altr None l .
Lemma first_Some_foldr {X} : forall (l : list (option X)) (x : option X),
fold_right altl x l = first_Some l <<|> x.
Proof.
induction l.
- auto.
- intros. simpl. rewrite IHl. rewrite altl_assoc. auto.
Qed.
Lemma last_Some_foldr {X} : forall (l : list (option X)) (x : option X),
fold_right altr x l = last_Some l <|>> x .
Proof.
induction l.
- intros. simpl. rewrite altr_None_l. auto.
- intros. simpl. rewrite IHl.
rewrite altr_assoc. auto.
Qed.
Lemma first_Some_app {X} : forall (l1 l2 : list (option X)),
first_Some (l1 ++ l2) = first_Some l1 <<|> first_Some l2.
Proof.
intros. unfold first_Some. rewrite fold_right_app.
rewrite first_Some_foldr. auto.
Qed.
Lemma last_Some_app {X} : forall (l1 l2 : list (option X)),
last_Some (l1 ++ l2) = last_Some l1 <|>> last_Some l2.
Proof.
intros. unfold last_Some. rewrite fold_right_app.
rewrite last_Some_foldr. auto.
Qed.
Lemma first_Some_None_iff {X} : forall (l : list (option X)),
first_Some l = None
<-> forall x, In x l -> x = None.
Proof.
split.
{ induction l.
- intros. destruct H0.
- intros. simpl in H.
apply altr_None_inv in H as [H1 H2].
subst a. destruct H0; auto.
}
{ induction l.
- auto.
- intros. simpl.
specialize (H a ltac:(left; auto)) as HH. subst a.
simpl. apply IHl. intros.
apply H. right. auto.
}
Qed.
Lemma last_Some_None_iff {X} : forall (l : list (option X)),
last_Some l = None
<-> forall x, In x l -> x = None.
Proof.
split.
{ induction l.
- intros. destruct H0.
- intros. simpl in H.
apply altr_None_inv in H as [H1 H2].
subst a. destruct H0; auto.
}
{ induction l.
- auto.
- intros. simpl.
specialize (H a ltac:(left; auto)) as HH. subst a.
rewrite altr_None_l. apply IHl. intros.
apply H. right. auto.
}
Qed.
Lemma first_Some_nth_error {X} : forall (l : list (option X)) i,
forall x, nth_error l i = Some (Some x)
-> (forall j, j < i -> nth_error l j = Some None)
-> first_Some l = Some x.
Proof.
intros.
assert (i < length l) as Li. {
rewrite <- nth_error_Some. congruence.
}
pose proof (firstn_skipn i l).
remember (firstn i l) as l1.
assert (length l1 = i) as Ll1. {
subst l1. rewrite firstn_length.
lia.
}
assert (forall b, In b l1 -> b = None) as Hnone. {
intros. subst l1.
apply In_nth_error in H2.
destruct H2 as [j Hj].
assert (j < i) as Hjlen. {
rewrite <- Ll1.
rewrite <- nth_error_Some. congruence.
}
erewrite nth_error_firstn in Hj by apply Hjlen.
specialize (H0 j ltac:(lia)).
congruence.
}
rewrite <- H1.
rewrite first_Some_app.
rewrite <- first_Some_None_iff in Hnone. rewrite Hnone.
simpl.
destruct (skipn i l) as [| a l2] eqn:E.
{
apply f_equal with (f := @length (option X)) in E.
rewrite skipn_length in E. simpl in E.
lia.
}
simpl. rewrite <- H1 in H.
rewrite nth_error_app2 in H by lia.
replace (i - length l1) with 0 in H by lia. simpl in H.
inversion H. auto.
Qed.
Lemma last_Some_nth_error {X} : forall (l : list (option X)) i,
forall x, nth_error l i = Some (Some x)
-> (forall j, j > i -> j < length l -> nth_error l j = Some None)
-> last_Some l = Some x.
Proof.
intros.
assert (i < length l) as Li. {
rewrite <- nth_error_Some. congruence.
}
pose proof (firstn_skipn (S i) l).
remember (skipn (S i) l) as l2.
assert (forall b, In b l2 -> b = None) as Hnone. {
intros. subst l2.
apply In_nth_error in H2.
destruct H2 as [j' Hj'].
rewrite <- nth_error_skipn in Hj'.
assert (j' + S i < length l) as Hjlen. {
rewrite <- nth_error_Some. congruence.
}
specialize (H0 (j' + S i) ltac:(lia) ltac:(lia)).
congruence.
}
rewrite <- H1.
rewrite last_Some_app.
rewrite <- last_Some_None_iff in Hnone. rewrite Hnone.
destruct (unsnoc (firstn (S i) l)) as [[l1 a] | ] eqn:E.
2 : {
apply unsnoc_None in E.
apply f_equal with (f := @length (option X)) in E.
rewrite firstn_length in E.
simpl length in E. lia.
}
rewrite unsnoc_Some in E.
rewrite E.
rewrite last_Some_app. simpl.
erewrite <- nth_error_firstn in H.
rewrite E in H. 2 : lia.
assert (length l1 = i) as Hl1. {
apply f_equal with (f := @length (option X)) in E.
rewrite firstn_length in E.
rewrite app_length in E. simpl length in E. lia.
}
rewrite nth_error_app2 in H by lia.
replace (i - length l1) with 0 in H by lia.
simpl in H. inversion H. auto.
Qed.
Lemma first_Some_nth_error_bw {X} : forall (l : list (option X)),
forall x, first_Some l = Some x
-> exists i, nth_error l i = Some (Some x)
/\ (forall j, j < i -> nth_error l j = Some None).
Proof.
induction l. {
intros. simpl in H. inversion H.
}
intros. simpl in H.
destruct a as [a | ]; simpl in H.
{
inversion H. subst a.
exists 0. split.
- simpl. auto.
- intros. inversion H0.
}
{
specialize (IHl x H) as [i [Hi Hnone]].
exists (S i). split.
- simpl. auto.
- intros. destruct j.
+ simpl. auto.
+ simpl. apply Hnone. lia.
}
Qed.
Lemma last_Some_nth_error_bw {X} : forall (l : list (option X)),
forall x, last_Some l = Some x
-> exists i, nth_error l i = Some (Some x)
/\ (forall j, j > i -> j < length l -> nth_error l j = Some None).
Proof.
induction l using rev_ind.
{
intros. simpl in H. inversion H.
}
intros. destruct x as [x | ].
{
rewrite last_Some_app in H.
simpl in H. inversion H. subst x0.
exists (length l). split.
- rewrite nth_error_app2. 2 : lia.
replace (length l - length l) with 0 by lia.
simpl. auto.
- intros. rewrite app_length in H1. simpl in H1. lia.
}
{
rewrite last_Some_app in H.
simpl in H.
specialize (IHl x0 H) as [i [Hi Hnone]].
exists i. split.
- rewrite nth_error_app1. auto.
apply nth_error_Some. congruence.
- intros. rewrite app_length in H1. simpl in H1.
assert (j < length l \/ j = length l) as [Hj | Hj] by lia.
+ rewrite nth_error_app1. apply Hnone. lia. auto. auto.
+ subst j. rewrite nth_error_app2. 2 : lia.
replace (length l - length l) with 0 by lia.
simpl. auto.
}
Qed.
Definition opt_enum (lb : list bool) : list (option nat) :=
zipWith (fun (b : bool) i => if b then Some i else None) lb (seq 0 (length lb)).
Lemma opt_enum_length : forall lb,
length (opt_enum lb) = length lb.
Proof.
intros. unfold opt_enum. rewrite zipWith_length.
rewrite seq_length. lia.
Qed.
Lemma opt_enum_nth_error : forall lb i,
i < length lb
-> nth_error (opt_enum lb) i = Some (Some i)
<-> nth_error lb i = Some true.
Proof.
intros. unfold opt_enum.
rewrite nth_error_zipWith.
rewrite seq_nth_error. 2 : lia.
simpl. rewrite nth_error_Some_ex in H.
destruct H as [x Hx].
rewrite Hx. split.
- intros X. inversion X. f_equal.
destruct x; [auto | discriminate].
- intros X. inversion X. f_equal.
Qed.
Lemma opt_enum_nth_error_2 : forall lb i,
i < length lb
-> nth_error (opt_enum lb) i = Some None
\/ nth_error (opt_enum lb) i = Some (Some i).
Proof.
intros. unfold opt_enum.
rewrite nth_error_zipWith.
rewrite seq_nth_error. 2 : lia.
simpl. rewrite nth_error_Some_ex in H.
destruct H as [x Hx].
destruct x.
- right. now rewrite Hx.
- left. now rewrite Hx.
Qed.
Lemma opt_enum_nth_error_3 : forall lb i,
i < length lb
-> nth_error (opt_enum lb) i = Some None
<-> nth_error lb i = Some false.
Proof.
intros.
pose proof (opt_enum_length lb).
assert (i < length (opt_enum lb)) by congruence.
assert (Hi := H). assert (Hi' := H1).
rewrite nth_error_Some_ex in H.
destruct H as [x Hx].
rewrite nth_error_Some_ex in H1.
destruct H1 as [y Hy].
destruct x.
-
split.
+ intros. rewrite <- opt_enum_nth_error in Hx. congruence. auto.
+ intros. congruence.
- split; intros.
+ destruct y.
* congruence.
* auto.
+ destruct y.
* pose proof (opt_enum_nth_error_2 lb i Hi) as [X | X].
-- congruence.
-- rewrite opt_enum_nth_error in X. 2 : auto.
congruence.
* auto.
Qed.
Lemma opt_enum_first_Some_fw : forall lb,
forall i, nth_error lb i = Some true
-> (forall j, j < i -> nth_error lb j = Some false)
-> first_Some (opt_enum lb) = Some i.
Proof.
intros. eapply first_Some_nth_error.
- rewrite opt_enum_nth_error; [ assumption | ].
apply nth_error_Some. congruence.
- intros.
rewrite opt_enum_nth_error_3; [ auto | ].
assert (i < length lb) by
(apply nth_error_Some; congruence).
lia.
Qed.
Lemma opt_enum_last_Some_fw : forall lb,
forall i, nth_error lb i = Some true
-> (forall j, j > i -> j < length lb -> nth_error lb j = Some false)
-> last_Some (opt_enum lb) = Some i.
Proof.
intros. eapply last_Some_nth_error.
- rewrite opt_enum_nth_error.
+ auto.
+ rewrite <- nth_error_Some. congruence.
- intros. rewrite opt_enum_length in H2.
rewrite opt_enum_nth_error_3; [ | assumption].
apply H0; [ | assumption]. assumption.
Qed.
Lemma opt_enum_first_Some_bw : forall lb i,
first_Some (opt_enum lb) = Some i
-> nth_error lb i = Some true
/\ (forall j, j < i -> nth_error lb j = Some false).
Proof.
intros. apply first_Some_nth_error_bw in H.
destruct H as [j [Hj Hnone]].
assert (j < length lb) as Hjlen. {
rewrite <- opt_enum_length.
rewrite <- nth_error_Some. congruence.
}
destruct (opt_enum_nth_error_2 lb j ltac:(lia)) as [Hj' | Hj'].
1 : congruence.
rewrite Hj' in Hj. inversion Hj. subst i.
rewrite opt_enum_nth_error in Hj'. 2 : auto.
split; [auto | ].
intros.
specialize (Hnone j0 H).
rewrite opt_enum_nth_error_3 in Hnone; auto.
assert (j < length lb) by (apply nth_error_Some; congruence).
lia.
Qed.
Lemma opt_enum_last_Some_bw : forall lb i,
last_Some (opt_enum lb) = Some i
-> nth_error lb i = Some true
/\ (forall j, j > i -> j < length lb -> nth_error lb j = Some false).
Proof.
intros. apply last_Some_nth_error_bw in H.
destruct H as [j [Hj Hnone]].
assert (j < length lb) as Hjlen. {
rewrite <- opt_enum_length.
rewrite <- nth_error_Some. congruence.
}
destruct (opt_enum_nth_error_2 lb j ltac:(lia)) as [Hj' | Hj'].
1 : congruence.
rewrite Hj' in Hj. inversion Hj. subst i.
rewrite opt_enum_nth_error in Hj'. 2 : auto.
split; [auto | ].
intros. rewrite opt_enum_length in Hnone.
specialize (Hnone j0 H H0).
rewrite opt_enum_nth_error_3 in Hnone; auto.
Qed.
Definition find_smallest_true (lb : list bool) : option nat :=
first_Some (opt_enum lb).
Definition find_largest_true (lb : list bool) : option nat :=
last_Some (opt_enum lb).
Lemma find_smallest_true_Some : forall lb i,
find_smallest_true lb = Some i
<-> nth_error lb i = Some true
/\ (forall j, j < i -> nth_error lb j = Some false).
Proof.
intros. unfold find_smallest_true.
split.
- intros. apply opt_enum_first_Some_bw in H.
auto.
- intros. destruct H as [H1 H2]. apply opt_enum_first_Some_fw; auto.
Qed.
Lemma find_largest_true_Some : forall lb i,
find_largest_true lb = Some i
<-> nth_error lb i = Some true
/\ (forall j, j > i -> j < length lb -> nth_error lb j = Some false).
Proof.
intros. unfold find_largest_true.
split.
- intros. apply opt_enum_last_Some_bw in H. auto.
- intros. destruct H as [H1 H2]. apply opt_enum_last_Some_fw; auto.
Qed.
Lemma find_smallest_true_None : forall lb,
find_smallest_true lb = None
<-> forall b, In b lb -> b = false.
Proof.
intros. unfold find_smallest_true.
rewrite first_Some_None_iff.
split.
- intros. apply In_nth_error in H0.
destruct H0 as [i Hi].
destruct (nth_error (opt_enum lb) i) eqn:E.
+ assert (E' := E). apply nth_error_In in E. apply H in E.
subst o. rewrite opt_enum_nth_error_3 in E'.
* congruence.
* apply nth_error_Some. congruence.
+ apply nth_error_None in E. rewrite opt_enum_length in E.
pose proof (nth_error_Some lb i).
rewrite Hi in H0. assert (Some b <> None) by discriminate.
rewrite H0 in H1. lia.
- intros. apply In_nth_error in H0.
destruct H0 as [i Hi].
destruct x. 2 : auto.
assert (i < length lb) as Hilen. {
replace (length lb) with (length (opt_enum lb)).
rewrite <- nth_error_Some. congruence.
apply opt_enum_length.
}
destruct (opt_enum_nth_error_2 lb i ltac:(lia)) as [H1 | H1].
{ congruence. }
rewrite H1 in Hi. inversion Hi. subst n.
rewrite opt_enum_nth_error in H1. 2 : apply Hilen.
apply nth_error_In in H1.
specialize (H true H1). discriminate.
Qed.
Lemma find_largest_true_None : forall lb,
find_largest_true lb = None
<-> forall b, In b lb -> b = false.
Proof.
intros. unfold find_largest_true.
rewrite last_Some_None_iff.
split.
- intros. apply In_nth_error in H0.
destruct H0 as [i Hi].
destruct (nth_error (opt_enum lb) i) eqn:E.
+ assert (E' := E). apply nth_error_In in E. apply H in E.
subst o. rewrite opt_enum_nth_error_3 in E'.
* congruence.
* apply nth_error_Some. congruence.
+ apply nth_error_None in E. rewrite opt_enum_length in E.
pose proof (nth_error_Some lb i).
rewrite Hi in H0. assert (Some b <> None) by discriminate.
rewrite H0 in H1. lia.
- intros. apply In_nth_error in H0.
destruct H0 as [i Hi].
destruct x. 2 : auto.
assert (i < length lb) as Hilen. {
replace (length lb) with (length (opt_enum lb)).
rewrite <- nth_error_Some. congruence.
apply opt_enum_length.
}
destruct (opt_enum_nth_error_2 lb i ltac:(lia)) as [H1 | H1].
{ congruence. }
rewrite H1 in Hi. inversion Hi. subst n.
rewrite opt_enum_nth_error in H1. 2 : apply Hilen.
apply nth_error_In in H1.
specialize (H true H1). discriminate.
Qed.
Lemma find_smallest_true_bounded : forall lb i,
find_smallest_true lb = Some i
-> i < length lb.
Proof.
intros. apply find_smallest_true_Some in H.
destruct H as [H1 H2].
apply nth_error_Some. congruence.
Qed.
Lemma find_largest_true_bounded : forall lb i,
find_largest_true lb = Some i
-> i < length lb.
Proof.
intros. apply find_largest_true_Some in H.
destruct H as [H1 H2].
apply nth_error_Some. congruence.
Qed.
(* concat *)
Lemma concat_length {A : Type} : forall (l : list (list A)),
length (concat l) = fold_right (plus) 0 (map (@length A) l).
Proof.
induction l.
- auto.
- simpl. rewrite app_length. rewrite IHl.
auto.
Qed.
Lemma concat_filter_negb_nilb {A : Type} : forall (l : list (list A)),
concat (filter (fun x => negb (nilb x)) l) = concat l.
Proof.
induction l.
- auto.
- simpl. destruct (nilb a) eqn:Ha.
+ simpl. rewrite IHl. rewrite nilb_true in Ha. subst a. auto.
+ simpl. f_equal. apply IHl.
Qed.
Lemma concat_nil {A : Type} : forall (l : list (list A)),
concat l = [] -> l = repeat [] (length l).
Proof.
induction l.
- auto.
- simpl. intros.
apply app_eq_nil in H as [H1 H2].
subst. f_equal. apply IHl. auto.
Qed.
(* forallb / existsb *)
Lemma existsb_false {A : Type} : forall (f : A -> bool) (l : list A),
existsb f l = false
<-> (forall x, In x l -> f x = false).
Proof.
induction l.
- simpl. split; tauto.
- simpl. split.
+ intros. rewrite Bool.orb_false_iff in H.
destruct H.
* intros. destruct H0; [ subst; auto | ].
rewrite IHl in H1. auto.
+ intros. rewrite Bool.orb_false_iff.
split.
* apply H. left. auto.
* apply IHl. intros. apply H. auto.
Qed.
Lemma forallb_false {A : Type} : forall (f : A -> bool) (l : list A),
forallb f l = false
<-> (exists x, In x l /\ f x = false).
Proof.
induction l.
- simpl. split; [ discriminate | firstorder].
- simpl. rewrite Bool.andb_false_iff. split.
+ intros. destruct H.
* exists a. split; auto.
* rewrite IHl in H. destruct H as [x [Hx1 Hx2]].
exists x. split; auto.
+ intros.
destruct H as [x [Hx1 Hx2]].
destruct Hx1.
* subst. auto.
* right. rewrite IHl. exists x. auto.
Qed.
Lemma forallb_existsb {A : Type} : forall (f : A -> bool) (l : list A),
forallb f l = negb (existsb (fun x => negb (f x)) l).
Proof.
induction l.
- auto.
- simpl. rewrite IHl.
rewrite Bool.negb_orb.
rewrite Bool.negb_involutive.
auto.
Qed.
Lemma existsb_forallb {A : Type} : forall (f : A -> bool) (l : list A),
existsb f l = negb (forallb (fun x => negb (f x)) l).
Proof.
induction l.
- auto.
- simpl. rewrite IHl.
rewrite Bool.negb_andb.
rewrite Bool.negb_involutive.
auto.
Qed.
(* scan_left *)
Fixpoint scan_left {A B : Type} (f : A -> B -> A) (l : list B) (init : A) : list A :=
match l with
| [] => [init]
| b :: l' => init :: scan_left f l' (f init b)
end.
Lemma scan_left_length {A B : Type} : forall (f : A -> B -> A) (l : list B) (init : A),
length (scan_left f l init) = S (length l).
Proof.
induction l.
- auto.
- simpl. intros. f_equal. apply IHl.
Qed.
Lemma scan_left_snoc {A B : Type} : forall (f : A -> B -> A) (l : list B) (init : A) (b : B),
scan_left f (l ++ [b]) init = scan_left f l init ++ [fold_left f (l ++ [b]) init].
Proof.
induction l.
- simpl. auto.
- intros. simpl. rewrite IHl. auto.
Qed.
Lemma scan_left_last_error {A B : Type} : forall (f : A -> B -> A) (l : list B) (init : A),
last_error (scan_left f l init) = Some (fold_left f l init).
Proof.
destruct l using rev_ind.
- auto.
- intros. rewrite scan_left_snoc. now rewrite last_error_snoc.
Qed.
Lemma scan_left_app {A B : Type} : forall (f : A -> B -> A) (l1 l2 : list B) (x : B) (init : A),
scan_left f (l1 ++ x :: l2) init = scan_left f l1 init ++ scan_left f l2 (fold_left f (l1 ++ [x]) init).
Proof.
induction l1.
- auto.
- intros. simpl. f_equal. apply IHl1.
Qed.
Lemma scan_left_nth_error {A B : Type} : forall (f : A -> B -> A) (l : list B) (init : A) (i : nat),
i <= length l
-> nth_error (scan_left f l init) i = Some (fold_left f (firstn i l) init).
Proof.
intros.
rewrite <- firstn_skipn with (n := i) (l := l) at 1.
remember (firstn i l) as l1. remember (skipn i l) as l2.
destruct l2 eqn:El2.
{ pose proof (skipn_length i l) as Hlen.
rewrite <- Heql2 in Hlen. simpl in Hlen.
assert (length l = i) as Hleni by lia.
assert (length l1 = i) as Hleni1 by (subst; apply firstn_length_le; lia).
rewrite app_nil_r, <- Hleni1.
replace (length l1) with (length (scan_left f l1 init) - 1).
2 : { rewrite scan_left_length. lia. }
rewrite <- last_error_nth_error.
now apply scan_left_last_error.
}
rewrite scan_left_app.
pose proof (firstn_length i l) as Hleni.
replace (min i (length l)) with i in Hleni by lia.
rewrite <- Heql1 in Hleni.
rewrite nth_error_app1 by (rewrite scan_left_length; lia).
replace i with (length (scan_left f l1 init) - 1) by (rewrite scan_left_length; lia).
rewrite <- last_error_nth_error.
now apply scan_left_last_error.
Qed.
Lemma scan_left_nth_error_incr {A B : Type} : forall (f : A -> B -> A) (l : list B) (init : A) (i : nat),
forall a, nth_error (scan_left f l init) i = Some a
-> forall b, nth_error l i = Some b
-> nth_error (scan_left f l init) (S i) = Some (f a b).
Proof.
intros.
assert (i < length l) as Hlen. {
rewrite <- nth_error_Some. congruence.
}
assert (i <= length l) as Hlen' by lia.
assert (S i <= length l) as Hlen'' by lia.
rewrite scan_left_nth_error in H |- * by auto.
assert (firstn (S i) l = firstn i l ++ [b]) as Hfirstn. {
rewrite <- firstn_skipn with (n := i) (l := l) at 1.
replace (S i) with (i + 1) by lia.
replace i with (length (firstn i l)) at 1 by (rewrite firstn_length; lia).
rewrite firstn_app_2.
f_equal.
destruct (firstn 1 (skipn i l)) eqn:E.
- pose proof (firstn_length 1 (skipn i l)).
rewrite E in H1. simpl length in H1.
assert (length (skipn i l) = 0) by lia.
rewrite skipn_length in H2. lia.
- f_equal.
+ apply f_equal with (f := @hd_error B) in E.
rewrite hd_error_nth_error in E.
rewrite nth_error_firstn in E by lia.
rewrite <- nth_error_skipn in E.
simpl in E. congruence.
+ destruct l0; [ auto | ].
apply f_equal with (f := @length B) in E.
rewrite firstn_length in E. simpl length in E. lia.
}
rewrite Hfirstn. rewrite fold_left_app.
inversion H. auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment