search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
97 stars 21 forks source link

HB does not preserve the name of implicit arguments #455

Open silene opened 3 hours ago

silene commented 3 hours ago 
From HB Require Import structures.

HB.mixin Record IsAddComoid A := { zero : A }.
HB.structure Definition AddComoid := { A of IsAddComoid A }.

About zero.
(* zero : forall {s : AddComoid.type}, s *)

Note how the implicit argument of zero is named s instead of A. This makes it a bit tedious to port developments. Here is an example of an actual modification I had to make to avoid depending on the automatically generated identifier:

-change Rmult with (scal (V := R)).
+change Rmult with (@scal _ R).

(I could also have written Arguments scal K V : rename. But I do not want to perform such a command for all the symbols of the hierarchy.)

gares commented 2 hours ago

I see your point, but both A in your directives denote the carrier of what HB called s, eg AddComoid.sort s, so it not really about preserving a name, but rather using one as a good default.

I don't if we have a better pattern for writing @scal _ R in mathcomp, since we surely don't rely on the s name. I suspect R should be inferred by a CS inference if you unify Rmult with @scal _ _ (and change should do it). Does rewrite -[Rmult]/(@scal) work?

CohenCyril commented 2 hours ago

We must indeed honor the name given by HB.structure

CohenCyril commented 2 hours ago

Actually naming is not really stable by operator transfer from one structure to another :-/ so I'm not sure how to handle this in a backward compatible way...

gares commented 2 hours ago

Let's first see if the use case for making the name part of the "API" is motivated by the tactic language or not.

silene commented 15 minutes ago

No, using rewrite -[Rmult]/scal (as well as @scal variants) does not work any better than change Rmult with (@scal _ R), since the "fold pattern scal does not match redex Rmult". I have to use rewrite -[Rmult]/(@scal _ R).

That said, you are at least right that, e.g., rewrite -[Rminus]/minus works better than change Rminus with minus. But in the case of scal, the relation with Rmult is not that canonical.