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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
