Require Import compcert.lib.Coqlib.
Require Import VST.msl.Coqlib2.
Require Import Coq.Lists.List.
Import ListNotations.

Class Inhabitant (A: Type) := default : A.

Instance Inhabitant_Z : Inhabitant Z := 0.
Instance Inhabitant_nat : Inhabitant nat := O.
Instance Inhabitant_positive : Inhabitant positive := 1%positive.
Instance Inhabitant_list {T: Type} : Inhabitant (list T) := @nil T.
Instance Inhabitant_fun {T1 T2: Type} {H: Inhabitant T2} : Inhabitant (T1->T2) := fun _ => H.
Instance Inhabitant_Prop : Inhabitant Prop := False.
Instance Inhabitant_bool : Inhabitant bool := false.
Instance Inhabitant_pair {T1 T2 : Type} {x1: Inhabitant T1} {x2: Inhabitant T2} : Inhabitant (T1*T2)%type := (x1,x2).

Lemma Zlength_length:
  forall A (al: list A) (n: Z),
    0 <= n ->
    (Zlength al = n <-> length al = Z.to_nat n).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. rewrite Zlength_correct.
(* Goal: iff (@eq Z (Z.of_nat (@Datatypes.length A al)) n) (@eq nat (@Datatypes.length A al) (Z.to_nat n)) *)
split; intro.
(* Goal: @eq nat (@Datatypes.length A al) (Z.to_nat n) *)
(* Goal: @eq Z (Z.of_nat (@Datatypes.length A al)) n *)
rewrite <- (Z2Nat.id n) in H0 by omega.
(* Goal: @eq nat (@Datatypes.length A al) (Z.to_nat n) *)
(* Goal: @eq Z (Z.of_nat (@Datatypes.length A al)) n *)
apply Nat2Z.inj in H0; auto.
(* Goal: @eq Z (Z.of_nat (@Datatypes.length A al)) n *)
rewrite H0.
(* Goal: @eq Z (Z.of_nat (Z.to_nat n)) n *)
apply Z2Nat.inj; try omega.
(* Goal: @eq nat (Init.Nat.sub (Z.to_nat i) (@Datatypes.length A l)) (Init.Nat.sub (Z.to_nat i) (Z.to_nat (Z.of_nat (@Datatypes.length A l)))) *)
(* Goal: ge (Z.to_nat i) (@Datatypes.length A l) *)
rewrite Nat2Z.id; auto.
Qed.

Lemma firstn_app1: forall {A} n (p l: list A),
  (n <= Datatypes.length p)%nat ->
   firstn n (p ++ l) = firstn n p.
(* Goal: forall (A : Type) (n : nat) (p l : list A) (_ : le n (@Datatypes.length A p)), @eq (list A) (@firstn A n (@app A p l)) (@firstn A n p) *)
Proof. intros A n.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; simpl; intros. trivial.
(* Goal: @eq (list A) match @app A p l with | nil => @nil A | cons a l => @cons A a (@firstn A n l) end match p with | nil => @nil A | cons a l => @cons A a (@firstn A n l) end *)
  destruct p; simpl in H. omega.
(* Goal: @eq (list A) match @app A (@cons A a p) l with | nil => @nil A | cons a l => @cons A a (@firstn A n l) end (@cons A a (@firstn A n p)) *)
  apply le_S_n in H. simpl. f_equal. auto.
Qed.

Lemma firstn_app2: forall {A} (n: nat) (al bl: list A),
 (n >= length al)%nat ->
 firstn n (al++bl) = al ++ firstn (n - length al) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. revert al H.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; destruct al; intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
(* Goal: @Forall A f al *)
destruct bl; auto.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal. apply IHn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
simpl in H; omega.
Qed.

Lemma firstn_list_repeat {A} (v:A): forall i k, (i<=k)%nat ->
      firstn i (list_repeat k v) = list_repeat i v.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  induction i; simpl; trivial; intros.
(* Goal: @eq A v v *)
  destruct k. omega. simpl. rewrite IHi; trivial. omega.
Qed.

Lemma firstn_app:
 forall {A} n m (al: list A), firstn n al ++ firstn m (skipn n al) =
  firstn (n+m) al.
(* Goal: @Forall A f al *)
Proof. induction n; destruct al; intros; simpl; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
destruct m; reflexivity.
(* Goal: @Forall A f al *)
f_equal; auto.
Qed.

Lemma nth_skipn:
  forall {A} i n data (d:A),
       nth i (skipn n data) d = nth (i+n) data d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
revert i data; induction n; simpl; intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal; omega.
(* Goal: @Forall A f al *)
destruct data; auto.
(* Goal: @Forall A f al *)
destruct i; simpl; auto.
(* Goal: @eq (list A) (@rev A (@skipn A n vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) n) (@app A (@rev A vl) (@cons A a (@nil A)))) *)
rewrite IHn.
(* Goal: @Forall A f al *)
replace (i + S n)%nat with (S (i + n))%nat by omega; auto.
Qed.

Lemma skipn_skipn: forall {A} n m (xs: list A),
  skipn n (skipn m xs) = skipn (m + n) xs.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  revert xs; induction m; intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  + simpl.
(* Goal: @eq (list A) (@skipn A n match xs with | nil => @nil A | cons a l => @skipn A m l end) match xs with | nil => @nil A | cons a l => @skipn A (Init.Nat.add m n) l end *)
    destruct xs.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - destruct n; reflexivity.
    - apply IHm.
Qed.

Lemma firstn_exact_length: forall {A} (xs: list A), firstn (length xs) xs = xs.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@skipn A (@Datatypes.length A xs) xs) (@nil A) *)
  induction xs.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  + simpl.
(* Goal: @eq (list A) (@skipn A (@Datatypes.length A xs) xs) (@nil A) *)
    rewrite IHxs.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    reflexivity.
Qed.

Lemma skipn_exact_length: forall {A} (xs: list A), skipn (length xs) xs = nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@skipn A (@Datatypes.length A xs) xs) (@nil A) *)
  induction xs.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  + simpl.
(* Goal: @eq (list A) (@skipn A (@Datatypes.length A xs) xs) (@nil A) *)
    rewrite IHxs.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    reflexivity.
Qed.

Lemma len_le_1_rev: forall {A} (contents: list A),
  (length contents <= 1)%nat ->
  contents = rev contents.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@cons A a contents) (@rev A (@cons A a contents)) *)
  destruct contents.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + reflexivity.
  + destruct contents.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - simpl in H. omega.
Qed.

Lemma firstn_firstn: forall {A} (contents: list A) n m,
  (n <= m)%nat ->
  firstn n (firstn m contents) = firstn n contents.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
  revert n m H;
  induction contents;
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + destruct n, m; reflexivity.
  + destruct n, m; try solve [omega].
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - simpl; reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - simpl; reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
    - simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      rewrite IHcontents by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      reflexivity.
Qed.

Lemma firstn_1_skipn: forall {A} n (ct: list A) d,
  (n < length ct)%nat ->
  nth n ct d :: nil = firstn 1 (skipn n ct).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@cons A (@nth A n ct d) (@nil A)) (@firstn A (S O) (@skipn A n ct)) *)
  revert ct H; induction n; intros; destruct ct.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + simpl in H; omega.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  + simpl. reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + simpl in H; omega.
  + simpl in H |- *.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    rewrite IHn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    reflexivity.
Qed.

Lemma skipn_length: forall {A} (contents: list A) n,
  length (skipn n contents) = (length contents - n)%nat.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
  revert n;
  induction contents;
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + destruct n; reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  + destruct n; simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - reflexivity.
    - apply IHcontents.
Qed.

Lemma nth_firstn: forall {A} (contents: list A) n m d,
  (n < m)%nat ->
  nth n (firstn m contents) d = nth n contents d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
  revert n m H;
  induction contents;
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + destruct n, m; reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + destruct n, m; try omega.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
    - simpl. reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - simpl. apply IHcontents. omega.
Qed.

Lemma skipn_length_short:
  forall {A} n (al: list A),
    (length al <= n)%nat ->
    (length (skipn n al) = 0)%nat.
Proof.
(* Goal: @Forall A f al *)
 induction n; destruct al; simpl; intros; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
 omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
 apply IHn. omega.
Qed.

Lemma skipn_short:
   forall {A} n (al: list A), (n >= length al)%nat -> skipn n al = nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@skipn A n al) (@nil A) *)
pose proof (skipn_length_short n al).
(* Goal: @Forall A f al *)
assert (length al <= n)%nat by auto.
(* Goal: @eq (list A) (@skipn A n al) (@nil A) *)
specialize (H0 H1).
(* Goal: @Forall A f al *)
destruct (skipn n al); inv H0; auto.
Qed.

