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)).

Definition sublist (v : list A) (start lengt : nat) :=
  trunc (strip v start) lengt.

Definition elemlist (v : list A) (i : nat) := trunc (strip v i) 1.


Lemma length_trunc :
 forall (v : list A) (i : nat),
 
 i <= length v -> length (trunc v i) = i.
simple induction v. simpl in |- *. auto with v62.
intros b b0 H. simple induction i. simpl in |- *. trivial with v62.
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).
simpl in |- *. trivial with v62.
Qed.

Lemma trunc_all : forall v : list A, trunc v (length v) = v.
simple induction v. simpl in |- *. trivial with v62.
intros. rewrite length_eq2. simpl in |- *. rewrite H. trivial with v62.
Qed. Hint Resolve trunc_all.

Lemma trunc_max :
 forall (v : list A) (i : nat),
 
 length v <= i -> trunc v i = v.
simple induction v. simpl in |- *. trivial with v62.
intros. inversion H0. rewrite trunc_all. trivial with v62.
simpl in |- *. rewrite H. trivial with v62.
apply le_Sn_le. generalize H1. simpl in |- *. trivial with v62.
Qed.

Lemma trunc_O : forall v : list A, trunc v 0 = nil.
simple induction v; auto with v62.
Qed. Hint Resolve trunc_O.

Lemma le_length_trunc :
 forall (v : list A) (i : nat), length (trunc v i) <= i.
simple induction v. simpl in |- *. auto with v62.
intros. case i. rewrite trunc_O. auto with v62.
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).
simple induction v1. simpl in |- *. auto with v62.
intros. rewrite app_eq2.
rewrite length_eq2. elim i. simpl in |- *. rewrite trunc_O. trivial with v62.
intros. simpl in |- *. rewrite H. trivial with v62.
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).
intros. rewrite trunc_app. rewrite (trunc_max v1 (length v1 + i)).
replace (length v1 + i - length v1) with i. trivial with v62. auto with v62.
auto with v62.
Qed.

Lemma trunc_eq :
 forall (v1 v2 : list A) (i : nat), v1 = v2 -> trunc v1 i = trunc v2 i.
intros. rewrite H. trivial with v62.
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.
simple induction v. simpl in |- *. trivial with v62.
simple induction i; simple induction j. trivial with v62.
repeat rewrite trunc_O. simpl in |- *. trivial with v62.
repeat rewrite trunc_O. simpl in |- *. trivial with v62.
intros. simpl in |- *. rewrite H. trivial with v62.
Qed.

Lemma trunc_trunc1 :
 forall (v : list A) (i : nat),
 
 trunc (trunc v i) i = trunc v i.
simple induction v. simpl in |- *. trivial with v62.
simple induction i. repeat rewrite trunc_O. trivial with v62.
intros. simpl in |- *. rewrite H. trivial with v62.
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.
intros. rewrite (trunc_max (trunc v i) j). trivial with v62.
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.
intros. rewrite <- (trunc_max (trunc v j) i). rewrite trunc_sym. trivial with v62.
apply le_trans with j. apply le_length_trunc.
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.
intros. rewrite <- H0. rewrite trunc_trunc3. trivial with v62. exact H.
Qed.


Lemma strip_nil : forall i : nat, strip nil i = nil.
intro. auto with v62.
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.
unfold strip in |- *. simple induction i. simpl in |- *.
elim minus_n_O. intro. replace (length v) with (length (rev A v)).
rewrite trunc_all. rewrite trunc_app. rewrite trunc_all.
elim minus_n_n. rewrite trunc_O. rewrite app_v_nil. trivial with v62.
apply length_rev.
intros. apply rev_eq. simpl in |- *.
rewrite trunc_app. rewrite length_rev. rewrite minus_minus_lem1.
rewrite trunc_O. rewrite app_v_nil. trivial with v62.
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.
unfold strip in |- *. intros. rewrite length_rev. rewrite length_trunc. trivial with v62.
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.
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.
unfold strip in |- *. trivial with v62.
Qed.

Lemma strip_all : forall v : list A, strip v (length v) = nil.
unfold strip in |- *. intro. rewrite <- minus_n_n. rewrite trunc_O. auto with v62.
Qed. Hint Resolve strip_all.

Lemma strip_max :
 forall (v : list A) (i : nat),
 
 length v <= i -> strip v i = nil.
unfold strip in |- *. intros. rewrite <- rev_eq1.
apply rev_eq. rewrite <- length_rev. rewrite minus_le_O. auto with v62.
rewrite length_rev. exact H.
Qed.

