Skip to content

Commit 129f0a3

Browse files
garesgares
authored
Merge pull request #62 from math-comp/factory-short-abbrev
Generate an abbreviation `F X` for `F.axioms X` (fix #61)
2 parents 22e86a2 + 52094ba commit 129f0a3

20 files changed

+267
-246
lines changed

‎README.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ HB.mixin Record AddComoid_of_Type A := {
1717
addrC : forall x y, add x y = add y x;
1818
add0r : forall x, add zero x = x;
1919
}.
20-
HB.structure Definition AddComoid := { A of AddComoid_of_Type.axioms A }.
20+
HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
2121
2222
Notation "0" := zero.
2323
Infix "+" := add.
@@ -32,17 +32,17 @@ We proceed by declaring how to obtain an Abelian group out of the
3232
additive, commutative, monoid.
3333

3434
```coq
35-
HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid.axioms A := {
35+
HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := {
3636
opp : A -> A;
3737
addNr : forall x, opp x + x = 0;
3838
}.
39-
HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid.axioms A & }.
39+
HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.
4040
4141
Notation "- x" := (opp x).
4242
```
4343

4444
Abelian groups feature the operations and properties given by the
45-
`AbelianGrp_of_AddComoid.axioms` and `AddComoid_of_Type.axioms` mixins.
45+
`AbelianGrp_of_AddComoid` and `AddComoid_of_Type` mixins.
4646

4747
```coq
4848
Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
@@ -53,9 +53,9 @@ We proceed by showing that `Z` is an example of both structures, and use
5353
the lemma just proved on a statement about `Z`.
5454

5555
```coq
56-
Definition Z_CoMoid := AddComoid_of_Type.Axioms Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
56+
Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
5757
HB.instance Z Z_CoMoid.
58-
Definition Z_AbGrp := AbelianGrp_of_AddComoid.Axioms Z Z.opp Z.add_opp_diag_l.
58+
Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
5959
HB.instance Z Z_AbGrp.
6060
6161
Lemma example2 (x : Z) : x + (- x) = - 0.

‎demo1/hierarchy_0.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ HB.mixin Record Ring_of_TYPE A := {
2323
mulrDl : left_distributive mul add;
2424
mulrDr : right_distributive mul add;
2525
}.
26-
HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
26+
HB.structure Definition Ring := { A of Ring_of_TYPE A }.
2727

2828
(* Notations *)
2929

‎demo1/hierarchy_1.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
1616
addrC : commutative add;
1717
add0r : left_id zero add;
1818
}.
19-
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
19+
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
2020

21-
HB.mixin Record Ring_of_AddComoid A of AddComoid.axioms A := {
21+
HB.mixin Record Ring_of_AddComoid A of AddComoid A := {
2222
opp : A -> A;
2323
one : A;
2424
mul : A -> A -> A;
@@ -47,22 +47,22 @@ HB.factory Record Ring_of_TYPE A := {
4747
mulrDr : right_distributive mul add;
4848
}.
4949

50-
HB.builders Context A (a : Ring_of_TYPE.axioms A).
50+
HB.builders Context A (a : Ring_of_TYPE A).
5151

5252
Definition to_AddComoid_of_TYPE :=
53-
AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
53+
AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
5454
HB.instance A to_AddComoid_of_TYPE.
5555

5656
Definition to_Ring_of_AddComoid :=
57-
Ring_of_AddComoid.Axioms A _ _ _ addNr_a mulrA_a mul1r_a
57+
Ring_of_AddComoid.Build A _ _ _ addNr_a mulrA_a mul1r_a
5858
mulr1_a mulrDl_a mulrDr_a.
5959
HB.instance A to_Ring_of_AddComoid.
6060

6161
HB.end.
6262

6363
(* End change *)
6464

65-
HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
65+
HB.structure Definition Ring := { A of Ring_of_TYPE A }.
6666

6767
(* Notations *)
6868

‎demo1/hierarchy_2.v‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -14,11 +14,11 @@ HB.mixin Record AddComoid_of_TYPE A := {
1414
addrC : commutative add;
1515
add0r : left_id zero add;
1616
}.
17-
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
17+
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
1818

1919
(* Begin change *)
2020

21-
HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
21+
HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
2222
opp : A -> A;
2323
addNr : left_inverse zero opp add;
2424
}.
@@ -32,20 +32,20 @@ HB.factory Record AddAG_of_TYPE A := {
3232
addNr : left_inverse zero opp add;
3333
}.
3434

35-
HB.builders Context A (a : AddAG_of_TYPE.axioms A).
35+
HB.builders Context A (a : AddAG_of_TYPE A).
3636

3737
Definition to_AddComoid_of_TYPE :=
38-
AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
38+
AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
3939
HB.instance A to_AddComoid_of_TYPE.
4040

4141
Definition to_AddAG_of_AddComoid :=
42-
AddAG_of_AddComoid.Axioms A _ addNr_a.
42+
AddAG_of_AddComoid.Build A _ addNr_a.
4343
HB.instance A to_AddAG_of_AddComoid.
4444

4545
HB.end.
46-
HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
46+
HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
4747

48-
HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
48+
HB.mixin Record Ring_of_AddAG A of AddAG A := {
4949
one : A;
5050
mul : A -> A -> A;
5151
mulrA : associative mul;
@@ -54,7 +54,7 @@ HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
5454
mulrDl : left_distributive mul add;
5555
mulrDr : right_distributive mul add;
5656
}.
57-
HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
57+
HB.factory Record Ring_of_AddComoid A of AddComoid A := {
5858
opp : A -> A;
5959
one : A;
6060
mul : A -> A -> A;
@@ -66,12 +66,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
6666
mulrDr : right_distributive mul add;
6767
}.
6868

69-
HB.builders Context A (a : Ring_of_AddComoid.axioms A).
69+
HB.builders Context A (a : Ring_of_AddComoid A).
7070

71-
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
71+
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
7272
HB.instance A to_AddAG_of_AddComoid.
7373

74-
Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
74+
Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
7575
_ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
7676
HB.instance A to_Ring_of_AddAG.
7777

@@ -96,18 +96,18 @@ HB.factory Record Ring_of_TYPE A := {
9696
mulrDr : right_distributive mul add;
9797
}.
9898

99-
HB.builders Context A (a : Ring_of_TYPE.axioms A).
99+
HB.builders Context A (a : Ring_of_TYPE A).
100100

101-
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
101+
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
102102
zero_a add_a addrA_a addrC_a add0r_a.
103103
HB.instance A to_AddComoid_of_TYPE.
104104

105-
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
105+
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
106106
_ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
107107
HB.instance A to_Ring_of_AddComoid.
108108
HB.end.
109109

110-
HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
110+
HB.structure Definition Ring := { A of Ring_of_TYPE A }.
111111

112112
(* Notations *)
113113

‎demo1/hierarchy_3.v‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
1616
addrC : commutative add;
1717
add0r : left_id zero add;
1818
}.
19-
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
19+
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.
2020

