Library Coq.Bool.BoolEq
Properties of a boolean equality
Require
Export
Bool
.
Section
Bool_eq_dec
.
Variable
A
:
Set
.
Variable
beq
:
A
->
A
->
bool
.
Variable
beq_refl
:
forall
x
:
A
,
true
=
beq
x
x
.
Variable
beq_eq
:
forall
x
y
:
A
,
true
=
beq
x
y
->
x
=
y
.
Definition
beq_eq_true
:
forall
x
y
:
A
,
x
=
y
->
true
=
beq
x
y
.
Definition
beq_eq_not_false
:
forall
x
y
:
A
,
x
=
y
->
false
<>
beq
x
y
.
Definition
beq_false_not_eq
:
forall
x
y
:
A
,
false
=
beq
x
y
->
x
<>
y
.
Definition
exists_beq_eq
:
forall
x
y
:
A
,
{
b
:
bool
|
b
=
beq
x
y
}
.
Definition
not_eq_false_beq
:
forall
x
y
:
A
,
x
<>
y
->
false
=
beq
x
y
.
Definition
eq_dec
:
forall
x
y
:
A
,
{
x
=
y
}
+
{
x
<>
y
}
.
End
Bool_eq_dec
.