Skip to content

Commit 491a23b

Browse files
ptorrxptorrx
committed
added monoid_enriched_cat.v as the original pull request by Cyril, inconclusively modified enriched_cat.v (the version I'm working on)
1 parent 684fc88 commit 491a23b

File tree

2 files changed

+145
-10
lines changed

2 files changed

+145
-10
lines changed

‎tests/enriched_cat.v

Lines changed: 84 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@
33
From HB Require Import structures.
44
From Coq Require Import ssreflect ssrfun.
55

6-
HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }.
6+
HB.mixin Record isQuiver (Obj: Type) : Type := { hom : Obj -> Obj -> Type }.
77

8-
HB.structure Definition Quiver := { Obj of isQuiver Obj }.
8+
HB.structure Definition Quiver : Type := { Obj of isQuiver Obj }.
99

10-
HB.mixin Record isMon A := {
10+
HB.mixin Record isMon (A: Type) : Type := {
1111
zero : A;
1212
add : A -> A -> A;
1313
addrA : associative add;
@@ -16,20 +16,94 @@ HB.mixin Record isMon A := {
1616
}.
1717

1818
HB.structure
19-
Definition Monoid := { A of isMon A }.
19+
Definition Monoid : Type := { A of isMon A }.
2020

21-
(**)
22-
HB.mixin Record hom_isMonT T of Quiver T :=
21+
HB.mixin Record hom_isMon T of Quiver T :=
2322
{ private : forall A B, isMon (@hom T A B) }.
2423

2524
HB.structure
26-
Definition Monoid_enriched_quiverT :=
27-
{ Obj of isQuiver Obj & hom_isMonT Obj }.
25+
Definition Monoid_enriched_quiver :=
26+
{ Obj of isQuiver Obj & hom_isMon Obj }.
27+
28+
(* unique projection from the axiom of Monoid_enriched_quiver *)
29+
HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) :=
30+
@private T A B.
31+
32+
HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B).
33+
34+
35+
(*********)
36+
37+
HB.mixin Record hom_isMonX T of Quiver T : Type :=
38+
{ private : forall A B, isMon (@hom T A B) }.
39+
40+
HB.structure
41+
Definition Monoid_enriched_quiverX :=
42+
{ Obj of isQuiver Obj & hom_isMonX Obj }.
43+
44+
Record isQuiverS (Obj: Type) : Type := { homS : Obj -> Obj -> Type }.
45+
46+
Structure QuiverS := { ObjS: Type; AxS: isQuiverS ObjS }.
47+
48+
Definition hom_isMon_type T (X: isQuiverS T) (A B: T) : Type :=
49+
isMon (@homS T X A B).
50+
51+
Record hom_isMonQ T (X: isQuiverS T) : Type :=
52+
hiMQ { privateQ : forall (A B: T), hom_isMon_type T X A B }.
53+
54+
Definition my_hom_isMonQ T (X: isQuiverS T) (F: forall A B, hom_isMon_type T X A B) :
55+
hom_isMonQ T X := hiMQ T X F.
56+
57+
Record Monoid_enriched_quiverQ := { ObjQ: Type; iQQ: isQuiverS ObjQ; hsM: hom_isMonQ ObjQ iQQ }.
58+
59+
Record hom_wrapper T (X: isQuiverS T) (Str: Type -> Type) : Type :=
60+
{ privateW : forall (A B: T), Str (@homS T X A B) }.
2861

29-
(**)
62+
Record hom_wrapperA T (Qv: Type -> Type) (hm: Qv T -> T -> T -> Type) (Str: Type -> Type) (x: Qv T) : Type :=
63+
{ privateWA : forall (A B: T), Str (hm x A B) }.
3064

65+
Definition my_quiver (T: Type) : isQuiverS T.
66+
Admitted.
3167

