Skip to content

use Coq's elaborator for factories and instances #109

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 13 commits into from
Aug 26, 2020
Merged

use Coq's elaborator for factories and instances #109

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
c00dcb6
MC: backward compatibility attribute #[mathcomp]
gares Aug 13, 2020
67fd65e
HB.structure: synthesize the clone Notation
gares Aug 13, 2020
0904414
use Coq's elaborator for factories and instances
gares Aug 14, 2020
a167996
argument->term uses elaborate (caveat, one may expect a type)
gares Aug 14, 2020
4783a10
HB.instance: elaborate the carrier as a type (coercions to Sortclass)
gares Aug 20, 2020
04178fc
better elaborate reference
gares Aug 20, 2020
3f8021a
HB.instance: read the factory from the type rather than the body
gares Aug 20, 2020
56e723a
typo
gares Aug 20, 2020
f7ba996
register phant-apprev for mixin builder
gares Aug 20, 2020
cf2e42e
MC: add Mixin abbreviation
gares Aug 20, 2020
1f8c27c
update opam
gares Aug 21, 2020
22cde66
update changelog
gares Aug 21, 2020
3ed1c43
fix opam
gares Aug 25, 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: 12 additions & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,17 @@
# 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).
Expand Down
6 changes: 2 additions & 4 deletions coq-hierarchy-builder.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,9 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder"

build: [ make ]
install: [ make "install" "VFILES=structures.v" ]
depends: [
"coq" {>= "8.11.0" & < "8.13.0~" }
"coq-elpi" {>= "1.5.0" & < "1.6.0~"}
]
depends: [ "coq-elpi" {> "1.5.99" & < "1.7.0~"} ]
synopsis: "Hierarchy Builder"
description: """
High level commands to declare and evolve a hierarchy based on packed classes.
"""
tags: [ "logpath:HB" ]
11 changes: 4 additions & 7 deletions demo2/stage10.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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.
Expand All @@ -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) :=
Expand Down
27 changes: 10 additions & 17 deletions demo2/stage11.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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))).
Expand Down Expand Up @@ -339,12 +334,11 @@ 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.
Expand All @@ -353,12 +347,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) :=
Expand Down
Loading