Library Coq.Vectors.VectorEq
Equalities and Vector relations
Author: Pierre Boutillier Institution: PPS, INRIA 07/2012
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
.