(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************)
(*           The Calculus of Inductive Constructions            *)
(*                       COQ v5.10                              *)
(*                                                              *)
(* Laurent Arditi.  Laboratoire I3S. CNRS ura 1376.             *)
(* Universite de Nice - Sophia Antipolis                        *)
(* arditi@unice.fr, http://wwwi3s.unice.fr/~arditi/lolo.html    *)
(*                                                              *)
(* date: may 1995                                               *)
(* file: Lists_field.v                                          *)
(* contents: trunc, strip, sublist and elemlist for polymorphic *)
(* lists.                                                       *)
(****************************************************************)

Require Import Arith_compl.
Require Export Minus.
Require Export Lists_compl.


Section Lists_field.
Variable A : Set.

Fixpoint trunc (v : list A) : nat -> list A :=
  fun n : nat =>
  match v return (list A) with
  | nil => nil
  | b :: w =>
      match n return (list A) with
      | O => nil
      | S p => b :: trunc w p
      end
  end.

Definition strip (v : list A) (n : nat) :=
  rev A (trunc (rev A v) (length v - n)).

(* Selection d'une sous liste commencant a la position start, de
   longueur lengt *)
Definition sublist (v : list A) (start lengt : nat) :=
  trunc (strip v start) lengt.

(* Selection de la liste contenant le i-eme element d'une liste *)
Definition elemlist (v : list A) (i : nat) := trunc (strip v i) 1.

(****************************************************************)
(* lemmes sur trunc *)

Lemma length_trunc :
 forall (v : list A) (i : nat),
 (*****************)
 i <= length v -> length (trunc v i) = i.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. auto with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros b b0 H. simple induction i. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. intros. apply eq_S. apply H. apply le_S_n. exact H1.
Qed.

Lemma trunc_inv :
 forall (v : list A) (i : nat) (b : A),
 (**************)
 b :: trunc v i = trunc (b :: v) (S i).
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. trivial with arith.
Qed.

Lemma trunc_all : forall v : list A, trunc v (length v) = v.
(**************)
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. rewrite length_eq2. simpl in |- *. rewrite H. trivial with arith.
Qed. Hint Resolve trunc_all.

Lemma trunc_max :
 forall (v : list A) (i : nat),
 (**************)
 length v <= i -> trunc v i = v.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. inversion H0. rewrite trunc_all. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. rewrite H. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
apply le_Sn_le. generalize H1. simpl in |- *. trivial with arith.
Qed.

Lemma trunc_O : forall v : list A, trunc v 0 = nil.
(************)
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
simple induction v; auto with arith.
Qed. Hint Resolve trunc_O.

Lemma le_length_trunc :
 forall (v : list A) (i : nat), length (trunc v i) <= i.
(********************)
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. auto with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
intros. case i. rewrite trunc_O. auto with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intro. simpl in |- *. apply le_n_S. apply H.
Qed. Hint Resolve le_length_trunc.

Lemma trunc_app :
 forall (v1 v2 : list A) (i : nat),
 (**************)
 trunc (v1 ++ v2) i = trunc v1 i ++ trunc v2 (i - length v1).
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simple induction v1. simpl in |- *. auto with arith.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros. rewrite app_eq2.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite length_eq2. elim i. simpl in |- *. rewrite trunc_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. simpl in |- *. rewrite H. trivial with arith.
Qed. Hint Resolve trunc_app.

Lemma app_v_trunc :
 forall (v1 v2 : list A) (i : nat),
 (****************)
 v1 ++ trunc v2 i = trunc (v1 ++ v2) (length v1 + i).
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros. rewrite trunc_app. rewrite (trunc_max v1 (length v1 + i)).
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
replace (length v1 + i - length v1) with i. trivial with arith. auto with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
auto with arith.
Qed.

Lemma trunc_eq :
 forall (v1 v2 : list A) (i : nat), v1 = v2 -> trunc v1 i = trunc v2 i.
(*************)
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite H. trivial with arith.
Qed. Hint Resolve trunc_eq.

Lemma trunc_sym :
 forall (v : list A) (i j : nat), 
 (**************)
 trunc (trunc v i) j = trunc (trunc v j) i.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
simple induction i; simple induction j. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
repeat rewrite trunc_O. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
repeat rewrite trunc_O. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. simpl in |- *. rewrite H. trivial with arith.
Qed.

Lemma trunc_trunc1 :
 forall (v : list A) (i : nat),
 (*****************)
 trunc (trunc v i) i = trunc v i.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. trivial with arith.
(* Goal: forall (a : A) (l : list A) (_ : forall (i : nat) (_ : le (S i) (@length A l)), @eq (list A) (@app A (trunc l i) (elemlist l i)) (trunc l (S i))) (i : nat) (_ : le (S i) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) i) (elemlist (@cons A a l) i)) (trunc (@cons A a l) (S i)) *)
simple induction i. repeat rewrite trunc_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. simpl in |- *. rewrite H. trivial with arith.
Qed. Hint Resolve trunc_trunc1.

