Indeed, they are both calculated. In one, you state the desired end-state and
head towards it with a tactic. In the other, you transform existing theorems
with rules of inference and derive a final statement (hence the good practice,
which you mentioned, of putting the statement into a comment).
Given that, what about
Theorem(derived) name (MLcode);
?
Michael
On 7/1/19, 20:31, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
Hi Michael,
Thanks, now I see your points: if it’s really a “lemma”, then there’s no
need to export it, thus `Q.prove` (or `prove`) should just do the job.
Among the two syntactic sugars, I personally like your first version
(Theorem(calculated) …), because it emphasized that, a `Theorem` generated by
`save_thm` has no differences (in use) with a `Theorem` generated by
`store_thm`, just the word “calculated” could have a better name, as both kinds
of theorems are essentially calculated.
—Chun
> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au ha
scritto:
>
> The Theorem keyword is a prettier way of writing `store_thm`, which, as
the name suggests, is indeed for theorems. In other words, the choice of
Theorem merely reflects our existing naming convention.
>
> If you have a lemma that shouldn’t be “stored”, then you should probably
be using `Q.prove` (or `prove`). The use of theory files that make theorem
values persistent is the way in which users can distinguish important results
that should persist (that is, “theorems”), and those that should be more
ephemeral.
>
> The existing `save_thm` entrypoint has the same problem with requiring
redundant typing of names. I’m thus tempted to invent a Theorem analogue to map
to it. My current feeling is to go for something like
>
> Theorem(calculated) thmname (ML code);
>
> Or
>
> Computed_Theorem thmname (ML code)
>
> Or …?
>
> Suggestions welcome.
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius <makar...@sketis.net>
> Cc: Michael Norrish <michael.norr...@data61.csiro.au>, hol-info
<hol-info@lists.sourceforge.net>
> Subject: Re: [Hol-info] New grammar of defining theorems?
>
> 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
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
