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> 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>
> *Date: *Tuesday, 17 January 2017 at 07:41
> *To: *Thomas Tuerk <tho...@tuerk-brechen.de>
> *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)
>
>
>
> 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>
> 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
> > 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
>
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
>
------------------------------------------------------------------------------
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