Lemma trunc_trunc2 :
 forall (v : list A) (i j : nat),
 (*****************)
 i <= j -> trunc (trunc v i) j = trunc v i.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite (trunc_max (trunc v i) j). trivial with arith.
(* Goal: le (@length A (trunc v i)) j *)
apply le_trans with i. apply le_length_trunc. exact H.
Qed.

Lemma trunc_trunc3 :
 forall (v : list A) (i j : nat),
 (*****************)
 j <= i -> trunc (trunc v i) j = trunc v j.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite <- (trunc_max (trunc v j) i). rewrite trunc_sym. trivial with arith.
(* Goal: le (@length A (trunc (rev A v) (Nat.sub (@length A v) i))) (Nat.sub (@length A v) i) *)
apply le_trans with j. apply le_length_trunc.
(* Goal: lt i (@length A l) *)
exact H.
Qed.

Lemma trunc_plus_petit :
 forall (v1 v2 : list A) (i j : nat),
 (*********************)
 j <= i -> trunc v1 i = v2 -> trunc v1 j = trunc v2 j.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite <- H0. rewrite trunc_trunc3. trivial with arith. exact H.
Qed.

(****************************************************************)
(* lemmes sur strip *)

Lemma strip_nil : forall i : nat, strip nil i = nil.
(**************)
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
intro. auto with arith.
Qed. Hint Resolve strip_nil.

Lemma strip_cons_S :
 forall (v : list A) (i : nat) (b : A),
 (*****************)
 strip (b :: v) (S i) = strip v i.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
unfold strip in |- *. simple induction i. simpl in |- *.
(* Goal: forall n : nat, @eq (list A) (@cons A a (@app A (trunc l (S n)) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) (S n)) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n))))))) (@cons A a l) *)
elim minus_n_O. intro. replace (length v) with (length (rev A v)).
(* Goal: @eq (list A) (@cons A a (rev A (trunc (rev A l) (@length A (rev A l))))) (@cons A a l) *)
(* Goal: forall n : nat, @eq (list A) (@cons A a (@app A (trunc l (S n)) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) (S n)) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n))))))) (@cons A a l) *)
rewrite trunc_all. rewrite trunc_app. rewrite trunc_all.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
elim minus_n_n. rewrite trunc_O. rewrite app_v_nil. trivial with arith.
(* Goal: @eq nat (@length A (rev A v)) (@length A v) *)
(* Goal: forall (n : nat) (_ : forall b : A, @eq (list A) (rev A (trunc (rev A (@cons A b v)) (Nat.sub (@length A (@cons A b v)) (S n)))) (rev A (trunc (rev A v) (Nat.sub (@length A v) n)))) (b : A), @eq (list A) (rev A (trunc (rev A (@cons A b v)) (Nat.sub (@length A (@cons A b v)) (S (S n))))) (rev A (trunc (rev A v) (Nat.sub (@length A v) (S n)))) *)
apply length_rev.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. apply rev_eq. simpl in |- *.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l n) (rev A (trunc (@app A (rev A l) (@cons A a (@nil A))) (Nat.sub (@length A l) n))))) (@cons A a l) *)
rewrite trunc_app. rewrite length_rev. rewrite minus_minus_lem1.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite trunc_O. rewrite app_v_nil. trivial with arith.
Qed. Hint Resolve strip_cons_S.

Lemma length_strip :
 forall (v : list A) (i : nat),
 (*****************)
 i <= length v -> length (strip v i) = length v - i.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold strip in |- *. intros. rewrite length_rev. rewrite length_trunc. trivial with arith.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l n) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) n) (@length A (rev A l))))) (rev A (trunc (rev A l) (Nat.sub (@length A l) n)))))) (@cons A a l) *)
rewrite length_rev. apply minus_le_lem2.
Qed.