Lemma strip_O : forall v : list A, strip v 0 = v.
intro. unfold strip in |- *. rewrite <- minus_n_O. rewrite <- length_rev.
rewrite trunc_all. rewrite rev_rev. trivial with v62.
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).
simple induction v1. simpl in |- *. intros. elim minus_n_O. trivial with v62.
simple induction v2. intro. simpl in |- *.
rewrite strip_nil. rewrite app_v_nil. rewrite app_v_nil. trivial with v62.
simple induction i.
rewrite strip_O. simpl in |- *. rewrite strip_O. rewrite strip_O. auto with v62.
intros. rewrite app_eq2. rewrite strip_cons_S.
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).
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with v62.
simple induction i. intros. rewrite strip_O.
do 2 rewrite strip_cons_S. rewrite strip_O. trivial with v62.
simple induction j. rewrite strip_O.
repeat rewrite strip_cons_S. elim n. rewrite strip_O. trivial with v62.
intros. rewrite <- H. rewrite strip_O. trivial with v62.
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.
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with v62.
simple induction i. intro. rewrite strip_O. rewrite strip_O. trivial with v62.
simple induction j. rewrite strip_O. rewrite strip_O. try trivial with v62.
intros. rewrite strip_cons_S. rewrite strip_cons_S.
replace (strip (strip l n) (S n0)) with (strip (strip l (S n)) 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.
intros. rewrite H. trivial with v62.
Qed. Hint Resolve strip_eq.

Lemma strip_strip :
 forall (v : list A) (i j : nat),
 
 strip (strip v i) j = strip v (i + j).
simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with v62.
simple induction i. intro. simpl in |- *. rewrite strip_O. trivial with v62.
simple induction j. rewrite strip_O. elim plus_n_O. trivial with v62.
intros. rewrite strip_cons_S. simpl in |- *. rewrite strip_cons_S. apply H.
Qed. Hint Resolve strip_strip.


Lemma app_trunc_strip :
 forall (v : list A) (i : nat),
 
 trunc v i ++ strip v i = v.
simple induction v. unfold strip in |- *. simpl in |- *. trivial with v62.
intros. elim i. rewrite trunc_O. rewrite strip_O. simpl in |- *. trivial with v62.
intros. unfold strip in |- *. simpl in |- *.
rewrite trunc_app. rewrite rev_app. rewrite length_rev.
case n. rewrite <- minus_n_O.
rewrite <- minus_n_n. rewrite trunc_O. rewrite trunc_O. simpl in |- *.
rewrite <- length_rev. rewrite trunc_all. rewrite rev_rev. trivial with v62.
intro. replace (length l - S n0 - length l) with 0.
rewrite trunc_O. simpl in |- *.
replace (rev A (trunc (rev A l) (length l - S n0))) with (strip l (S n0)).
rewrite H. trivial with v62.
unfold strip in |- *. trivial with v62.
rewrite minus_minus_lem1. trivial with v62.
Qed.

Lemma strip_trunc_i :
 forall (v : list A) (i : nat), strip (trunc v i) i = nil.
simple induction v. auto with v62.
simple induction i. auto with v62.
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).
simple induction v. simpl in |- *. unfold strip in |- *. simpl in |- *. trivial with v62.
simple induction i; simple induction j.
simpl in |- *. rewrite strip_O. rewrite trunc_O. trivial with v62.
rewrite trunc_O.
simpl in |- *. intros. unfold strip in |- *. simpl in |- *. rewrite trunc_O. trivial with v62.
rewrite strip_O. rewrite strip_O. elim minus_n_O. trivial with v62.
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.
simple induction v. unfold strip in |- *. simpl in |- *. trivial with v62.
simple induction i; simple induction j. rewrite trunc_O. rewrite strip_O. auto with v62.
intros. rewrite strip_O. rewrite strip_O. auto with v62.
rewrite trunc_O. elim plus_n_O. rewrite strip_trunc_i. trivial with v62.
intros.
rewrite strip_cons_S. replace (S n + S n0) with (S (n + S n0)).
simpl in |- *. rewrite strip_cons_S. apply H.
auto with v62.
Qed.


Lemma elemlist_is_sublist :
 forall (v : list A) (i : nat),
 
 elemlist v i = sublist v i 1.
unfold elemlist, sublist in |- *. trivial with v62.
Qed.

Lemma elemlist_cons_S :
 forall (v : list A) (i : nat) (b : A),
 
 elemlist (b :: v) (S i) = elemlist v i.
unfold elemlist in |- *. intros. rewrite strip_cons_S. trivial with v62.
Qed.

Lemma elemlist_cons_O :
 forall (v : list A) (b : A),
 
 elemlist (b :: v) 0 = b :: nil.
intros.
unfold elemlist in |- *. rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with v62.
Qed.

Lemma elemlist_inv :
 forall (l : list A) (i : nat),
 
 trunc (strip l i) 1 = elemlist l i.
unfold elemlist in |- *. trivial with v62.
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).
simple induction v. unfold elemlist in |- *. simpl in |- *. trivial with v62.
simple induction i. simpl in |- *. unfold elemlist in |- *. rewrite trunc_O.
rewrite strip_O. simpl in |- *. rewrite trunc_O. trivial with v62.
intros. simpl in |- *. unfold elemlist in |- *.
rewrite strip_cons_S. unfold elemlist in H. rewrite H. trivial with v62.
generalize H1. simpl in |- *. auto with v62.
Qed.

Lemma length_elemlist :
 forall (l : list A) (i : nat),
 
 i < length l -> length (elemlist l i) = 1.
intros. unfold elemlist in |- *. rewrite length_trunc. trivial with v62.
rewrite length_strip. inversion H. rewrite <- minus_Sn_m. auto with v62. auto with v62.
rewrite <- minus_Sn_m. auto with v62. apply le_Sn_le. exact H1. apply lt_le_weak. exact H.
Qed.

End Lists_field.