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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
(* Accompanying material to https://hal.inria.fr/hal-02478907 *)
From Coq Require Import ssreflect ssrfun ZArith.
From HB Require Import structures.
Declare Scope hb_scope.
Delimit Scope hb_scope with G.
Open Scope hb_scope.
(* Bottom mixin in Fig. 1. *)
HB.mixin Record Monoid_of_Type M := {
zero : M;
add : M -> M -> M;
addrA : associative add;
add0r : left_id zero add;
addr0 : right_id zero add;
}.
HB.structure Definition Monoid := { M of Monoid_of_Type M }.
Notation "0" := zero : hb_scope.
Infix "+" := (@add _) : hb_scope.
(* Bottom right mixin in Fig. 1. *)
HB.mixin Record AbelianGroup_of_Monoid A of Monoid A := {
opp : A -> A;
addrC : commutative (add : A -> A -> A);
addNr : left_inverse zero opp add;
}.
HB.structure Definition AbelianGroup :=
{ A of Monoid A & AbelianGroup_of_Monoid A }.
Notation "- x" := (@opp _ x) : hb_scope.
Notation "x - y" := (x + - y) : hb_scope.
(* Top right mixin in Fig. 1. *)
HB.mixin Record Ring_of_AbelianGroup R of AbelianGroup R := {
one : R;
mul : R -> R -> R;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.structure Definition Ring :=
{ R of AbelianGroup R & Ring_of_AbelianGroup R }.
Notation "1" := one : hb_scope.
Infix "*" := (@mul _) : hb_scope.
Lemma addrN {R : AbelianGroup.type} : right_inverse (zero : R) opp add.
Proof. by move=> x; rewrite addrC addNr. Qed.
(* Left factory in Fig. 1. *)
HB.factory Record Ring_of_Monoid R of Monoid R := {
one : R;
opp : R -> R;
mul : R -> R -> R;
addNr : left_inverse zero opp add;
addrN : right_inverse zero opp add;
mulrA : associative mul;
mul1r : left_id one mul;
mulr1 : right_id one mul;
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.builders Context (R : Type) (f : Ring_of_Monoid R).
Lemma addrC : commutative (add : R -> R -> R).
Proof.
have innerC (a b : R) : a + b + (a + b) = a + a + (b + b).
by rewrite -[a+b]mul1r -mulrDl mulrDr !mulrDl !mul1r.
have addKl (a b c : R) : a + b = a + c -> b = c.
apply: can_inj (add a) (add (opp a)) _ _ _.
by move=> x; rewrite addrA addNr add0r.
have addKr (a b c : R) : b + a = c + a -> b = c.
apply: can_inj (add ^~ a) (add ^~ (opp a)) _ _ _.
by move=> x; rewrite /= -addrA addrN addr0.
move=> x y; apply: addKl (x) _ _ _; apply: addKr (y) _ _ _.
by rewrite -!addrA [in RHS]addrA innerC !addrA.
Qed.
(* Builder to the bottom right mixin. *)
HB.instance
Definition to_AbelianGroup_of_Monoid :=
AbelianGroup_of_Monoid.Build R opp addrC addNr.
(* Builder to the top right mixin. *)
HB.instance
Definition to_Ring_of_AbelianGroup := Ring_of_AbelianGroup.Build R one mul
mulrA mul1r mulr1 mulrDl mulrDr.
HB.end.
(********)
(* TEST *)
(********)
Print Monoid.type.
(* Monoid.type := { sort : Type; ... } *)
Check @add.
(* add : forall M : Monoid.type, M -> M -> M *)
Check @addNr.
(* addNr : forall R : AbelianGroup.type, left_inverse 0 opp add *)
Check @addrC. (* is still an axiom of abelian groups *)
(* addrC : forall R : AbelianGroup.type, commutative add *)
HB.instance
Definition Z_Monoid_axioms : Monoid_of_Type Z :=
Monoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_0_l Z.add_0_r.
HB.instance
Definition Z_Ring_axioms : Ring_of_Monoid Z :=
Ring_of_Monoid.Build Z 1%Z Z.opp Z.mul
Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_assoc Z.mul_1_l Z.mul_1_r
Z.mul_add_distr_r Z.mul_add_distr_l.
Lemma exercise (m n : Z) : (n + m) - n * 1 = m.
Proof. by rewrite mulr1 (addrC n) -(addrA m) addrN addr0. Qed.
|
