Set Implicit Arguments.

Require Import Lia.
Require Import Vericertlib.
From Coq Require Import Lists.List Datatypes.

Import ListNotations.

Local Open Scope nat_scope.

Record Array (A : Type) : Type :=
  mk_array
    { arr_contents : list A
    ; arr_length : nat
    ; arr_wf : length arr_contents = arr_length
    }.

Definition make_array {A : Type} (l : list A) : Array A :=
  @mk_array A l (length l) eq_refl.

Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
  match i, l with
  | _, nil => nil
  | S n, h :: t => h :: list_set n x t
  | O, h :: t => x :: t
  end.

Lemma list_set_spec1 {A : Type} :
  forall l i (x : A),
    i < length l -> nth_error (list_set i x l) i = Some x.
A:Type
forall (l : list A) (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
Proof.
A:Type
forall (l : list A) (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
  induction l; intros; destruct i; crush; firstorder.
A:Type
a:A
l:list A
IHl:forall (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
i:nat
x:A
H:S i < S (length l)
nth_error (list_set i x l) i = Some x intuition.
Qed.
Hint Resolve list_set_spec1 : array.

Lemma list_set_spec2 {A : Type} :
  forall l i (x : A) d,
    i < length l -> nth i (list_set i x l) d = x.
A:Type
forall (l : list A) (i : nat) (x d : A),
i < length l -> nth i (list_set i x l) d = x
Proof.
A:Type
forall (l : list A) (i : nat) (x d : A),
i < length l -> nth i (list_set i x l) d = x
  induction l; intros; destruct i; crush; firstorder.
A:Type
a:A
l:list A
IHl:forall (i : nat) (x d : A), i < length l -> nth i (list_set i x l) d = x
i:nat
x, d:A
H:S i < S (length l)
nth i (list_set i x l) d = x intuition.
Qed.
Hint Resolve list_set_spec2 : array.

Lemma list_set_spec3 {A : Type} :
  forall l i1 i2 (x : A),
    i1 <> i2 ->
    nth_error (list_set i1 x l) i2 = nth_error l i2.
A:Type
forall (l : list A) (i1 i2 : nat) (x : A),
i1 <> i2 ->
nth_error (list_set i1 x l) i2 = nth_error l i2
Proof.
A:Type
forall (l : list A) (i1 i2 : nat) (x : A),
i1 <> i2 ->
nth_error (list_set i1 x l) i2 = nth_error l i2
  induction l; intros; destruct i1; destruct i2; crush; firstorder.
Qed.
Hint Resolve list_set_spec3 : array.

Lemma array_set_wf {A : Type} :
  forall l ln i (x : A),
    length l = ln -> length (list_set i x l) = ln.
A:Type
forall (l : list A) (ln i : nat) (x : A),
length l = ln -> length (list_set i x l) = ln
Proof.
A:Type
forall (l : list A) (ln i : nat) (x : A),
length l = ln -> length (list_set i x l) = ln
  induction l; intros; destruct i; auto.
A:Type
a:A
l:list A
IHl:forall (ln i : nat) (x : A), length l = ln -> length (list_set i x l) = ln
ln, i:nat
x:A
H:length (a :: l) = ln
length (list_set (S i) x (a :: l)) = ln

  invert H; crush; auto.
Qed.

Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
  let l := a.(arr_contents) in
  let ln := a.(arr_length) in
  let WF := a.(arr_wf) in
  @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).

Lemma array_set_spec1 {A : Type} :
  forall a i (x : A),
    i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
nth_error (arr_contents (array_set i x a)) i = Some x
Proof.
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
nth_error (arr_contents (array_set i x a)) i = Some x
  intros.
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
nth_error (arr_contents (array_set i x a)) i = Some x

  rewrite <- a.(arr_wf) in H.
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error (arr_contents (array_set i x a)) i = Some x
  unfold array_set.
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error
  (arr_contents
     {|
     arr_contents := list_set i x (arr_contents a);
     arr_length := arr_length a;
     arr_wf := array_set_wf (arr_contents a) i x
                 (arr_wf a) |}) i = Some x crush.
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error (list_set i x (arr_contents a)) i = Some x
  eauto with array.
Qed.
Hint Resolve array_set_spec1 : array.

Lemma array_set_spec2 {A : Type} :
  forall a i (x : A) d,
    i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
A:Type
forall (a : Array A) (i : nat) (x d : A),
i < arr_length a ->
nth i (arr_contents (array_set i x a)) d = x
Proof.
A:Type
forall (a : Array A) (i : nat) (x d : A),
i < arr_length a ->
nth i (arr_contents (array_set i x a)) d = x
  intros.
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
nth i (arr_contents (array_set i x a)) d = x

  rewrite <- a.(arr_wf) in H.
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i (arr_contents (array_set i x a)) d = x
  unfold array_set.
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i
  (arr_contents
     {|
     arr_contents := list_set i x (arr_contents a);
     arr_length := arr_length a;
     arr_wf := array_set_wf (arr_contents a) i x
                 (arr_wf a) |}) d = x crush.
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i (list_set i x (arr_contents a)) d = x
  eauto with array.
Qed.
Hint Resolve array_set_spec2 : array.

Lemma array_set_len {A : Type} :
  forall a i (x : A),
    a.(arr_length) = (array_set i x a).(arr_length).
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a = arr_length (array_set i x a)
Proof.
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a = arr_length (array_set i x a)
  unfold array_set.
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a =
arr_length
  {|
  arr_contents := list_set i x (arr_contents a);
  arr_length := arr_length a;
  arr_wf := array_set_wf (arr_contents a) i x
              (arr_wf a) |} crush.
Qed.

Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
  nth_error a.(arr_contents) i.

Lemma array_get_error_equal {A : Type} :
  forall (a b : Array A) i,
    a.(arr_contents) = b.(arr_contents) ->
    array_get_error i a = array_get_error i b.
A:Type
forall (a b : Array A) (i : nat),
arr_contents a = arr_contents b ->
array_get_error i a = array_get_error i b
Proof.
A:Type
forall (a b : Array A) (i : nat),
arr_contents a = arr_contents b ->
array_get_error i a = array_get_error i b
  unfold array_get_error.
A:Type
forall (a b : Array A) (i : nat),
arr_contents a = arr_contents b ->
nth_error (arr_contents a) i =
nth_error (arr_contents b) i crush.
Qed.

Lemma array_get_error_bound {A : Type} :
  forall (a : Array A) i,
    i < a.(arr_length) -> exists x, array_get_error i a = Some x.
A:Type
forall (a : Array A) (i : nat),
i < arr_length a ->
exists x : A, array_get_error i a = Some x
Proof.
A:Type
forall (a : Array A) (i : nat),
i < arr_length a ->
exists x : A, array_get_error i a = Some x
  intros.
A:Type
a:Array A
i:nat
H:i < arr_length a
exists x : A, array_get_error i a = Some x

  rewrite <- a.(arr_wf) in H.
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
exists x : A, array_get_error i a = Some x
  assert (~ length (arr_contents a) <= i) by lia.
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
exists x : A, array_get_error i a = Some x

  pose proof (nth_error_None a.(arr_contents) i).
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
H1:nth_error (arr_contents a) i = None <->
length (arr_contents a) <= i
exists x : A, array_get_error i a = Some x
  apply not_iff_compat in H1.
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
H1:nth_error (arr_contents a) i <> None <->
~ length (arr_contents a) <= i
exists x : A, array_get_error i a = Some x
  apply <- H1 in H0.
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:nth_error (arr_contents a) i <> None
H1:nth_error (arr_contents a) i <> None <->
~ length (arr_contents a) <= i
exists x : A, array_get_error i a = Some x

  destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto.
Qed.

Lemma array_get_error_set_bound {A : Type} :
  forall (a : Array A) i x,
    i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
array_get_error i (array_set i x a) = Some x
Proof.
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
array_get_error i (array_set i x a) = Some x
  intros.
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
array_get_error i (array_set i x a) = Some x

  unfold array_get_error.
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
nth_error (arr_contents (array_set i x a)) i = Some x
  eauto with array.
Qed.

Lemma array_gso {A : Type} :
  forall (a : Array A) i1 i2 x,
    i1 <> i2 ->
    array_get_error i2 (array_set i1 x a) = array_get_error i2 a.
A:Type
forall (a : Array A) (i1 i2 : nat) (x : A),
i1 <> i2 ->
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a
Proof.
A:Type
forall (a : Array A) (i1 i2 : nat) (x : A),
i1 <> i2 ->
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a
  intros.
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a

  unfold array_get_error.
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error (arr_contents (array_set i1 x a)) i2 =
nth_error (arr_contents a) i2
  unfold array_set.
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error
  (arr_contents
     {|
     arr_contents := list_set i1 x (arr_contents a);
     arr_length := arr_length a;
     arr_wf := array_set_wf (arr_contents a) i1 x
                 (arr_wf a) |}) i2 =
nth_error (arr_contents a) i2
  crush.
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error (list_set i1 x (arr_contents a)) i2 =
nth_error (arr_contents a) i2
  eauto with array.
Qed.

Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
  nth i a.(arr_contents) x.

Lemma array_get_set_bound {A : Type} :
  forall (a : Array A) i x d,
    i < a.(arr_length) -> array_get i d (array_set i x a) = x.
A:Type
forall (a : Array A) (i : nat) (x d : A),
i < arr_length a ->
array_get i d (array_set i x a) = x
Proof.
A:Type
forall (a : Array A) (i : nat) (x d : A),
i < arr_length a ->
array_get i d (array_set i x a) = x
  intros.
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
array_get i d (array_set i x a) = x

  unfold array_get.
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
nth i (arr_contents (array_set i x a)) d = x
  eauto with array.
Qed.

Lemma array_get_get_error {A : Type} :
  forall (a : Array A) i x d,
    array_get_error i a = Some x ->
    array_get i d a = x.
A:Type
forall (a : Array A) (i : nat) (x d : A),
array_get_error i a = Some x -> array_get i d a = x
Proof.
A:Type
forall (a : Array A) (i : nat) (x d : A),
array_get_error i a = Some x -> array_get i d a = x
  intros.
A:Type
a:Array A
i:nat
x, d:A
H:array_get_error i a = Some x
array_get i d a = x
  unfold array_get.
A:Type
a:Array A
i:nat
x, d:A
H:array_get_error i a = Some x
nth i (arr_contents a) d = x
  unfold array_get_error in H.
A:Type
a:Array A
i:nat
x, d:A
H:nth_error (arr_contents a) i = Some x
nth i (arr_contents a) d = x
  auto using nth_error_nth.
Qed.

(** Tail recursive version of standard library function. *)
Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
  match n with
  | O => acc
  | S n => list_repeat' (a::acc) a n
  end.

Lemma list_repeat'_len {A : Type} : forall (a : A) n l,
    length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
A:Type
forall (a : A) (n : nat) (l : list A),
length (list_repeat' l a n) = n + length l
Proof.
A:Type
forall (a : A) (n : nat) (l : list A),
length (list_repeat' l a n) = n + length l
  induction n; intros; crush; try reflexivity.
A:Type
a:A
n:nat
IHn:forall l : list A, length (list_repeat' l a n) = n + length l
l:list A
length (list_repeat' (a :: l) a n) = S (n + length l)

  specialize (IHn (a :: l)).
A:Type
a:A
n:nat
l:list A
IHn:length (list_repeat' (a :: l) a n) = n + length (a :: l)
length (list_repeat' (a :: l) a n) = S (n + length l)
  rewrite IHn.
A:Type
a:A
n:nat
l:list A
IHn:length (list_repeat' (a :: l) a n) = n + length (a :: l)
n + length (a :: l) = S (n + length l)
  crush.
Qed.

Lemma list_repeat'_app {A : Type} : forall (a : A) n l,
    list_repeat' l a n = list_repeat' [] a n ++ l.
A:Type
forall (a : A) (n : nat) (l : list A),
list_repeat' l a n = list_repeat' [] a n ++ l
Proof.
A:Type
forall (a : A) (n : nat) (l : list A),
list_repeat' l a n = list_repeat' [] a n ++ l
  induction n; intros; crush; try reflexivity.
A:Type
a:A
n:nat
IHn:forall l : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l

  pose proof IHn.
A:Type
a:A
n:nat
IHn:forall l : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:forall l : list A,
list_repeat' l a n = list_repeat' [] a n ++ l
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l
  specialize (H (a :: l)).
A:Type
a:A
n:nat
IHn:forall l : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:list_repeat' (a :: l) a n =
list_repeat' [] a n ++ a :: l
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l
  rewrite H.
A:Type
a:A
n:nat
IHn:forall l : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:list_repeat' (a :: l) a n =
list_repeat' [] a n ++ a :: l
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l clear H.
A:Type
a:A
n:nat
IHn:forall l : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l
  specialize (IHn (a :: nil)).
A:Type
a:A
n:nat
IHn:list_repeat' [a] a n = list_repeat' [] a n ++ [a]
l:list A
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l
  rewrite IHn.
A:Type
a:A
n:nat
IHn:list_repeat' [a] a n = list_repeat' [] a n ++ [a]
l:list A
list_repeat' [] a n ++ a :: l =
(list_repeat' [] a n ++ [a]) ++ l clear IHn.
A:Type
a:A
n:nat
l:list A
list_repeat' [] a n ++ a :: l =
(list_repeat' [] a n ++ [a]) ++ l
  remember (list_repeat' [] a n) as l0.
A:Type
a:A
n:nat
l, l0:list A
Heql0:l0 = list_repeat' [] a n
l0 ++ a :: l = (l0 ++ [a]) ++ l

  rewrite <- app_assoc.
A:Type
a:A
n:nat
l, l0:list A
Heql0:l0 = list_repeat' [] a n
l0 ++ a :: l = l0 ++ [a] ++ l
  f_equal.
Qed.

Lemma list_repeat'_head_tail {A : Type} : forall n (a : A),
  a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
Proof.
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
  induction n; intros; crush; try reflexivity.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
a :: list_repeat' [a] a n =
list_repeat' [a] a n ++ [a]
  rewrite list_repeat'_app.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
a :: list_repeat' [] a n ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]

  replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]).
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
a :: list_repeat' [] a n ++ [a]
  2: {
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
a :: list_repeat' [] a n ++ [a] rewrite app_comm_cons.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(a :: list_repeat' [] a n) ++ [a] rewrite IHn; auto.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
       rewrite app_assoc.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
(list_repeat' [] a n ++ [a]) ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a] reflexivity. }
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
  rewrite app_assoc.
A:Type
n:nat
IHn:forall a : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
(list_repeat' [] a n ++ [a]) ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a] reflexivity.
Qed.

Lemma list_repeat'_cons {A : Type} : forall (a : A) n,
    list_repeat' [a] a n = a :: list_repeat' [] a n.
A:Type
forall (a : A) (n : nat),
list_repeat' [a] a n = a :: list_repeat' [] a n
Proof.
A:Type
forall (a : A) (n : nat),
list_repeat' [a] a n = a :: list_repeat' [] a n
  intros.
A:Type
a:A
n:nat
list_repeat' [a] a n = a :: list_repeat' [] a n

  rewrite list_repeat'_head_tail; auto.
A:Type
a:A
n:nat
list_repeat' [a] a n = list_repeat' [] a n ++ [a]
  apply list_repeat'_app.
Qed.

Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.

Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n.
A:Type
forall (n : nat) (a : A), length (list_repeat a n) = n
Proof.
A:Type
forall (n : nat) (a : A), length (list_repeat a n) = n
  intros.
A:Type
n:nat
a:A
length (list_repeat a n) = n
  unfold list_repeat.
A:Type
n:nat
a:A
length (list_repeat' [] a n) = n
  rewrite list_repeat'_len.
A:Type
n:nat
a:A
n + length [] = n
  crush.
Qed.

Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a',
    (forall x x' : A, {x' = x} + {~ x' = x}) ->
    In a' (list_repeat a n) -> a' = a.
A:Type
forall (n : nat) (a a' : A),
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat a n) -> a' = a
Proof.
A:Type
forall (n : nat) (a a' : A),
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat a n) -> a' = a
  induction n; intros; crush.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) -> In a' (list_repeat a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat a (S n))
a' = a

  unfold list_repeat in *.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a (S n))
a' = a
  crush.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [a] a n)
a' = a

  rewrite list_repeat'_app in H.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
a' = a
  pose proof (X a a').
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
H0:{a' = a} + {a' <> a}
a' = a
  destruct H0; auto.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
n0:a' <> a
a' = a

  (* This is actually a degenerate case, not an unprovable goal. *)
  pose proof (in_app_or (list_repeat' [] a n) ([a])).
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
a' = a
  apply H0 in H.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n) \/ In a' [a]
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
a' = a invert H.
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' (list_repeat' [] a n)
a' = a
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' [a]
a' = a

  -
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' (list_repeat' [] a n)
a' = a eapply IHn in X; eassumption.
  -
A:Type
n:nat
IHn:forall a a' : A,
(forall x x' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forall x x' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:forall a0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' [a]
a' = a invert H1; contradiction.
Qed.

Lemma list_repeat_head_tail {A : Type} : forall n (a : A),
    a :: list_repeat a n = list_repeat a n ++ [a].
A:Type
forall (n : nat) (a : A),
a :: list_repeat a n = list_repeat a n ++ [a]
Proof.
A:Type
forall (n : nat) (a : A),
a :: list_repeat a n = list_repeat a n ++ [a]
  unfold list_repeat.
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a] apply list_repeat'_head_tail.
Qed.

Lemma list_repeat_cons {A : Type} : forall n (a : A),
    list_repeat a (S n) = a :: list_repeat a n.
A:Type
forall (n : nat) (a : A),
list_repeat a (S n) = a :: list_repeat a n
Proof.
A:Type
forall (n : nat) (a : A),
list_repeat a (S n) = a :: list_repeat a n
  intros.
A:Type
n:nat
a:A
list_repeat a (S n) = a :: list_repeat a n

  unfold list_repeat.
A:Type
n:nat
a:A
list_repeat' [] a (S n) = a :: list_repeat' [] a n
  apply list_repeat'_cons.
Qed.

Lemma list_repeat_lookup {A : Type} :
  forall n i (a : A),
    i < n ->
    nth_error (list_repeat a n) i = Some a.
A:Type
forall (n i : nat) (a : A),
i < n -> nth_error (list_repeat a n) i = Some a
Proof.
A:Type
forall (n i : nat) (a : A),
i < n -> nth_error (list_repeat a n) i = Some a
  induction n; intros.
A:Type
i:nat
a:A
H:i < 0
nth_error (list_repeat a 0) i = Some a
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (list_repeat a (S n)) i = Some a

  destruct i; crush.
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (list_repeat a (S n)) i = Some a

  rewrite list_repeat_cons.
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (a :: list_repeat a n) i = Some a
  destruct i; crush; firstorder.
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:S i < S n
nth_error (list_repeat a n) i = Some a intuition.
Qed.

Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).

Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n.
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n
Proof.
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n
  unfold list_repeat.
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n crush.
A:Type
n:nat
a:A
length (list_repeat a n) = n apply list_repeat_len.
Qed.

Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
  match x, y with
  | a :: t, b :: t' => f a b :: list_combine f t t'
  | _, _ => nil
  end.

Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B),
    length (list_combine f x y) = min (length x) (length y).
A, B, C:Type
f:A -> B -> C
forall (x : list A) (y : list B),
length (list_combine f x y) =
Init.Nat.min (length x) (length y)
Proof.
A, B, C:Type
f:A -> B -> C
forall (x : list A) (y : list B),
length (list_combine f x y) =
Init.Nat.min (length x) (length y)
  induction x; intros; crush.
A, B, C:Type
f:A -> B -> C
a:A
x:list A
IHx:forall y : list B,
length (list_combine f x y) = Init.Nat.min (length x) (length y)
y:list B
length
  match y with
  | [] => []
  | b :: t' => f a b :: list_combine f x t'
  end =
match length y with
| 0 => 0
| S m' => S (Init.Nat.min (length x) m')
end

  destruct y; crush; auto.
Qed.

Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
  make_array (list_combine f x.(arr_contents) y.(arr_contents)).

Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C),
    x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).
A, B, C:Type
forall (x : Array A) (y : Array B) (f : A -> B -> C),
arr_length x = arr_length y ->
arr_length (combine f x y) = arr_length x
Proof.
A, B, C:Type
forall (x : Array A) (y : Array B) (f : A -> B -> C),
arr_length x = arr_length y ->
arr_length (combine f x y) = arr_length x
  intros.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length (combine f x y) = arr_length x

  unfold combine.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length
  (make_array
     (list_combine f (arr_contents x) (arr_contents y))) =
arr_length x
  unfold make_array.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length
  {|
  arr_contents := list_combine f (arr_contents x)
                    (arr_contents y);
  arr_length := length
                  (list_combine f (arr_contents x)
                     (arr_contents y));
  arr_wf := eq_refl |} = arr_length x
  crush.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
length
  (list_combine f (arr_contents x) (arr_contents y)) =
arr_length x

  rewrite <- (arr_wf x) in *.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:length (arr_contents x) = arr_length y
length
  (list_combine f (arr_contents x) (arr_contents y)) =
length (arr_contents x)
  rewrite <- (arr_wf y) in *.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:length (arr_contents x) = length (arr_contents y)
length
  (list_combine f (arr_contents x) (arr_contents y)) =
length (arr_contents x)

  destruct (arr_contents x); destruct (arr_contents y); crush.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
a:A
l:list A
b:B
l0:list B
H:S (length l) = S (length l0)
length (list_combine f l l0) = length l
  rewrite list_combine_length.
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
a:A
l:list A
b:B
l0:list B
H:S (length l) = S (length l0)
Init.Nat.min (length l) (length l0) = length l
  destruct (Min.min_dec (length l) (length l0)); congruence.
Qed.

Ltac array :=
  try match goal with
      | [ |- context[arr_length (combine _ _ _)] ] =>
        rewrite combine_length
      | [ |- context[length (list_repeat _ _)] ] =>
        rewrite list_repeat_len
      | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] =>
        unfold array_get_error, arr_repeat
      | |- context[nth_error (list_repeat ?x _) _ = Some ?x] =>
        apply list_repeat_lookup
      end.