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