(* File: My_Nth.v  (last edited on 25/10/2000) (c) Klaus Weich  *)

Require Export List.
Require Export Plus.


Section My_Nth.

Variable B : Set.

Inductive my_nth : nat -> list B -> B -> Prop :=
  | My_NthO : forall (l : list B) (a : B), my_nth 0 (a :: l) a
  | My_NthS :
      forall (n : nat) (l : list B) (b : B),
      my_nth n l b -> forall a : B, my_nth (S n) (a :: l) b.


Lemma inv_nth_nil : forall (n : nat) (a : B), my_nth n nil a -> False.
(* Goal: forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : @In B b l) (a : B), @In B b (@cons B a l) *)
intros.
(* Goal: my_nth n l b *)
inversion H.
Qed.


Lemma inv_nthO :
 forall (a : B) (l : list B) (b : B), my_nth 0 (a :: l) b -> a = b.
(* Goal: forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : @In B b l) (a : B), @In B b (@cons B a l) *)
intros.
(* Goal: my_nth n l b *)
inversion H.
(* Goal: @eq B b b *)
trivial.
Qed.


Lemma inv_nthS :
 forall (n : nat) (a : B) (l : list B) (b : B),
 my_nth (S n) (a :: l) b -> my_nth n l b.
(* Goal: forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : @In B b l) (a : B), @In B b (@cons B a l) *)
intros.
(* Goal: my_nth n l b *)
inversion H.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
assumption.
Qed.


Lemma my_nth_rec :
 forall P : nat -> list B -> B -> Set,
 (forall (l : list B) (a : B), P 0 (a :: l) a) ->
 (forall (n : nat) (l : list B) (b : B),
  my_nth n l b -> P n l b -> forall a : B, P (S n) (a :: l) b) ->
 forall (n : nat) (l : list B) (y : B), my_nth n l y -> P n l y.
(* Goal: forall (P : forall (_ : nat) (_ : list B) (_ : B), Set) (_ : forall (l : list B) (a : B), P O (@cons B a l) a) (_ : forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : P n l b) (a : B), P (S n) (@cons B a l) b) (n : nat) (l : list B) (y : B) (_ : my_nth n l y), P n l y *)
intros P base step n.
(* Goal: forall (l : list B) (y : B) (_ : my_nth n l y), P n l y *)
elim n; clear n.
(* Goal: forall (l : list B) (y : B) (_ : my_nth O l y), P O l y *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (y : B) (_ : my_nth n l y), P n l y) (l : list B) (y : B) (_ : my_nth (S n) l y), P (S n) l y *)
intros l; case l; clear l.
(* Goal: forall (y : B) (_ : my_nth (S n) (@nil B) y), P (S n) (@nil B) y *)
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth (S n) (@cons B b l) y), P (S n) (@cons B b l) y *)
intros y nth; elimtype False.
(* Goal: False *)
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth O (@cons B b l) y), P O (@cons B b l) y *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (y : B) (_ : my_nth n l y), P n l y) (l : list B) (y : B) (_ : my_nth (S n) l y), P (S n) l y *)
apply (inv_nth_nil 0 y nth).
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth (S n) (@cons B b l) y), P (S n) (@cons B b l) y *)
intros a l b nth.
(* Goal: P O (@cons B a l) b *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (y : B) (_ : my_nth n l y), P n l y) (l : list B) (y : B) (_ : my_nth (S n) l y), P (S n) l y *)
 rewrite (inv_nthO a l b nth).
(* Goal: P O (@cons B b l) b *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (y : B) (_ : my_nth n l y), P n l y) (l : list B) (y : B) (_ : my_nth (S n) l y), P (S n) l y *)
apply base.

(* Goal: forall (n : nat) (_ : forall (l : list B) (y : B) (_ : my_nth n l y), P n l y) (l : list B) (y : B) (_ : my_nth (S n) l y), P (S n) l y *)
intros n ih l.
(* Goal: forall _ : my_nth (S n) l a, nth_split a l *)
case l; clear l.
(* Goal: forall (y : B) (_ : my_nth (S n) (@nil B) y), P (S n) (@nil B) y *)
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth (S n) (@cons B b l) y), P (S n) (@cons B b l) y *)
intros y nth; elimtype False.
(* Goal: False *)
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth (S n) (@cons B b l) y), P (S n) (@cons B b l) y *)
apply (inv_nth_nil (S n) y nth).
(* Goal: forall (b : B) (l : list B) (y : B) (_ : my_nth (S n) (@cons B b l) y), P (S n) (@cons B b l) y *)
intros a l b nth.
(* Goal: P (S n) (@cons B a l) b *)
apply step.
(* Goal: my_nth n l b *)
apply (inv_nthS n a l b nth).
(* Goal: my_nth (Nat.add (@length B l0) n) (@app B l0 l1) a *)
apply ih.
(* Goal: my_nth n l b *)
apply (inv_nthS n a l b nth).
Qed.


