[Hol-info] Relations which build upon each other
Hello, I’m doing a project on proof theory, and I’m trying to define the proof rules with Hol_reln. I am defining multiple proof systems which build upon each other, i.e. intuitionistic logic then classical logic. It seems natural to have something like: var (Sys1_rules, …,…) = Hol_reln `…`; var (Sys2_rules,…,…) = Hol_reln `!x. Sys1 x ==> Sys2 x /\ …` But when I go to prove something which needs to use Sys2 rules then Sys1 rules, I don’t know how to get it to work, since the Sys1 rules don’t know mention Sys2 (nor should they). For example: `Sys2 x` by metis_tac[Sys2_rules] `Sys2 y` by metis_tac[Sys1_rules,Sys2_rules] (* Sys1 has no rules for Sys2, so this fails! *) The obvious solution is to just keep them independent and have all the rules in each of them, but I thought I might be missing some elegant way of achieving this. Please let me know if there is such a trick. Thank you, Alex ___ 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
