Hi.
I have been building an HB structure (see below), but I need to modify the default output that HB produces, to add annotations about universe polymorphism.
I was hoping that I could cut-and-paste the output of HB.structure called with the #[log] parameter, and then perform my
modifications.
However, it seems there is some disconnect between the log and what HB actually does. More concretely, I considered the following example.
From HB Require Import structures.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype seq path fintype.
Export Set Implicit Arguments.
Export Unset Strict Implicit.
Export Unset Printing Implicit Defensive.
Definition ordtype_axiom (T : eqType) (ord : rel T) :=
[/\ irreflexive ord & transitive ord].
HB.mixin Record isOrdered T of Equality T := {
ord : rel T;
ordtype_subproof : ordtype_axiom ord}.
#[log]
#[short(type="ordType")]
HB.structure Definition Ordered :=
{T of Equality T & isOrdered T}.
In this context, I can define
Definition unit_ord (x y : unit) := false.
Lemma unit_is_ordtype : ordtype_axiom unit_ord. Proof. by []. Qed.
HB.instance Definition _ := isOrdered.Build unit unit_is_ordtype.
Check (Ordered.clone unit _).
The last command typechecks, indicating that the ordered structure for unit type has been declared.
However, if I replace the structure definition what the #[log] that it produces, then
Check (Ordered.clone unit _).
stops working.
Is there some way to obtain the correct code implementing the HB.structure declaration?
Thanks,
Aleks
Try #[log(raw)].
If it does not work, please open an issue.
In general replacing one bit of HB with its "equivalent" Coq code won't work for what follows.
In particular all (maybe most of) the additions to Coq-Elpi databases are just comments, and subsequent calls to HB commands need these extra clauses (unless you replace them too with the equivalent Coq code).
If HB is not flexible enough, I recommend you open an issue and explain us what you need to change.
so Plan B is effectively infeasible now? Maybe good to update https://github.com/math-comp/hierarchy-builder#plan-b
Karl Palmskog said:
so Plan B is effectively infeasible now? Maybe good to update https://github.com/math-comp/hierarchy-builder#plan-b
Indeed plan B is out of the picture https://github.com/math-comp/hierarchy-builder/pull/389, thanks for pointing out the readme bit.
We are going to remove it from CI. But planB has never been about mixing HB with non-HB. This would require much more infrastructure.
Just to give an example, HB.pack is a tactic that uses metadata stored in Elpi. If you declare your structures by hand, there is no Elpi clause telling you which is the constructor for the record to package the structure. Of course one could find it another way, after all it is a Coq inductive type, but we don't have such code. The log
options are still very useful to explain how things work, we are keeping them.
Plan-B was to cope with the fact that maybe HB does not work for MC, so we drop it, and someone used it but cannot take over the maintainership, so he at least gets some code that compiles without HB via this planB thing. Now that HB is used in MC, we will maintain it.
maybe this is worth flagging up explicitly in README - that (at least in my reading) adopting HB is practically all-or-nothing, not least for technical reasons, and log
is only informative, not usable for copy-paste
Hi.
Indeed, I figured that the problem comes from what Enrico pointed out. If the structure isn't built with HB.structure, then the subsequent calls to HB.instance don't have access to the appropriate information in Elpi and can define the mixin, but don't declare the canonical instances.
In my example, the solution is to explicitly add the canonical declaration, as in
Definition unit_ord (x y : unit) := false.
Lemma unit_is_ordtype : ordtype_axiom unit_ord. Proof. by []. Qed.
HB.instance Definition unit_ord_mix := isOrdered.Build unit unit_is_ordtype.
Canonical unit_ordType : ordType :=
Ordered.Pack (sort:=unit) (Ordered.Class unit_ord_mix).
That said, I wanted to modify HB code by hand in order to declare the structure polymorphic. Concretely, where the generated code is
Section type.
Record type : Type := Pack { sort : Type; class : axioms_ sort; }.
End type.
Definition phant_clone := ....
I wanted to change it into
Section type.
Polymorphic Cumulative Record
type : Type := Pack { sort : Type; _ : axioms_ sort; }.
End type.
Section PolymorphicClonePack.
Polymorphic Universe ou.
Polymorphic Variables (T : Type@{ou}) (cT : type@{ou}).
Polymorphic Definition phant_clone := ...
Maybe there's an option that could be passed to HB to do this automatically?
Not yet, Elpi has access to the APIs for universe polymorphic stuff, but we did not manage to use them in a satisfactory way. https://github.com/math-comp/hierarchy-builder/tree/univ-poly
I cannot promise anything, but starting from November I may have the time to work again on this.
Our little experience was that just turning on universe polymorphism would result in too many universe arguments.
So the plan was to allow for something like HB.structure Definition s@{u1} := { T : Type@{u1} of M1... MN }
, but this requires some work.
In the meanwhile, we could continue some experiments just tuning universe checking off. (never tried to fiddle with cumulativity).
Last updated: Oct 13 2024 at 01:02 UTC