Hi, i'm starting using HB and a typical pattern i'm using is the following:
Program Definition foo_IsBar := IsBar.Build foo easy1 _ _.
Next Obligation. ... Qed.
Next Obligation. ... Qed.
HB.instance Definition _ := foo_IsBar.
More explicitely, some of the fields of the mixin are easy to give a term for, but some are not (and i don't want to extract a lemma since the type might be a bit long to write down) hence i want to prove them interactively. Trying to use HB.instance Program Definition ...
gives me Error: Could not locate Program
. Is there a way to build HB.instance
interactively?
Completely unrelated, but also a beginner question: HB seems to be quite mixin-oriented, since HB.instance
builds mixins and the corresponding Foo.type
canonical structure has a mangled name. So i'm not so sure what the proper api is for building a Foo.type
structure with smart builders as for mixins: Foo.Pack
seems to be a bit internal api (it mentions Foo.axioms_
). Part of the reason i'm starting to use HB (and canonical structures), is because i want to have a clear distinction between implementing a structure for some type and declaring it canonical (i will sometimes need to talk about several instances of the same structure for the same type/parameter, something which is very painful with typeclasses). I'm not really sure what is the proper HB way to do this sort of things. For example i don't know how to properly declare local canonical structures (which will not leak outside), is this done with a module?
Lapinot said:
Hi, i'm starting using HB and a typical pattern i'm using is the following:
Program Definition foo_IsBar := IsBar.Build foo easy1 _ _. Next Obligation. ... Qed. Next Obligation. ... Qed. HB.instance Definition _ := foo_IsBar.
More explicitely, some of the fields of the mixin are easy to give a term for, but some are not (and i don't want to extract a lemma since the type might be a bit long to write down) hence i want to prove them interactively. Trying to use
HB.instance Program Definition ...
gives meError: Could not locate Program
. Is there a way to buildHB.instance
interactively?
If I have, for instance, a mixin with one operation op
and two properties op1
and op2
, I would probably do something like
Program Definition foo_isOp := @isOp.Build foo op _ _.
(note however that while Program
is a nice tool for easy development, I'm not sure I would recommend it's use in final scripts, since, at least with the default program tactic, it tends to give not very robust proof scripts (it introduces automatically named variables for instance))
@Pierre Roux yes indeed that is what i am more or less doing. So then you need to add a second line with HB.instance ...
, and this seems a bit ugly to me since there will be a second definition (HB doesn't seem to have anything like "existing instance", meaning "here is the full mixin term, just hook it up"). Using the Definition _ := ..
pattern is ok since i don't have to come up with a new name, but it doesn't feel very nice (i'm already a bit scared of all the name mangling done by HB).
Lapinot said:
i will sometimes need to talk about several instances of the same structure for the same type/parameter
A common way to do this is to attach the alternative structure to an alias:
HB.instance Definition _ := isBar.Build foo foo_is_regular_bar.
Definition foo_alt := foo.
HB.instance Definition _ := isBar.Build foo_alt foo_is_alternative_bar.
Check foo : barType. (* regular structure *)
Check foo_alt : barType. (* alternative structure *)
another solution is to isolate instances in modules and only open the one you need (if you are not mixing the instances).
Ok, so canonical structure resolution will only look at syntactic equality on the key? This is nice to know.
Yes, it only unfolds when no instance is found.
To answer your question about Program
, if it were fixed to respect the same variable introduction scheme as Definition
, Lemma
, etc there would be no obstacle to use it. Moreover the reason why we do not provide interactive HB
command is a current limitation of coq-elpi.
Lapinot said:
(HB doesn't seem to have anything like "existing instance", meaning "here is the full mixin term, just hook it up")
There used to be HB.instance foo
command which is however deprecated because the implementation is not correct. It could be revived.
Thanks for the replies! Ok, I will keep doing an intermediate (interactive) definition then, I was mostly asking to know what was the idiomatic way to do this, so I think i'm happy with this.
Last updated: Oct 13 2024 at 01:02 UTC