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
