Require Import Arith Coq.Lists.List Setoid Coq.Lists.SetoidList.
Require Export Infra.Option EqDec AutoIndTac Util LengthEq.

Set Implicit Arguments.

Inductive getT (X:Type) : list X → nat → X → Type :=
| getTLB xl x : getT (x::xl) 0 x
| getTLS n xl x x´ : getT xl n x → getT (x´::xl) (S n) x.

Inductive get (X:Type) : list X → nat → X → Prop :=
| getLB xl x : get (x::xl) 0 x
| getLS n xl x x´ : get xl n x → get (x´::xl) (S n) x.

Lemma get_getT X (x:X) n L
  : get L n x → getT L n x.

Lemma getT_get X (x:X) n L
  : getT L n x → get L n x.

Lemma get_functional X (xl:list X) n (x x´:X) :
  get xl n x → get xl n x´ → x = x´.

Lemma get_shift X (L:list X) k L1 blk :
  get L k blk → get (L1 ++ L) (length L1+k) blk.

Lemma shift_get X (L:list X) k L1 blk :
  get (L1 ++ L) (length L1+k) blk → get L k blk.

Lemma get_app X (L L´:list X) k x
  : get L k x → get (L ++ L´) k x.

Lemma get_nth_default {X:Type} L n m (default:X):
get L n m → nth n L default = m.

Lemma get_length {X:Type} L n (s:X)
(getl : get L n s) :
n < length L.

Lemma get_nth X L n m (d:X) :
get L n m → nth n L d = m.

Lemma nth_default_nil X (v : X) x : nth_default v nil x = v.

Lemma get_nth_error X (L : list X) k x :
  get L k x → nth_error L k = Some x.

Lemma nth_error_nth X (L:list X) d x n
  : nth_error L n = Some x → nth n L d = x.

Lemma nth_get {X:Type} L n s {default:X}
(lt : n < length L)
(nthL : nth n L default = s):
get L n s.

Lemma nth_get_neq {X:Type} L n s {default:X}
(neq:s ≠ default)
(nthL : nth n L default = s):
get L n s.

Lemma nth_error_get X (L : list X) k x :
  nth_error L k = Some x → get L k x.

Lemma nth_error_app X (L L´:list X) k x
 : nth_error L k = Some x → nth_error (L++L´) k = Some x.

Lemma nth_error_shift X (L L´:list X) x
  : nth_error (L++(x::L´)) (length L) = Some x.

Lemma nth_app_shift X (L L´:list X) x d
  : x < length L → nth x (L++L´) d = nth x L d.

Ltac get_functional :=
  match goal with
    | [ H : get ?XL ?n _, H´ : get ?XL ?n _ |- _ ] ⇒
      simplify_eq (get_functional H H´); intros; clear H
    | _ ⇒ fail "no matching get assumptions"
  end.

Ltac eval_nth_get :=
  match goal with
    | [ H : get ?XL ?n _ |- (bind (nth_error ?XL ?n) _) = _ ] ⇒
        rewrite (get_nth_error H); simpl
    | _ ⇒ fail "no matching get assumptions"
  end.

Lemma get_dec {X} (L:list X) n
      : { x | get L n x } + { ∀ x, get L n x → False }.

Hint Constructors get : get.
Hint Resolve get_functional : get.
Hint Resolve get_shift : get.
Hint Resolve nth_error_get : get.

Ltac simplify_get := try repeat get_functional; repeat eval_nth_get; eauto with get.

Lemma nth_shift X x (L L´:list X) d
  : nth (length L+x) (L++L´) d = nth x L´ d.

Lemma get_range X (L:list X) n v
  : get L n v → n < length L.

Lemma get_in_range X (L:list X) n
  : n < length L → { x:X & get L n x }.

Lemma nth_in X L x (d:X)
  : x < length L → In (nth x L d) L.

Lemma in_get X `{EqDec X eq} (xl : list X) (x : X) :
  In x xl → { n : nat & get xl n x }.

Lemma get_in X `{EqDec X eq} (xl : list X) (x : X) n :
  get xl n x → In x xl.

Lemma list_map_eq X Y Z (f:X→Z) g (L:list X) (L´:list Y) n x
  : List.map f L = List.map g L´
    → get L n x → ∃ y, get L´ n y ∧ f x = g y.

Lemma map_get_1 X Y (L:list X) (f:X → Y) n x
  : get L n x → get (List.map f L) n (f x).

Lemma map_get_2 X Y (L:list X) (f:X → Y) n x
  : get (List.map f L) n x → ∃ x´ : X, get L n x´.

Lemma map_get_3 X Y (L:list X) (f:X → Y) n x
  : getT (List.map f L) n x → { x´ : X & (getT L n x´ × (f x´ = x))%type }.

Lemma map_get_4 X Y (L:list X) (f:X → Y) n x
  : get (List.map f L) n x → { x´ : X | get L n x´ ∧ f x´ = x }.

Lemma map_get X Y (L:list X) (f:X → Y) n blk Z
  : get L n blk
  → get (List.map f L) n Z
  → Z = f blk.

Lemma get_length_eq X Y (L:list X) (L´:list Y) n x
  : get L n x → length L = length L´ → ∃ y, get L´ n y.

Require Compare_dec.

Lemma get_in_range_app X L L´ n (x:X)
  : n < length L → get (L ++ L´) n x → get L n x.

Lemma get_subst X (L L´:list X) x x´ n
  : get (L ++ x :: L´) n x´
    → get L n x´
       ∨ (x = x´ ∧ n = length L)
       ∨ (get L´ (n - S (length L)) x´ ∧ n > length L).

Lemma get_app_cases X (L L´:list X) x´ n
  : get (L ++ L´) n x´
    → get L n x´
       ∨ (get L´ (n - length L) x´ ∧ n ≥ length L).

Lemma get_app_right X (L L´:list X) n n´ x
  : n´ = (length L´ + n) → get L n x → get (L´ ++ L) n´ x.

Lemma get_length_app X (L L´:list X) x
  : get (L ++ x :: L´) (length L) x.

Lemma get_app_le X (L L´:list X) n x (LE:n < length L)
  : get (L ++ L´) n x → get L n x.

Lemma tl_map X Y L (f:X → Y)
  : List.map f (tl L) = tl (List.map f L).

Lemma nth_error_default {X:Type} v E a (x : X) : Some v = nth_error E a → v = nth_default x E a.