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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.
HB.mixin Record MulMonoid_of_Type A := {
one : A;
mul : A -> A -> A;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
}.
HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
HB.mixin Record AddMonoid_of_Type A := {
zero : A;
add : A -> A -> A;
addrA : associative add;
add0r : left_id zero add;
addr0 : right_id zero add;
}.
HB.structure Definition AddMonoid := { A of AddMonoid_of_Type A }.
HB.mixin Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
opp : A -> A;
addrC : commutative (add : A -> A -> A);
addNr : left_inverse zero opp add;
mulrDl : left_distributive mul (add : A -> A -> A);
mulrDr : right_distributive mul (add : A -> A -> A);
}.
HB.structure Definition Ring := { A of MulMonoid A & AddMonoid A & Ring_of_AddMulMonoid A }.
HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
zero : A;
add : A -> A -> A;
addrA : associative add;
add0r : left_id zero add;
addr0 : right_id zero add;
opp : A -> A;
addrC : commutative (add : A -> A -> A);
addNr : left_inverse zero opp add;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.builders Context A (a : Ring_of_MulMonoid A).
HB.instance
Definition to_AddMonoid_of_Type :=
AddMonoid_of_Type.Build A zero add addrA add0r addr0.
HB.instance
Definition to_Ring_of_AddMulMonoid :=
Ring_of_AddMulMonoid.Build A opp addrC addNr mulrDl mulrDr.
HB.end.
|
