
Set Implicit Arguments.
Unset Strict Implicit.

Require Export List.

Section Listes.

  Variable A : Set.

  Let List := list A.



  Inductive item (x : A) : List -> nat -> Prop :=
    | item_hd : forall l : List, item x (x :: l) 0
    | item_tl :
        forall (l : List) (n : nat) (y : A),
        item x l n -> item x (y :: l) (S n).

  Lemma fun_item :
   forall (u v : A) (e : List) (n : nat), item u e n -> item v e n -> u = v.
Proof.
(* Goal: forall (u v : A) (e : List) (n : nat) (_ : item u e n) (_ : item v e n), @eq A u v *)
simple induction 1; intros.
(* Goal: @eq A u v *)
(* Goal: @eq A u v *)
inversion_clear H0; auto.

(* Goal: @eq A u v *)
inversion_clear H2; auto.
Qed.


  Lemma list_item :
   forall e n, {t : _ | item t e n} + {(forall t, ~ item t e n)}.
Proof.
(* Goal: forall (e : List) (n : nat), sumor (@sig A (fun t : A => item t e n)) (forall t : A, not (item t e n)) *)
fix item_rec 1.
(* Goal: forall (e : List) (n : nat), sumor (@sig A (fun t : A => item t e n)) (forall t : A, not (item t e n)) *)
intros [| h l].
(* Goal: forall n : nat, sumor (@sig A (fun t : A => item t (@nil A) n)) (forall t : A, not (item t (@nil A) n)) *)
(* Goal: forall n : nat, sumor (@sig A (fun t : A => item t (@cons A h l) n)) (forall t : A, not (item t (@cons A h l) n)) *)
right; red in |- *; intros t in_nil; inversion in_nil.

(* Goal: forall n : nat, sumor (@sig A (fun t : A => item t (@cons A h l) n)) (forall t : A, not (item t (@cons A h l) n)) *)
intros [| k].
(* Goal: sumor (@sig A (fun t : A => item t (@cons A h l) O)) (forall t : A, not (item t (@cons A h l) O)) *)
(* Goal: sumor (@sig A (fun t : A => item t (@cons A h l) (S k))) (forall t : A, not (item t (@cons A h l) (S k))) *)
left; exists h; constructor.

(* Goal: sumor (@sig A (fun t : A => item t (@cons A h l) (S k))) (forall t : A, not (item t (@cons A h l) (S k))) *)
case (item_rec l k).
(* Goal: forall _ : @sig A (fun t : A => item t l k), sumor (@sig A (fun t : A => item t (@cons A h l) (S k))) (forall t : A, not (item t (@cons A h l) (S k))) *)
(* Goal: forall _ : forall t : A, not (item t l k), sumor (@sig A (fun t : A => item t (@cons A h l) (S k))) (forall t : A, not (item t (@cons A h l) (S k))) *)
intros (y, in_tl); left; exists y; constructor; trivial.

intros not_in_tl; right; intros t in_tl_l; inversion_clear in_tl_l;
 red in not_in_tl; eauto.
Defined.



  Inductive trunc : nat -> List -> List -> Prop :=
    | trunc_O : forall e : List, trunc 0 e e
    | trunc_S :
        forall (k : nat) (e f : List) (x : A),
        trunc k e f -> trunc (S k) (x :: e) f.

  Lemma item_trunc :
   forall (n : nat) (e : List) (t : A),
   item t e n -> exists f : List, trunc (S n) e f.
Proof.
(* Goal: forall (n : nat) (e : List) (t : A) (_ : item t e n), @ex List (fun f : List => trunc (S n) e f) *)
simple induction n; intros.
(* Goal: @ex List (fun f : List => trunc (S O) e f) *)
(* Goal: @ex List (fun f : List => trunc (S (S n0)) e f) *)
inversion_clear H.
(* Goal: @ex List (fun f : List => trunc (S O) (@cons A t l) f) *)
(* Goal: @ex List (fun f : List => trunc (S (S n0)) e f) *)
exists l.
(* Goal: trunc (S (S n0)) (@cons A y l) x *)
(* Goal: item t l n0 *)
apply trunc_S.
(* Goal: trunc O l l *)
(* Goal: @ex List (fun f : List => trunc (S (S n0)) e f) *)
apply trunc_O.

(* Goal: @ex List (fun f : List => trunc (S (S n0)) e f) *)
inversion_clear H0.
(* Goal: @ex List (fun f : List => trunc (S (S n0)) (@cons A y l) f) *)
elim H with l t; intros.
(* Goal: @ex List (fun f : List => trunc (S (S n0)) (@cons A y l) f) *)
(* Goal: item t l n0 *)
exists x.
(* Goal: trunc (S (S n0)) (@cons A y l) x *)
(* Goal: item t l n0 *)
apply trunc_S.
(* Goal: item t l n0 *)
trivial.

(* Goal: item t l n0 *)
trivial.
Qed.


End Listes.

  Hint Resolve item_hd item_tl trunc_O trunc_S: core.

