Proposal: Comment marking for intentionally unused hypothesis/hypotheses

[David A. Wheeler]

In:
https://github.com/metamath/set.mm/issues/2648
@savask reveals some great analysis of theorems that don't use some of their hypotheses.
In most cases this is something that should be fixed.
It's great work, thanks!!

However, as @savask notes:
> ... there are also theorems which contain useless hypotheses by design, like a1ii, which shouldn't be corrected.

I think every assertion that intentionally does *not* use all its hypotheses should be *clearly* documented
in its descriptive comment. I think we should have a convention so we can automatically detect
those cases later, similar to "(New usage is discouraged.)". That way, both humans and automated
analysis programs will know that this is on purpose.

I propose using these comment markings for assertions ($a and $p) where hypotheses
are not used on *purpose*:
* "(Intentionally unused hypothesis)" if exactly one hypothesis is unused
* "(Intentionally unused hypotheses)" if more than one hypotheses are unused

I was originally going to propose both simply because that's how English plurals work.
However, there's an error-detect advantage to making their meaning different -
if you only intended 1 hypothesis to be unused, but more than one is, it
can still be caught.

--- David A. Wheeler

[Alexander van der Vekens]

On Sunday, July 17, 2022 at 6:36:13 PM UTC+2 David A. Wheeler wrote:

I propose using these comment markings for assertions ($a and $p) where hypotheses
are not used on *purpose*:
* "(Intentionally unused hypothesis)" if exactly one hypothesis is unused
* "(Intentionally unused hypotheses)" if more than one hypotheses are unused

I was originally going to propose both simply because that's how English plurals work.
However, there's an error-detect advantage to making their meaning different -
if you only intended 1 hypothesis to be unused, but more than one is, it
can still be caught.

 

This is a good idea, especially if there is a tool/script which checks automatically if there are (unintentionally) unused hypotheses. But from this tool perspective, I would suggest to have only one marking:

* "(Intentionally unused hypotheses)" if at least one hypothesis is unused

It is the responsibility of the contributor who uses such a marking that the hypotheses are as intended - the tool/script can check all other cases, which will be the vast majority.

[Mario Carneiro]

I also wonder whether this would be better expressed as a $j comment rather than another plain text comment in the doc string. It's not really important user-facing information.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d1f0a889-7d14-4e56-95d9-acef10ba8102n%40googlegroups.com.

[David A. Wheeler]

> On Jul 17, 2022, at 1:01 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> I also wonder whether this would be better expressed as a $j comment rather than another plain text comment in the doc string. It's not really important user-facing information.

Maybe. I think it *is* useful for users to know that at least one of they hypotheses they see isn't really necessary, and it doesn't really impact the mathematical interpretation of the assertion. Obviously it would *work* either way. I'm curious what other think.

BTW, if we just a comment marking, it should have a full stop before the closing parenthesis just like similar markings. That is:

* "(Intentionally unused hypotheses.)"

--- David A. Wheeler

[Benoit]

I think it's overkill for something that basically never happens.  Are there cases in set.mm apart from a1ii (which is said to be useful for use in some proof assistants, but I don't even know if it's ever used) and bj-df-clel, bj-df-cleq (which are candidates to replace df-clel, df-cleq, in which case they will become $a-statements anyway) ?

Benoît

[Mario Carneiro]

I think that if it's only going to appear once or a few times, I would rather have it as a $j comment than a markup keyword, since the latter is more likely to not be recognized as a keyword. (I am generally opposed to markup keywords altogether - I would rather have computer-readable keywords be explicitly called out as such and presentation tools should incorporate this in the e.g. HTML display if desired.) $j commands are also fairly low cost since they do not mandate the existence of any tool that recognizes them (there are a couple $j commands that are already in that category) - the only thing that is needed is to make up a keyword and write it in the file, and tools can decide to honor the annotation if they want to.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3c546ae4-c8da-4bc0-96d5-9727b9039690n%40googlegroups.com.

[David A. Wheeler]

> On Jul 17, 2022, at 1:42 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> I think that if it's only going to appear once or a few times, I would rather have it as a $j comment than a markup keyword, since the latter is more likely to not be recognized as a keyword. (I am generally opposed to markup keywords altogether - I would rather have computer-readable keywords be explicitly called out as such and presentation tools should incorporate this in the e.g. HTML display if desired.) $j commands are also fairly low cost since they do not mandate the existence of any tool that recognizes them (there are a couple $j commands that are already in that category) - the only thing that is needed is to make up a keyword and write it in the file, and tools can decide to honor the annotation if they want to.

A "$j" works for me, I just want theorems with intentionally-unused hypotheses marked in a way that automated tools *can* detect it. It should be very rare.

-- David A. Wheeler

[savask]

I fully agree with Benoit here, this almost never happens so adding a $j command or a special comment is just over-bureaucratization of set.mm.

I would also argue that an automatic check for unused hypotheses (like we do with markup) is not needed. It may happen that a proof of some statement uses all its hypotheses originally, but stops using some hypothesis after automatic minimization. This will trigger our hypothetical automatic check, and while minimization can be done automatically very easily, removing unused hypotheses requires work. This will impose additional toll on already not-so-easy process of contributing to set.mm.

In any case, automatic tools, $j commands etc are dealing with symptoms of the problem, but not its root: neither mmj2 nor metamath-exe warn the user that their theorem proof doesn't use some hypothesis.