Lemma le_length_strip :
 forall (v : list A) (i : nat),
 (********************)
 length (strip v i) <= length v - i.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
unfold strip in |- *. intros. rewrite length_rev. apply le_length_trunc.
Qed.

Lemma strip_inv :
 forall (v : list A) (i : nat),
 (***************)
 rev A (trunc (rev A v) (length v - i)) = strip v i.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold strip in |- *. trivial with arith.
Qed.

Lemma strip_all : forall v : list A, strip v (length v) = nil.
(**************)
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
unfold strip in |- *. intro. rewrite <- minus_n_n. rewrite trunc_O. auto with arith.
Qed. Hint Resolve strip_all.

Lemma strip_max :
 forall (v : list A) (i : nat),
 (**************)
 length v <= i -> strip v i = nil.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
unfold strip in |- *. intros. rewrite <- rev_eq1.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
apply rev_eq. rewrite <- length_rev. rewrite minus_le_O. auto with arith.
(* Goal: lt i (@length A l) *)
rewrite length_rev. exact H.
Qed.

Lemma strip_O : forall v : list A, strip v 0 = v.
(************)
(* Goal: forall n : nat, @eq (list A) (@cons A a (@app A (trunc l (S n)) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) (S n)) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n))))))) (@cons A a l) *)
intro. unfold strip in |- *. rewrite <- minus_n_O. rewrite <- length_rev.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite trunc_all. rewrite rev_rev. trivial with arith.
Qed. Hint Resolve strip_O.

Lemma strip_app :
 forall (v1 v2 : list A) (i : nat),
 (**************)
 strip (v1 ++ v2) i = strip v1 i ++ strip v2 (i - length v1).
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simple induction v1. simpl in |- *. intros. elim minus_n_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simple induction v2. intro. simpl in |- *.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite strip_nil. rewrite app_v_nil. rewrite app_v_nil. trivial with arith.
(* Goal: forall (a : A) (l : list A) (_ : forall (i : nat) (_ : le (S i) (@length A l)), @eq (list A) (@app A (trunc l i) (elemlist l i)) (trunc l (S i))) (i : nat) (_ : le (S i) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) i) (elemlist (@cons A a l) i)) (trunc (@cons A a l) (S i)) *)
simple induction i.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite strip_O. simpl in |- *. rewrite strip_O. rewrite strip_O. auto with arith.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros. rewrite app_eq2. rewrite strip_cons_S.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite strip_cons_S. rewrite length_eq2. simpl in |- *. apply H.
Qed.

Lemma strip_strip_S :
 forall (v : list A) (i j : nat),
 (******************)
 strip (strip v (S i)) j = strip (strip v i) (S j).
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith.
(* Goal: forall (a : A) (l : list A) (_ : forall (i : nat) (_ : le (S i) (@length A l)), @eq (list A) (@app A (trunc l i) (elemlist l i)) (trunc l (S i))) (i : nat) (_ : le (S i) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) i) (elemlist (@cons A a l) i)) (trunc (@cons A a l) (S i)) *)
simple induction i. intros. rewrite strip_O.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
do 2 rewrite strip_cons_S. rewrite strip_O. trivial with arith.
(* Goal: forall _ : le (S O) (S (@length A l)), @eq (list A) (trunc (strip (@cons A a l) O) (S O)) (@cons A a (@nil A)) *)
(* Goal: forall (n : nat) (_ : forall _ : le (S n) (@length A (@cons A a l)), @eq (list A) (@app A (trunc (@cons A a l) n) (elemlist (@cons A a l) n)) (trunc (@cons A a l) (S n))) (_ : le (S (S n)) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) (S n)) (elemlist (@cons A a l) (S n))) (trunc (@cons A a l) (S (S n))) *)
simple induction j. rewrite strip_O.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
repeat rewrite strip_cons_S. elim n. rewrite strip_O. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite <- H. rewrite strip_O. trivial with arith.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros. do 2 rewrite strip_cons_S. apply H.
Qed.

Lemma strip_sym :
 forall (v : list A) (i j : nat),
 (**************)
 strip (strip v i) j = strip (strip v j) i.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith.
