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 <konrad.sl...@gmail.com>
Date: Tuesday, 17 January 2017 at 15:22
To: "Norrish, Michael (Data61, Canberra City)" <michael.norr...@data61.csiro.au>
Cc: HOL-info mailing list <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)
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,
<michael.norr...@data61.csiro.au<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 <konrad.sl...@gmail.com<mailto:konrad.sl...@gmail.com>>
Date: Tuesday, 17 January 2017 at 07:41
To: Thomas Tuerk <tho...@tuerk-brechen.de<mailto:tho...@tuerk-brechen.de>>
Cc: HOL-info mailing list
<hol-info@lists.sourceforge.net<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
<tho...@tuerk-brechen.de<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`));
> <<HOL message: inventing new type variable names: 'a>>
> 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`;
> <<HOL message: inventing new type variable names: 'a>>
>> 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`));
> <<HOL message: inventing new type variable names: 'a>>
> 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
>
>
>
>
> ------------------------------------------------------------------------------
> 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<mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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
