blob: 2d9e85b54ee02cde7fa30ec568507908af594ee9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
Require Import Setoid Ring Ring_theory.
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 Ring CoefRing : cRth.
End abs_ring.
Import abs_ring.
Theorem check_setoid_ring_modules :
forall a b, ceq (cadd a b) (cadd b a).
intros.
ring.
Qed.
|
