I quote the beginning of the 2nd paragraph of Chapter 4 (Goal Directed Proof: Tactics and Tacticals) in The HOL System DESCRIPTION:
"Even with recourse to derived inference rules, it is still surprisingly awkward to work *forward*, to find a chain of theorems that culminates in a desired theorem. …" This is where the keyword “forward” comes from. —Chun > Il giorno 08 gen 2019, alle ore 02:38, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > 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