Lemma nth_in : forall (n : nat) (l : list B) (a : B), my_nth n l a -> In a l.
(* Goal: forall (n : nat) (l : list B) (a : B) (_ : my_nth n l a), @In B a l *)
intros n l a nth.
(* Goal: @In B a l *)
elim nth; clear nth.
(* Goal: forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : @In B b l) (a : B), @In B b (@cons B a l) *)
intros.
(* Goal: @eq B b b *)
simpl in |- *; left; trivial.
(* Goal: forall (n : nat) (l : list B) (b : B) (_ : my_nth n l b) (_ : @In B b l) (a : B), @In B b (@cons B a l) *)
intros.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
simpl in |- *; right; assumption.
Qed.


Lemma nth_app0 :
 forall (n : nat) (l0 l1 : list B) (a : B),
 my_nth n l0 a -> my_nth n (l0 ++ l1) a.
(* Goal: forall (n : nat) (l0 l1 : list B) (a : B) (_ : my_nth n l0 a), my_nth n (@app B l0 l1) a *)
intros n l0.
(* Goal: forall _ : my_nth n (@app B l0 l1) a, inv_my_nth_app n l0 l1 a *)
generalize n; clear n.
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth n l0 a), my_nth n (@app B l0 l1) a *)
elim l0; clear l0.
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth n (@nil B) a), my_nth n (@app B (@nil B) l1) a *)
(* Goal: forall (a : B) (l : list B) (_ : forall (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n l a0), my_nth n (@app B l l1) a0) (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n (@cons B a l) a0), my_nth n (@app B (@cons B a l) l1) a0 *)
intros n l1 a nth; elimtype False.
(* Goal: False *)
(* Goal: forall (a : B) (l : list B) (_ : forall (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n l a0), my_nth n (@app B l l1) a0) (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n (@cons B a l) a0), my_nth n (@app B (@cons B a l) l1) a0 *)
apply (inv_nth_nil n a nth).
(* Goal: forall (a : B) (l : list B) (_ : forall (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n l a0), my_nth n (@app B l l1) a0) (n : nat) (l1 : list B) (a0 : B) (_ : my_nth n (@cons B a l) a0), my_nth n (@app B (@cons B a l) l1) a0 *)
intros a0 l0 ih n.
(* Goal: forall _ : my_nth n (@cons B a0 (@app B l0 l1)) a, inv_my_nth_app n (@cons B a0 l0) l1 a *)
case n; clear n.
(* Goal: forall (l1 : list B) (a : B) (_ : my_nth O (@cons B a0 l0) a), my_nth O (@app B (@cons B a0 l0) l1) a *)
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth (S n) (@cons B a0 l0) a), my_nth (S n) (@app B (@cons B a0 l0) l1) a *)
intros l1 a nth.
(* Goal: my_nth O (@app B (@cons B a0 l0) l1) a *)
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth (S n) (@cons B a0 l0) a), my_nth (S n) (@app B (@cons B a0 l0) l1) a *)
 rewrite (inv_nthO a0 l0 a nth).
(* Goal: my_nth O (@app B (@cons B a l0) l1) a *)
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth (S n) (@cons B a0 l0) a), my_nth (S n) (@app B (@cons B a0 l0) l1) a *)
simpl in |- *; apply My_NthO.
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth (S n) (@cons B a0 l0) a), my_nth (S n) (@app B (@cons B a0 l0) l1) a *)
intros n l1 a nth.
(* Goal: my_nth (S n) (@app B (@cons B a0 l0) l1) a *)
simpl in |- *; apply My_NthS.
(* Goal: my_nth (Nat.add (@length B l0) n) (@app B l0 l1) a *)
apply ih.
(* Goal: my_nth n l0 a *)
apply (inv_nthS n a0 l0 a nth).
Qed.


Lemma nth_app1 :
 forall (n : nat) (l0 l1 : list B) (a : B),
 my_nth n l1 a -> my_nth (length l0 + n) (l0 ++ l1) a.
