So the key is to make sure that they’re not distinguished internally by some tools, and if some tools do, it’s their problems but HOL’s.
I personally don’t like the keyword “Theorem” because I think many small
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct
way of using these conventions should be aligned with majority math books,
which I believe there must be some “rules” mentioned somewhere.
On the other side, HOL4 users always have multiple ways to build a theorem. For
example, sometimes I perfer using “save_thm” to build theorems forwardly and
put the statement as comments before it, sometimes multiple theorems were put
into a “local” block sharing common tactics. As a result, HOL4 proof scripts
were *not* documents but essentially raw ML programs, thus extremely flexible.
I may not adopt this new grammar in a complex proof script in which different
ways of building theorems were used together.
—Chun
P. S. Coq seems to have even more synonyms: (do Coq users here share the same
concerns?)
Lemma ident [binders] : type.
Remark ident [binders] : type.
Fact ident [binders] : type.
Corollary ident [binders] : type.
Proposition ident [binders] : type.
These commands are synonyms of Theorem ident [binders] : type.
> Il giorno 03 gen 2019, alle ore 12:23, Makarius <makar...@sketis.net> ha
> scritto:
>
> On 03/01/2019 11:23, Chun Tian (binghe) wrote:
>> Hi Michael,
>>
>> thanks for fixing the bugs. (now I see why I can’t find its definition…)
>>
>> Going in this direction, have you considered adding also “Lemma” and
>> “Corollary”? Internally they're equivalent with “Theorem”, but they could
>> literally help writers (and readers) identifying different levels of
>> theorems, like those in math books.
>
> This reminds me of Isabelle/Isar. Some decades ago I introduced these
> variants of 'theorem' and it became a running gag of confusion and
> unclear corner cases, because aliases were not really identical, but
> distinguished internally by some tools.
>
> Recently, we even introduced 'proposition' as another variant, but it is
> unclear if it is more prominent than 'theorem' or less prominent than
> 'lemma'. Thus it depends on local conventions of particular
> formalization projects how to treat it, e.g. in document presentation.
>
> If I had another chance today, I would probably eliminate all funny
> aliases of Isar commands.
>
>
> Makarius
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
