Checks that abstract setoid rings can be defined in a module and the tactic

can be used outside the module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9071 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v
new file mode 100644
index 000000000..661f17878
--- /dev/null
+++ b/test-suite/success/setoid_ring_module.v
@@ -0,0 +1,44 @@
+Require Import Setoid ZRing_th Ring_th.
+
+Module abs_ring.
+
+Parameters (Coef:Set)(c0 c1 : Coef)
+(cadd cmul csub: Coef -> Coef -> Coef)
+(copp : Coef -> Coef)
+(ceq : Coef -> Coef -> Prop)
+(ceq_sym : forall x y, ceq x y -> ceq y x)
+(ceq_trans : forall x y z, ceq x y -> ceq y z -> ceq x z)
+(ceq_refl : forall x, ceq x x).
+
+
+Add Relation Coef ceq 
+  reflexivity proved by ceq_refl symmetry proved by ceq_sym
+  transitivity proved by ceq_trans
+  as ceq_relation.
+  
+Add Morphism cadd with signature ceq ==> ceq ==> ceq as cadd_Morphism.
+Admitted.
+
+Add Morphism cmul with signature ceq ==> ceq ==> ceq as cmul_Morphism.
+Admitted.
+
+Add Morphism copp with signature ceq ==> ceq as copp_Morphism.
+Admitted.
+
+Definition cRth : ring_theory c0 c1 cadd cmul csub copp ceq.
+Admitted.
+
+Add New Ring CoefRing : cRth Abstract. 
+
+(* Here the tactic that I would like to be implemented by 
+   "setoid ring" when it is applied on a "ceq _ _" goal.
+   This tactic was designed by copying what happens in newring.ml4 *)
+
+End abs_ring.
+Import abs_ring.
+
+Theorem check_setoid_ring_modules :
+  forall a b, ceq (cadd a b) (cadd b a).
+intros.
+setoid ring.
+Qed.