(* Goal: forall (n : nat) (l1 : list B) (a : B) (_ : my_nth n l0 a), my_nth n (@app B l0 l1) a *)
intros n l0; elim l0; clear l0.
(* Goal: @eq B b b *)
simpl in |- *; trivial.
(* Goal: forall (a : B) (l : list B) (_ : forall (l1 : list B) (a0 : B) (_ : my_nth n l1 a0), my_nth (Nat.add (@length B l) n) (@app B l l1) a0) (l1 : list B) (a0 : B) (_ : my_nth n l1 a0), my_nth (Nat.add (@length B (@cons B a l)) n) (@app B (@cons B a l) l1) a0 *)
intros a0 l0 ih l1 a nth.
(* Goal: my_nth (Nat.add (@length B (@cons B a0 l0)) n) (@app B (@cons B a0 l0) l1) a *)
simpl in |- *.
(* Goal: my_nth (S (Nat.add (@length B l0) n)) (@cons B a0 (@app B l0 l1)) a *)
apply My_NthS.
(* Goal: my_nth (Nat.add (@length B l0) n) (@app B l0 l1) a *)
apply ih.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
assumption.
Qed.


Inductive inv_my_nth_app (n : nat) (l0 l1 : list B) (a : B) : Set :=
  | Inv_Nth_App0 : my_nth n l0 a -> inv_my_nth_app n l0 l1 a
  | Inv_Nth_App1 :
      forall n' : nat, my_nth n' l1 a -> inv_my_nth_app n l0 l1 a.

Lemma inv_nth_app :
 forall (n : nat) (l0 l1 : list B) (a : B),
 my_nth n (l0 ++ l1) a -> inv_my_nth_app n l0 l1 a.
