Require Import ExtLib.Data.Fin.

Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.

Fixpoint vector (T : Type) (n : nat) : Type :=
  match n with
    | 0 => unit
    | S n => prod T (vector T n)
  end.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Fixpoint get {T} {n : nat} (f : fin n) : vector T n -> T :=
  match f in fin n return vector T n -> T with
    | F0 n => fun v : T * vector T n => fst v
    | FS n f => fun v : T * vector T n => get f (snd v)
  end.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Fixpoint put {T} {n : nat} (f : fin n) (t : T) : vector T n -> vector T n :=
  match f in fin n return vector T n -> vector T n with
    | F0 _ => fun v => (t, snd v)
    | FS _ f => fun v => (fst v, put f t (snd v))
  end.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Theorem get_put_eq : forall {T n} (v : vector T n) (f : fin n) val,
  get f (put f val v) = val.
Proof.
(* Goal: forall (T : Type) (n : nat) (v : vector T n) (f f' : fin n) (val : T) (_ : not (@eq (fin n) f f')), @eq T (@get T n f (@put T n f' val v)) (@get T n f v) *)
  induction n.
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
  { inversion f. }
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
  { remember (S n). destruct f.
(* Goal: forall val : T, @eq T (@get T (S n0) (@F0 n0) (@put T (S n0) (@F0 n0) val v)) val *)
(* Goal: forall val : T, @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) (@FS n0 f) val v)) val *)
    inversion Heqn0; subst; intros; reflexivity.
    inversion Heqn0; subst; simpl; auto. }
Qed.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Theorem get_put_neq : forall {T n} (v : vector T n) (f f' : fin n) val,
  f <> f' ->
  get f (put f' val v) = get f v.
Proof.
(* Goal: forall (T : Type) (n : nat) (v : vector T n) (f f' : fin n) (val : T) (_ : not (@eq (fin n) f f')), @eq T (@get T n f (@put T n f' val v)) (@get T n f v) *)
  induction n.
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
  { inversion f. }
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
  { remember (S n); destruct f.
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
    { inversion Heqn0; clear Heqn0; subst; intros.
(* Goal: @eq T (@get T (S n) (@F0 n) (@put T (S n) f' val v)) (@get T (S n) (@F0 n) v) *)
      destruct (fin_case f'); try congruence.
      destruct H0; subst. auto. }
(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
    { inversion Heqn0; clear Heqn0; subst; intros.
(* Goal: @eq T (@get T (S n) (@FS n f) (@put T (S n) f' val v)) (@get T (S n) (@FS n f) v) *)
      destruct (fin_case f').
(* Goal: @eq T (@get T (S n) (@F0 n) (@put T (S n) (@FS n x) val v)) (@get T (S n) (@F0 n) v) *)
      subst; auto.
(* Goal: @eq T (@get T (S n) (@FS n f) (@put T (S n) f' val v)) (@get T (S n) (@FS n f) v) *)
      destruct H0; subst. simpl.
      eapply IHn. congruence. } }
Qed.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Definition vector_tl {T : Type} {n : nat} (v : vector T (S n)) : vector T n :=
  snd v.

(* Goal: forall (f' : fin (S n0)) (val : T) (_ : not (@eq (fin (S n0)) (@FS n0 f) f')), @eq T (@get T (S n0) (@FS n0 f) (@put T (S n0) f' val v)) (@get T (S n0) (@FS n0 f) v) *)
Definition vector_hd {T : Type} {n : nat} (v : vector T (S n)) : T :=
  fst v.
