John, I'm sorry it took me so long to respond to your MP_TAC vs MESON_TAC post
of Jun 1:
| What's the difference between MESON_TAC[th1; th2; th3];; and
| MP_TAC th3;;
| MESON_TAC[th1; th2];;
The difference is that after MP_TAC any free variables or free type
variables effectively get "frozen" so they cannot be instantiated,
whereas when given directly to MESON_TAC, they can be generalized
and instantiated.
This makes a difference in general where the theorem concerned is
either not universally generalized or contains polymorphic types.
Sometimes it can be positively beneficial to "freeze" things, to
reduce search space or otherwise constrain later steps, and there
is a little-used theorem-tactical FREEZE_THEN to do this directly.
I think I have an example which illustrates your beneficial freezing. In the
current version of RichterHilbertAxiomGeometry/HilbertAxiom_read.ml, the proof
of AngleAddition has the SUBGOAL_TAC statement & proof using fol = MESON_TAC:
∃! r. Ray r ∧ ∃ X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O
X ≡ ∡ A' O' B' []
proof
MP_TAC SPECL [∡ A' O' B'; O; A; a; G] C4;
fol - angles Distinct a_line H1';
qed;
The original miz3 version didn't need MP_TAC SPECL, because miz3 uses your
HOL_BY from Examples/holby.ml, and I guess that handled the specialization. I
tried getting rid of the MP_TAC, but this didn't work:
∃! r. Ray r ∧ ∃ X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O
X ≡ ∡ A' O' B' []
proof
fol SPECL [∡ A' O' B'; O; A; a; G] C4 - angles Distinct a_line H1';
qed;
I quit with a MESON number of 24,145,469. This must be evidence for your
beneficial freezing, but I don't really get it. My guess is that the only
variables "not universally generalized" at this point in the proof are the
existential variables r and X, and that there are no "polymorphic types." BTW
C4 is an axiom with 5 universal variables:
C4 |- ∀ α O A l Y.
Angle α ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
⇒ ∃! r. Ray r ∧ ∃ B. ¬(O = B) ∧ r = ray O B ∧
B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α
Now replacing fol with simplify (SIMP_TAC) worked!
∃! r. Ray r ∧ ∃ X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O
X ≡ ∡ A' O' B' [] by simplify SPECL [∡ A' O' B'; O; A; a; G] C4 - angles
Distinct a_line H1';
Does that mean that SIMP_TAC doesn't need to "reduce search space or otherwise
constrain later steps" as much as MESON_TAC? I don't even need to SPECL now:
∃! r. Ray r ∧ ∃ X. ¬(O = X) ∧ r = ray O X ∧ X ∉ a ∧ X,G same_side a ∧ ∡ A O
X ≡ ∡ A' O' B' [] by simplify C4 - angles Distinct a_line H1';
--
Best,
Bill
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60133471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
