Library MyList
Require Import Le.
Require Import Gt.
Require Export List.
Section Listes.
Variable A : Set.
Let List := list A.
Inductive item (x : A) : List -> nat -> Prop :=
| item_hd : ∀ l, item x (x :: l) 0
| item_tl : ∀ l n y, item x l n -> item x (y :: l) (S n).
Lemma fun_item : ∀ u v e n, item u e n -> item v e n -> u = v.
Fixpoint nth_def (d : A) (l : List) (n : nat) {struct l} : A :=
match l, n with
| nil, _ => d
| x :: _, O => x
| _ :: tl, S k => nth_def d tl k
end.
Lemma nth_sound : ∀ x l n d, item x l n -> nth_def d l n = x.
Lemma inv_nth_nl : ∀ x n, ~ item x nil n.
Lemma inv_nth_cs : ∀ x y l n, item x (y :: l) (S n) -> item x l n.
Inductive insert (x : A) : nat -> List -> List -> Prop :=
| insert_hd : ∀ l, insert x 0 l (x :: l)
| insert_tl :
∀ n l il y, insert x n l il -> insert x (S n) (y :: l) (y :: il).
Inductive trunc : nat -> List -> List -> Prop :=
| trunc_O : ∀ e, trunc 0 e e
| trunc_S : ∀ k e f x, trunc k e f -> trunc (S k) (x :: e) f.
Hint Constructors trunc: core.
Lemma item_trunc :
∀ n e t, item t e n -> exists f : _, trunc (S n) e f.
Lemma ins_le :
∀ k f g d x,
insert x k f g -> ∀ n, k <= n -> nth_def d f n = nth_def d g (S n).
Lemma ins_gt :
∀ k f g d x,
insert x k f g -> ∀ n, k > n -> nth_def d f n = nth_def d g n.
Lemma ins_eq : ∀ k f g d x, insert x k f g -> nth_def d g k = x.
Lemma list_item :
∀ e n, {t : _ | item t e n} + {∀ t, ~ item t e n}.
End Listes.
Hint Constructors item: core.
Hint Constructors insert: core.
Hint Constructors trunc: core.
Fixpoint map (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
match l with
| nil => nil (A:=B)
| x :: t => f x :: map f t
end.
Require Import Gt.
Require Export List.
Section Listes.
Variable A : Set.
Let List := list A.
Inductive item (x : A) : List -> nat -> Prop :=
| item_hd : ∀ l, item x (x :: l) 0
| item_tl : ∀ l n y, item x l n -> item x (y :: l) (S n).
Lemma fun_item : ∀ u v e n, item u e n -> item v e n -> u = v.
Fixpoint nth_def (d : A) (l : List) (n : nat) {struct l} : A :=
match l, n with
| nil, _ => d
| x :: _, O => x
| _ :: tl, S k => nth_def d tl k
end.
Lemma nth_sound : ∀ x l n d, item x l n -> nth_def d l n = x.
Lemma inv_nth_nl : ∀ x n, ~ item x nil n.
Lemma inv_nth_cs : ∀ x y l n, item x (y :: l) (S n) -> item x l n.
Inductive insert (x : A) : nat -> List -> List -> Prop :=
| insert_hd : ∀ l, insert x 0 l (x :: l)
| insert_tl :
∀ n l il y, insert x n l il -> insert x (S n) (y :: l) (y :: il).
Inductive trunc : nat -> List -> List -> Prop :=
| trunc_O : ∀ e, trunc 0 e e
| trunc_S : ∀ k e f x, trunc k e f -> trunc (S k) (x :: e) f.
Hint Constructors trunc: core.
Lemma item_trunc :
∀ n e t, item t e n -> exists f : _, trunc (S n) e f.
Lemma ins_le :
∀ k f g d x,
insert x k f g -> ∀ n, k <= n -> nth_def d f n = nth_def d g (S n).
Lemma ins_gt :
∀ k f g d x,
insert x k f g -> ∀ n, k > n -> nth_def d f n = nth_def d g n.
Lemma ins_eq : ∀ k f g d x, insert x k f g -> nth_def d g k = x.
Lemma list_item :
∀ e n, {t : _ | item t e n} + {∀ t, ~ item t e n}.
End Listes.
Hint Constructors item: core.
Hint Constructors insert: core.
Hint Constructors trunc: core.
Fixpoint map (A B : Set) (f : A -> B) (l : list A) {struct l} : list B :=
match l with
| nil => nil (A:=B)
| x :: t => f x :: map f t
end.