Stream: Hierarchy Builder devs & users

Topic: beginner: interactive definition of instance


view this post on Zulip Lapinot (Apr 22 2024 at 12:23):

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?

view this post on Zulip Lapinot (Apr 22 2024 at 12:45):

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?

view this post on Zulip Pierre Roux (Apr 22 2024 at 13:40):

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 me Error: Could not locate Program. Is there a way to build HB.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))

view this post on Zulip Lapinot (Apr 22 2024 at 13:45):

@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).

view this post on Zulip Pierre Roux (Apr 22 2024 at 13:46):

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).

view this post on Zulip Lapinot (Apr 22 2024 at 13:47):

Ok, so canonical structure resolution will only look at syntactic equality on the key? This is nice to know.

view this post on Zulip Pierre Roux (Apr 22 2024 at 13:49):

Yes, it only unfolds when no instance is found.

view this post on Zulip Cyril Cohen (Apr 23 2024 at 08:13):

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.

view this post on Zulip Cyril Cohen (Apr 23 2024 at 08:15):

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.

view this post on Zulip Lapinot (Apr 23 2024 at 11:37):

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