Lemma nth_map':
  forall {A B} (f: A -> B) d d' i al,
  (i < length al)%nat ->
   nth i (map f al) d = f (nth i al d').
Proof.
(* Goal: @Forall A f al *)
induction i; destruct al; simpl; intros; try omega; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply IHi; omega.
Qed.


Lemma skipn_nil: forall A n, skipn n (@nil A) = nil.
(* Goal: @Forall A f al *)
Proof. induction n; simpl; auto.
Qed.

Lemma skipn_drop:
 forall A n m (al: list A), skipn n (skipn m al) = skipn (n+m) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction m; intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
* simpl; auto. f_equal; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
* replace (n + S m)%nat with (S (n + m))%nat by omega.
(* Goal: @eq (list A) (@skipn A n (@skipn A (S m) al)) (@skipn A (S (Init.Nat.add n m)) al) *)
  destruct al; [ rewrite skipn_nil; auto | ].
(* Goal: @eq (list A) (@skipn A n (@skipn A (S m) (@cons A a al))) (@skipn A (S (Init.Nat.add n m)) (@cons A a al)) *)
  unfold skipn at 3; fold skipn.
 rewrite <- IHm.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
 f_equal.
Qed.

Lemma skipn_app1:
 forall A n (al bl: list A),
  (n <= length al)%nat ->
  skipn n (al++bl) = skipn n al ++ bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. revert al H;
(* Goal: @Forall A f al *)
induction n; destruct al; intros; simpl in *; try omega; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply IHn; omega.
Qed.

Lemma skipn_app2:
 forall A n (al bl: list A),
  (n >= length al)%nat ->
  skipn n (al++bl) = skipn (n-length al) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. revert al H;
(* Goal: @Forall A f al *)
induction n; destruct al; intros; simpl in *; try omega; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply IHn; omega.
Qed.

Lemma list_repeat_app: forall A a b (x:A),
  list_repeat a x ++ list_repeat b x = list_repeat (a+b) x.
Proof.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
intros; induction a; simpl; f_equal.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma firstn_same:
  forall A n (b: list A), (n >= length b)%nat -> firstn n b = b.
Proof.
(* Goal: @Forall A f al *)
induction n; destruct b; simpl; intros; auto.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H.
(* Goal: @Forall A f al *)
f_equal; auto.
(* Goal: @eq (list A) (@firstn A n b) b *)
apply IHn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma nth_firstn_low:
 forall A i n al (d: A),
  (i < n <= length al)%nat -> nth i (firstn n al) d = nth i al d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
revert n al H; induction i; destruct n,al; simpl; intros; auto; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply IHi; omega.
Qed.

Lemma nth_error_nth:
  forall A (d: A) i al, (i < length al)%nat -> nth_error al i = Some (nth i al d).
Proof.
(* Goal: @Forall A f al *)
induction i; destruct al; simpl; intros; auto.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply IHi; omega.
Qed.

Lemma skipn_rev:
  forall {A} n (vl: list A),
   skipn n (rev vl) = rev (firstn (length vl - n) vl).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. rewrite Nat.sub_0_r. rewrite firstn_exact_length. auto.
(* Goal: @eq (list A) (@skipn A (S n) (@rev A vl)) (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) vl)) *)
destruct (rev vl) eqn:?.
(* Goal: @eq (list A) (@skipn A (S n) (@nil A)) (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) vl)) *)
(* Goal: @eq (list A) (@skipn A (S n) (@cons A a l)) (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) vl)) *)
pose proof (rev_length vl). rewrite Heql in H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
destruct vl; inv H. reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
assert (vl = rev l ++ rev [a]).
(* Goal: @Forall A f al *)
rewrite <- rev_app_distr. simpl app. rewrite <- Heql; rewrite rev_involutive; auto.
(* Goal: @eq (list A) (@skipn A n l) (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) vl)) *)
rewrite H.
(* Goal: @eq (list A) (@skipn A n l) (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A (@app A (@rev A l) (@rev A (@cons A a (@nil A))))) (S n)) (@app A (@rev A l) (@rev A (@cons A a (@nil A)))))) *)
rewrite app_length.
(* Goal: @eq (list A) (@skipn A n l) (@rev A (@firstn A (Init.Nat.sub (Init.Nat.add (@Datatypes.length A (@rev A l)) (@Datatypes.length A (@rev A (@cons A a (@nil A))))) (S n)) (@app A (@rev A l) (@rev A (@cons A a (@nil A)))))) *)
simpl length.
rewrite <- (rev_involutive l) at 1.
(* Goal: @eq (list A) (@rev A (@skipn A n vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) n) (@app A (@rev A vl) (@cons A a (@nil A)))) *)
rewrite IHn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
replace (length (rev l) + 1 - S n)%nat with (length (rev l) -n)%nat by omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite firstn_app1 by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
reflexivity.
Qed.

Lemma Forall_list_repeat:
  forall {A} (P: A -> Prop) (n: nat) (a: A),
    P a -> Forall P (list_repeat n a).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; intros.
(* Goal: @Forall A f (@skipn A (S n) (@nil A)) *)
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
constructor.
(* Goal: @Forall A f al *)
constructor; auto.
Qed.

Lemma skipn_firstn: forall {A} n m (xs: list A),
  skipn n (firstn m xs) = firstn (m-n) (skipn n xs).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
revert xs n; induction m; intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. destruct n; reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
destruct xs; simpl.
(* Goal: @eq (list A) (@skipn A n (@nil A)) (@firstn A match n with | O => S m | S l => Init.Nat.sub m l end (@skipn A n (@nil A))) *)
(* Goal: @eq (list A) (@skipn A n (@cons A a (@firstn A m xs))) (@firstn A match n with | O => S m | S l => Init.Nat.sub m l end (@skipn A n (@cons A a xs))) *)
rewrite skipn_nil.
destruct match n with
            | O => S m
            | S l => (m - l)%nat
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
            end; reflexivity.
(* Goal: @eq (list A) (@skipn A n (@cons A a (@firstn A m xs))) (@firstn A match n with | O => S m | S l => Init.Nat.sub m l end (@skipn A n (@cons A a xs))) *)
destruct n.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. reflexivity.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
(* Goal: @eq (list A) (@skipn A n (@firstn A m xs)) (@firstn A (Init.Nat.sub m n) (@skipn A n xs)) *)
apply IHm.
Qed.

Lemma rev_skipn:
 forall {A} n (vl: list A),
  rev (skipn n vl) = firstn (length vl -n) (rev vl).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. rewrite Nat.sub_0_r.
rewrite <- rev_length.
(* Goal: @eq (list A) (@rev A vl) (@firstn A (@Datatypes.length A (@rev A vl)) (@rev A vl)) *)
(* Goal: @eq (list A) (@rev A (@skipn A (S n) vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) (@rev A vl)) *)
rewrite firstn_exact_length.
(* Goal: @Forall A f al *)
auto.
(* Goal: @eq (list A) (@rev A (@skipn A (S n) vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) (S n)) (@rev A vl)) *)
destruct vl.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. auto.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
(* Goal: @eq (list A) (@rev A (@skipn A n vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) n) (@app A (@rev A vl) (@cons A a (@nil A)))) *)
rewrite IHn.
(* Goal: @eq (list A) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) n) (@rev A vl)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) n) (@app A (@rev A vl) (@cons A a (@nil A)))) *)
rewrite firstn_app1 by (rewrite rev_length; omega).
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma firstn_skipn_rev:
  forall {A} lo n (vl: list A),
  (n+lo <= length vl)%nat ->
  firstn n (skipn lo (rev vl)) =
  rev (firstn n (skipn (length vl - (lo+n))%nat vl)).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@firstn A n (@skipn A lo (@rev A vl))) (@rev A (@firstn A n (@skipn A (Init.Nat.sub (@Datatypes.length A vl) (Init.Nat.add lo n)) vl))) *)
rewrite skipn_rev.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
assert (n = (length vl - lo) - (length vl - (lo+n)))%nat by omega.
(* Goal: @eq (list A) (@firstn A n (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) lo) vl))) (@rev A (@firstn A n (@skipn A (Init.Nat.sub (@Datatypes.length A vl) (Init.Nat.add lo n)) vl))) *)
rewrite H0 at 2.
rewrite <- skipn_firstn.
(* Goal: @eq (list A) (@firstn A n (@rev A (@firstn A (Init.Nat.sub (@Datatypes.length A vl) lo) vl))) (@rev A (@skipn A (Init.Nat.sub (@Datatypes.length A vl) (Init.Nat.add lo n)) (@firstn A (Init.Nat.sub (@Datatypes.length A vl) lo) vl))) *)
rewrite rev_skipn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite firstn_length. rewrite min_l by omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma map_firstn:
  forall A B (F: A -> B) n (al: list A),
  map F (firstn n al) = firstn n (map F al).
Proof.
(* Goal: @Forall A f al *)
induction n; destruct al; simpl; intros; auto.
(* Goal: @Forall A f al *)
f_equal; auto.
Qed.

Lemma map_skipn:
  forall A B (F: A -> B) n (al: list A),
  map F (skipn n al) = skipn n (map F al).
Proof.
(* Goal: @Forall A f al *)
induction n; destruct al; simpl; intros; auto.
Qed.

Lemma Zlength_app: forall T (al bl: list T),
    Zlength (al++bl) = Zlength al + Zlength bl.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. induction al; intros. simpl app; rewrite Zlength_nil; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
 simpl app; repeat rewrite Zlength_cons; rewrite IHal; omega.
Qed.

Lemma Zlength_rev: forall T (vl: list T), Zlength (rev vl) = Zlength vl.
(* Goal: @Forall A f al *)
Proof. induction vl; simpl; auto. rewrite Zlength_cons. rewrite <- IHvl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zlength_app. rewrite Zlength_cons. rewrite Zlength_nil; omega.
Qed.

Lemma Zlength_map: forall A B (f: A -> B) l, Zlength (map f l) = Zlength l.
(* Goal: @Forall A f al *)
Proof. induction l; simpl; auto. repeat rewrite Zlength_cons. f_equal; auto.
Qed.

Lemma ZtoNat_Zlength:
 forall {A} (l: list A), Z.to_nat (Zlength l) = length l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. rewrite Zlength_correct. apply Nat2Z.id.
Qed.
Hint Rewrite @ZtoNat_Zlength : norm.

Lemma Zlength_nonneg:
 forall {A} (l: list A), 0 <= Zlength l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. rewrite Zlength_correct. omega.
Qed.

Definition Zlength' := @Zlength.

Ltac pose_Zlength_nonneg1 T A :=
     lazymatch goal with
      | H:  0 <= @Zlength T A |- _ => idtac
      | H:  0 <= @Zlength T A /\ _ |- _ => idtac
      | |- _ => pose proof (@Zlength_nonneg T A)
     end;
     (* the next three lines are to avoid blowups in the change command *)
     let x := fresh "x" in set (x:= @Zlength T A) in *;
     let y := fresh "y" in set (y := @Zlength) in x;
     fold @Zlength' in y; subst y; subst x.

Ltac pose_Zlength_nonneg :=
 repeat
  match goal with
  | |- context [@Zlength ?T ?A] => pose_Zlength_nonneg1 T A
  | H: context [@Zlength ?T ?A] |- _ => pose_Zlength_nonneg1 T A
 end;
  unfold Zlength' in *.

(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
Ltac list_solve := autorewrite with sublist; pose_Zlength_nonneg; omega.

Definition Znth {X}{d: Inhabitant X} n (xs: list X) :=
  if (zlt n 0) then default else nth (Z.to_nat n) xs d.

Lemma Znth_map:
  forall {A:Type} {da: Inhabitant A}{B:Type}{db: Inhabitant B} i (f: A -> B) (al: list A),
  0 <= i < Zlength al ->
  Znth i (map f al)  = f (Znth i al).
Proof.
(* Goal: @eq A (@Znth A d i al) d *)
unfold Znth.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite if_false by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite if_false by omega.
(* Goal: @Forall A f al *)
rewrite nth_map' with (d' := da); auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega.
(* Goal: Z.lt i (Z.of_nat (@Datatypes.length (Inhabitant A) al)) *)
change (Inhabitant A) with A.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite <- Zlength_correct. omega.
Qed.

Hint Rewrite 
   (@Znth_map Z _) (@Znth_map nat _) (@Znth_map positive _)
    using (auto; rewrite ?Zlength_map in *; omega) : sublist.

(* Add these in a later file where things are in scope ...
Hint Rewrite (Znth_map Int.zero) (Znth_map Vundef)
    using (auto; rewrite ?Zlength_map in *; omega) : sublist.
*)