(* Goal: forall (a : A) (l : list A) (_ : forall (i : nat) (_ : le (S i) (@length A l)), @eq (list A) (@app A (trunc l i) (elemlist l i)) (trunc l (S i))) (i : nat) (_ : le (S i) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) i) (elemlist (@cons A a l) i)) (trunc (@cons A a l) (S i)) *)
simple induction i. intro. rewrite strip_O. rewrite strip_O. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
simple induction j. rewrite strip_O. rewrite strip_O. try trivial with arith.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros. rewrite strip_cons_S. rewrite strip_cons_S.
(* Goal: @eq (list A) (strip (strip l n) (S n0)) (strip (strip l n0) (S n)) *)
replace (strip (strip l n) (S n0)) with (strip (strip l (S n)) n0).
(* Goal: @eq (list A) (trunc (strip l n) (S n0)) (strip (trunc l (Nat.add n (S n0))) n) *)
(* Goal: @eq nat (S (Nat.add n (S n0))) (Nat.add (S n) (S n0)) *)
apply H. apply strip_strip_S.
Qed.

Lemma strip_eq :
 forall (v1 v2 : list A) (i : nat), v1 = v2 -> strip v1 i = strip v2 i.
(*************)
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. rewrite H. trivial with arith.
Qed. Hint Resolve strip_eq.

Lemma strip_strip :
 forall (v : list A) (i j : nat),
 (****************)
 strip (strip v i) j = strip v (i + j).
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simple induction i. intro. simpl in |- *. rewrite strip_O. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
simple induction j. rewrite strip_O. elim plus_n_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. rewrite strip_cons_S. simpl in |- *. rewrite strip_cons_S. apply H.
Qed. Hint Resolve strip_strip.

(****************************************************************)
(* lemmes sur trunc et strip ensembles *)

Lemma app_trunc_strip :
 forall (v : list A) (i : nat),
 (********************)
 trunc v i ++ strip v i = v.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. unfold strip in |- *. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. elim i. rewrite trunc_O. rewrite strip_O. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. unfold strip in |- *. simpl in |- *.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l n) (rev A (trunc (@app A (rev A l) (@cons A a (@nil A))) (Nat.sub (@length A l) n))))) (@cons A a l) *)
rewrite trunc_app. rewrite rev_app. rewrite length_rev.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l O) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) O) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) O)))))) (@cons A a l) *)
(* Goal: forall n : nat, @eq (list A) (@cons A a (@app A (trunc l (S n)) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) (S n)) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n))))))) (@cons A a l) *)
case n. rewrite <- minus_n_O.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite <- minus_n_n. rewrite trunc_O. rewrite trunc_O. simpl in |- *.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite <- length_rev. rewrite trunc_all. rewrite rev_rev. trivial with arith.
(* Goal: forall n : nat, @eq (list A) (@cons A a (@app A (trunc l (S n)) (@app A (rev A (trunc (@cons A a (@nil A)) (Nat.sub (Nat.sub (@length A l) (S n)) (@length A l)))) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n))))))) (@cons A a l) *)
intro. replace (length l - S n0 - length l) with 0.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite trunc_O. simpl in |- *.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l (S n0)) (rev A (trunc (rev A l) (Nat.sub (@length A l) (S n0)))))) (@cons A a l) *)
(* Goal: @eq nat O (Nat.sub (Nat.sub (@length A l) (S n0)) (@length A l)) *)
replace (rev A (trunc (rev A l) (length l - S n0))) with (strip l (S n0)).
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite H. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold strip in |- *. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite minus_minus_lem1. trivial with arith.
Qed.

Lemma strip_trunc_i :
 forall (v : list A) (i : nat), strip (trunc v i) i = nil.
(******************)
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. auto with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
simple induction i. auto with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. simpl in |- *. rewrite strip_cons_S. apply H.
Qed. Hint Resolve strip_trunc_i.

