Stream: Coq users

Topic: A Way to Define Custom Attribute?


view this post on Zulip Jiahong Lee (Jul 10 2022 at 12:59):

Hi, is there a way to define and attach a custom attribute to a theorem? Mainly to communicate the intention to another reader or tooling in a more structured way.

Use cases in mind:

  1. Annotate some metadata to the theorem, instead of forcing it into its name. E.g. a simple theorem that expands a term:
#[purpose = "expand"]
Theorem negb_false : true = negb false.
  1. Can be searched easily by grep. Or it'll be better if it can be searched by Search?

view this post on Zulip Enrico Tassi (Jul 10 2022 at 13:15):

I'm in favour of implementing this.

In hierarchy builder we leaverage this possibility since all commands are implemented in coq-elpi which gives you an API for this.
One attribute of general interest we use is #[doc="..."] which is printed by HB.about.
I'd be happy to help coding this in plain Coq.

view this post on Zulip Enrico Tassi (Jul 10 2022 at 13:19):

IMO the first step is to identify a few use cases and then write a CEP

view this post on Zulip Enrico Tassi (Jul 10 2022 at 13:22):

Note that there is already some hard coded form of attribute, eg Hint Resolve can be seen like a very rigid version of what you propose.

view this post on Zulip Jiahong Lee (Jul 10 2022 at 14:06):

Enrico Tassi said:

Note that there is already some hard coded form of attribute, eg Hint Resolve can be seen like a very rigid version of what you propose.

Thanks, just knew about it! It does solve the automation part, but what I've in mind is more towards the systematic organisation of theorems. Then the automation is the natural application out of the organisation.

Edit: On reflection, I've commit the XY Problem. This custom attribute feature is what I have in mind to solve my actual problem

view this post on Zulip Jiahong Lee (Jul 10 2022 at 14:10):

I don't really have many solid use cases in mind at the moment. I'm simply overwhelmed by the increasing amount of theorems as one keep working in Coq. Not sure if that warrants a CEP...

view this post on Zulip Jiahong Lee (Jul 10 2022 at 14:12):

I'd be happy to help coding this in plain Coq.

Thank you for your interest! I'm not familiar with OCaml. But if it can be done in Coq, then I can look into it

view this post on Zulip Théo Zimmermann (Jul 10 2022 at 14:37):

Jiahong Lee said:

I'd be happy to help coding this in plain Coq.

Thank you for your interest! I'm not familiar with OCaml. But if it can be done in Coq, then I can look into it

I think that's not Enrico meant. Probably, he meant: I'm happy to code this into the code of Coq so that it can be used without the Coq-Elpi plugin.

view this post on Zulip Jiahong Lee (Jul 10 2022 at 14:40):

I see, thanks!


Last updated: Jan 27 2023 at 02:04 UTC