(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import VectorDef.
Require Import VectorSpec.
Import VectorNotations.

Section BEQ.

 Variables (A: Type) (A_beq: A -> A -> bool).
 Hypothesis A_eqb_eq: forall x y, A_beq x y = true <-> x = y.

 Definition eqb:
   forall {m n} (v1: t A m) (v2: t A n), bool :=
   fix fix_beq {m n} v1 v2 :=
   match v1, v2 with
     |[], [] => true
     |_ :: _, [] |[], _ :: _ => false
     |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2
   end%bool.

 Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n)
  (Hbeq: eqb v1 v2 = true), m = n.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
forall (m n : nat) (v1 : t A m) (v2 : t A n),
eqb v1 v2 = true -> m = n
 Proof.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
forall (m n : nat) (v1 : t A m) (v2 : t A n),
eqb v1 v2 = true -> m = n
   intros m n v1; revert n.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
m:nat
v1:t A m
forall (n : nat) (v2 : t A n),
eqb v1 v2 = true -> m = n
   induction v1; destruct v2;
     [now constructor | discriminate | discriminate | simpl].
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
h:A
n:nat
v1:t A n
IHv1:forall (n1 : nat) (v0 : t A n1),
eqb v1 v0 = true -> n = n1
h0:A
n0:nat
v2:t A n0
(A_beq h h0 && eqb v1 v2)%bool = true -> S n = S n0
   intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
h:A
n:nat
v1:t A n
IHv1:forall (n1 : nat) (v0 : t A n1),
eqb v1 v0 = true -> n = n1
h0:A
n0:nat
v2:t A n0
H:A_beq h h0 = true
H0:eqb v1 v2 = true
S n = S n0
   f_equal; eauto.
 Qed.

 Lemma eqb_eq: forall n (v1: t A n) (v2: t A n),
  eqb v1 v2 = true <-> v1 = v2.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
forall (n : nat) (v1 v2 : t A n),
eqb v1 v2 = true <-> v1 = v2
 Proof.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
forall (n : nat) (v1 v2 : t A n),
eqb v1 v2 = true <-> v1 = v2
   refine (@rect2 _ _ _ _ _); [now constructor | simpl].
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
forall (n : nat) (v1 v2 : t A n),
eqb v1 v2 = true <-> v1 = v2 ->
forall a b : A,
(A_beq a b && eqb v1 v2)%bool = true <->
a :: v1 = b :: v2
   intros ? ? ? Hrec h1 h2; destruct Hrec; destruct (A_eqb_eq h1 h2); split.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
(A_beq h1 h2 && eqb v1 v2)%bool = true ->
h1 :: v1 = h2 :: v2
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
h1 :: v1 = h2 :: v2 ->
(A_beq h1 h2 && eqb v1 v2)%bool = true
   +
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
(A_beq h1 h2 && eqb v1 v2)%bool = true ->
h1 :: v1 = h2 :: v2 intros Hbeq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
Hbeq:(A_beq h1 h2 && eqb v1 v2)%bool = true
h1 :: v1 = h2 :: v2 apply andb_prop in Hbeq; destruct Hbeq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
H3:A_beq h1 h2 = true
H4:eqb v1 v2 = true
h1 :: v1 = h2 :: v2
     f_equal; now auto.
   +
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
h1 :: v1 = h2 :: v2 ->
(A_beq h1 h2 && eqb v1 v2)%bool = true intros Heq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
Heq:h1 :: v1 = h2 :: v2
(A_beq h1 h2 && eqb v1 v2)%bool = true destruct (cons_inj Heq).
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
Heq:h1 :: v1 = h2 :: v2
H3:h1 = h2
H4:v1 = v2
(A_beq h1 h2 && eqb v1 v2)%bool = true apply andb_true_intro.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true -> v1 = v2
H0:v1 = v2 -> eqb v1 v2 = true
h1, h2:A
H1:A_beq h1 h2 = true -> h1 = h2
H2:h1 = h2 -> A_beq h1 h2 = true
Heq:h1 :: v1 = h2 :: v2
H3:h1 = h2
H4:v1 = v2
A_beq h1 h2 = true /\ eqb v1 v2 = true
     split; now auto.
 Qed.

 Definition eq_dec n (v1 v2: t A n): {v1 = v2} + {v1 <> v2}.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
{v1 = v2} + {v1 <> v2}
 Proof.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
{v1 = v2} + {v1 <> v2}
 case_eq (eqb v1 v2); intros.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true
{v1 = v2} + {v1 <> v2}
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = false
{v1 = v2} + {v1 <> v2}
  +
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = true
{v1 = v2} + {v1 <> v2} left; now apply eqb_eq.
  +
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = false
{v1 = v2} + {v1 <> v2} right.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = false
v1 <> v2 intros Heq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = false
Heq:v1 = v2
False apply <- eqb_eq in Heq.
A:Type
A_beq:A -> A -> bool
A_eqb_eq:forall x y : A, A_beq x y = true <-> x = y
n:nat
v1, v2:t A n
H:eqb v1 v2 = false
Heq:eqb v1 v2 = true
False congruence.
 Defined.

End BEQ.

Section CAST.

 Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.
forall (A : Type) (m : nat),
t A m -> forall n : nat, m = n -> t A n
 Proof.
forall (A : Type) (m : nat),
t A m -> forall n : nat, m = n -> t A n
 refine (fix cast {A m} (v: t A m) {struct v} :=
  match v in t _ m' return forall n, m' = n -> t A n with
  |[] => fun n => match n with
    | 0 => fun _ => []
    | S _ => fun H => False_rect _ _
  end
  |h :: w => fun n => match n with
    | 0 => fun H => False_rect _ _
    | S n' => fun H => h :: (cast w n' (f_equal pred H))
  end
 end); discriminate.
 Defined.

End CAST.