Lemma strip_trunc :
 forall (v : list A) (i j : nat),
 (****************)
 strip (trunc v i) j = trunc (strip v j) (i - j).
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. simpl in |- *. unfold strip in |- *. simpl in |- *. trivial with arith.
(* Goal: forall (a : A) (l : list A) (_ : forall i j : nat, @eq (list A) (trunc (strip l i) j) (strip (trunc l (Nat.add i j)) i)) (i j : nat), @eq (list A) (trunc (strip (@cons A a l) i) j) (strip (trunc (@cons A a l) (Nat.add i j)) i) *)
simple induction i; simple induction j.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. rewrite strip_O. rewrite trunc_O. trivial with arith.
(* Goal: forall _ : le (S O) (S (@length A l)), @eq (list A) (@cons A a (trunc l O)) (@cons A a (@nil A)) *)
(* Goal: forall (n : nat) (_ : forall _ : le (S n) (@length A (@cons A a l)), @eq (list A) (@app A (trunc (@cons A a l) n) (elemlist (@cons A a l) n)) (trunc (@cons A a l) (S n))) (_ : le (S (S n)) (@length A (@cons A a l))), @eq (list A) (@app A (trunc (@cons A a l) (S n)) (elemlist (@cons A a l) (S n))) (trunc (@cons A a l) (S (S n))) *)
rewrite trunc_O.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. intros. unfold strip in |- *. simpl in |- *. rewrite trunc_O. trivial with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite strip_O. rewrite strip_O. elim minus_n_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. rewrite strip_cons_S. simpl in |- *. rewrite strip_cons_S. apply H.
Qed.

Lemma trunc_strip :
 forall (v : list A) (i j : nat),
 (****************)
 trunc (strip v i) j = strip (trunc v (i + j)) i.
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. unfold strip in |- *. simpl in |- *. trivial with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
simple induction i; simple induction j. rewrite trunc_O. rewrite strip_O. auto with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
intros. rewrite strip_O. rewrite strip_O. auto with arith.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite trunc_O. elim plus_n_O. rewrite strip_trunc_i. trivial with arith.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros.
(* Goal: @eq (list A) (@cons A a (@app A (trunc l n) (trunc (strip (@cons A a l) (S n)) (S O)))) (@cons A a (trunc l (S n))) *)
rewrite strip_cons_S. replace (S n + S n0) with (S (n + S n0)).
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simpl in |- *. rewrite strip_cons_S. apply H.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
auto with arith.
Qed.

(****************************************************************)
(* lemmes sur elemlist et sublist *)

Lemma elemlist_is_sublist :
 forall (v : list A) (i : nat),
 (************************)
 elemlist v i = sublist v i 1.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold elemlist, sublist in |- *. trivial with arith.
Qed.

Lemma elemlist_cons_S :
 forall (v : list A) (i : nat) (b : A),
 (********************)
 elemlist (b :: v) (S i) = elemlist v i.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold elemlist in |- *. intros. rewrite strip_cons_S. trivial with arith.
Qed.

Lemma elemlist_cons_O :
 forall (v : list A) (b : A),
 (********************)
 elemlist (b :: v) 0 = b :: nil.
(* Goal: forall (l : list A) (i : nat) (_ : lt i (@length A l)), @eq nat (@length A (elemlist l i)) (S O) *)
intros.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
unfold elemlist in |- *. rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with arith.
Qed.

Lemma elemlist_inv :
 forall (l : list A) (i : nat),
 (*****************)
 trunc (strip l i) 1 = elemlist l i.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
unfold elemlist in |- *. trivial with arith.
Qed.

Lemma app_trunc_elemlist :
 forall (v : list A) (i : nat),
 (***********************)
 S i <= length v -> trunc v i ++ elemlist v i = trunc v (S i).
(* Goal: forall (v : list A) (i : nat) (_ : le (S i) (@length A v)), @eq (list A) (@app A (trunc v i) (elemlist v i)) (trunc v (S i)) *)
simple induction v. unfold elemlist in |- *. simpl in |- *. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
simple induction i. simpl in |- *. unfold elemlist in |- *. rewrite trunc_O.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
intros. simpl in |- *. unfold elemlist in |- *.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
rewrite strip_cons_S. unfold elemlist in H. rewrite H. trivial with arith.
(* Goal: forall _ : le (S (S n)) (@length A (@cons A a l)), le (S n) (@length A l) *)
generalize H1. simpl in |- *. auto with arith.
Qed.


Lemma length_elemlist :
 forall (l : list A) (i : nat),
 (********************)
 i < length l -> length (elemlist l i) = 1.
(* Goal: @eq nat (S O) (S O) *)
(* Goal: le (S O) (@length A (strip l i)) *)
intros. unfold elemlist in |- *. rewrite length_trunc. trivial with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
rewrite length_strip. inversion H. rewrite <- minus_Sn_m. auto with arith. auto with arith.
(* Goal: le (S O) (S (Nat.sub m i)) *)
(* Goal: le i m *)
(* Goal: le i (@length A l) *)
rewrite <- minus_Sn_m. auto with arith. apply le_Sn_le. exact H1. apply lt_le_weak. exact H.
Qed.


End Lists_field.