If you are using the working copy of HOL from the git repository, you should
check the release notes in HOLDIR/doc. We document major incompatibilities
there.
Note also that the last official release was K10. There is a tag for K11 in
the repository, and some release notes for it, but it hasn’t been released due
to issues with the Windows build. The change to PAT_ASSUM is documented in
doc/next-release.md, which will eventually be renamed to the K12 release notes
in all likelihood.
The working repo did not have corrected .doc files for those functions though,
so thank you very much for writing those!
Michael
On 17/1/17, 05:47, "Chun Tian (binghe)" <binghe.l...@gmail.com> 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