(* Goal: forall (n : nat) (l0 l1 : list B) (a : B) (_ : my_nth n (@app B l0 l1) a), inv_my_nth_app n l0 l1 a *)
intros n l0 l1 a.
(* Goal: forall _ : my_nth n (@app B l0 l1) a, inv_my_nth_app n l0 l1 a *)
generalize n; clear n.
(* Goal: my_nth (Nat.add (@length B (@cons B a0 l0)) n) (@app B (@cons B a0 l0) l1) a *)
elim l0; clear l0; simpl in |- *.
(* Goal: forall (x : nat) (_ : my_nth x l b), @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
intros n nth.
(* Goal: inv_my_nth_app n (@nil B) l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
right with n.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
assumption.
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
intros a0 l0 ih_l0 n.
(* Goal: forall _ : my_nth n (@cons B a0 (@app B l0 l1)) a, inv_my_nth_app n (@cons B a0 l0) l1 a *)
case n; clear n.
(* Goal: forall _ : my_nth O (@cons B a0 (@app B l0 l1)) a, inv_my_nth_app O (@cons B a0 l0) l1 a *)
(* Goal: forall (n : nat) (_ : my_nth (S n) (@cons B a0 (@app B l0 l1)) a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
intros nth.
(* Goal: inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: forall (n' : nat) (_ : my_nth n' l1 a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: my_nth n (@app B l0 l1) a *)
left.
(* Goal: my_nth O (@cons B a0 l0) a *)
(* Goal: forall (n : nat) (_ : my_nth (S n) (@cons B a0 (@app B l0 l1)) a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
 rewrite (inv_nthO a0 (l0 ++ l1) a nth).
(* Goal: my_nth O (@cons B b l) b *)
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
apply My_NthO.
(* Goal: forall (x : nat) (_ : my_nth x l b), @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
intros n nth.
(* Goal: inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
elim (ih_l0 n).
(* Goal: forall _ : my_nth n l0 a, inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: forall (n' : nat) (_ : my_nth n' l1 a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: my_nth n (@app B l0 l1) a *)
intros nth_l0.
(* Goal: inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: forall (n' : nat) (_ : my_nth n' l1 a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: my_nth n (@app B l0 l1) a *)
left.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
apply My_NthS; assumption.
(* Goal: forall (n' : nat) (_ : my_nth n' l1 a), inv_my_nth_app (S n) (@cons B a0 l0) l1 a *)
(* Goal: my_nth n (@app B l0 l1) a *)
intros n' nth_l1.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
right with n'; assumption.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
apply inv_nthS with a0; assumption.
Qed.



Inductive nth_split (a : B) (l : list B) : Set :=
    Nth_Split_Intro :
      forall l1 l2 : list B, l = l1 ++ a :: l2 -> nth_split a l.     

Lemma my_nth_split :
 forall (n : nat) (l : list B) (a : B), my_nth n l a -> nth_split a l.
(* Goal: forall (l : list B) (y : B) (_ : my_nth n l y), P n l y *)
intros n; elim n; clear n.
(* Goal: forall (l : list B) (a : B) (_ : my_nth O l a), nth_split a l *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (a : B) (_ : my_nth n l a), nth_split a l) (l : list B) (a : B) (_ : my_nth (S n) l a), nth_split a l *)
intros l a nth.
(* Goal: nth_split a l *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (a : B) (_ : my_nth n l a), nth_split a l) (l : list B) (a : B) (_ : my_nth (S n) l a), nth_split a l *)
apply Nth_Split_Intro with (nil (A:=B)) (tail l).
(* Goal: @eq (list B) l (@app B (@nil B) (@cons B a (@tl B l))) *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (a : B) (_ : my_nth n l a), nth_split a l) (l : list B) (a : B) (_ : my_nth (S n) l a), nth_split a l *)
inversion_clear nth.
(* Goal: @eq B b b *)
simpl in |- *; trivial.
(* Goal: forall (n : nat) (_ : forall (l : list B) (a : B) (_ : my_nth n l a), nth_split a l) (l : list B) (a : B) (_ : my_nth (S n) l a), nth_split a l *)
intros n ih l a. 
(* Goal: forall _ : my_nth (S n) l a, nth_split a l *)
case l; clear l.
(* Goal: @eq (list B) l (@app B (@nil B) (@cons B a (@tl B l))) *)
(* Goal: forall (n : nat) (_ : forall (l : list B) (a : B) (_ : my_nth n l a), nth_split a l) (l : list B) (a : B) (_ : my_nth (S n) l a), nth_split a l *)
intros nth; elimtype False; inversion_clear nth.
(* Goal: forall (b : B) (l : list B) (_ : my_nth (S n) (@cons B b l) a), nth_split a (@cons B b l) *)
intros a0 l nth.
(* Goal: nth_split a (@cons B a0 l) *)
elim (ih l a); clear ih.
(* Goal: forall (l1 l2 : list B) (_ : @eq (list B) l (@app B l1 (@cons B a l2))), nth_split a (@cons B a0 l) *)
(* Goal: my_nth n l a *)
intros l1 l2 H.
(* Goal: nth_split a (@cons B a0 l) *)
(* Goal: my_nth n l a *)
apply Nth_Split_Intro with (a0 :: l1) l2.
(* Goal: @eq B b b *)
 rewrite H; simpl in |- *; trivial.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
inversion_clear nth; assumption.
Qed.

Lemma in_nth :
 forall (a : B) (l : list B), In a l -> exists n : nat, my_nth n l a.
(* Goal: forall (a : B) (l : list B) (_ : @In B a l), @ex nat (fun n : nat => my_nth n l a) *)
intros b l; elim l; clear l.
(* Goal: forall _ : @In B b (@nil B), @ex nat (fun n : nat => my_nth n (@nil B) b) *)
(* Goal: forall (a : B) (l : list B) (_ : forall _ : @In B b l, @ex nat (fun n : nat => my_nth n l b)) (_ : @In B b (@cons B a l)), @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
intros in_b; inversion_clear in_b.
(* Goal: forall (a : B) (l : list B) (_ : forall _ : @In B b l, @ex nat (fun n : nat => my_nth n l b)) (_ : @In B b (@cons B a l)), @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
intros a l ih in_a.
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
inversion_clear in_a.
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
exists 0.
(* Goal: my_nth O (@cons B a l) b *)
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
 rewrite H.
(* Goal: my_nth O (@cons B b l) b *)
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
apply My_NthO.
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
elim ih; try assumption.
(* Goal: forall (x : nat) (_ : my_nth x l b), @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
intros n nth.
(* Goal: @ex nat (fun n : nat => my_nth n (@cons B a l) b) *)
exists (S n).
(* Goal: my_nth n l1 a *)
(* Goal: forall (a0 : B) (l : list B) (_ : forall (n : nat) (_ : my_nth n (@app B l l1) a), inv_my_nth_app n l l1 a) (n : nat) (_ : my_nth n (@cons B a0 (@app B l l1)) a), inv_my_nth_app n (@cons B a0 l) l1 a *)
apply My_NthS; assumption.
Qed.

End My_Nth.