Isn't it clear just from the form? Theorem name quote (ML) --> val name = Q.store_thm(name,quote,ML) Theorem name (ML) --> val name = save_thm(name,ML)
On Mon, Jan 7, 2019 at 8:34 PM <michael.norr...@data61.csiro.au> wrote: > Forward and backward give us nice terminology, thanks! It may also be > possible to have the quotation filter figure things out by looking for the > left-parenthesis that is required to follow the name in the forward case. > I may play with that. > > Michael > > On 8/1/19, 12:38, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: > > Hmmm, well… all theorems are essentially *derived* from earlier > theorems or axioms, thus it seems (to me) that the word “derived” still > doesn’t capture the characterization of “save_thm” from “store_thm”. But > the word “dervied” makes more senses than previous “calculated” as > “save_thm”’s body is mainly using “derived rules” instead of “tactics”. > However, I see the essential difference is the direction in the proof: from > proof goal to existing theorems, or from existing theorems to proof goal. > > This whole mail thread is not really a technical discussion, thus > whatever I said here must be highly subjective, however I suggest the > following: > > 1. using keyword “forward” and “backward” to distinguish theorems > built by “save_thm” and “store_thm”, respectively: > > - Theorem(forward) name (MLcode); > - Theorem(backward) name tmquote (MLcode); > > 2. the keyword (backward) is optional (simply because this is the most > case), thus backward theorems can also be expressed (if detected the > tmquote part, somehow) in your current way: > > - Theorem name tmquote (MLcode); > > 3. if ML’s parser is smart enough, even the keyword (forward) can be > eliminated, because the number of arguments is different: in forward proof > it is 2, in backward proof it is 3: > > - Theorem name (MLcode); > - Theorem name tmquote (MLcode); > > How much you can go with above idea, depends on how powerful the ML > quotation code can be. > > Hope this helps, > > —Chun > > > Il giorno 08 gen 2019, alle ore 02:10, > michael.norr...@data61.csiro.au ha scritto: > > > > 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 > > > > > _______________________________________________ > 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
