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)
> <binghe.l...@gmail.com> 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`));
> <<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
>
>
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