21-
HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
21+
HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
2222
opp : A -> A;
2323
addNr : left_inverse zero opp add;
2424
}.
@@ -32,20 +32,20 @@ HB.factory Record AddAG_of_TYPE A := {
3232
addNr : left_inverse zero opp add;
3333
}.
3434

35-
HB.builders Context A (a : AddAG_of_TYPE.axioms A).
35+
HB.builders Context A (a : AddAG_of_TYPE A).
3636

37-
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
37+
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
3838
zero_a add_a addrA_a addrC_a add0r_a.
3939
HB.instance A to_AddComoid_of_TYPE.
4040

41-
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
41+
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
4242
HB.instance A to_AddAG_of_AddComoid.
4343
HB.end.
44-
HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
44+
HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
4545

4646
(* Begin change *)
4747

48-
HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
48+
HB.mixin Record SemiRing_of_AddComoid A of AddComoid A := {
4949
one : A;
5050
mul : A -> A -> A;
5151
mulrA : associative mul;
@@ -56,9 +56,9 @@ HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
5656
mul0r : left_zero zero mul;
5757
mulr0 : right_zero zero mul;
5858
}.
59-
HB.structure Definition SemiRing := { A of AddComoid.axioms A & SemiRing_of_AddComoid.axioms A }.
59+
HB.structure Definition SemiRing := { A of AddComoid A & SemiRing_of_AddComoid A }.
6060

61-
HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
61+
HB.factory Record Ring_of_AddAG A of AddAG A := {
6262
one : A;
6363
mul : A -> A -> A;
6464
mulrA : associative mul;
@@ -68,7 +68,7 @@ HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
6868
mulrDr : right_distributive mul add;
6969
}.
7070

71-
HB.builders Context A (a : Ring_of_AddAG.axioms A).
71+
HB.builders Context A (a : Ring_of_AddAG A).
7272

7373
Fact mul0r : left_zero zero mul_a.
7474
Proof.
@@ -84,15 +84,15 @@ HB.builders Context A (a : Ring_of_AddAG.axioms A).
8484
by rewrite -mulrDr_a add0r addrC addNr.
8585
Qed.
8686

87-
Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Axioms A
87+
Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Build A
8888
_ mul_a mulrA_a mulr1_a mul1r_a
8989
mulrDl_a mulrDr_a mul0r mulr0.
9090
HB.instance A to_SemiRing_of_AddComoid.
9191

9292
HB.end.
9393

9494
(* End change *)
95-
HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
95+
HB.factory Record Ring_of_AddComoid A of AddComoid A := {
9696
opp : A -> A;
9797
one : A;
9898
mul : A -> A -> A;
@@ -104,12 +104,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
104104
mulrDr : right_distributive mul add;
105105
}.
106106

107-
HB.builders Context A (a : Ring_of_AddComoid.axioms A).
107+
HB.builders Context A (a : Ring_of_AddComoid A).
108108

109-
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
109+
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
110110
HB.instance A to_AddAG_of_AddComoid.
111111

112-
Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
112+
Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
113113
_ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
114114
HB.instance A to_Ring_of_AddAG.
115115

@@ -134,18 +134,18 @@ HB.factory Record Ring_of_TYPE A := {
134134
mulrDr : right_distributive mul add;
135135
}.
136136

137-
HB.builders Context A (a : Ring_of_TYPE.axioms A).
137+
HB.builders Context A (a : Ring_of_TYPE A).
138138

139-
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
139+
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
140140
zero_a add_a addrA_a addrC_a add0r_a.
141141
HB.instance A to_AddComoid_of_TYPE.
142142

143-
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
143+
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
144144
_ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
145145
HB.instance A to_Ring_of_AddComoid.
146146
HB.end.
147147

148-
HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
148+
HB.structure Definition Ring := { A of Ring_of_TYPE A }.
149149

150150
(* Notations *)
151151

0 commit comments

Comments
 (0)