Lemma Znth_succ: forall {A}{a: Inhabitant A} i lo (v: list A), Z.succ lo <= i -> Znth (i - lo) v = Znth (i - (Z.succ lo)) (skipn 1 v).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@Znth A d i al) d *)
  unfold Znth.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat (Z.sub mid lo)) ct)) (@cons A (if zlt (Z.sub mid lo) Z0 then @default A a else @nth A (Z.to_nat (Z.sub mid lo)) ct a) (@nil A)) *)
  if_tac; [omega |].
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat (Z.sub mid lo)) ct)) (@cons A (if zlt (Z.sub mid lo) Z0 then @default A a else @nth A (Z.to_nat (Z.sub mid lo)) ct a) (@nil A)) *)
  if_tac; [omega |].
(* Goal: @eq A (@nth A (Z.to_nat i) (@skipn A (nat_of_Z n) xs) a) (@nth A (Z.to_nat (Z.add i n)) xs a) *)
  rewrite nth_skipn.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
  f_equal.
(* Goal: @eq nat (Z.to_nat (Z.sub i lo)) (Init.Nat.add (Z.to_nat (Z.sub i (Z.succ lo))) (S O)) *)
  change 1%nat with (Z.to_nat 1).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite <- Z2Nat.inj_add by omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
  f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  omega.
Qed.

Lemma Znth_0_cons {A}{a: Inhabitant A} l (v:A): Znth 0 (v::l) = v.
Proof. reflexivity. Qed.
Hint Rewrite @Znth_0_cons : sublist.

Lemma Znth_pos_cons {A}{a: Inhabitant A} i l (v:A): 0<i -> Znth i (v::l) = Znth (i-1) l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. unfold Znth. if_tac. omega. if_tac. omega.
  assert (Z.to_nat i = S (Z.to_nat (i-1))).
(* Goal: @eq A v v *)
    rewrite <- Z2Nat.inj_succ. assert (i = Z.succ (i - 1)). omega. rewrite <- H2. trivial. omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite H2; reflexivity.
Qed.

Lemma Znth_In : forall {A}{a: Inhabitant A} i l, 0 <= i < Zlength l -> In (Znth i l) l.
Proof.
(* Goal: @eq A (@Znth A d i al) d *)
  intros; unfold Znth.
(* Goal: @In A (if zlt i Z0 then @default A a else @nth A (Z.to_nat i) l a) l *)
  destruct (zlt i 0); [omega|].
  apply nth_In; rewrite Zlength_correct in *.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Nat2Z.inj_lt; rewrite Z2Nat.id; omega.
Qed.

Lemma split3_full_length_list: forall {A}{a: Inhabitant A} lo mid hi (ct: list A),
  lo <= mid < hi ->
  Zlength ct = hi - lo ->
  ct = firstn (Z.to_nat (mid - lo)) ct ++
       (Znth (mid - lo) ct :: nil) ++
       skipn (Z.to_nat (mid - lo + 1)) ct.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
  rewrite <- firstn_skipn with (l := ct) (n := Z.to_nat (mid - lo)) at 1.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
  f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z2Nat.inj_add by omega.
  rewrite <- skipn_skipn.
  replace (Znth (mid - lo) ct :: nil) with (firstn (Z.to_nat 1) (skipn (Z.to_nat (mid - lo)) ct)).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  + rewrite firstn_skipn; reflexivity.
  + unfold Znth.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat (Z.sub mid lo)) ct)) (@cons A (if zlt (Z.sub mid lo) Z0 then @default A a else @nth A (Z.to_nat (Z.sub mid lo)) ct a) (@nil A)) *)
    if_tac; [omega |].
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat (Z.sub mid lo)) ct)) (@cons A (@nth A (Z.to_nat (Z.sub mid lo)) ct a) (@nil A)) *)
    rewrite firstn_1_skipn; [reflexivity |].
    rewrite <- (Nat2Z.id (length ct)).
(* Goal: lt (Z.to_nat (Z.sub mid lo)) (Z.to_nat (Z.of_nat (@Datatypes.length A ct))) *)
    apply Z2Nat.inj_lt.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - omega.
    - rewrite Zlength_correct in H0.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      omega.
Qed.

Lemma Forall_Znth:
 forall {A}{a: Inhabitant A} (F: A -> Prop) (al: list A) i,
   0 <= i < Zlength al ->
   Forall F al ->
   F (Znth i al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
unfold Znth. rewrite if_false by omega.
(* Goal: le (Z.to_nat n) (@Datatypes.length A al) *)
rewrite Zlength_correct in H.
(* Goal: @eq A (@nth A (Z.to_nat i) (@rev A al) d) (@nth A (Init.Nat.sub (Init.Nat.sub (@Datatypes.length A al) (Z.to_nat i)) (Z.to_nat (Zpos xH))) al d) *)
assert (Z.to_nat i < length al)%nat.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega; omega.
(* Goal: @eq A (@nth A (Z.to_nat i) (@rev A al) d) (@nth A (Init.Nat.sub (Init.Nat.sub (@Datatypes.length A al) (Z.to_nat i)) (S O)) al d) *)
clear H.
revert al H0 H1; induction (Z.to_nat i); destruct al; intros; simpl in *.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @Forall A f al *)
inv H0. auto.
(* Goal: F a *)
(* Goal: F (@nth A n al a) *)
inv H1.
(* Goal: F (@nth A n al a) *)
inv H0.
(* Goal: @Forall A f al *)
apply IHn; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Hint Rewrite @app_nil_l @app_nil_r : sublist.

Lemma app_Znth1:
  forall A (a: Inhabitant A) (l l': list A) (i:Z),
  i < Zlength l -> Znth i (l++l') = Znth i l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@Znth A d i al) d *)
unfold Znth.
(* Goal: @Forall A f al *)
if_tac; auto.
(* Goal: @eq A (@nth A (Z.to_nat i) (@app A l l') a) (@nth A (Z.to_nat i) l a) *)
apply app_nth1.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
rewrite Zlength_correct in H; auto.
Qed.

Lemma app_Znth2:
  forall A (a: Inhabitant A) (l l': list A) (i:Z),
  i >= Zlength l -> Znth i (l++l') = Znth (i-Zlength l) l'.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@Znth A d i al) d *)
unfold Znth.
(* Goal: @eq A (if zlt i Z0 then @default A a else @nth A (Z.to_nat i) (@app A l l') a) (if zlt (Z.sub i (@Zlength A l)) Z0 then @default A a else @nth A (Z.to_nat (Z.sub i (@Zlength A l))) l' a) *)
pose proof (Zlength_nonneg l).
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac.
(* Goal: @Forall A f al *)
rewrite if_true by omega; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite if_false by omega.
(* Goal: @eq A (@nth A (Z.to_nat i) (@app A l l') a) (@nth A (Z.to_nat (Z.sub i (@Zlength A l))) l' a) *)
rewrite app_nth2.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @Forall A f al *)
rewrite Z2Nat.inj_sub by auto.
(* Goal: @eq Z (@Zlength A (@list_repeat A (Z.to_nat n) x)) n *)
rewrite Zlength_correct.
(* Goal: @eq nat (Init.Nat.sub (Z.to_nat i) (@Datatypes.length A l)) (Init.Nat.sub (Z.to_nat i) (Z.to_nat (Z.of_nat (@Datatypes.length A l)))) *)
(* Goal: ge (Z.to_nat i) (@Datatypes.length A l) *)
rewrite Nat2Z.id; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Nat2Z.inj_ge. rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
rewrite <- Zlength_correct; auto.
Qed.

Lemma Znth_firstn:
  forall {A}{a: Inhabitant A} (al: list A) (n m : Z),
  n<m -> Znth n (firstn (Z.to_nat m) al) = Znth n al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@Znth A d i al) d *)
unfold Znth.
(* Goal: @Forall A f al *)
if_tac; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) (@firstn A (Z.to_nat m) al) a) (@nth A (Z.to_nat n) al a) *)
apply nth_firstn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Z2Nat.inj_lt; omega.
Qed.

Lemma Znth_skipn: forall {A}{a: Inhabitant A}  i n xs,
  0 <= i ->
  0 <= n ->
  Znth i (skipn (nat_of_Z n) xs) = Znth (i+n) xs.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@Znth A d i al) d *)
  unfold Znth.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite if_false by omega. rewrite if_false by omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
  rewrite nth_skipn. f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z2Nat.inj_add by omega. auto.
Qed.

Lemma Z2Nat_neg: forall i, i < 0 -> Z.to_nat i = 0%nat.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  destruct i; try reflexivity.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  pose proof Zgt_pos_0 p; omega.
Qed.

Lemma Zlength_firstn:
  forall {A} n (v: list A), Zlength (firstn (Z.to_nat n) v) = Z.min (Z.max 0 n) (Zlength v).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. rewrite !Zlength_correct.
(* Goal: @eq Z (Z.of_nat (@Datatypes.length A (@firstn A (Z.to_nat n) v))) (Z.min (Z.max Z0 n) (Z.of_nat (@Datatypes.length A v))) *)
rewrite firstn_length.
(* solve by SMT *)
(* Goal: @eq Z (Z.of_nat (Init.Nat.min (Z.to_nat n) (@Datatypes.length A v))) (Z.min (Z.max Z0 n) (Z.of_nat (@Datatypes.length A v))) *)
rewrite Zmin_spec, Zmax_spec.
(* Goal: @eq Z (Z.of_nat (Init.Nat.min (Z.to_nat n) (@Datatypes.length A v))) (if zlt (if zlt n Z0 then Z0 else n) (Z.of_nat (@Datatypes.length A v)) then if zlt n Z0 then Z0 else n else Z.of_nat (@Datatypes.length A v)) *)
if_tac; [rewrite min_l | rewrite min_r].
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac.
(* Goal: @Forall A f al *)
rewrite Z2Nat_neg; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Z2Nat.id; omega.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) Z0 *)
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac in H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat_neg; auto. omega.
rewrite <- (Nat2Z.id (length v)).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Z2Nat.inj_le; try omega.
(* Goal: @Forall A f al *)
auto.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) Z0 *)
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac in H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
destruct (length v); try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite inj_S in H. omega.
rewrite <- (Nat2Z.id (length v)).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Z2Nat.inj_le; try omega.
Qed.

Lemma Zlength_skipn:
  forall {A} n (v: list A),
  Zlength (skipn (Z.to_nat n) v) = Z.max 0 (Zlength v - (Z.max 0n)).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* solve by SMT *)
