You can’t/don’t want to write a regular expression to distinguish these by matching the entirety of the goal and tactic.
Michael From: Konrad Slind <konrad.sl...@gmail.com> Date: Tuesday, 8 January 2019 at 14:41 To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> Cc: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] New grammar of defining theorems? 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<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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<mailto:binghe.l...@gmail.com>> >> Date: Thursday, 3 January 2019 at 23:20 >> To: Makarius <makar...@sketis.net<mailto:makar...@sketis.net>> >> Cc: Michael Norrish <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>, hol-info <hol-info@lists.sourceforge.net<mailto: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<mailto: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<mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info > > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto: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
