Merge pull request #126 from math-comp/coq-master+coq-elpi-1.7.0+elpi-1.12

Coq master+coq elpi 1.7.0+elpi 1.12

Author: gares

Changelog.md

@@ -1,10 +1,22 @@
 # Changelog
 
+## UNRELEASED
+
+- Use Coq's elaborator to typecheck factories and structures (coercions are
+  now inserted properly)
+- New attribute `#[mathcomp]` for `HB.structure` to synthesize backward
+  compatibility code for the Mathematical Components library.
+  When the mixin contains a single axiom its name can be given as
+  `#[mathcomp(axiom="eq_axiom")]`.
+- `HB.instance Definition name : factory T := term` works even if term is not
+  a known builder. In this case the type (key) is read from the factory
+  (the type of the definition).
+
 ## [0.10.0] - 2020-08-08
 
 - HB now supports parameters (experimental).
 - Port to Coq-Elpi 1.5.
-- NBetter error message in case classes are not defined in the right order.
+- Better error message in case classes are not defined in the right order.
 - Structure operations are not reexported by substructures.
 - Spurious trivial `TYPE` structure removed from demo1.
 

README.md

@@ -69,9 +69,7 @@ Proof. by rewrite example. Qed.
 
 The software is beta-quality, it works but error messages should be improved.
 