(* Goal: @eq Z (@Zlength A (@skipn A (Z.to_nat n) v)) (Z.max Z0 (Z.sub (@Zlength A v) (Z.max Z0 n))) *)
rewrite !Zlength_correct.
(* Goal: ge (Z.to_nat (Z.sub (@Zlength A l) i)) (@Datatypes.length A (@skipn A (Z.to_nat i) l)) *)
rewrite skipn_length. rewrite !Zmax_spec.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) Z0 *)
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac in H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply inj_minus2. apply Nat2Z.inj_gt. rewrite Z2Nat.id by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) (if zlt n Z0 then Z0 else n)) *)
if_tac.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z2Nat_neg n) by omega.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) O)) (Z.sub (Z.of_nat (@Datatypes.length A v)) Z0) *)
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A v) (Z.to_nat n))) (Z.sub (Z.of_nat (@Datatypes.length A v)) n) *)
rewrite Nat.sub_0_r.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A al) (Init.Nat.add (Z.to_nat (Z.sub (@Zlength A al) hi)) (Z.to_nat (Z.sub hi lo))))) (Z.of_nat (Z.to_nat lo)) *)
rewrite Nat2Z.inj_sub.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega. auto.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
apply Nat2Z.inj_le.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.  omega.
Qed.

Lemma Znth_cons:
 forall {A}(a: Inhabitant A)  i (al: list A) bl,
  0 <= i < Zlength al  ->
  Znth i al :: bl = firstn (Z.to_nat 1) (skipn (Z.to_nat i) al) ++ bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@cons A (@Znth A a i al) bl) (@app A (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) bl) *)
pose proof (Znth_skipn 0 i al).
(* Goal: @eq (list A) (@cons A (@Znth A a i al) bl) (@app A (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) bl) *)
rewrite Z.add_0_l in H0.
rewrite <- H0 by omega; clear H0.
change (Znth 0 (skipn (nat_of_Z i) al) :: bl) with
   ([Znth 0 (skipn (Z.to_nat i) al)] ++ bl).
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@Znth A d i al) d *)
unfold Znth.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite if_false  by omega.
(* Goal: @eq (list A) (@cons A (@nth A (Z.to_nat Z0) (@skipn A (Z.to_nat i) al) a) (@nil A)) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) *)
assert (Zlength (skipn (Z.to_nat i) al) > 0).
(* Goal: Z.lt (@Zlength A (@skipn A (Z.to_nat lo) l)) (Z.sub hi lo) *)
rewrite Zlength_skipn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_r 0 i) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z.max_r by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq (list A) (@cons A (@nth A (Z.to_nat Z0) (@skipn A (Z.to_nat i) al) a) (@nil A)) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) *)
destruct (skipn (Z.to_nat i) al).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zlength_nil in H0; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
reflexivity.
Qed.

Lemma Zfirstn_app1:
 forall A n (al bl: list A),
  n <= Zlength al -> firstn (Z.to_nat n) (al++bl) = firstn (Z.to_nat n) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat n) (@app A al bl)) (@firstn A (Z.to_nat n) al) *)
apply firstn_app1.
(* Goal: le (Z.to_nat n) (@Datatypes.length A al) *)
apply Nat2Z.inj_le. rewrite Zlength_correct in H.
(* Goal: Z.ge (Z.of_nat (Z.to_nat n)) (Z.of_nat (@Datatypes.length A al)) *)
destruct (zlt n 0).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat_neg by auto. change (Z.of_nat 0) with 0; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma Zfirstn_same:
  forall A n (b: list A), n >= Zlength b -> firstn (Z.to_nat n) b = b.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub (@Zlength A l) i)) (@skipn A (Z.to_nat i) l)) (@skipn A (Z.to_nat i) l) *)
apply firstn_same.
(* Goal: le (Z.to_nat n) (@Datatypes.length A al) *)
rewrite Zlength_correct in H.
(* Goal: ge (Z.to_nat n) (@Datatypes.length A al) *)
apply Nat2Z.inj_ge.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma Zfirstn_app2: forall {A} n (al bl: list A),
 n >= Zlength al ->
 firstn (Z.to_nat n) (al++bl) = al ++ firstn (Z.to_nat (n - Zlength al)) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat n) (@app A al bl)) (@app A al (@firstn A (Z.to_nat (Z.sub n (@Zlength A al))) bl)) *)
rewrite firstn_app2.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal. f_equal.
(* Goal: @eq (list A) (@firstn A (Init.Nat.sub (Z.to_nat n) (Pos.to_nat xH)) l) (@firstn A (Z.to_nat (Z.sub n (Zpos xH))) l) *)
(* Goal: Z.le Z0 (Zpos xH) *)
rewrite Z2Nat.inj_sub.
(* Goal: @Forall A f al *)
rewrite Zlength_correct, Nat2Z.id. auto.
(* Goal: Z.le Z0 (@Zlength A al) *)
(* Goal: ge (Z.to_nat n) (@Datatypes.length A al) *)
apply Zlength_nonneg.
(* Goal: ge (Z.to_nat n) (@Datatypes.length A al) *)
apply Nat2Z.inj_ge.
(* Goal: le (Z.to_nat n) (@Datatypes.length A al) *)
rewrite Zlength_correct in H.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma Zfirstn_firstn: forall {A} (contents: list A) n m,
  n <= m ->
  firstn (Z.to_nat n) (firstn (Z.to_nat m) contents) = firstn (Z.to_nat n) contents.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.ge (Z.of_nat (Z.to_nat n)) (Z.of_nat (@Datatypes.length A al)) *)
destruct (zlt n 0).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z2Nat_neg n) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
reflexivity.
(* Goal: @eq (list A) (@firstn A (Z.to_nat n) (@firstn A (Z.to_nat m) contents)) (@firstn A (Z.to_nat n) contents) *)
apply firstn_firstn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Z2Nat.inj_le; omega.
Qed.
Lemma Zskipn_app1:
 forall A n (al bl: list A),
  n <= Zlength al ->
  skipn (Z.to_nat n) (al++bl) = skipn (Z.to_nat n) al ++ bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@skipn A (Z.to_nat n) (@app A al bl)) (@app A (@skipn A (Z.to_nat n) al) bl) *)
apply skipn_app1.
(* Goal: le (Z.to_nat n) (@Datatypes.length A al) *)
rewrite Zlength_correct in H.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
apply Nat2Z.inj_le.
(* Goal: Z.ge (Z.of_nat (Z.to_nat n)) (Z.of_nat (@Datatypes.length A al)) *)
destruct (zlt n 0).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z2Nat_neg n) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
change (Z.of_nat 0) with 0.  omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma Zskipn_app2:
 forall A n (al bl: list A),
  n >= Zlength al ->
  skipn (Z.to_nat n) (al++bl) = skipn (Z.to_nat (n-Zlength al)) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
rewrite Zlength_correct in *.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub j i)) (@skipn A (Z.to_nat i) (@app A al bl))) (@firstn A (Z.to_nat (Z.sub (Z.sub j (@Zlength A al)) (Z.sub i (@Zlength A al)))) (@skipn A (Z.to_nat (Z.sub i (@Zlength A al))) bl)) *)
rewrite skipn_app2.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.inj_sub by omega.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.of_nat (@Datatypes.length A al))) al) al *)
rewrite Nat2Z.id.
(* Goal: @Forall A f al *)
auto.
(* Goal: ge (Z.to_nat n) (@Datatypes.length A al) *)
apply Nat2Z.inj_ge.
(* Goal: Z.ge (Z.of_nat (Z.to_nat n)) (Z.of_nat (@Datatypes.length A al)) *)
destruct (zlt n 0).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z2Nat_neg n) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
change (Z.of_nat 0) with 0.  omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id by omega.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma Znth_rev:
  forall {A}{d: Inhabitant A} i (al:list A),
  0 <= i < Zlength al ->
  Znth i (rev al) = Znth (Zlength al - i - 1) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
 unfold Znth. rewrite !if_false by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite !Z2Nat.inj_sub by omega.
rewrite Zlength_correct in*.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.of_nat (@Datatypes.length A al))) al) al *)
rewrite Nat2Z.id.
(* Goal: @eq A (@nth A (Z.to_nat i) (@rev A al) d) (@nth A (Init.Nat.sub (Init.Nat.sub (@Datatypes.length A al) (Z.to_nat i)) (Z.to_nat (Zpos xH))) al d) *)
assert (Z.to_nat i < length al)%nat.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega. omega.
(* Goal: @eq A (@nth A (Z.to_nat i) (@rev A al) d) (@nth A (Init.Nat.sub (Init.Nat.sub (@Datatypes.length A al) (Z.to_nat i)) (Z.to_nat (Zpos xH))) al d) *)
change (Z.to_nat 1) with 1%nat.
(* Goal: @eq A (@nth A (Z.to_nat i) (@rev A al) d) (@nth A (Init.Nat.sub (Init.Nat.sub (@Datatypes.length A al) (Z.to_nat i)) (S O)) al d) *)
clear H.
(* Goal: @Forall A f al *)
rewrite rev_nth; auto.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma Zskipn_firstn: forall {A} n m (xs: list A),
 0 <= n ->
 skipn (Z.to_nat n) (firstn (Z.to_nat m) xs) =
  firstn (Z.to_nat (m-n)) (skipn (Z.to_nat n) xs).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub i k)) (@skipn A (Z.to_nat k) (@firstn A (Z.to_nat (Z.sub j m)) (@skipn A (Z.to_nat m) l)))) (@firstn A (Z.to_nat (Z.sub (Z.add i m) (Z.add k m))) (@skipn A (Z.to_nat (Z.add k m)) l)) *)
rewrite skipn_firstn.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @Forall A f al *)
rewrite Z2Nat.inj_sub; auto.
Qed.

Lemma Zskipn_skipn: forall {A} n m (xs: list A),
  0 <= n -> 0 <= m ->
  skipn (Z.to_nat n) (skipn (Z.to_nat m) xs) = skipn (Z.to_nat (m + n)) xs.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@skipn A (Z.to_nat n) (@skipn A (Z.to_nat m) xs)) (@skipn A (Z.to_nat (Z.add m n)) xs) *)
  rewrite skipn_skipn.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
 f_equal.
(* Goal: @Forall A f al *)
 rewrite Z2Nat.inj_add; auto.
Qed.

Lemma Zfirstn_app:
 forall {A} n m (al: list A),
  0 <= n -> 0 <= m ->
  firstn (Z.to_nat n) al ++ firstn (Z.to_nat m) (skipn (Z.to_nat n) al) =
  firstn (Z.to_nat (n+m)) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@app A (@firstn A (Z.to_nat n) al) (@firstn A (Z.to_nat m) (@skipn A (Z.to_nat n) al))) (@firstn A (Z.to_nat (Z.add n m)) al) *)
rewrite firstn_app.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.inj_add; omega.
Qed.

Lemma Zfirstn_exact_length:
  forall {A} n (al: list A),
  n = Zlength al ->
  firstn (Z.to_nat n) al = al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@sublist A lo hi al) (@cons A (@Znth A d lo al) (@nil A)) *)
