Re: [Hol-info] New grammar of defining theorems?
I was hesitant to document anything before nailing down the final form of the
syntax. But it's clear that a fairly radical change like this one will need
good explanation.
It's particularly confusing because it's a form that cannot be explained in
terms of standard ML programming. (Our quotation syntax has the same problem.)
Michael
On 8/1/19, 17:08, "Jeremy Dawson" wrote:
On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood.
that's true, sorry.
> Here the advantage is quite clear and valuable: in the existing system,
you have to type the same string of symbols twice in order to avoid annoying
maintenance issues when theorems get moved. There's no utility in allowing
people to write things like
>
> val foo = save_thm("bar", ...)
>
> and it just leads to real pain.
>
there's certainly a discernible advantage in this particular case, I agree
> Slippery slope arguments cut no mustard.
>
Let's hope it's not the start of one. And do work out a way of getting
it into the online documentation (eg, in
HOL/help/src-sml/htmlsigs/idIndex.html)
Jeremy
___
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
Re: [Hol-info] New grammar of defining theorems?
On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood.
that's true, sorry.
> Here the advantage is quite clear and valuable: in the existing system, you
> have to type the same string of symbols twice in order to avoid annoying
> maintenance issues when theorems get moved. There's no utility in allowing
> people to write things like
>
> val foo = save_thm("bar", ...)
>
> and it just leads to real pain.
>
there's certainly a discernible advantage in this particular case, I agree
> Slippery slope arguments cut no mustard.
>
Let's hope it's not the start of one. And do work out a way of getting
it into the online documentation (eg, in
HOL/help/src-sml/htmlsigs/idIndex.html)
Jeremy
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New grammar of defining theorems?
I think you've misunderstood. One form maps to store_thm; the other maps to
save_thm. In both cases the name is likely to be fresh, just as the names
passed to store_thm and save_thm are usually fresh. (If they're not, the
underlying SML functions emit warning messages.)
Here the advantage is quite clear and valuable: in the existing system, you
have to type the same string of symbols twice in order to avoid annoying
maintenance issues when theorems get moved. There's no utility in allowing
people to write things like
val foo = save_thm("bar", ...)
and it just leads to real pain.
Slippery slope arguments cut no mustard.
Michael
On 8/1/19, 15:09, "Jeremy Dawson" wrote:
This summary seems to make it clear that this new feature achieves very
little, with the following costs:
- it gives users yet something else (as if there isn't already enough!)
to lookup in the documentation, or ask questions about
- it's positively confusing, in that
"Theorem name ... " has totally different meanings, depending on which
case applies (eg, in one case, name must already exist, in the other, it
ought not to already exist)
This idea looks like the start of the path followed in Isabelle and Coq,
of having a multitude of commands, some with a multitude of variants (eg
optional arguments) with no coherent consistent grammar rules - just so
that the user doesn't need to type a few punctuation symbols.
Jeremy
On 8/1/19 2:41 pm, Konrad Slind wrote:
> 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)
>
>
___
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
Re: [Hol-info] New grammar of defining theorems?
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 Date: Tuesday, 8 January 2019 at 14:41 To: "Norrish, Michael (Data61, Acton)" Cc: hol-info 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 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)" 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)" 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: "Ch
Re: [Hol-info] New grammar of defining theorems?
This summary seems to make it clear that this new feature achieves very little, with the following costs: - it gives users yet something else (as if there isn't already enough!) to lookup in the documentation, or ask questions about - it's positively confusing, in that "Theorem name ... " has totally different meanings, depending on which case applies (eg, in one case, name must already exist, in the other, it ought not to already exist) This idea looks like the start of the path followed in Isabelle and Coq, of having a multitude of commands, some with a multitude of variants (eg optional arguments) with no coherent consistent grammar rules - just so that the user doesn't need to type a few punctuation symbols. Jeremy On 8/1/19 2:41 pm, Konrad Slind wrote: > 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) > > ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
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 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)" 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)" > 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)"
Re: [Hol-info] New grammar of defining theorems?
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)" 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)" 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)"
>> Date: Thursday, 3 January 2019 at 23:20
>> To: Makarius
>> Cc: Michael Norrish , hol-info
>> 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” men
Re: [Hol-info] New grammar of defining theorems?
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) > 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)" 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)" >>> Date: Thursday, 3 January 2019 at 23:20 >>> To: Makarius >>> Cc: Michael Norrish , hol-info >>> >>> Subject: Re: [Hol-info] New grammar of defining theorems? >>> >>> S
Re: [Hol-info] New grammar of defining theorems?
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)" 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)" >> Date: Thursday, 3 January 2019 at 23:20 >> To: Makarius >> Cc: Michael Norrish , hol-info >> >> 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, th
Re: [Hol-info] New grammar of defining theorems?
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)" 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)"
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius
> Cc: Michael Norrish , hol-info
> 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 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 proje
Re: [Hol-info] New grammar of defining theorems?
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)" > Date: Thursday, 3 January 2019 at 23:20 > To: Makarius > Cc: Michael Norrish , hol-info > > 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 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
Re: [Hol-info] New grammar of defining theorems?
On 03/01/2019 13:20, Chun Tian (binghe) wrote: > > 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. Isar started with 'theorem', then added 'lemma' and 'corollary', much later 'proposition'. In everyday use 'lemma' quickly became the most popular one. So if there were only one keyword, it would be 'lemma'. Makarius signature.asc Description: OpenPGP digital signature ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
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 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 > 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
Re: [Hol-info] New grammar of defining theorems?
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 signature.asc Description: OpenPGP digital signature ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] New grammar of defining theorems?
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. —Chun > Il giorno 02 gen 2019, alle ore 15:44, > ha scritto: > > Dear Chun, > > This is indeed a new feature of the quotation filter. Its purpose is to keep > names consistent, and to reduce the amount of boilerplate typing that > script-writers have to generate. > > It's as yet undocumented, but I hope to get to that soon. > > Michael > > On 2/1/19, 06:20, "Chun Tian (binghe)" wrote: > >Hi, > >(Happy New Year) I found the following code in > src/patricia/sptreeScript.sml (added in commit > 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e) > >Theorem list_to_num_set_append > `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) > (list_to_num_set l2)` > (Induct \\ rw[list_to_num_set_def] > \\ rw[Once insert_union] > \\ rw[Once insert_union,SimpRHS] > \\ rw[union_assoc]); > >Where is the definition of the keyword “Theorem”? Is this a new grammar of > defining theroems, aiming at preventing inconsistent theorem names in > exported theories? > >Regards, > >Chun > > > > > ___ > 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
Re: [Hol-info] New grammar of defining theorems?
I see… thanks, but currently Moscow ML cannot compile that file [1], and I can’t even find the definition of this new feature … —Chun [1] https://github.com/HOL-Theorem-Prover/HOL/pull/634 > Il giorno 02 gen 2019, alle ore 15:44, > ha scritto: > > Dear Chun, > > This is indeed a new feature of the quotation filter. Its purpose is to keep > names consistent, and to reduce the amount of boilerplate typing that > script-writers have to generate. > > It's as yet undocumented, but I hope to get to that soon. > > Michael > > On 2/1/19, 06:20, "Chun Tian (binghe)" wrote: > >Hi, > >(Happy New Year) I found the following code in > src/patricia/sptreeScript.sml (added in commit > 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e) > >Theorem list_to_num_set_append > `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) > (list_to_num_set l2)` > (Induct \\ rw[list_to_num_set_def] > \\ rw[Once insert_union] > \\ rw[Once insert_union,SimpRHS] > \\ rw[union_assoc]); > >Where is the definition of the keyword “Theorem”? Is this a new grammar of > defining theroems, aiming at preventing inconsistent theorem names in > exported theories? > >Regards, > >Chun > > > > > ___ > 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
Re: [Hol-info] New grammar of defining theorems?
Dear Chun, This is indeed a new feature of the quotation filter. Its purpose is to keep names consistent, and to reduce the amount of boilerplate typing that script-writers have to generate. It's as yet undocumented, but I hope to get to that soon. Michael On 2/1/19, 06:20, "Chun Tian (binghe)" wrote: Hi, (Happy New Year) I found the following code in src/patricia/sptreeScript.sml (added in commit 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e) Theorem list_to_num_set_append `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) (list_to_num_set l2)` (Induct \\ rw[list_to_num_set_def] \\ rw[Once insert_union] \\ rw[Once insert_union,SimpRHS] \\ rw[union_assoc]); Where is the definition of the keyword “Theorem”? Is this a new grammar of defining theroems, aiming at preventing inconsistent theorem names in exported theories? Regards, Chun ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] New grammar of defining theorems?
Hi, (Happy New Year) I found the following code in src/patricia/sptreeScript.sml (added in commit 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e) Theorem list_to_num_set_append `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) (list_to_num_set l2)` (Induct \\ rw[list_to_num_set_def] \\ rw[Once insert_union] \\ rw[Once insert_union,SimpRHS] \\ rw[union_assoc]); Where is the definition of the keyword “Theorem”? Is this a new grammar of defining theroems, aiming at preventing inconsistent theorem names in exported theories? Regards, Chun 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
