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:

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

- Can be searched easily by
`grep`

. Or it'll be better if it can be searched by`Search`

? - By attaching more metadata to the theorems, maybe some forms of proof automation can be realised by searching through relevant attributes?

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.

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

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.

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

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

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

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.

I see, thanks!

Last updated: Oct 12 2024 at 13:01 UTC