aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring/Ring.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring/Ring.v')
-rw-r--r--plugins/setoid_ring/Ring.v44
1 files changed, 44 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
new file mode 100644
index 000000000..d01b16258
--- /dev/null
+++ b/plugins/setoid_ring/Ring.v
@@ -0,0 +1,44 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+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)).
+split; simpl in |- *.
+destruct x; reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; destruct z; reflexivity.
+reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; reflexivity.
+destruct x; destruct y; destruct z; reflexivity.
+reflexivity.
+destruct x; reflexivity.
+Qed.
+
+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.
+destruct b1; destruct b2; auto.
+Qed.
+
+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]).