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