Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Hi Makarius, Yeah, this is why I never succeeded in building PolyML on Windows in Cygwin or MinGW. When the building process stopped at some assembly code files, I thought they're for Microsoft compilers only. I don't believe PolyML depends on any deep GCC feature which is only available in old versions, because PolyML builds correctly on Linux and Mac using whatever versions of GCC. PolyML maintainers may be interested enough to fix the building issues, if both HOL-4 and Isabelle want to have Windows versions based on easily build-able PolyML. And thank you very much for pointing out the hidden Mercurial repository of Isabelle [1] ^_^ Now I can see how "active" it is for a "not dying" theorem prover: stable 10-20 code commits on everyday basis, and new theories keep going into core Isabelle libraries. Regards, Chun Tian [1] hg clone http://isabelle.in.tum.de/repos/isabelle/ On 18 January 2017 at 11:54, Makarius wrote: > On 17/01/17 15:24, Chun Tian (binghe) wrote: > > Sorry, I re-checked my Isabelle environment and found that the PolyML in > > Isabelle is actually built by GCC (mingw versions), so my statement > > about "PolyML cannot be built in ..." was completely wrong. The rest > > ideas should still hold. > > It is indeed built with MinGW, but that is very difficult to do. See > http://isabelle.in.tum.de/repos/isabelle/raw-file/ > Isabelle2016-1/Admin/polyml/INSTALL-MinGW > which is just a reminder for me for the precise versions need to be > used. Otherwise it won't work. > > Maybe we can open a discussion on the Poly/ML mailing list, if this > rather old version of gcc on MinGW is still needed, or if things can be > updated and simplified. > > > Concerning system structures in ML, see also: > > http://isabelle.in.tum.de/repos/isabelle/raw-file/ > Isabelle2016-1/src/Pure/ML/ml_system.ML > > http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/ > System/bash.ML > > Here the bash.exe is the one from Cygwin -- that is required for add-on > tools of Isabelle. > > > Makarius > > -- --- Chun Tian (binghe) University of Bologna (Italy) -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
On 17/01/17 15:24, Chun Tian (binghe) wrote: > Sorry, I re-checked my Isabelle environment and found that the PolyML in > Isabelle is actually built by GCC (mingw versions), so my statement > about "PolyML cannot be built in ..." was completely wrong. The rest > ideas should still hold. It is indeed built with MinGW, but that is very difficult to do. See http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/Admin/polyml/INSTALL-MinGW which is just a reminder for me for the precise versions need to be used. Otherwise it won't work. Maybe we can open a discussion on the Poly/ML mailing list, if this rather old version of gcc on MinGW is still needed, or if things can be updated and simplified. Concerning system structures in ML, see also: http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/ML/ml_system.ML http://isabelle.in.tum.de/repos/isabelle/raw-file/Isabelle2016-1/src/Pure/System/bash.ML Here the bash.exe is the one from Cygwin -- that is required for add-on tools of Isabelle. Makarius -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Thank you for taking the time to look into this. I agree that a Cygwin poly/ml version is the best route to a Windows build (Moscow ML is simply too slow for serious work). Initially, I’d be happy to not use the Holmake code that depends on Posix. Instead, we could use the Moscow ML approach, and just have single-threaded Holmake. If there’s an easy way to emulate the fork/exec approach that Holmake exploits on Unix, then that would be better of course. As you say, the core of the system is pretty pure SML and should work just fine on Windows. Best wishes, Michael From: "Chun Tian (binghe)" Date: Wednesday, 18 January 2017 at 01:24 To: "Norrish, Michael (Data61, Canberra City)" Cc: hol-info Subject: Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Sorry, I re-checked my Isabelle environment and found that the PolyML in Isabelle is actually built by GCC (mingw versions), so my statement about "PolyML cannot be built in ..." was completely wrong. The rest ideas should still hold. On 17 January 2017 at 13:36, Chun Tian (binghe) mailto:binghe.l...@gmail.com>> wrote: No, it’s actually my pleasure to make a little contribution. For the Windows build issue, I think the correct path is to try to build HOL using the PolyML (32bit and 64bit) and Cygwin environment shipped with Isabelle2016-1 (installed on Windows 10). This version of PolyML is built by Visual Studio 2010, it has normal executions, DLLs and other files, the structure looks exactly like those we manually build on Linux and Mac. PolyML cannot be built in Mingw32 or Cygwin32 using GCC compilers, thus trying to build HOL in pure Cygwin environment results into failure. So we can expect the final HOL build should be able to run standalone in Windows CMD shell, if this plan works. MosML shouldn’t be considered at all. I ever tried to make some initial fixes. The most obvious issue is that, HOL’s ML code used functions from the “Posix” structure, but this structure is not available on Windows. Some of these unavailable functions can be found in OS structure, which is available on all platforms. Others may need to be manually implemented on Windows using functions from OS or Windows structures. Also, when detecting the location of executions, HOL’s ML code doesn’t consider “.exe” as part of file name at all. These are all minor issues is irrelevant to the theorem proving related code. However, I’m not an experienced ML programmer (I’m actually a Common Lisp programmer), can’t do complex ML coding at current moment … On 17 January 2017 at 00:23, mailto:michael.norr...@data61.csiro.au>> wrote: If you are using the working copy of HOL from the git repository, you should check the release notes in HOLDIR/doc. We document major incompatibilities there. Note also that the last official release was K10. There is a tag for K11 in the repository, and some release notes for it, but it hasn’t been released due to issues with the Windows build. The change to PAT_ASSUM is documented in doc/next-release.md<http://next-release.md>, which will eventually be renamed to the K12 release notes in all likelihood. The working repo did not have corrected .doc files for those functions though, so thank you very much for writing those! Michael On 17/1/17, 05:47, "Chun Tian (binghe)" mailto:binghe.l...@gmail.com>> wrote: Hi, HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches the term argument, applies the theorem tactic to it, and removes this assumption.” But I found it actually doesn’t remove the assumption in latest Kananaskis 11. To see this, try the following goal (open listTheory first): > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l : proofs First I rewrite it: > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); OK.. 1 subgoal: val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof Then I want to pick the assumption 0 and specialize the quantifier with `x`: > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); <> OK.. 1 subgoal: val it = ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof > Now you can see, the assumption 0 is still here. It’s not remov
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Sorry, I re-checked my Isabelle environment and found that the PolyML in Isabelle is actually built by GCC (mingw versions), so my statement about "PolyML cannot be built in ..." was completely wrong. The rest ideas should still hold. On 17 January 2017 at 13:36, Chun Tian (binghe) wrote: > No, it’s actually my pleasure to make a little contribution. > > For the Windows build issue, I think the correct path is to try to build > HOL using the PolyML (32bit and 64bit) and Cygwin environment shipped with > Isabelle2016-1 (installed on Windows 10). This version of PolyML is built > by Visual Studio 2010, it has normal executions, DLLs and other files, the > structure looks exactly like those we manually build on Linux and Mac. > PolyML cannot be built in Mingw32 or Cygwin32 using GCC compilers, thus > trying to build HOL in pure Cygwin environment results into failure. So we > can expect the final HOL build should be able to run standalone in Windows > CMD shell, if this plan works. MosML shouldn’t be considered at all. > > I ever tried to make some initial fixes. The most obvious issue is that, > HOL’s ML code used functions from the “Posix” structure, but this structure > is not available on Windows. Some of these unavailable functions can be > found in OS structure, which is available on all platforms. Others may need > to be manually implemented on Windows using functions from OS or Windows > structures. Also, when detecting the location of executions, HOL’s ML code > doesn’t consider “.exe” as part of file name at all. These are all minor > issues is irrelevant to the theorem proving related code. However, I’m not > an experienced ML programmer (I’m actually a Common Lisp programmer), can’t > do complex ML coding at current moment … > > > On 17 January 2017 at 00:23, wrote: > >> If you are using the working copy of HOL from the git repository, you >> should check the release notes in HOLDIR/doc. We document major >> incompatibilities there. >> >> Note also that the last official release was K10. There is a tag for K11 >> in the repository, and some release notes for it, but it hasn’t been >> released due to issues with the Windows build. The change to PAT_ASSUM is >> documented in doc/next-release.md, which will eventually be renamed to >> the K12 release notes in all likelihood. >> >> The working repo did not have corrected .doc files for those functions >> though, so thank you very much for writing those! >> >> Michael >> >> On 17/1/17, 05:47, "Chun Tian (binghe)" wrote: >> >> Hi, >> >> HOL Reference said that, PAT_ASSUM "Finds the first assumption that >> matches the term argument, applies the theorem tactic to it, and removes >> this assumption.” But I found it actually doesn’t remove the assumption in >> latest Kananaskis 11. >> >> To see this, try the following goal (open listTheory first): >> >> > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; >> val it = >>Proof manager status: 1 proof. >> 1. Incomplete goalstack: >> Initial goal: >> ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l >> : >>proofs >> >> First I rewrite it: >> >> > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); >> OK.. >> 1 subgoal: >> val it = >> FILTER ($= x) l = [x] >> >> 0. ∀x. >> (x = h) ∨ MEM x l ⇒ >> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = >> [x]) >> 1. MEM x l >> : >>proof >> >> Then I want to pick the assumption 0 and specialize the quantifier >> with `x`: >> >> > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); >> <> >> OK.. >> 1 subgoal: >> val it = >> ((x = h) ∨ MEM x l ⇒ >> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ >> (FILTER ($= x) l = [x]) >> >> 0. ∀x. >> (x = h) ∨ MEM x l ⇒ >> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = >> [x]) >> 1. MEM x l >> : >>proof >> > >> >> Now you can see, the assumption 0 is still here. It’s not removed as >> the manual said. >> >> In Kananaskis 10, the behavior is exactly the same as described in >> the manual: >> >> - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; >> <> >> > val it = >> Proof manager status: 1 proof. >> 1. Incomplete goalstack: >> Initial goal: >> ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l >> : proofs >> >> - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); >> OK.. >> 1 subgoal: >> > val it = >> FILTER ($= x) l = [x] >> >> 0. ∀x. >> (x = h) ∨ MEM x l ⇒ >> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) >> = [x]) >> 1. MEM x l >> : proof >> >> - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`))
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
No, it’s actually my pleasure to make a little contribution. For the Windows build issue, I think the correct path is to try to build HOL using the PolyML (32bit and 64bit) and Cygwin environment shipped with Isabelle2016-1 (installed on Windows 10). This version of PolyML is built by Visual Studio 2010, it has normal executions, DLLs and other files, the structure looks exactly like those we manually build on Linux and Mac. PolyML cannot be built in Mingw32 or Cygwin32 using GCC compilers, thus trying to build HOL in pure Cygwin environment results into failure. So we can expect the final HOL build should be able to run standalone in Windows CMD shell, if this plan works. MosML shouldn’t be considered at all. I ever tried to make some initial fixes. The most obvious issue is that, HOL’s ML code used functions from the “Posix” structure, but this structure is not available on Windows. Some of these unavailable functions can be found in OS structure, which is available on all platforms. Others may need to be manually implemented on Windows using functions from OS or Windows structures. Also, when detecting the location of executions, HOL’s ML code doesn’t consider “.exe” as part of file name at all. These are all minor issues is irrelevant to the theorem proving related code. However, I’m not an experienced ML programmer (I’m actually a Common Lisp programmer), can’t do complex ML coding at current moment … On 17 January 2017 at 00:23, wrote: > If you are using the working copy of HOL from the git repository, you > should check the release notes in HOLDIR/doc. We document major > incompatibilities there. > > Note also that the last official release was K10. There is a tag for K11 > in the repository, and some release notes for it, but it hasn’t been > released due to issues with the Windows build. The change to PAT_ASSUM is > documented in doc/next-release.md, which will eventually be renamed to > the K12 release notes in all likelihood. > > The working repo did not have corrected .doc files for those functions > though, so thank you very much for writing those! > > Michael > > On 17/1/17, 05:47, "Chun Tian (binghe)" wrote: > > Hi, > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that > matches the term argument, applies the theorem tactic to it, and removes > this assumption.” But I found it actually doesn’t remove the assumption in > latest Kananaskis 11. > > To see this, try the following goal (open listTheory first): > > > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > val it = >Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : >proofs > > First I rewrite it: > > > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > Then I want to pick the assumption 0 and specialize the quantifier > with `x`: > > > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > > > Now you can see, the assumption 0 is still here. It’s not removed as > the manual said. > > In Kananaskis 10, the behavior is exactly the same as described in the > manual: > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > <> > > val it = > Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : proofs > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > > val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = > [x]) > 1. MEM x l > : proof > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > MEM x l > : proof > > See, the used assumption has been removed. > > > Now let’s insist that, the behavior in latest Kananaskis 11 is more > reasonable (thus we should up
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
There hasn’t been any change in FIRST_ASSUM and FIRST_X_ASSUM. As always, FIRST_ASSUM leaves the assumption in place, and FIRST_X_ASSUM pulls it out. Michael From: Konrad Slind Date: Tuesday, 17 January 2017 at 15:22 To: "Norrish, Michael (Data61, Canberra City)" Cc: HOL-info mailing list Subject: Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) Oh, and the other thing that now bites (I think) is the FIRST_ASSUM --> FIRST_X_ASSUM replacement, which, if not done, can derail proofs. Konrad. On Mon, Jan 16, 2017 at 5:47 PM, mailto:michael.norr...@data61.csiro.au>> wrote: There were really two changes. If it was just a rename, then a find-and-replace (pat_assum -> pat_x_assum) would solve all the problems. However, there was another change to do with the handling of free variables in the pattern. As per the release notes, that change might require the use of underscores where previously needlessly specific variable names were being used. Michael From: Konrad Slind mailto:konrad.sl...@gmail.com>> Date: Tuesday, 17 January 2017 at 07:41 To: Thomas Tuerk mailto:tho...@tuerk-brechen.de>> Cc: HOL-info mailing list mailto:hol-info@lists.sourceforge.net>> Subject: Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has caused me a lot of pain. I can see the argument for the renaming, but it has broken a lot of proofs. Konrad. On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk mailto:tho...@tuerk-brechen.de>> wrote: Hi Chun, PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit fa81d70b67a61d6eddc6a517f968594c21be384d https://github.com/HOL-Theorem-Prover/HOL/commit/fa81d70b67a61d6eddc6a517f968594c21be384d for details and explanation. The reason was to unify naming. The X actually indicates that the assumption is removed, while the version without X keeps it. So in order to get your old proof working, you just need to replace "PAT_ASSUM" with "PAT_X_ASSUM". Best Thomas Tuerk On 16.01.2017 19:47, Chun Tian (binghe) wrote: > Hi, > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches > the term argument, applies the theorem tactic to it, and removes this > assumption.” But I found it actually doesn’t remove the assumption in latest > Kananaskis 11. > > To see this, try the following goal (open listTheory first): > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > val it = >Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : >proofs > > First I rewrite it: > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > Then I want to pick the assumption 0 and specialize the quantifier with `x`: > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > In Kananaskis 10, the behavior is exactly the same as described in the manual: > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > <> >> val it = > Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : proofs > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: >> val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : proof > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: >> val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > MEM x l > : proof > > See, the used assumption has been removed. > > > Now let’s insist that, the behavior
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Oh, and the other thing that now bites (I think) is the FIRST_ASSUM --> FIRST_X_ASSUM replacement, which, if not done, can derail proofs. Konrad. On Mon, Jan 16, 2017 at 5:47 PM, wrote: > There were really two changes. If it was just a rename, then a > find-and-replace (pat_assum -> pat_x_assum) would solve all the problems. > However, there was another change to do with the handling of free variables > in the pattern. As per the release notes, that change might require the > use of underscores where previously needlessly specific variable names were > being used. > > > > Michael > > > > *From: *Konrad Slind > *Date: *Tuesday, 17 January 2017 at 07:41 > *To: *Thomas Tuerk > *Cc: *HOL-info mailing list > *Subject: *Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? > (and a theorem cannot be proved in K11 any more) > > > > I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has > > caused me a lot of pain. I can see the argument for the renaming, but > > it has broken a lot of proofs. > > > > Konrad. > > > > > > On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk > wrote: > > Hi Chun, > > PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit > fa81d70b67a61d6eddc6a517f968594c21be384d > > https://github.com/HOL-Theorem-Prover/HOL/commit/ > fa81d70b67a61d6eddc6a517f968594c21be384d > > for details and explanation. The reason was to unify naming. The X > actually indicates that the assumption is removed, while the version > without X keeps it. So in order to get your old proof working, you just > need to replace "PAT_ASSUM" with "PAT_X_ASSUM". > > Best > > Thomas Tuerk > > On 16.01.2017 19:47, Chun Tian (binghe) wrote: > > Hi, > > > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that > matches the term argument, applies the theorem tactic to it, and removes > this assumption.” But I found it actually doesn’t remove the assumption in > latest Kananaskis 11. > > > > To see this, try the following goal (open listTheory first): > > > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > > val it = > >Proof manager status: 1 proof. > > 1. Incomplete goalstack: > > Initial goal: > > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > > : > >proofs > > > > First I rewrite it: > > > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > > OK.. > > 1 subgoal: > > val it = > > FILTER ($= x) l = [x] > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > > 1. MEM x l > > : > >proof > > > > Then I want to pick the assumption 0 and specialize the quantifier with > `x`: > > > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > > <> > > OK.. > > 1 subgoal: > > val it = > > ((x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > > (FILTER ($= x) l = [x]) > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > > 1. MEM x l > > : > >proof > > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > > > In Kananaskis 10, the behavior is exactly the same as described in the > manual: > > > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > > <> > >> val it = > > Proof manager status: 1 proof. > > 1. Incomplete goalstack: > > Initial goal: > > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > > : proofs > > > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > > OK.. > > 1 subgoal: > >> val it = > > FILTER ($= x) l = [x] > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = > [x]) > > 1. MEM x l > > : proof > > > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > > <> > > OK.. > > 1 subgoal: > >> val it = > > ((x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > > (FILTER ($= x) l = [x]) > > > > MEM x l > > : proof > > > > See, t
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
There were really two changes. If it was just a rename, then a find-and-replace (pat_assum -> pat_x_assum) would solve all the problems. However, there was another change to do with the handling of free variables in the pattern. As per the release notes, that change might require the use of underscores where previously needlessly specific variable names were being used. Michael From: Konrad Slind Date: Tuesday, 17 January 2017 at 07:41 To: Thomas Tuerk Cc: HOL-info mailing list Subject: Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more) I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has caused me a lot of pain. I can see the argument for the renaming, but it has broken a lot of proofs. Konrad. On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk mailto:tho...@tuerk-brechen.de>> wrote: Hi Chun, PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit fa81d70b67a61d6eddc6a517f968594c21be384d https://github.com/HOL-Theorem-Prover/HOL/commit/fa81d70b67a61d6eddc6a517f968594c21be384d for details and explanation. The reason was to unify naming. The X actually indicates that the assumption is removed, while the version without X keeps it. So in order to get your old proof working, you just need to replace "PAT_ASSUM" with "PAT_X_ASSUM". Best Thomas Tuerk On 16.01.2017 19:47, Chun Tian (binghe) wrote: > Hi, > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches > the term argument, applies the theorem tactic to it, and removes this > assumption.” But I found it actually doesn’t remove the assumption in latest > Kananaskis 11. > > To see this, try the following goal (open listTheory first): > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > val it = >Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : >proofs > > First I rewrite it: > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > Then I want to pick the assumption 0 and specialize the quantifier with `x`: > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > In Kananaskis 10, the behavior is exactly the same as described in the manual: > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > <> >> val it = > Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : proofs > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: >> val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : proof > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: >> val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > MEM x l > : proof > > See, the used assumption has been removed. > > > Now let’s insist that, the behavior in latest Kananaskis 11 is more > reasonable (thus we should update the manual), because later we may be able > to use the assumption again for another different purpose. Now to finish the > proof, in Kananaskis 10 a single rewrite almost finish the job using theorem > FILTER_NEQ_NIL: > > - FILTER_NEQ_NIL; >> val it = > |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x > : thm > - e (RW_TAC std_ss [FILTER_NEQ_NIL]); > OK.. > 1 subgoal: >> val it = > MEM h l > > MEM h l > : proof > > Now the goal is the same as the only assumption left: > > - e (FIRST_ASSUM ACCEPT_TAC); > OK.. > > Goal proved. > [.] |- MEM h l > > Goal proved. >
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
If you are using the working copy of HOL from the git repository, you should check the release notes in HOLDIR/doc. We document major incompatibilities there. Note also that the last official release was K10. There is a tag for K11 in the repository, and some release notes for it, but it hasn’t been released due to issues with the Windows build. The change to PAT_ASSUM is documented in doc/next-release.md, which will eventually be renamed to the K12 release notes in all likelihood. The working repo did not have corrected .doc files for those functions though, so thank you very much for writing those! Michael On 17/1/17, 05:47, "Chun Tian (binghe)" wrote: Hi, HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches the term argument, applies the theorem tactic to it, and removes this assumption.” But I found it actually doesn’t remove the assumption in latest Kananaskis 11. To see this, try the following goal (open listTheory first): > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l : proofs First I rewrite it: > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); OK.. 1 subgoal: val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof Then I want to pick the assumption 0 and specialize the quantifier with `x`: > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); <> OK.. 1 subgoal: val it = ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof > Now you can see, the assumption 0 is still here. It’s not removed as the manual said. In Kananaskis 10, the behavior is exactly the same as described in the manual: - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; <> > val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l : proofs - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); OK.. 1 subgoal: > val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); <> OK.. 1 subgoal: > val it = ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) MEM x l : proof See, the used assumption has been removed. Now let’s insist that, the behavior in latest Kananaskis 11 is more reasonable (thus we should update the manual), because later we may be able to use the assumption again for another different purpose. Now to finish the proof, in Kananaskis 10 a single rewrite almost finish the job using theorem FILTER_NEQ_NIL: - FILTER_NEQ_NIL; > val it = |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x : thm - e (RW_TAC std_ss [FILTER_NEQ_NIL]); OK.. 1 subgoal: > val it = MEM h l MEM h l : proof Now the goal is the same as the only assumption left: - e (FIRST_ASSUM ACCEPT_TAC); OK.. Goal proved. [.] |- MEM h l Goal proved. [.] |- ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) Goal proved. [..] |- FILTER ($= x) l = [x] But in Kananaskis 11 the same tactical cannot prove the theorem any more: > FILTER_NEQ_NIL; val it = |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x: thm > e (RW_TAC std_ss [FILTER_NEQ_NIL]); OK.. 1 subgoal: val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof In fact we’re going back to previous status before PAT_ASSUM was used! In short words, the following theorem definition doesn’t work any more: (it works in Kananaskis 10) (* BROKEN !!! *) val ALL
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
I have to say that the PAT_ASSUM --> PAT_X_ASSUM change has caused me a lot of pain. I can see the argument for the renaming, but it has broken a lot of proofs. Konrad. On Mon, Jan 16, 2017 at 1:06 PM, Thomas Tuerk wrote: > Hi Chun, > > PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit > fa81d70b67a61d6eddc6a517f968594c21be384d > > https://github.com/HOL-Theorem-Prover/HOL/commit/ > fa81d70b67a61d6eddc6a517f968594c21be384d > > for details and explanation. The reason was to unify naming. The X > actually indicates that the assumption is removed, while the version > without X keeps it. So in order to get your old proof working, you just > need to replace "PAT_ASSUM" with "PAT_X_ASSUM". > > Best > > Thomas Tuerk > On 16.01.2017 19:47, Chun Tian (binghe) wrote: > > Hi, > > > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that > matches the term argument, applies the theorem tactic to it, and removes > this assumption.” But I found it actually doesn’t remove the assumption in > latest Kananaskis 11. > > > > To see this, try the following goal (open listTheory first): > > > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > > val it = > >Proof manager status: 1 proof. > > 1. Incomplete goalstack: > > Initial goal: > > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > > : > >proofs > > > > First I rewrite it: > > > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > > OK.. > > 1 subgoal: > > val it = > > FILTER ($= x) l = [x] > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > > 1. MEM x l > > : > >proof > > > > Then I want to pick the assumption 0 and specialize the quantifier with > `x`: > > > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > > <> > > OK.. > > 1 subgoal: > > val it = > > ((x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > > (FILTER ($= x) l = [x]) > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > > 1. MEM x l > > : > >proof > > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > > > In Kananaskis 10, the behavior is exactly the same as described in the > manual: > > > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > > <> > >> val it = > > Proof manager status: 1 proof. > > 1. Incomplete goalstack: > > Initial goal: > > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > > : proofs > > > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > > OK.. > > 1 subgoal: > >> val it = > > FILTER ($= x) l = [x] > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = > [x]) > > 1. MEM x l > > : proof > > > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > > <> > > OK.. > > 1 subgoal: > >> val it = > > ((x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > > (FILTER ($= x) l = [x]) > > > > MEM x l > > : proof > > > > See, the used assumption has been removed. > > > > > > Now let’s insist that, the behavior in latest Kananaskis 11 is more > reasonable (thus we should update the manual), because later we may be able > to use the assumption again for another different purpose. Now to finish > the proof, in Kananaskis 10 a single rewrite almost finish the job using > theorem FILTER_NEQ_NIL: > > > > - FILTER_NEQ_NIL; > >> val it = > > |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x > > : thm > > - e (RW_TAC std_ss [FILTER_NEQ_NIL]); > > OK.. > > 1 subgoal: > >> val it = > > MEM h l > > > > MEM h l > > : proof > > > > Now the goal is the same as the only assumption left: > > > > - e (FIRST_ASSUM ACCEPT_TAC); > > OK.. > > > > Goal proved. > > [.] |- MEM h l > > > > Goal proved. > > [.] > > |- ((x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > >(FILTER ($= x) l = [x]) > > > > Goal proved. > > [..] |- FILTER ($= x) l = [x] > > > > But in Kananaskis 11 the same tactical cannot prove the theorem any more: > > > >> FILTER_NEQ_NIL; > > val it = > >|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x: > >thm > > > >> e (RW_TAC std_ss [FILTER_NEQ_NIL]); > > OK.. > > 1 subgoal: > > val it = > > > > FILTER ($= x) l = [x] > > > > 0. ∀x. > > (x = h) ∨ MEM x l ⇒ > > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > > 1. MEM x l > > : > >proof > > > > In fact we’re going back to previous status before PAT_ASSUM was used! > In short words, the following theorem definition doesn’t work any more: (it > wo
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Hi Chun, PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit fa81d70b67a61d6eddc6a517f968594c21be384d https://github.com/HOL-Theorem-Prover/HOL/commit/fa81d70b67a61d6eddc6a517f968594c21be384d for details and explanation. The reason was to unify naming. The X actually indicates that the assumption is removed, while the version without X keeps it. So in order to get your old proof working, you just need to replace "PAT_ASSUM" with "PAT_X_ASSUM". Best Thomas Tuerk On 16.01.2017 19:47, Chun Tian (binghe) wrote: > Hi, > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches > the term argument, applies the theorem tactic to it, and removes this > assumption.” But I found it actually doesn’t remove the assumption in latest > Kananaskis 11. > > To see this, try the following goal (open listTheory first): > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > val it = >Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : >proofs > > First I rewrite it: > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > Then I want to pick the assumption 0 and specialize the quantifier with `x`: > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > In Kananaskis 10, the behavior is exactly the same as described in the manual: > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > <> >> val it = > Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : proofs > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: >> val it = > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : proof > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: >> val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > MEM x l > : proof > > See, the used assumption has been removed. > > > Now let’s insist that, the behavior in latest Kananaskis 11 is more > reasonable (thus we should update the manual), because later we may be able > to use the assumption again for another different purpose. Now to finish the > proof, in Kananaskis 10 a single rewrite almost finish the job using theorem > FILTER_NEQ_NIL: > > - FILTER_NEQ_NIL; >> val it = > |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x > : thm > - e (RW_TAC std_ss [FILTER_NEQ_NIL]); > OK.. > 1 subgoal: >> val it = > MEM h l > > MEM h l > : proof > > Now the goal is the same as the only assumption left: > > - e (FIRST_ASSUM ACCEPT_TAC); > OK.. > > Goal proved. > [.] |- MEM h l > > Goal proved. > [.] > |- ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ >(FILTER ($= x) l = [x]) > > Goal proved. > [..] |- FILTER ($= x) l = [x] > > But in Kananaskis 11 the same tactical cannot prove the theorem any more: > >> FILTER_NEQ_NIL; > val it = >|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x: >thm > >> e (RW_TAC std_ss [FILTER_NEQ_NIL]); > OK.. > 1 subgoal: > val it = > > FILTER ($= x) l = [x] > > 0. ∀x. > (x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : >proof > > In fact we’re going back to previous status before PAT_ASSUM was used! In > short words, the following theorem definition doesn’t work any more: (it > works in Kananaskis 10) > > > (* BROKEN !!! *) > val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", > ``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, > RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN > PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`) THEN > RW_TAC std_ss [FILTER_NEQ_NIL] THEN > FIRST_ASSUM ACCEPT_TAC); > > > Could anyone please explain these strange behaviors and point out a correct > way to prove this theorem? (it’s actually part of the HOL-ACL2 bridge, > defined in “examples/acl2/ml/fmap_e
Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Hi again, Actually I found a solution: val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", ``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN Q.PAT_X_ASSUM `!y. P` (MP_TAC o Q.SPEC `x`) THEN RW_TAC std_ss [FILTER_NEQ_NIL] THEN FIRST_ASSUM ACCEPT_TAC); That is, using Q.PAT_X_ASSUM instead of PAT_ASSUM. Q.PAT_X_ASSUM correctly removed the used assumption. But I still don’t understand why such an extra seeming useless assumption could prevent the rest tactics proving the theorem ... I luckily found this by comparing the proof of probability theorems between K10 and K11, while PAT_X_ASSUM is not mentioned in the manual at all. How to proceed? I write a reference page for it? Regards, Chun > Il giorno 16/gen/2017, alle ore 19:47, Chun Tian (binghe) > ha scritto: > > Hi, > > HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches > the term argument, applies the theorem tactic to it, and removes this > assumption.” But I found it actually doesn’t remove the assumption in latest > Kananaskis 11. > > To see this, try the following goal (open listTheory first): > >> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > val it = > Proof manager status: 1 proof. > 1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : > proofs > > First I rewrite it: > >> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: > val it = > FILTER ($= x) l = [x] > > 0. ∀x. >(x = h) ∨ MEM x l ⇒ >((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : > proof > > Then I want to pick the assumption 0 and specialize the quantifier with `x`: > >> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: > val it = > ((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > 0. ∀x. >(x = h) ∨ MEM x l ⇒ >((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : > proof >> > > Now you can see, the assumption 0 is still here. It’s not removed as the > manual said. > > In Kananaskis 10, the behavior is exactly the same as described in the manual: > > - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; > <> >> val it = >Proof manager status: 1 proof. >1. Incomplete goalstack: > Initial goal: > ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l > : proofs > > - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); > OK.. > 1 subgoal: >> val it = >FILTER ($= x) l = [x] > > 0. ∀x. >(x = h) ∨ MEM x l ⇒ >((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : proof > > - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); > <> > OK.. > 1 subgoal: >> val it = >((x = h) ∨ MEM x l ⇒ > ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ >(FILTER ($= x) l = [x]) > > MEM x l > : proof > > See, the used assumption has been removed. > > > Now let’s insist that, the behavior in latest Kananaskis 11 is more > reasonable (thus we should update the manual), because later we may be able > to use the assumption again for another different purpose. Now to finish the > proof, in Kananaskis 10 a single rewrite almost finish the job using theorem > FILTER_NEQ_NIL: > > - FILTER_NEQ_NIL; >> val it = >|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x > : thm > - e (RW_TAC std_ss [FILTER_NEQ_NIL]); > OK.. > 1 subgoal: >> val it = > >MEM h l > > MEM h l > : proof > > Now the goal is the same as the only assumption left: > > - e (FIRST_ASSUM ACCEPT_TAC); > OK.. > > Goal proved. > [.] |- MEM h l > > Goal proved. > [.] > |- ((x = h) ∨ MEM x l ⇒ >((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ > (FILTER ($= x) l = [x]) > > Goal proved. > [..] |- FILTER ($= x) l = [x] > > But in Kananaskis 11 the same tactical cannot prove the theorem any more: > >> FILTER_NEQ_NIL; > val it = > |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x: > thm > >> e (RW_TAC std_ss [FILTER_NEQ_NIL]); > OK.. > 1 subgoal: > val it = > > FILTER ($= x) l = [x] > > 0. ∀x. >(x = h) ∨ MEM x l ⇒ >((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) > 1. MEM x l > : > proof > > In fact we’re going back to previous status before PAT_ASSUM was used! In > short words, the following theorem definition doesn’t work any more: (it > works in Kananaskis 10) > > > (* BROKEN !!! *) > val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", >``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, >RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN >
[Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)
Hi, HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches the term argument, applies the theorem tactic to it, and removes this assumption.” But I found it actually doesn’t remove the assumption in latest Kananaskis 11. To see this, try the following goal (open listTheory first): > g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l : proofs First I rewrite it: > e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); OK.. 1 subgoal: val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof Then I want to pick the assumption 0 and specialize the quantifier with `x`: > e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); <> OK.. 1 subgoal: val it = ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof > Now you can see, the assumption 0 is still here. It’s not removed as the manual said. In Kananaskis 10, the behavior is exactly the same as described in the manual: - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`; <> > val it = Proof manager status: 1 proof. 1. Incomplete goalstack: Initial goal: ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l : proofs - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]); OK.. 1 subgoal: > val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`)); <> OK.. 1 subgoal: > val it = ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) MEM x l : proof See, the used assumption has been removed. Now let’s insist that, the behavior in latest Kananaskis 11 is more reasonable (thus we should update the manual), because later we may be able to use the assumption again for another different purpose. Now to finish the proof, in Kananaskis 10 a single rewrite almost finish the job using theorem FILTER_NEQ_NIL: - FILTER_NEQ_NIL; > val it = |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x : thm - e (RW_TAC std_ss [FILTER_NEQ_NIL]); OK.. 1 subgoal: > val it = MEM h l MEM h l : proof Now the goal is the same as the only assumption left: - e (FIRST_ASSUM ACCEPT_TAC); OK.. Goal proved. [.] |- MEM h l Goal proved. [.] |- ((x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒ (FILTER ($= x) l = [x]) Goal proved. [..] |- FILTER ($= x) l = [x] But in Kananaskis 11 the same tactical cannot prove the theorem any more: > FILTER_NEQ_NIL; val it = |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x: thm > e (RW_TAC std_ss [FILTER_NEQ_NIL]); OK.. 1 subgoal: val it = FILTER ($= x) l = [x] 0. ∀x. (x = h) ∨ MEM x l ⇒ ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x]) 1. MEM x l : proof In fact we’re going back to previous status before PAT_ASSUM was used! In short words, the following theorem definition doesn’t work any more: (it works in Kananaskis 10) (* BROKEN !!! *) val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS", ``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``, RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`) THEN RW_TAC std_ss [FILTER_NEQ_NIL] THEN FIRST_ASSUM ACCEPT_TAC); Could anyone please explain these strange behaviors and point out a correct way to prove this theorem? (it’s actually part of the HOL-ACL2 bridge, defined in “examples/acl2/ml/fmap_encodeScript.sml”) Best regards, Chun Tian signature.asc Description: Message signed with OpenPGP using GPGMail -- Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info