Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

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)

[Makarius]

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)

[Michael.Norrish]

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) 
> 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
   

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

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 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

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 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Michael.Norrish]

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, 
> 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, 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. 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Konrad Slind]

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, 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
> 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Michael.Norrish]

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, 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:
>

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Michael.Norrish]

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)


(* 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Konrad Slind]

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 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Thomas Tuerk]

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 

Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

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 

[Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Chun Tian (binghe)]

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