diff options
| -rw-r--r-- | test-suite/success/setoid_ring_module.v | 44 |
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 0000000000..661f17878e --- /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. |