subst.
(* Goal: @eq Z (@Zlength A (@list_repeat A (Z.to_nat n) x)) n *)
rewrite Zlength_correct.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.of_nat (@Datatypes.length A al))) al) al *)
rewrite Nat2Z.id.
(* Goal: @eq (list A) (@firstn A (@Datatypes.length A al) al) al *)
apply firstn_exact_length.
Qed.

(*****   SUBLIST  ******)

Definition sublist {A} (lo hi: Z) (al: list A) : list A :=
  firstn (Z.to_nat (hi-lo)) (skipn (Z.to_nat lo) al).

Definition upd_Znth {A} (i: Z) (al: list A) (x: A): list A :=
   sublist 0 i al ++ x :: sublist (i+1) (Zlength al) al.

Lemma sublist_sublist {A} i j k m (l:list A): 0<=m -> 0<=k <=i -> i <= j-m ->
  sublist k i (sublist m j l) = sublist (k+m) (i+m) l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
 unfold sublist; intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub i k)) (@skipn A (Z.to_nat k) (@firstn A (Z.to_nat (Z.sub j m)) (@skipn A (Z.to_nat m) l)))) (@firstn A (Z.to_nat (Z.sub (Z.add i m) (Z.add k m))) (@skipn A (Z.to_nat (Z.add k m)) l)) *)
  rewrite skipn_firstn.
(* Goal: @eq A v v *)
  rewrite firstn_firstn, skipn_skipn, <- Z2Nat.inj_add,(Z.add_comm _ k), Zminus_plus_simpl_r; trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  omega.
(* Goal: @eq A v v *)
  rewrite <- Z2Nat.inj_sub; trivial. apply Z2Nat.inj_le; try omega. omega.
Qed.
(*
Lemma sublist_sublist:
  forall {A} lo hi lo' hi' (al: list A),
 0 <= lo <= hi ->
 hi <= hi'-lo' ->
 0 <= lo' <= hi' ->
 hi' <= Zlength al ->
 sublist lo hi (sublist lo' hi' al) = sublist (lo+lo') (hi+lo') al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_firstn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zfirstn_firstn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_skipn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal. f_equal. omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal. f_equal. omega.
Qed.
*)
Lemma sublist_rejoin:
  forall {A} lo mid hi (al: list A),
  0 <= lo <= mid ->
  mid <= hi <= Zlength al ->
  sublist lo mid al ++ sublist mid hi al = sublist lo hi al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
replace (hi-lo) with ((mid-lo)+(hi-mid)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite <- Zfirstn_app by omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_skipn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal. f_equal. f_equal. omega.
Qed.

Lemma sublist_map:
  forall {A B} (F: A -> B) lo hi (al: list A),
  sublist lo hi (map F al) = map F (sublist lo hi al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @Forall A f al *)
rewrite map_firstn, map_skipn; auto.
Qed.

Lemma map_sublist:
  forall {A B} (F: A -> B) lo hi (al: list A),
  map F (sublist lo hi al) = sublist lo hi (map F al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@rev A al) al *)
symmetry. apply sublist_map.
Qed.

Lemma sublist_len_1:
  forall {A}{d: Inhabitant A} i (al: list A),
  0 <= i < Zlength al ->
  sublist i (i+1) al = Znth i al :: nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  replace (i+1-i) with 1 by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Znth_cons by omega.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) (@app A (@firstn A (Z.to_nat (Zpos xH)) (@skipn A (Z.to_nat i) al)) (@nil A)) *)
  symmetry; apply app_nil_r.
Qed.

Lemma Znth_cons_sublist:
  forall {A}{d: Inhabitant A} i (al: list A) bl,
  0 <= i < Zlength al ->
  Znth i al :: bl = sublist i (i+1) al ++ bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @Forall A f al *)
  erewrite sublist_len_1 by eauto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  reflexivity.
Qed.

Lemma Zlength_sublist:
  forall {A} lo hi (al: list A),
 0 <= lo <= hi -> hi <= Zlength al ->
 Zlength (sublist lo hi al) = hi-lo.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zlength_firstn, Z.max_r by omega.
(* Goal: Z.lt (@Zlength A (@skipn A (Z.to_nat lo) l)) (Z.sub hi lo) *)
rewrite Zlength_skipn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_r 0 lo) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z.max_r by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z.min_l by omega.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma sublist_same_gen:
forall {A} lo hi (al: list A),
  lo = 0 -> hi >= Zlength al ->
  sublist lo hi al = al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@sublist A lo hi al) (@cons A (@Znth A d lo al) (@nil A)) *)
unfold sublist; subst.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi Z0)) (@skipn A (Z.to_nat Z0) al)) al *)
rewrite Z.sub_0_r.
(* Goal: @Forall A f al *)
simpl; rewrite firstn_all2; auto.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
apply Nat2Z.inj_le.
(* Goal: @eq A (@Znth A d i al) d *)
pose proof (Zlength_nonneg al).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z2Nat.id, <- Zlength_correct; omega.
Qed.

Lemma sublist_same:
forall {A} lo hi (al: list A),
  lo = 0 -> hi = Zlength al ->
  sublist lo hi al = al.
Proof.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
intros; apply sublist_same_gen; omega.
Qed.

Lemma Znth_sublist:
  forall {A}{d: Inhabitant A} lo i hi (al: list A),
 0 <= lo ->
 0 <= i < hi-lo ->
 Znth i (sublist lo hi al) = Znth (i+lo) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Znth_firstn by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Znth_skipn by omega. auto.
Qed.

Lemma rev_sublist:
  forall {A} lo hi (al: list A),
  0 <= lo <= hi -> hi <= Zlength al ->
  rev (sublist lo hi al) = sublist (Zlength al - hi) (Zlength al - lo) (rev al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
replace (skipn (Z.to_nat lo) al)
 with (skipn (length al - (Z.to_nat (Zlength al - hi) + (Z.to_nat (hi - lo)))) al).
rewrite <- firstn_skipn_rev.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal. omega.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
apply Nat2Z.inj_le.
(* Goal: Z.le (Z.of_nat (Init.Nat.add (Z.to_nat (Z.sub (@Zlength A al) hi)) (Z.to_nat (Z.sub hi lo)))) (@Zlength A al) *)
rewrite Nat2Z.inj_add.
rewrite <- Zlength_correct.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite !Z2Nat.id by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq nat (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) (Z.to_nat (Z.add a b)) *)
apply Nat2Z.inj.
(* Goal: @eq Z (Z.of_nat (Init.Nat.sub (@Datatypes.length A al) (Init.Nat.add (Z.to_nat (Z.sub (@Zlength A al) hi)) (Z.to_nat (Z.sub hi lo))))) (Z.of_nat (Z.to_nat lo)) *)
rewrite Nat2Z.inj_sub.
(* Goal: Z.le (Z.of_nat (Init.Nat.add (Z.to_nat (Z.sub (@Zlength A al) hi)) (Z.to_nat (Z.sub hi lo)))) (@Zlength A al) *)
rewrite Nat2Z.inj_add.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite !Z2Nat.id by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite <- Zlength_correct; omega.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
apply Nat2Z.inj_le.
rewrite <- Zlength_correct.
(* Goal: Z.le (Z.of_nat (Init.Nat.add (Z.to_nat (Z.sub (@Zlength A al) hi)) (Z.to_nat (Z.sub hi lo)))) (@Zlength A al) *)
rewrite Nat2Z.inj_add.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite !Z2Nat.id by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma sublist_nil:
  forall {A} lo (al: list A),
  sublist lo lo al = nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z.sub_diag. reflexivity.
Qed.

Lemma sublist_nil_gen : forall {A} (l : list A) i j, j <= i -> sublist i j l = [].
Proof.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros; unfold sublist.
(* Goal: @Forall A f al *)
  replace (Z.to_nat (j - i)) with O; auto.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  apply Nat2Z.inj; simpl.
  destruct (Z.eq_dec (j - i) 0); [rewrite e; auto|].
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z2Nat_neg; auto; omega.
Qed.

Lemma sublist_rev:
  forall {A} lo hi (al: list A),
  0 <= lo <= hi -> hi <= Zlength al ->
  sublist lo hi (rev al) = rev (sublist (Zlength al - hi) (Zlength al - lo) al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite rev_sublist by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
f_equal; omega.
Qed.

Lemma sublist_app:
  forall {A} lo hi (al bl: list A),
  0 <= lo <= hi -> hi <= Zlength al + Zlength bl ->
  sublist lo hi (al++bl) =
  sublist (Z.min lo (Zlength al)) (Z.min hi (Zlength al)) al ++
  sublist (Z.max (lo-Zlength al) 0) (Z.max (hi-Zlength al) 0) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) (@app A al bl))) (@app A (@firstn A (Z.to_nat (Z.sub (Z.min hi (@Zlength A al)) (Z.min lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.min lo (@Zlength A al))) al)) (@firstn A (Z.to_nat (Z.sub (Z.max (Z.sub hi (@Zlength A al)) Z0) (Z.max (Z.sub lo (@Zlength A al)) Z0))) (@skipn A (Z.to_nat (Z.max (Z.sub lo (@Zlength A al)) Z0)) bl))) *)
destruct (zlt hi (Zlength al)).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.min_l hi (Zlength al)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.min_l lo (Zlength al)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_r (hi-Zlength al) 0) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_r (lo-Zlength al) 0) by omega.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) (@app A al bl))) (@app A (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) al)) (@firstn A (Z.to_nat (Z.sub Z0 Z0)) (@skipn A (Z.to_nat Z0) bl))) *)
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) (@app A al bl))) (@app A (@firstn A (Z.to_nat (Z.sub (Z.min hi (@Zlength A al)) (Z.min lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.min lo (@Zlength A al))) al)) (@firstn A (Z.to_nat (Z.sub (Z.max (Z.sub hi (@Zlength A al)) Z0) (Z.max (Z.sub lo (@Zlength A al)) Z0))) (@skipn A (Z.to_nat (Z.max (Z.sub lo (@Zlength A al)) Z0)) bl))) *)
simpl firstn.
rewrite <- app_nil_end.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_app1 by omega.
rewrite Zfirstn_app1
 by (rewrite Zlength_skipn, !Z.max_r; try omega;
      rewrite Z.max_r; omega).
(* Goal: @Forall A f al *)
auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.min_r hi (Zlength al)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_l (hi-Zlength al) 0) by omega.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) (@app A al bl))) (@app A (@firstn A (Z.to_nat (Z.sub (@Zlength A al) (Z.min lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.min lo (@Zlength A al))) al)) (@firstn A (Z.to_nat (Z.sub (Z.sub hi (@Zlength A al)) (Z.max (Z.sub lo (@Zlength A al)) Z0))) (@skipn A (Z.to_nat (Z.max (Z.sub lo (@Zlength A al)) Z0)) bl))) *)
destruct (zlt lo (Zlength al)).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.min_l lo (Zlength al)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_r (lo-Zlength al) 0) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_app1 by omega.
rewrite Zfirstn_app2
 by (rewrite Zlength_skipn, !Z.max_r; try omega;
      rewrite Z.max_r; omega).
