Merge pull request #277 from math-comp/GReTA

GReTA talk demo + Draft of category theory

Author: CohenCyril

HB/common/utils.elpi

@@ -318,3 +318,7 @@ w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.
 pred purge-id i:term, o:term.
 purge-id T T1 :-
   (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1.
+
+pred prod-last i:term, o:term.
+prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y.
+prod-last X X :- !.

HB/structure.elpi

@@ -5,8 +5,8 @@ namespace structure {
 
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
 %  cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
-pred declare i:string, i:term.
-declare Module B :- std.do! [
+pred declare i:string, i:term, i:universe.
+declare Module B Sort :- std.do! [
   purge-id B B1, std.assert-ok! (coq.elaborate-skeleton B1 _ B2) "illtyped structure definition",
   private.sigT->list-w-params B2 GRFSwP ClosureCheck,
 
@@ -35,7 +35,7 @@ declare Module B :- std.do! [
 
   log.coq.env.begin-module Module none,
 
-  private.declare-class+structure MLwP
+  private.declare-class+structure MLwP Sort
     ClassName Structure SortProjection ClassProjection Factories StructKeyClause,
 
   w-params.map MLwP (_\_\_\ mk-nil) NilwP,
@@ -493,17 +493,20 @@ pred synthesize-fields.body i:list term, i:term, i:list (w-args mixinname), o:in
 synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :-
   synthesize-fields T ML FS.
 
-pred mk-record+sort-field i:name, i:term, i:(term -> record-decl), o:indt-decl.
-mk-record+sort-field _ T F (record RecordName {{ Type }} "Pack" (field _ "sort" T F)) :-
-  if (get-option "infer" _) (RecordName = "type_") (RecordName = "type").
+pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl.
+mk-record+sort-field Sort _ T F (record RecordName (sort Sort) "Pack" (field _ "sort" T F)) :- !, std.do! [
+  if (get-option "infer" _) (RecordName = "type_") (RecordName = "type")
+].
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
 mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global ClassName|Args]) _\end-record) :-
   std.append Params [T] Args.
 
 % Builds the axioms record and the factories from this class to each mixin
-pred declare-class+structure i:mixins, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
-declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories (structure-key SortP ClassP (indt StructureInd)):- std.do! [
+pred declare-class+structure i:mixins, i:universe, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
+declare-class+structure MLwP Sort
+    (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories
+    (structure-key SortP ClassP (indt StructureInd)):- std.do! [
 
   if-verbose (coq.say {header} "declare axioms record"MLwP ),
 
@@ -525,7 +528,7 @@ declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection
 
   if-verbose (coq.say {header} "declare type record"),
 
-  w-params.then MLwP (mk-parameter explicit) mk-record+sort-field
+  w-params.then MLwP (mk-parameter explicit) (mk-record+sort-field Sort)
     (mk-class-field (indt ClassInd)) StructureDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare: illtyped",

_CoqProject

@@ -1,3 +1,3 @@
 structures.v
 
--Q . HB
+-Q . HB

examples/GReTA_talk/V1.v

@@ -0,0 +1,15 @@
+Require Import ZArith ssreflect ssrfun.
+From HB Require Import structures.
+
+HB.mixin Record is_monoid (M : Type) := {
+  zero  : M;
+  add   : M -> M -> M;
+  addrA : associative add; (* add is associative. *)
+  add0r : forall x, add zero x = x; (* zero is neutral *)
+  addr0 : forall x, add x zero = x; (*        wrt add. *)
+}.
+
+HB.structure Definition Monoid := { M of is_monoid M }.
+
+HB.instance Definition Z_is_monoid : is_monoid Z :=
+  is_monoid.Build Z 0%Z Z.add Z.add_assoc Z.add_0_l Z.add_0_r.

examples/GReTA_talk/V2.v

@@ -0,0 +1,24 @@
+Require Import ZArith ssreflect ssrfun.
+From HB Require Import structures.
+
+HB.mixin Record is_semigroup (S : Type) := {
+  add   : S -> S -> S;
+  addrA : associative add;
+}.
+HB.structure Definition SemiGroup :=
+  { S of is_semigroup S }.
+
+HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+  zero  : M;
+  add0r : forall x, add zero x = x;
+  addr0 : forall x, add x zero = x;
+}.
+HB.structure Definition Monoid :=
+  { M of is_semigroup M & semigroup_is_monoid M }.
+
+(* is_monoid does not exist anymore *)
+Fail Check is_monoid.
+
+HB.instance Definition Z_is_monoid : is_monoid Z :=
+  is_monoid.Build Z 0%Z Z.add Z.add_assoc Z.add_0_l Z.add_0_r.
+HB.mixin Record xxxx P A := { F : bool }.

examples/GReTA_talk/V3.v

@@ -0,0 +1,36 @@
+Require Import ZArith ssreflect ssrfun.
+From HB Require Import structures.
+
+HB.mixin Record is_semigroup (S : Type) := {
+  add   : S -> S -> S;
+  addrA : associative add;
+}.
+HB.structure Definition SemiGroup :=
+  { S & is_semigroup S }.
+
+HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+  zero  : M;
+  add0r : forall x, add zero x = x;
+  addr0 : forall x, add x zero = x;
+}.
+
+HB.factory Record is_monoid (M : Type) := {
+  zero  : M;
+  add   : M -> M -> M;
+  addrA : associative add;
+  add0r : forall x, add zero x = x;
+  addr0 : forall x, add x zero = x;
+}.
+HB.builders Context (M : Type) (f : is_monoid M).
+  HB.instance Definition _ : is_semigroup M :=
+    is_semigroup.Build M add addrA.
+  HB.instance Definition _ : semigroup_is_monoid M :=
+    semigroup_is_monoid.Build M zero add0r addr0.
+HB.end.
+
+HB.structure Definition Monoid :=
+  { M & is_monoid M }.
+
+HB.instance Definition Z_is_monoid : is_monoid Z :=
+  is_monoid.Build Z 0%Z Z.add
+    Z.add_assoc Z.add_0_l Z.add_0_r.

examples/GReTA_talk/V4.v

@@ -0,0 +1,56 @@
+Require Import ZArith ssreflect ssrfun.
+From HB Require Import structures.
+
+HB.mixin Record is_semigroup (S : Type) := {
+  add   : S -> S -> S;
+  addrA : associative add;
+}.
+HB.structure Definition SemiGroup := { S & is_semigroup S }.
+
+HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+  zero  : M;
+  add0r : forall x, add zero x = x;
+  addr0 : forall x, add x zero = x;
+}.
+
+HB.factory Record is_monoid M := {
+  zero  : M;
+  add   : M -> M -> M;
+  addrA : associative add;
+  add0r : forall x, add zero x = x;
+  addr0 : forall x, add x zero = x;
+}.
+HB.builders Context (M : Type) of is_monoid M.
+  HB.instance Definition _ := is_semigroup.Build M add addrA.
+  HB.instance Definition _ := semigroup_is_monoid.Build M zero add0r addr0.
+HB.end.
+
+HB.structure Definition Monoid := { M & is_monoid M }.
+
+HB.mixin Record monoid_is_group G of is_monoid G := {
+  opp : G -> G;
+  subrr : forall x, add x (opp x) = zero;
+  addNr : forall x, add (opp x) x = zero;
+}.
+
+HB.factory Record is_group G := {
+  zero : G;
+  add : G -> G -> G;
+  opp : G -> G;
+  addrA : associative add;
+  add0r : forall x, add zero x = x;
+  (* addr0 : forall x, add x zero = x; (* spurious *) *)
+  subrr : forall x, add x (opp x) = zero;
+  addNr : forall x, add (opp x) x = zero;
+}.
+HB.builders Context G of is_group G.
+  Let addr0 : forall x, add x zero = x.
+  Proof. by move=> x; rewrite -(addNr x) addrA subrr add0r. Qed.
+  HB.instance Definition _ := is_monoid.Build G zero add addrA add0r addr0.
+  HB.instance Definition _ := monoid_is_group.Build G opp subrr addNr.
+HB.end.
+
+HB.instance Definition Z_is_group : is_group Z :=
+  is_group.Build Z 0%Z Z.add Z.opp
+    Z.add_assoc Z.add_0_l (* Z.add_0_r (*spurious *) *)
+    Z.sub_diag Z.add_opp_diag_l.