Stream: Coq users

Topic: A Way to Define Custom Attribute?

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.

2. Can be searched easily by grep. Or it'll be better if it can be searched by Search?
3. By attaching more metadata to the theorems, maybe some forms of proof automation can be realised by searching through relevant attributes?

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.

Enrico Tassi (Jul 10 2022 at 13:19):

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

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.

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

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

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

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.

Jiahong Lee (Jul 10 2022 at 14:40):

I see, thanks!

Last updated: Oct 12 2024 at 13:01 UTC