Library Coq.Vectors.VectorEq

N.B.: Using this encoding of vectors is discouraged. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.

Equalities and Vector relations

Initial Author: Pierre Boutillier Institution: PPS, INRIA 07/2012

#[local] Set Warnings "-stdlib-vector".
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.

Lemma eqb_eq: forall n (v1: t A n) (v2: t A n),
  eqb v1 v2 = true <-> v1 = v2.

Definition eq_dec n (v1 v2: t A n): {v1 = v2 } + {v1 <> v2 }.

End BEQ.

Section CAST.

Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.

End CAST.

Navigation