rewrite Zlength_skipn, !Z.max_r; try omega;
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      rewrite ?Z.max_r; try omega.
(* Goal: @eq (list A) (@app A (@skipn A (Z.to_nat lo) al) (@firstn A (Z.to_nat (Z.sub (Z.sub hi lo) (Z.sub (@Zlength A al) lo))) bl)) (@app A (@firstn A (Z.to_nat (Z.sub (@Zlength A al) lo)) (@skipn A (Z.to_nat lo) al)) (@firstn A (Z.to_nat (Z.sub (Z.sub hi (@Zlength A al)) Z0)) (@skipn A (Z.to_nat Z0) bl))) *)
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) (@app A al bl))) (@app A (@firstn A (Z.to_nat (Z.sub (@Zlength A al) (Z.min lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.min lo (@Zlength A al))) al)) (@firstn A (Z.to_nat (Z.sub (Z.sub hi (@Zlength A al)) (Z.max (Z.sub lo (@Zlength A al)) Z0))) (@skipn A (Z.to_nat (Z.max (Z.sub lo (@Zlength A al)) Z0)) bl))) *)
simpl skipn.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.

(* Goal: @Forall A f al *)
rewrite Zfirstn_exact_length; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zlength_skipn, !Z.max_r; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Z.max_r; omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.min_r lo (Zlength al)) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite (Z.max_l (lo-Zlength al) 0) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_app2 by omega.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat (Z.sub lo (@Zlength A al))) bl)) (@app A (@firstn A (Z.to_nat (Z.sub (@Zlength A al) (@Zlength A al))) (@skipn A (Z.to_nat (@Zlength A al)) al)) (@firstn A (Z.to_nat (Z.sub (Z.sub hi (@Zlength A al)) (Z.sub lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.sub lo (@Zlength A al))) bl))) *)
rewrite Z.sub_diag.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat (Z.sub lo (@Zlength A al))) bl)) (@app A (@firstn A (Z.to_nat Z0) (@skipn A (Z.to_nat (@Zlength A al)) al)) (@firstn A (Z.to_nat (Z.sub (Z.sub hi (@Zlength A al)) (Z.sub lo (@Zlength A al)))) (@skipn A (Z.to_nat (Z.sub lo (@Zlength A al))) bl))) *)
simpl app.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma sublist_split:
  forall {A} lo mid hi (al: list A),
  0 <= lo <= mid ->
  mid <= hi <= Zlength al ->
  sublist lo hi al = sublist lo mid al ++ sublist mid hi al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @Forall A f al *)
symmetry; apply sublist_rejoin; auto.
Qed.

Lemma sublist_last_1 : forall {A}{d: Inhabitant A} lo hi (al : list A), 0 <= lo <= hi -> hi + 1 <= Zlength al ->
  sublist lo (hi + 1) al = sublist lo hi al ++ [Znth hi al].
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  erewrite sublist_split with (mid := hi)(hi0 := hi + 1), sublist_len_1; auto; omega.
Qed.

Lemma Zlen_le_1_rev:
 forall {A} (al: list A),
  Zlength al <= 1 -> rev al = al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@rev A al) al *)
symmetry.
(* Goal: @eq (list A) al (@rev A al) *)
apply len_le_1_rev.
apply Nat2Z.inj_le. rewrite <- Zlength_correct; apply H.
Qed.

Lemma skipn_0:
  forall A (l: list A), skipn 0 l = l.
Proof.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
reflexivity.
Qed.

Lemma sublist_1_cons {A} l (v:A) n: sublist 1 n (v::l) = sublist 0 (n-1) l.
Proof.
(* Goal: @eq A v v *)
  unfold sublist. rewrite Z2Nat.inj_sub, skipn_0, Zminus_0_r. simpl. rewrite Z2Nat.inj_sub. trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  omega. omega.
Qed.

Lemma sublist_nil': forall (A : Type) (lo lo': Z) (al : list A), lo=lo' -> sublist lo lo' al = [].
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. subst. apply sublist_nil. Qed.

Lemma sublist_skip {A} (l:list A) i : 0<=i ->  sublist i (Zlength l) l = skipn (Z.to_nat i) l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. unfold sublist; intros. apply firstn_same. rewrite skipn_length.
(* Goal: @eq A v v *)
  rewrite Z2Nat.inj_sub, Zlength_correct, Nat2Z.id. omega. trivial.
Qed.

Lemma sublist_firstn {A} (l:list A) i: sublist 0 i l = firstn (Z.to_nat i) l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. unfold sublist; intros. rewrite Zminus_0_r, skipn_0. trivial. Qed.

Lemma sublist_app1:
  forall (A : Type) (k i : Z) (al bl : list A),
  0 <= k <= i -> i <= Zlength al -> sublist k i (al ++ bl) = sublist k i al.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros.
(* Goal: @eq A v v *)
  unfold sublist. rewrite skipn_app1. rewrite firstn_app1. trivial.
(* Goal: le (@Datatypes.length A al) (Z.to_nat i) *)
  rewrite skipn_length, Z2Nat.inj_sub. apply Nat2Z.inj_le.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  repeat rewrite Nat2Z.inj_sub. rewrite Z2Nat.id, <- Zlength_correct. omega. omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite <- ZtoNat_Zlength. apply Z2Nat.inj_le; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Z2Nat.inj_le; omega. omega. rewrite <- ZtoNat_Zlength. apply Z2Nat.inj_le; omega.
Qed.

Lemma sublist0_app1 {A} i (al bl:list A): 0<= i <= Zlength al ->
  sublist 0 i (al ++ bl) = sublist 0 i al.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. apply sublist_app1; omega. Qed.

Lemma sublist_app2 {A} i j (al bl:list A): 0<=Zlength al <= i->
  sublist i j (al ++ bl) = sublist (i-Zlength al) (j-Zlength al) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist; intros.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub j i)) (@skipn A (Z.to_nat i) (@app A al bl))) (@firstn A (Z.to_nat (Z.sub (Z.sub j (@Zlength A al)) (Z.sub i (@Zlength A al)))) (@skipn A (Z.to_nat (Z.sub i (@Zlength A al))) bl)) *)
  rewrite skipn_app2.
(* Goal: @eq (list A) (@firstn A (Init.Nat.sub (Z.to_nat n) (Pos.to_nat xH)) l) (@firstn A (Z.to_nat (Z.sub n (Zpos xH))) l) *)
(* Goal: Z.le Z0 (Zpos xH) *)
  repeat rewrite Z2Nat.inj_sub. repeat rewrite ZtoNat_Zlength.
  remember ((Z.to_nat i - length al)%nat) as k.
  rewrite <- Nat.sub_add_distr.
  assert (K: (length al + k = Z.to_nat i)%nat).
(* Goal: @eq A v v *)
    subst k. rewrite <- le_plus_minus. trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    apply Nat2Z.inj_le. rewrite Z2Nat.id. rewrite Zlength_correct in H; apply H. omega.
(* Goal: @eq A v v *)
  rewrite K. trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  omega. omega. omega. omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Nat2Z.inj_le. rewrite Z2Nat.id. rewrite Zlength_correct in H; apply H. omega.
Qed.

Lemma sublist_sublist0 {A} i j k (l:list A): 0<=k -> k<=i<=j ->
  sublist k i (sublist 0 j l) = sublist k i l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. rewrite sublist_sublist; repeat rewrite Zplus_0_r; trivial; omega. Qed.

Lemma sublist_sublist00 {A} i j (l:list A): 0<=i<=j ->
  sublist 0 i (sublist 0 j l) = sublist 0 i l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. apply sublist_sublist0; omega. Qed.

Lemma skipn_list_repeat:
   forall A k n (a: A),
     (k <= n)%nat -> skipn k (list_repeat n a) = list_repeat (n-k) a.
Proof.
(* Goal: @Forall A f al *)
 induction k; destruct n; simpl; intros; auto.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
 apply IHk; auto. omega.
Qed.

(* not this version!
Lemma sublist_list_repeat {A} i j k (v:A) (I: 0<=i)
          (IJK: (Z.to_nat i <= Z.to_nat j <= k)%nat):
      sublist i j (list_repeat k v) = list_repeat (Z.to_nat (j-i)) v.
Proof.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite skipn_list_repeat; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z2Nat.inj_sub; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite firstn_list_repeat; trivial; omega.
Qed.
*)

Lemma sublist_list_repeat {A} i j k (v:A) (I: 0<=i)
          (IJK: i <= j <= k):
      sublist i j (list_repeat (Z.to_nat k) v) = list_repeat (Z.to_nat (j-i)) v.
Proof.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub j i)) (@skipn A (Z.to_nat i) (@list_repeat A (Z.to_nat k) v))) (@list_repeat A (Z.to_nat (Z.sub j i)) v) *)
  rewrite skipn_list_repeat.
(* Goal: @eq (list A) (@firstn A (Z.to_nat (Z.sub j i)) (@list_repeat A (Init.Nat.sub (Z.to_nat k) (Z.to_nat i)) v)) (@list_repeat A (Z.to_nat (Z.sub j i)) v) *)
(* Goal: le (Z.to_nat i) (Z.to_nat k) *)
  rewrite firstn_list_repeat.
(* Goal: @eq A v v *)
  trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite <- Z2Nat.inj_sub by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Z2Nat.inj_le; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Z2Nat.inj_le; omega.
Qed.

Lemma Zlength_list_repeat:
  forall {A} n (x: A),
  0 <= n ->
  Zlength (list_repeat (Z.to_nat n) x) = n.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq Z (@Zlength A (@list_repeat A (Z.to_nat n) x)) n *)
rewrite Zlength_correct.
(* Goal: @eq Z (Z.of_nat (@Datatypes.length A (@list_repeat A (Z.to_nat n) x))) n *)
rewrite length_list_repeat.
(* Goal: @Forall A f al *)
apply Z2Nat.id; auto.
Qed.

Lemma list_repeat_0:
  forall {A} (x:A), list_repeat (Z.to_nat 0) x = nil.
Proof.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. auto.
Qed.

Lemma Znth_list_repeat_inrange:
  forall {A}{d: Inhabitant A} i n (a: A),
   (0 <= i < n)%Z ->
   Znth i (list_repeat (Z.to_nat n) a) = a.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
unfold Znth; rewrite if_false by omega.
assert (Z.to_nat i < Z.to_nat n)%nat
  by (apply Z2Nat.inj_lt; omega).
