Skip to content

Generate an abbreviation F X for F.axioms X (fix #61) #62

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Mar 11, 2020
Merged

Generate an abbreviation F X for F.axioms X (fix #61) #62

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
574dcf5
Generate an abbreviation `F X` for `F.axioms X` (fix #61)
gares Mar 11, 2020
606033a
update all files wrt axioms
gares Mar 11, 2020
39e84df
Use `F.Build` rather than `F.Axioms` for the smart builder of F
gares Mar 11, 2020
77b137b
tentative fix for stage11
gares Mar 11, 2020
52094ba
TAddAG_ -> tAddAG
CohenCyril Mar 11, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ HB.mixin Record AddComoid_of_Type A := {
addrC : forall x y, add x y = add y x;
add0r : forall x, add zero x = x;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_Type.axioms A }.
HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.

Notation "0" := zero.
Infix "+" := add.
Expand All @@ -32,17 +32,17 @@ We proceed by declaring how to obtain an Abelian group out of the
additive, commutative, monoid.

```coq
HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid.axioms A := {
HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := {
opp : A -> A;
addNr : forall x, opp x + x = 0;
}.
HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid.axioms A & }.
HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.

Notation "- x" := (opp x).
```

Abelian groups feature the operations and properties given by the
`AbelianGrp_of_AddComoid.axioms` and `AddComoid_of_Type.axioms` mixins.
`AbelianGrp_of_AddComoid` and `AddComoid_of_Type` mixins.

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

```coq
Definition Z_CoMoid := AddComoid_of_Type.Axioms Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
Definition Z_CoMoid := AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
HB.instance Z Z_CoMoid.
Definition Z_AbGrp := AbelianGrp_of_AddComoid.Axioms Z Z.opp Z.add_opp_diag_l.
Definition Z_AbGrp := AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
HB.instance Z Z_AbGrp.

Lemma example2 (x : Z) : x + (- x) = - 0.
Expand Down
2 changes: 1 addition & 1 deletion demo1/hierarchy_0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ HB.mixin Record Ring_of_TYPE A := {
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
HB.structure Definition Ring := { A of Ring_of_TYPE A }.

(* Notations *)

Expand Down
12 changes: 6 additions & 6 deletions demo1/hierarchy_1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
addrC : commutative add;
add0r : left_id zero add;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.

HB.mixin Record Ring_of_AddComoid A of AddComoid.axioms A := {
HB.mixin Record Ring_of_AddComoid A of AddComoid A := {
opp : A -> A;
one : A;
mul : A -> A -> A;
Expand Down Expand Up @@ -47,22 +47,22 @@ HB.factory Record Ring_of_TYPE A := {
mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_TYPE.axioms A).
HB.builders Context A (a : Ring_of_TYPE A).

Definition to_AddComoid_of_TYPE :=
AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
HB.instance A to_AddComoid_of_TYPE.

Definition to_Ring_of_AddComoid :=
Ring_of_AddComoid.Axioms A _ _ _ addNr_a mulrA_a mul1r_a
Ring_of_AddComoid.Build A _ _ _ addNr_a mulrA_a mul1r_a
mulr1_a mulrDl_a mulrDr_a.
HB.instance A to_Ring_of_AddComoid.

HB.end.

(* End change *)

HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
HB.structure Definition Ring := { A of Ring_of_TYPE A }.

(* Notations *)

Expand Down
30 changes: 15 additions & 15 deletions demo1/hierarchy_2.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,11 @@ HB.mixin Record AddComoid_of_TYPE A := {
addrC : commutative add;
add0r : left_id zero add;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.

(* Begin change *)

HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
opp : A -> A;
addNr : left_inverse zero opp add;
}.
Expand All @@ -32,20 +32,20 @@ HB.factory Record AddAG_of_TYPE A := {
addNr : left_inverse zero opp add;
}.

HB.builders Context A (a : AddAG_of_TYPE.axioms A).
HB.builders Context A (a : AddAG_of_TYPE A).

Definition to_AddComoid_of_TYPE :=
AddComoid_of_TYPE.Axioms A zero_a add_a addrA_a addrC_a add0r_a.
AddComoid_of_TYPE.Build A zero_a add_a addrA_a addrC_a add0r_a.
HB.instance A to_AddComoid_of_TYPE.

Definition to_AddAG_of_AddComoid :=
AddAG_of_AddComoid.Axioms A _ addNr_a.
AddAG_of_AddComoid.Build A _ addNr_a.
HB.instance A to_AddAG_of_AddComoid.

HB.end.
HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.

HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
HB.mixin Record Ring_of_AddAG A of AddAG A := {
one : A;
mul : A -> A -> A;
mulrA : associative mul;
Expand All @@ -54,7 +54,7 @@ HB.mixin Record Ring_of_AddAG A of AddAG.axioms A := {
mulrDl : left_distributive mul add;
mulrDr : right_distributive mul add;
}.
HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
HB.factory Record Ring_of_AddComoid A of AddComoid A := {
opp : A -> A;
one : A;
mul : A -> A -> A;
Expand All @@ -66,12 +66,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_AddComoid.axioms A).
HB.builders Context A (a : Ring_of_AddComoid A).

Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
HB.instance A to_AddAG_of_AddComoid.

Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
_ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
HB.instance A to_Ring_of_AddAG.

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

HB.builders Context A (a : Ring_of_TYPE.axioms A).
HB.builders Context A (a : Ring_of_TYPE A).

Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
zero_a add_a addrA_a addrC_a add0r_a.
HB.instance A to_AddComoid_of_TYPE.

Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
_ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
HB.instance A to_Ring_of_AddComoid.
HB.end.

HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
HB.structure Definition Ring := { A of Ring_of_TYPE A }.

(* Notations *)

Expand Down
38 changes: 19 additions & 19 deletions demo1/hierarchy_3.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ HB.mixin Record AddComoid_of_TYPE A := {
addrC : commutative add;
add0r : left_id zero add;
}.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE.axioms A }.
HB.structure Definition AddComoid := { A of AddComoid_of_TYPE A }.

HB.mixin Record AddAG_of_AddComoid A of AddComoid.axioms A := {
HB.mixin Record AddAG_of_AddComoid A of AddComoid A := {
opp : A -> A;
addNr : left_inverse zero opp add;
}.
Expand All @@ -32,20 +32,20 @@ HB.factory Record AddAG_of_TYPE A := {
addNr : left_inverse zero opp add;
}.

HB.builders Context A (a : AddAG_of_TYPE.axioms A).
HB.builders Context A (a : AddAG_of_TYPE A).

Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
zero_a add_a addrA_a addrC_a add0r_a.
HB.instance A to_AddComoid_of_TYPE.

Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
HB.instance A to_AddAG_of_AddComoid.
HB.end.
HB.structure Definition AddAG := { A of AddAG_of_TYPE.axioms A }.
HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.

(* Begin change *)

HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
HB.mixin Record SemiRing_of_AddComoid A of AddComoid A := {
one : A;
mul : A -> A -> A;
mulrA : associative mul;
Expand All @@ -56,9 +56,9 @@ HB.mixin Record SemiRing_of_AddComoid A of AddComoid.axioms A := {
mul0r : left_zero zero mul;
mulr0 : right_zero zero mul;
}.
HB.structure Definition SemiRing := { A of AddComoid.axioms A & SemiRing_of_AddComoid.axioms A }.
HB.structure Definition SemiRing := { A of AddComoid A & SemiRing_of_AddComoid A }.

HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
HB.factory Record Ring_of_AddAG A of AddAG A := {
one : A;
mul : A -> A -> A;
mulrA : associative mul;
Expand All @@ -68,7 +68,7 @@ HB.factory Record Ring_of_AddAG A of AddAG.axioms A := {
mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_AddAG.axioms A).
HB.builders Context A (a : Ring_of_AddAG A).

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

Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Axioms A
Definition to_SemiRing_of_AddComoid := SemiRing_of_AddComoid.Build A
_ mul_a mulrA_a mulr1_a mul1r_a
mulrDl_a mulrDr_a mul0r mulr0.
HB.instance A to_SemiRing_of_AddComoid.

HB.end.

(* End change *)
HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
HB.factory Record Ring_of_AddComoid A of AddComoid A := {
opp : A -> A;
one : A;
mul : A -> A -> A;
Expand All @@ -104,12 +104,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid.axioms A := {
mulrDr : right_distributive mul add;
}.

HB.builders Context A (a : Ring_of_AddComoid.axioms A).
HB.builders Context A (a : Ring_of_AddComoid A).

Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Axioms A _ addNr_a.
Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr_a.
HB.instance A to_AddAG_of_AddComoid.

Definition to_Ring_of_AddAG := Ring_of_AddAG.Axioms A
Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
_ _ mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
HB.instance A to_Ring_of_AddAG.

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

HB.builders Context A (a : Ring_of_TYPE.axioms A).
HB.builders Context A (a : Ring_of_TYPE A).

Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Axioms A
Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
zero_a add_a addrA_a addrC_a add0r_a.
HB.instance A to_AddComoid_of_TYPE.

Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Axioms A
Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
_ _ _ addNr_a mulrA_a mul1r_a mulr1_a mulrDl_a mulrDr_a.
HB.instance A to_Ring_of_AddComoid.
HB.end.

HB.structure Definition Ring := { A of Ring_of_TYPE.axioms A }.
HB.structure Definition Ring := { A of Ring_of_TYPE A }.

(* Notations *)

Expand Down
Loading