32-
Fail HB.structure
68+
Lemma my_quiver_mon (T: Type) : forall (A B: T), isMon (@homS T (my_quiver T) A B).
69+
Admitted.
70+
71+
Definition my_hom_isMon (T: Type) : hom_isMonQ T (my_quiver T) :=
72+
my_hom_isMonQ T (my_quiver T) (my_quiver_mon T).
73+
74+
Definition Mixin : Type := Type -> Type.
75+
76+
(* write two versions of Monoid_enriched_quiver: one using hom_isMon
77+
(a mixin, hence a record), the other one using hom_isMon_type as naked
78+
field type. The former corresponds to the wrapped version, the latter
79+
to the intuitive, wrapper-less version. Now the latter should agree
80+
with the former... (broadly corresponding to 2?) *)
81+
82+
83+
84+
Lemma quiver_ok (T: Type) (Str: Type -> Type) :
85+
forall (A B: T), @homS (my_quiver T) A B
86+
87+
88+
Class wrapper (T: Type) () (P: T -> T -> Prop) { prop: forall A B: T, P A B }.
89+
90+
Definition wrapped_hom (T: Type) (F: isMon (@hom T A B)) := wrapper T (isMon (@hom T))
91+
92+
93+
Elpi Accumulate lp:{{
94+
95+
pred wrapper-mixin o:mixinname, o:gref, o:mixinname.
96+
97+
}}.
98+
99+
100+
101+
HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *).
102+
103+
(*********)
104+
105+
106+
HB.structure
33107
Definition Monoid_enriched_quiver :=
34108
{ Obj of isQuiver Obj &
35109
(forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }.

‎tests/monoid_enriched_cat.v

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
From HB Require Import structures.
2+
From Coq Require Import ssreflect ssrfun.
3+
4+
HB.mixin Record isQuiver Obj := { hom : Obj -> Obj -> Type }.
5+
6+
HB.structure Definition Quiver := { Obj of isQuiver Obj }.
7+
8+
HB.mixin Record isMon A := {
9+
zero : A;
10+
add : A -> A -> A;
11+
addrA : associative add;
12+
add0r : left_id zero add;
13+
addr0 : right_id zero add;
14+
}.
15+
16+
HB.structure
17+
Definition Monoid := { A of isMon A }.
18+
19+
Fail HB.structure
20+
Definition Monoid_enriched_quiver :=
21+
{ Obj of isQuiver Obj &
22+
(forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }.
23+
24+
25+
(* Step 0: define a wrapper predicate in coq-elpi *)
26+
(* 5 lines of documentation + 1 line of elpi code in structure.v
27+
`pred wrapper-mixin o:mixinname, o:gref, o:mixinname`
28+
*)
29+
(* Step 1: add a wrapper attribute to declare wrappers,
30+
they should index:
31+
- the wrapped mixin (`isMon`)
32+
- the wrapper mixin (`hom_isMon`)
33+
- the new subject (`hom`)
34+
This attribute will add an entry in the `wrapper-mixin` database.
35+
As an addition substep, we should check that the wrapper has
36+
exactly one field, which is the wrapped mixin.
37+
*)
38+
#[wrapper]
39+
HB.mixin Record hom_isMon T of Quiver T :=
40+
{ private : forall A B, isMon (@hom T A B) }.
41+
42+
(* Step 2: at structure declaration, export the main and only projection
43+
of each declared wrapper as an instance of the wrapped structure on
44+
its subject *)
45+
HB.structure
46+
Definition Monoid_enriched_quiver :=
47+
{ Obj of isQuiver Obj & hom_isMon Obj }.
48+
49+
HB.instance Definition _ (T : Monoid_enriched_quiver.type) (A B : T) : isMon (@hom T A B) :=
50+
@private T A B.
51+
52+
(* each instance of isMon should be tried as an instance of hom_isMon *)
53+
54+
(* Step 3: for each instance of a wrapped mixin on a subject known
55+
to be wrapped, automatically produce an instance of the wrapper mixin too. *)
56+
HB.instance Definition _ := isQuiver.Build Type (fun A B => A -> B).
57+
Fail HB.instance Definition homTypeMon (A B : Quiver.type) := isMon.Build (hom A B) (* ... *).
58+
(* This last command should create a `Monoid_enriched_quiver`, in order to do so it should
59+
automatically instanciate the wrapper `hom_isMon`:
60+
HB.instance Definition _ := hom_isMon.Build Type homTypeMon.
61+
*)

0 commit comments

Comments
 (0)