(* Goal: @eq A (@nth A (Z.to_nat i) (@list_repeat A (Z.to_nat n) a) d) a *)
forget (Z.to_nat n) as k.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
revert k H0; induction (Z.to_nat i); destruct k; simpl; intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega. auto. omega. apply IHn0; omega.
Qed.

Lemma firstn_nil {A} n: firstn n (nil:list A) = nil.
Proof.  destruct n; reflexivity. Qed.

Lemma firstn_In {A} (x:A): forall l n, In x (firstn n l) -> In x l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  induction l; simpl; intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  rewrite firstn_nil in H. inv H.
  destruct n; simpl in *. contradiction.
(* Goal: @Forall A f al *)
  destruct H; eauto.
Qed.
Lemma skipn_In {A} (x:A): forall l n, In x (skipn n l) -> In x l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  induction l; simpl; intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  rewrite skipn_nil in H. inv H.
(* Goal: @eq A v v *)
  destruct n; simpl in *. trivial. right; eauto.
Qed.

Lemma sublist_In {A} lo hi data (x:A) (I:In x (sublist lo hi data)): In x data.
Proof. eapply skipn_In. eapply firstn_In. apply I. Qed.

Lemma Zlength_list_repeat' {A} n (v:A): Zlength (list_repeat n v) = Z.of_nat n.
Proof. rewrite Zlength_correct, length_list_repeat; trivial. Qed.

Lemma sublist0_app2 {A : Type} i (al bl : list A):
  Zlength al <= i <= Zlength al + Zlength bl ->
  sublist 0 i (al ++ bl) = al ++ sublist 0 (i - Zlength al) bl.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. specialize (Zlength_nonneg al); specialize (Zlength_nonneg bl); intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite <- (sublist_rejoin 0 (Zlength al) i); try rewrite Zlength_app; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite sublist0_app1, sublist_same; try omega.
(* Goal: @eq A v v *)
 rewrite sublist_app2, Zminus_diag; trivial. omega.
Qed.


Lemma sublist_rejoin':
  forall {A} lo mid mid' hi (al: list A),
  mid=mid' ->
  0 <= lo <= mid ->
  mid' <= hi <= Zlength al ->
  sublist lo mid al ++ sublist mid' hi al = sublist lo hi al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@app A (@sublist A lo mid al) (@sublist A mid' hi al)) (@sublist A lo hi al) *)
subst mid'.
(* Goal: @Forall A f al *)
apply sublist_rejoin; auto.
Qed.

Hint Rewrite @sublist_nil' using list_solve: sublist.
Hint Rewrite @app_nil_l : sublist.
Hint Rewrite @Zlength_rev : sublist.
Hint Rewrite @sublist_rejoin' using list_solve : sublist.

Lemma subsub1:
 forall a b : Z, (a-(a-b)) = b.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof.  intros. omega. Qed.
Hint Rewrite subsub1 : sublist.

Lemma sublist_app':
  forall {A} lo hi (al bl: list A),
  0 <= lo <= Zlength al ->
  0 <= hi-Zlength al <= Zlength bl ->
  sublist lo hi (al++bl) =
  sublist lo (Zlength al) al ++
  sublist 0 (hi-Zlength al) bl.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
unfold sublist.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Zskipn_app1 by omega.
rewrite Zfirstn_app2
 by (rewrite Zlength_skipn, Z.max_r;
      rewrite ?Z.max_r; omega).
rewrite Zlength_skipn, Z.max_r;
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      rewrite ?Z.max_r; try omega.
rewrite (Zfirstn_exact_length (Zlength al - lo))
 by (rewrite Zlength_skipn, Z.max_r;
      rewrite ?Z.max_r; omega).
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
omega.
Qed.

Lemma upd_Znth_Zlength {A} i (l:list A) v: 0<=i < Zlength l ->
      Zlength (upd_Znth i l v) = Zlength l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
   unfold upd_Znth. rewrite Zlength_app, Zlength_cons; simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  repeat rewrite Zlength_sublist; simpl; omega.
Qed.

Lemma upd_Znth_map {A B} (f:A -> B) i l v:
      upd_Znth i (map f l) (f v) =
      map f (upd_Znth i l v).
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. unfold upd_Znth; intros. rewrite map_app, Zlength_map.
(* Goal: @eq A v v *)
  do 2 rewrite sublist_map; trivial.
Qed.

Lemma upd_Znth_lookup K {A}{d: Inhabitant A}: forall l (L:Zlength l = K) i j (v:A) (I: 0<=i<K) (J: 0<=j<K),
   (i=j /\ Znth i (upd_Znth j l v) = v) \/
   (i<>j /\ Znth i (upd_Znth j l v) = Znth i l).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros. unfold upd_Znth.
(* Goal: @eq (list A) (@sublist A lo hi al) (@cons A (@Znth A d lo al) (@nil A)) *)
  destruct (zeq i j); subst.
(* Goal: @eq A v v *)
  + left; split; trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    rewrite app_Znth2; rewrite Zlength_sublist; try rewrite Zminus_0_r; try rewrite Zminus_diag; try omega.
(* Goal: @eq A v v *)
    rewrite Znth_0_cons. trivial.
(* Goal: @eq A v v *)
  + right; split; trivial.
(* Goal: @eq A (@Znth A d i (@app A (@sublist A Z0 j l) (@cons A v (@sublist A (Z.add j (Zpos xH)) (@Zlength A l) l)))) (@Znth A d i l) *)
    destruct (zlt i j).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - rewrite app_Znth1; try rewrite Zlength_sublist; try omega.
(* Goal: @eq A v v *)
      rewrite Znth_sublist; try omega. rewrite Zplus_0_r; trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
    - rewrite app_Znth2; rewrite Zlength_sublist; try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
      rewrite Zminus_0_r, Znth_pos_cons, Znth_sublist; try omega.
(* Goal: @eq A v v *)
      assert (H: i - j - 1 + (j + 1) = i) by omega. rewrite H; trivial.
Qed.

Lemma upd_Znth_lookup' K {A}{d: Inhabitant A}: forall l (L:Zlength l = K) i (I: 0<=i<K) j (J: 0<=j<K) (v:A),
    Znth i (upd_Znth j l v) = if zeq i j then v else Znth i l.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros.
(* Goal: @eq A v v *)
  destruct (upd_Znth_lookup K l L i j v I J) as [[X Y] | [X Y]]; if_tac; try omega; trivial.
Qed.

Lemma upd_Znth_char {A} n l1 (v:A) l2 w: Zlength l1=n ->
      upd_Znth n (l1 ++ v :: l2) w = l1 ++ w :: l2.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. intros. unfold upd_Znth.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  specialize (Zlength_nonneg l1); intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  f_equal. rewrite sublist0_app1. apply sublist_same; omega. omega.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
  f_equal. rewrite sublist_app2, <- H, Zlength_app, Zlength_cons. do 2 rewrite Zminus_plus.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
                rewrite sublist_1_cons. apply sublist_same; omega. omega.
Qed.

Lemma upd_Znth_same {A}{d: Inhabitant A}: forall i l u, 0<= i< Zlength l -> Znth i (upd_Znth i l u) = u.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros. rewrite (upd_Znth_lookup' _ _ (eq_refl _)); trivial.
(* Goal: @eq A v v *)
  rewrite zeq_true; trivial.
Qed.

Lemma upd_Znth_diff {A}{d: Inhabitant A}: forall i j l u, 0<= i< Zlength l -> 0<= j< Zlength l -> i<>j ->
      Znth i (upd_Znth j l u) = Znth i l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros. rewrite (upd_Znth_lookup' _ _ (eq_refl _)); trivial.
(* Goal: @eq A v v *)
  rewrite zeq_false; trivial.
Qed.

Lemma upd_Znth_app1 {A} i l1 l2 (I: 0 <= i < Zlength l1) (v:A):
      upd_Znth i (l1++l2) v = upd_Znth i l1 v ++ l2.
Proof.
(* Goal: @eq (list A) (@upd_Znth A i (@app A l1 l2) v) (@app A (@upd_Znth A i l1 v) l2) *)
  assert (L2NN:= Zlength_nonneg l2).
(* Goal: @eq (list A) (@upd_Znth A Z0 l v) (@cons A v (@sublist A (Zpos xH) (@Zlength A l) l)) *)
  unfold upd_Znth.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite sublist_app1, Zlength_app, <- app_assoc; try omega.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  f_equal. simpl. f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite <- (sublist_rejoin (i+1) (Zlength l1)); try omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite sublist_app1; try omega. f_equal.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite sublist_app2, Zminus_diag, Zminus_plus; try omega.
(* Goal: @eq A v v *)
  apply sublist_same; trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Zlength_app; omega.
Qed.

Lemma upd_Znth_app2 {A} (l1 l2:list A) i v:
  Zlength l1 <= i <= Zlength l1 + Zlength l2 ->
  upd_Znth i (l1 ++ l2) v = l1 ++ upd_Znth (i-Zlength l1) l2 v.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
Proof. unfold upd_Znth. intros.
(* Goal: @eq A v v *)
  rewrite sublist0_app2; trivial. rewrite <- app_assoc. f_equal. f_equal. f_equal.
(* Goal: @eq (list A) (@sublist A (Z.add i (Zpos xH)) (@Zlength A (@app A l1 l2)) (@app A l1 l2)) (@sublist A (Z.add (Z.sub i (@Zlength A l1)) (Zpos xH)) (@Zlength A l2) l2) *)
  rewrite sublist_app2, Zlength_app, Zminus_plus.
(* Goal: @eq A v v *)
  assert (i + 1 - Zlength l1 = i - Zlength l1 + 1) by omega. rewrite H0; trivial.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  specialize (Zlength_nonneg l1); omega.
Qed.

Lemma upd_Znth0 {A} (l:list A) v:
upd_Znth 0 l v = v :: sublist 1 (Zlength l) l.
Proof. unfold upd_Znth. rewrite sublist_nil. reflexivity. Qed.

Lemma sublist_upd_Znth_l: forall {A} (l: list A) i lo hi v,
  0 <= lo <= hi ->
  hi <= i < Zlength l ->
  sublist lo hi (upd_Znth i l v) = sublist lo hi l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@upd_Znth A Z0 l v) (@cons A v (@sublist A (Zpos xH) (@Zlength A l) l)) *)
  unfold upd_Znth.
  rewrite sublist_app1.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: rewrite Zlength_sublist by omega; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite sublist_sublist by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  f_equal; omega.
Qed.

