Thanks for explaining the ((asl,w) as g) of tactics.ml, Vince! I now see your
explanation is also in ocaml-4.00-refman.pdf, sec 6.6 Patterns. I know you
told me about your HOL-Light-Q, but you told me not to read it, and you did not
tell me how to get the nonempty environment we need. But it's fine! It was a
great pleasure to work your exercise, even if I didn't figure out anything new.
I think we had a communication failure based on miz3, so I'll say a little
more about it:
I don't know the syntax of miz3 proofs so I can't tell.
I only want to remove inferrable type annotations to improve the readability of
the code. Do you agree? But that's not the only readability issue. Here's
the same proof in both miz3 (from Examples/inverse_bug_puzzle_miz3.ml) and my
new type annotation reducing code. If you look, I think you'll say that the
miz3 proof is a lot more readable:
let FourStepMoveABBAreach = thm `;
let A B C A' B' C' be real^2;
assume ~collinear {A,B,C} [H1];
assume move2Cond (A,B,C) (A',B',C') [H2];
thus ? Y. reachableN (A,B,C) (A',B',Y) 4
proof
cases by H2, move2Cond;
suppose ~collinear {B,A,A'} /\ ~collinear {A',B,B'};
qed by H1, -, FourStepMoveAB, reachableN_Four;
suppose ~collinear {A,B,B'} /\ ~collinear {B',A,A'} [Case2];
~collinear {B,A,C} by H1, collinearSymmetry;
consider X Y such that
move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y) by -, Case2,
FourStepMoveAB;
qed by -, moveSymmetry, reachableN_Four;
end;
`;;
let FourStepMoveABBAreach = prove
(`∀A B C A' B'. ¬collinear {A,B,C} ∧ move2Cond A B A' B' ⇒
∃ Y. reachableN (A,B,C) (A',B',Y) 4`,
INTRO_TAC "∀A B C A' B'; H1 H2" THEN
case_split "Case1 | Case2"
[`"¬collinear {B,A,A'} ∧ ¬collinear {A',B,B'}`;
`"¬collinear {A,B,B'} ∧ ¬collinear {B',A,A'}`]
[HYP MESON_TAC "H2" [move2Cond]]
THENL
[so (HYP MESON_TAC "H1" [FourStepMoveAB; reachableN_Four]);
subgoal_TAC "" `"¬collinear {B,A,C}`
[HYP MESON_TAC "H1" [collinearSymmetry]]] THEN
subgoal_TAC "" `"¬collinear {B,A,C}`
[HYP MESON_TAC "H1" [collinearSymmetry]] THEN
consider `"X Y such that
move (B,A,C) (B,A,X) ∧ move (B,A,X) (B',A,X) ∧
move (B',A,X) (B',A,Y) ∧ move (B',A,Y) (B',A',Y)`
[so (HYP MESON_TAC "Case2" [FourStepMoveAB])] "BAX" THEN
HYP MESON_TAC "BAX" [moveSymmetry; reachableN_Four]);;
Note that the miz3 proof has no type annotations beyond the initial
let A B C A' B' C' be real^2;
That helps readability, but my tactics proof above has no type annotations, and
it's a lot less readable, because of all the TACs, backquotes, doublequotes,
square braces, and 6 occurrences of MESON_TAC, which is used silently in the
miz3 code. I think it wouldn't be too hard to write a Ocaml program using the
str library to produce my tactics proof above from a string written more like
my miz3 proof above. But now look at miz3/miz3.ml, which performs some such
translation with preterms instead of strings. It looks really hard to read.
Or look at the first such code, John's Examples/mizar.ml, which ends with nice
readable proof of the Knaster-Tarski fixpoint theorem.
I'll try to dig up a specific debugging problem. I think I tried first to do
what you succeeded in:
For EXISTS_TAC, my code also extracts the type of the bound variable and
enforces the type of witness to be the same.
But my code didn't work, and I would have liked to debug it. I think my
solution should be adequate. How about explaining something really simple,
from your code https://github.com/aravantv/HOL-Light-Q. I think your c in
(asms,c as g) is the goal, and asms is the list of assumptions (so g is
actually the goal)
let CONTEXT_TAC ttac (asms,c as g) =
let vs = frees c @ freesl (map (concl o snd) asms) in
ttac (map (fun x -> name_of x,pretype_of_type(type_of x)) vs) g
But I'd like to run some kind of a test to be sure of that. It's not obvious
how you'd run such a test, because a tactic is a function goal -> goalstate, so
the only way I would know how to test this is to set up an interactive proof
which used a tactic. That's pretty indirect. BTW is the reason you don't need
double semicolons here because Pa is a module, explained in section 2 The
module system of the ocaml manual?
For SUBGOAL_THEN, it enforces the type of the overall expression to
be boolean (thanks to a remark by Michael Norrish, when I first
submitted this module on this mailing list). Same thing for
SUBGOAL_TAC.
Great for Michael, but why do you want that? What should be boolean here in my
version:
let (subgoal_THEN: string -> thm_tactic -> tactic) =
fun stm ttac (asl,w) ->
let wa = parse_env_string (make_env (asl,w)) stm in
let meta,gl,just = ttac (ASSUME wa) (asl,w) in
meta,(asl,wa)::gl,fun i l -> PROVE_HYP (hd l) (just i (tl l));;
--
Best,
Bill
------------------------------------------------------------------------------
Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET
Get 100% visibility into your production application - at no cost.
Code-level diagnostics for performance bottlenecks with <2% overhead
Download for free and get started troubleshooting in minutes.
http://p.sf.net/sfu/appdyn_d2d_ap1
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
