forked from math-comp/hierarchy-builder
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhierarchy_1.v
96 lines (76 loc) · 2.3 KB
/
hierarchy_1.v
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
From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.
(**************************************************************************)
(* Stage 1: +AddComoid+ -> Ring *)
(**************************************************************************)
(* Begin change *)
HB.mixin Record AddComoid_of_TYPE A := {
zero : A;
add : A -> A -> A;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
HB.mixin Record Ring_of_AddComoid A of AddComoid A := {
opp : A -> A;
one : A;
mul : A -> A -> A;
addNr : left_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.factory Record Ring_of_TYPE A := {
zero : A;
one : A;
add : A -> A -> A;
opp : A -> A;
mul : A -> A -> A;
addrA : associative add;
addrC : commutative add;
add0r : left_id zero add;
addNr : left_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;
}.
#[verbose]
HB.builders Context A (a : Ring_of_TYPE A).
HB.instance
Definition to_AddComoid_of_TYPE :=
AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
HB.instance
Definition to_Ring_of_AddComoid :=
Ring_of_AddComoid.Build A _ _ _ addNr mulrA mul1r
mulr1 mulrDl mulrDr.
HB.end.
(* End change *)
HB.structure Definition Ring := { A of Ring_of_TYPE A }.
(* Notations *)
Declare Scope hb_scope.
Delimit Scope hb_scope with G.
Local Open Scope hb_scope.
Notation "0" := zero : hb_scope.
Notation "1" := one : hb_scope.
Infix "+" := (@add _) : hb_scope.
Notation "- x" := (@opp _ x) : hb_scope.
Infix "*" := (@mul _) : hb_scope.
Notation "x - y" := (x + - y) : hb_scope.
(* Theory *)
Section Theory.
Variable R : Ring.type.
Implicit Type (x : R).
Lemma addr0 : right_id (@zero R) add.
Proof. by move=> x; rewrite addrC add0r. Qed.
Lemma addrN : right_inverse (@zero R) opp add.
Proof. by move=> x; rewrite addrC addNr. Qed.
Lemma subrr x : x - x = 0.
Proof. by rewrite addrN. Qed.
Lemma addrNK x y : x + y - y = x.
Proof. by rewrite -addrA subrr addr0. Qed.
End Theory.