-The current version does not handle structures with parameters (for example
-modules over a ring), and forces the carrier to be a type (excluding hierarchies
-of morphisms).
+The current version forces the carrier to be a type, ruling hierarchies of morphisms out.
 
 This [draft paper](https://hal.inria.fr/hal-02478907) describes the language
 in full detail.

_CoqProject

@@ -49,6 +49,8 @@ Coq2020_material/CoqWS_expansion/withoutHB.v
 
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
+tests/instance_params_no_type.v
+tests/test_CS_db_filtering.v
+tests/subtype.v
 
 -R . HB
-

coq-hierarchy-builder.opam

@@ -17,3 +17,4 @@ synopsis: "Hierarchy Builder"
 description: """
 High level commands to declare and evolve a hierarchy based on packed classes.
 """
+tags: [ "logpath:HB" ]

default.nix

@@ -1,19 +1,19 @@
 {withEmacs ? false,
- nixpkgs ? (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/e97fdce4e1b945c9ec30d4d90a451f1577f5cf4a.tar.gz),
+ nixpkgs ? (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/4aa5466cbc741097218a1c494a7b832a17d1967d.tar.gz),
  coq-version ? "8.11",
  print-env ? false
 }:
 with import nixpkgs {
-  overlays = [ (super: self: {
-    coqPackages = { "8.11" = super.coqPackages_8_11;  }."${coq-version}".overrideScope' (self: super: {
-      # Coq package override example:
-      coq-elpi = super.coq-elpi.overrideAttrs (old: {
-        name = "coq8.11-elpi-1.5.0";
-        src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.5.0.tar.gz;
-      });
-    });
-    coq = self.coqPackages.coq;
-  })];
+  # overlays = [ (super: self: {
+  #   coqPackages = { "8.11" = super.coqPackages_8_11;  }."${coq-version}".overrideScope' (self: super: {
+  #     # Coq package override example:
+  #     coq-elpi = super.coq-elpi.overrideAttrs (old: {
+  #       name = "coq8.11-elpi-1.5.0";
+  #       src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.5.0.tar.gz;
+  #     });
+  #   });
+  #   coq = self.coqPackages.coq;
+  # })];
 };
 let pgEmacs = emacsWithPackages (epkgs: with epkgs.melpaStablePackages; [proof-general]); in
 coqPackages.hierarchy-builder.overrideAttrs (old: {

demo1/hierarchy_1.v

@@ -47,14 +47,14 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
-  HB.instance A to_AddComoid_of_TYPE.
-
-  Definition to_Ring_of_AddComoid :=
-    Ring_of_AddComoid.Build A _ _ _ addNr mulrA mul1r
-      mulr1 mulrDl mulrDr.
-  HB.instance A to_Ring_of_AddComoid.
+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.
 

demo1/hierarchy_2.v

@@ -32,13 +32,13 @@ HB.factory Record AddAG_of_TYPE A := {
 
 HB.builders Context A (a : AddAG_of_TYPE A).
 
+  HB.instance
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
-  HB.instance A to_AddComoid_of_TYPE.
 
+  HB.instance
   Definition to_AddAG_of_AddComoid :=
     AddAG_of_AddComoid.Build A _ addNr.
-  HB.instance A to_AddAG_of_AddComoid.
 
 HB.end.
 HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
@@ -66,12 +66,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a : Ring_of_AddComoid A).
 
+  HB.instance
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr.
-  HB.instance A to_AddAG_of_AddComoid.
 
+  HB.instance
   Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA mul1r mulr1 mulrDl mulrDr.
-  HB.instance A to_Ring_of_AddAG.
 
 HB.end.
 
@@ -96,9 +96,9 @@ HB.factory Record Ring_of_TYPE A := {
 
 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 A to_AddComoid_of_TYPE.
 
   Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr mulrA mul1r mulr1 mulrDl mulrDr.

demo2/stage10.v

@@ -188,9 +188,8 @@ Section ProductTopology.
   by split => // [[x1 x2] [[/=Ax1 Bx1] [/=Ax2 Bx2]]].
   Qed.
 
-  Definition prod_topology :=
-    TopologicalBase.Build (TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type _ prod_open_base_covers prod_open_base_setU.
-  HB.instance ((TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type) prod_topology.
+  HB.instance Definition prod_topology :=
+    TopologicalBase.Build (T1 * T2)%type _ prod_open_base_covers prod_open_base_setU.
 
 End ProductTopology.
 
@@ -209,12 +208,11 @@ HB.structure Definition TAddAG := { A of Topological A & AddAG_of_TYPE A & JoinT
 
 (* Instance *)
 
-Definition Z_ring_axioms :=
+HB.instance Definition Z_ring_axioms :=
   Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
     Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
     Z.mul_assoc Z.mul_1_l Z.mul_1_r
     Z.mul_add_distr_r Z.mul_add_distr_l.
-HB.instance Z Z_ring_axioms.
 
 Example test1 (m n : Z) : (m + n) - n + 0 = m.
 Proof. by rewrite addrK addr0. Qed.
@@ -225,12 +223,11 @@ Search _ Qc "plus" "opp".
 Lemma Qcplus_opp_l q : - q + q = 0.
 Proof. by rewrite Qcplus_comm Qcplus_opp_r. Qed.
 
-Definition Qc_ring_axioms :=
+HB.instance Definition Qc_ring_axioms :=
   Ring_of_TYPE.Build Qc 0%Qc 1%Qc Qcplus Qcopp Qcmult
     Qcplus_assoc Qcplus_comm Qcplus_0_l Qcplus_opp_l
     Qcmult_assoc Qcmult_1_l Qcmult_1_r
     Qcmult_plus_distr_l Qcmult_plus_distr_r.
-HB.instance Qc Qc_ring_axioms.
 
 Obligation Tactic := idtac.
 Definition Qcopen_base : set (set Qc) :=

demo2/stage11.v

@@ -193,11 +193,8 @@ Section ProductTopology.
   by split => // [[x1 x2] [[/=Ax1 Bx1] [/=Ax2 Bx2]]].
   Qed.
 
-  Definition prod_topology :=
-    TopologicalBase.Build _ _ prod_open_base_covers prod_open_base_setU.
-
-  (* TODO: make elpi insert coercions! *)
-  HB.instance ((TopologicalSpace.sort T1 * TopologicalSpace.sort T2)%type) prod_topology.
+  HB.instance Definition prod_topology :=
+    TopologicalBase.Build (T1 * T2)%type _ prod_open_base_covers prod_open_base_setU.
 
 End ProductTopology.
 
@@ -241,9 +238,8 @@ Section Uniform_Topology.
      uniform_open X -> uniform_open Y -> uniform_open (setI X Y).
   Admitted.
 
-  Definition uniform_topology :=
-    Topological.Build _ _ uniform_open_setT (@uniform_open_bigcup) uniform_open_setI.
-  HB.instance (uniform (UniformSpace_wo_Topology.sort U)) uniform_topology.
+  HB.instance Definition uniform_topology :=
+    Topological.Build (uniform U) _ uniform_open_setT (@uniform_open_bigcup) uniform_open_setI.
 
 End Uniform_Topology.
 
@@ -281,10 +277,9 @@ Section TAddAGUniform.
       exists2 B, TAddAG_entourage B & graph_comp B B `<=` A.
   Admitted.
 
-  Definition TAddAG_uniform :=
-    Uniform_wo_Topology.Build _ _ filter_TAddAG_entourage TAddAG_entourage_sub
+  HB.instance Definition TAddAG_uniform :=
+    Uniform_wo_Topology.Build (tAddAG T) _ filter_TAddAG_entourage TAddAG_entourage_sub
       TAddAG_entourage_sym TAddAG_entourage_split.
-  HB.instance (tAddAG (TAddAG_wo_Uniform.sort T)) TAddAG_uniform.
 
   Lemma TAddAG_uniform_topologyE :
      open = (uniform_open _ : set (set (uniform TT))).
@@ -311,15 +306,20 @@ HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined T := {
   (* TODO: should be subsumed by the type alias TAddAG *)
 HB.factory Record TAddAG_Uniform U of TAddAG_wo_Uniform U := { }.
 
-HB.builders Context U of TAddAG_Uniform U.
-  Definition to_Uniform_wo_Topology : Uniform_wo_Topology U := (TAddAG_uniform _).
-  HB.instance U to_Uniform_wo_Topology.
+HB.builders Context U (a : TAddAG_Uniform U).
+
+  HB.instance
+  Definition to_Uniform_wo_Topology : Uniform_wo_Topology U :=
+    TAddAG_uniform _.
+
+  HB.instance
   Definition to_Join_Uniform_Topology : Join_Uniform_Topology U :=
-    (TAddAG_Join_Uniform_Topology _).
-  HB.instance U to_Join_Uniform_Topology.
-  Definition to_Join_TAddAG_Uniform :=
-    (Join_TAddAG_Uniform.Build U (TAddAG_entourageE _)).
-  HB.instance U to_Join_TAddAG_Uniform.
+    TAddAG_Join_Uniform_Topology _.
+
+  HB.instance
+  Definition to_Join_TAddAG_Uniform : Join_TAddAG_Uniform U :=
+    Join_TAddAG_Uniform.Build U (TAddAG_entourageE _).
+
 HB.end.
 
 HB.structure Definition TAddAG :=
@@ -333,18 +333,17 @@ HB.builders Context T (a : JoinTAddAG T).
   Definition to_JoinTAddAG_wo_Uniform : JoinTAddAG_wo_Uniform T := a.
   HB.instance T to_JoinTAddAG_wo_Uniform.
   (* TODO: Nice error message when factory builders do not depend on the source factory 'a'*)
-  Definition to_Uniform := let _ := a in TAddAG_Uniform.Build T.
+  Definition to_Uniform : TAddAG_Uniform T := let _ := a in TAddAG_Uniform.Build T.
   HB.instance T to_Uniform.
 HB.end.
 
 (* Instance *)
 
-Definition Z_ring_axioms :=
-  Ring_of_TYPE.Build _ 0%Z 1%Z Z.add Z.opp Z.mul
+HB.instance Definition Z_ring_axioms :=
+  Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul
     Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l
     Z.mul_assoc Z.mul_1_l Z.mul_1_r
     Z.mul_add_distr_r Z.mul_add_distr_l.
-HB.instance Z Z_ring_axioms.
 
 Example test1 (m n : Z) : (m + n) - n + 0 = m.
 Proof. by rewrite addrK addr0. Qed.
@@ -353,12 +352,11 @@ Require Import Qcanon.
 Lemma Qcplus_opp_l q : - q + q = 0.
 Proof. by rewrite Qcplus_comm Qcplus_opp_r. Qed.
 
-Definition Qc_ring_axioms :=
-  Ring_of_TYPE.Build _ 0%Qc 1%Qc Qcplus Qcopp Qcmult
+HB.instance Definition Qc_ring_axioms :=
+  Ring_of_TYPE.Build Qc 0%Qc 1%Qc Qcplus Qcopp Qcmult
     Qcplus_assoc Qcplus_comm Qcplus_0_l Qcplus_opp_l
     Qcmult_assoc Qcmult_1_l Qcmult_1_r
     Qcmult_plus_distr_l Qcmult_plus_distr_r.
-HB.instance Qc Qc_ring_axioms.
 
 Obligation Tactic := idtac.
 Definition Qcopen_base : set (set Qc) :=