Library Coq.setoid_ring.Ring
Require
Import
Bool
.
Require
Export
Ring_theory
.
Require
Export
Ring_base
.
Require
Export
InitialRing
.
Require
Export
Ring_tac
.
Lemma
BoolTheory
:
ring_theory
false
true
xorb
andb
xorb
(
fun
b
:
bool
=>
b
) (
eq
(
A
:=
bool
)).
Definition
bool_eq
(
b1
b2
:
bool
) :=
if
b1
then
b2
else
negb
b2
.
Lemma
bool_eq_ok
:
forall
b1
b2
,
bool_eq
b1
b2
=
true
->
b1
=
b2
.
Ltac
bool_cst
t
:=
let
t
:=
eval
hnf
in
t
in
match
t
with
true
=>
constr
:(
true
)
|
false
=>
constr
:(
false
)
|
_
=>
constr
:(
NotConstant
)
end
.
Add
Ring
bool_ring
:
BoolTheory
(
decidable
bool_eq_ok
,
constants
[
bool_cst
]).