Lemma sublist_upd_Znth_r: forall {A} (l: list A) i lo hi v,
  0 <= i < lo ->
  lo <= hi <= Zlength l ->
  sublist lo hi (upd_Znth i l v) = sublist lo hi l.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@upd_Znth A Z0 l v) (@cons A v (@sublist A (Zpos xH) (@Zlength A l) l)) *)
  unfold upd_Znth.
  replace (sublist 0 i l ++ v :: sublist (i + 1) (Zlength l) l) with
    ((sublist 0 i l ++ v :: nil) ++ sublist (i + 1) (Zlength l) l)
    by (rewrite <- app_assoc; auto).
  rewrite sublist_app2.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: rewrite Zlength_app, Zlength_sublist, Zlength_correct by omega; simpl; omega.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  rewrite Zlength_app, Zlength_sublist, Zlength_correct by omega; simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite sublist_sublist by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  f_equal; omega.
Qed.

Lemma sublist_upd_Znth_lr: forall {A} (l: list A) i lo hi v,
  0 <= lo <= i->
  i < hi <= Zlength l ->
  sublist lo hi (upd_Znth i l v) = upd_Znth (i - lo) (sublist lo hi l) v.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: @eq (list A) (@upd_Znth A Z0 l v) (@cons A v (@sublist A (Zpos xH) (@Zlength A l) l)) *)
  unfold upd_Znth.
  change (v :: sublist (i + 1) (Zlength l) l) with
    ((v :: nil) ++ sublist (i + 1) (Zlength l) l).
  rewrite !sublist_app'.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: change (Zlength [v]) with 1; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: change (Zlength [v]) with 1; rewrite !Zlength_sublist by omega; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: rewrite !Zlength_sublist by omega; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  2: rewrite Zlength_app, !Zlength_sublist by omega; change (Zlength [v]) with 1; omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite !Zlength_sublist by omega.
  change (Zlength [v]) with 1.
  rewrite (@sublist_len_1 _ v) by (change (Zlength [v]) with 1; omega).
  change (@Znth _ v 0 [v]) with v.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
  simpl.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite !sublist_sublist by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  f_equal; [| f_equal]; f_equal; omega.
Qed.

(*Hint Rewrite @Zlength_list_repeat'  : sublist.*)
Hint Rewrite @Znth_list_repeat_inrange : sublist.
Hint Rewrite @Zlength_cons @Zlength_nil: sublist.
Hint Rewrite @list_repeat_0: sublist.
Hint Rewrite <- @app_nil_end : sublist.
Hint Rewrite @Zlength_app: sublist.
Hint Rewrite @Zlength_map: sublist.
Hint Rewrite @Zlength_list_repeat using list_solve: sublist.
Hint Rewrite Z.sub_0_r Z.add_0_l Z.add_0_r : sublist.
Hint Rewrite @Zlength_sublist using list_solve: sublist.
Hint Rewrite Z.max_r Z.max_l using omega : sublist.
Hint Rewrite Z.min_r Z.min_l using omega : sublist.
Hint Rewrite Z.add_simpl_r Z.sub_add Z.sub_diag : sublist.
Hint Rewrite @sublist_sublist using list_solve : sublist.
Hint Rewrite @sublist_app1 using list_solve : sublist.
Hint Rewrite @sublist_app2 using list_solve : sublist.
Hint Rewrite @sublist_list_repeat  using list_solve : sublist.
Hint Rewrite @sublist_same using list_solve : sublist.
Hint Rewrite Z.add_simpl_l : sublist.
Hint Rewrite Z.add_add_simpl_l_l Z.add_add_simpl_l_r
     Z.add_add_simpl_r_l Z.add_add_simpl_r_r : sublist.
Hint Rewrite Z.add_0_r : sublist.
Hint Rewrite @app_Znth1 using list_solve : sublist.
Hint Rewrite @app_Znth2 using list_solve : sublist.
Hint Rewrite @Znth_sublist using list_solve : sublist.
Hint Rewrite @upd_Znth_Zlength using list_solve : sublist.


Hint Rewrite @sublist_nil : sublist.


Lemma list_repeat_app':
 forall {A: Type} a b (x:A), 
    0 <= a -> 0 <= b ->
    list_repeat (Z.to_nat a) x ++ list_repeat (Z.to_nat b) x = list_repeat (Z.to_nat (a+b)) x.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
 intros.
(* Goal: @eq (list A) (@list_repeat A (Init.Nat.add (Z.to_nat a) (Z.to_nat b)) x) (@list_repeat A (Z.to_nat (Z.add a b)) x) *)
 rewrite list_repeat_app. f_equal.
(* Goal: @Forall A f al *)
  apply Nat2Z.inj. rewrite <- Z2Nat.inj_add; auto.
Qed.

Lemma Znth_overflow:
  forall {A}{d: Inhabitant A} i (al: list A), i >= Zlength al -> Znth i al = d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@Znth A d i al) d *)
  pose proof (Zlength_nonneg al).
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
   unfold Znth. rewrite if_false by omega.
(* Goal: @eq A (@nth A (Z.to_nat i) al d) d *)
  apply nth_overflow.
  apply Nat2Z.inj_le. rewrite <- Zlength_correct.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z2Nat.id by omega. omega.
Qed.

Lemma Znth_underflow:
  forall {A}{d: Inhabitant A} i (al: list A),  i < 0 -> Znth i al = d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
   unfold Znth. rewrite if_true by omega. auto.
Qed.

Lemma Znth_outofbounds:
  forall {A}{d: Inhabitant A} i (al: list A),  (i < 0 \/ i >= Zlength al) -> Znth i al = d.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @Forall A f al *)
  destruct H. apply Znth_underflow; auto. apply Znth_overflow; auto.
Qed.

Lemma sublist_one:
  forall {A}{d: Inhabitant A} lo hi (al: list A),
    0 <= lo -> hi <= Zlength al ->
    lo+1=hi -> sublist lo hi al = Znth lo al :: nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: @eq (list A) (@sublist A lo hi al) (@cons A (@Znth A d lo al) (@nil A)) *)
subst.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
rewrite Znth_cons_sublist by omega. rewrite <- app_nil_end.
(* Goal: @Forall A f al *)
auto.
Qed.

Lemma Forall_app :
forall {A} P (l1 l2 :list A),
Forall P (l1 ++ l2) <->
Forall P l1 /\ Forall P l2.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
split; induction l1; intros.
(* Goal: @Forall A f al *)
inv H. destruct l2; inv H0. auto.
(* Goal: @Forall A f al *)
split. auto. simpl in H2. inv H2.
(* Goal: @Forall A f al *)
constructor; auto.
(* Goal: @Forall A f al *)
split. inv H. constructor; auto. apply IHl1 in H3.
(* Goal: and (@Forall A P l1) (@Forall A P l2) *)
intuition.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H. apply IHl1 in H3. intuition.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. intuition.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
simpl. constructor.
(* Goal: @Forall A f al *)
destruct H. inv H. auto.
(* Goal: and (@Forall A P l1) (@Forall A P l2) *)
apply IHl1. intuition.
(* Goal: @Forall A f al *)
inv H0; auto.
Qed.

Lemma Forall_firstn:
  forall A (f: A -> Prop) n l, Forall f l -> Forall f (firstn n l).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; destruct l; intros.
(* Goal: @Forall A f (@skipn A (S n) (@nil A)) *)
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
constructor. constructor. constructor.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H. simpl. constructor; auto.
Qed.

Lemma Forall_skipn:
  forall A (f: A -> Prop) n l, Forall f l -> Forall f (skipn n l).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
induction n; destruct l; intros.
(* Goal: @Forall A f al *)
constructor. inv H; constructor; auto. constructor.
(* Goal: @Forall A f (@skipn A (S n) (@cons A a l)) *)
inv H. simpl.  auto.
Qed.

Lemma Forall_map:
  forall {A B} (f: B -> Prop) (g: A -> B) al,
   Forall f (map g al) <-> Forall (Basics.compose f g) al.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros.
(* Goal: and (@Forall A P l1) (@Forall A P l2) *)
induction al; simpl; intuition; inv H1; constructor; intuition.
Qed.

Lemma Forall_sublist:
  forall {A} (f: A -> Prop) lo hi al,
   Forall f al -> Forall f (sublist lo hi al).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. unfold sublist.
(* Goal: @Forall A f al *)
apply Forall_firstn. apply Forall_skipn. auto.
Qed.

Hint Rewrite @upd_Znth_app1 using list_solve : sublist.
Hint Rewrite @upd_Znth_app2 using list_solve : sublist.

Lemma map_list_repeat: forall {A B} (f: A->B) n (x:A), map f (list_repeat n x) = list_repeat n (f x).
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
intros. induction n; simpl; f_equal; auto.
Qed.
Hint Rewrite @map_list_repeat : sublist.

Lemma Zlength_sublist_correct: forall {A} (l: list A) (lo hi: Z),
  0 <= lo <= hi ->
  hi <= Zlength l ->
  Zlength (sublist lo hi l) = hi - lo.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist.
(* Goal: Z.lt (@Zlength A (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) l))) (Z.sub hi lo) *)
  rewrite Zlength_firstn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z.max_r by omega.
(* Goal: @Forall A f al *)
  rewrite Z.min_l; auto.
(* Goal: Z.lt (@Zlength A (@skipn A (Z.to_nat lo) l)) (Z.sub hi lo) *)
  rewrite Zlength_skipn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite (Z.max_r 0 lo) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z.max_r by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  omega.
Qed.

Lemma Zlength_sublist_incorrect: forall {A} (l: list A) (lo hi: Z),
  0 <= lo < hi ->
  hi > Zlength l ->
  Zlength (sublist lo hi l) < hi - lo.
Proof.
(* Goal: forall (A : Type) (l : list A) (lo hi : Z) (_ : and (Z.le Z0 lo) (Z.lt lo hi)) (_ : Z.gt hi (@Zlength A l)), Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  intros.
(* Goal: Z.lt (@Zlength A (@sublist A lo hi l)) (Z.sub hi lo) *)
  unfold sublist.
(* Goal: Z.lt (@Zlength A (@firstn A (Z.to_nat (Z.sub hi lo)) (@skipn A (Z.to_nat lo) l))) (Z.sub hi lo) *)
  rewrite Zlength_firstn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite Z.max_r by omega.
  assert (Zlength (skipn (Z.to_nat lo) l) < hi - lo); [| rewrite Z.min_r; omega].
(* Goal: Z.lt (@Zlength A (@skipn A (Z.to_nat lo) l)) (Z.sub hi lo) *)
  rewrite Zlength_skipn.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  rewrite (Z.max_r 0 lo) by omega.
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) d *)
(* Goal: @eq A (@nth A (Z.to_nat n) xs d) (@nth A (Z.to_nat n) xs d) *)
  apply Z.max_lub_lt; omega.
Qed.

Lemma nth_Znth {A} {d: Inhabitant A}:
forall n (xs:list A), 0 <= n < Zlength xs -> (nth (Z.to_nat n) xs d) = (Znth n xs).
Proof. intros; unfold Znth; if_tac; unfold default. omega. reflexivity. Qed.


 