Thanks, Vince! I think we haven't quite gotten it right yet, as it's tricky to
talk about intentions. You correctly pointed out there was something wrong
with the way I used REWRITE_TAC[DIST_SYM]. John's proof uses ONCE_REWRITE_TAC
correctly, but he's using DIST_TRIANGLE_ALT, while I tried to get clever and
use DIST_TRIANGLE. You'll enjoy stepping through John's proof and checking
this.
I think it's fine to use powerful tools that aren't well understood/documented
as long as we're using those tools as they were intended. REWRITE_TAC,
SIMP_TAC and MESON_TAC are powerful tools to simplify a goal or to solve a
first order logic problem. If we're trying to solve/simplify, it's fine to use
these tools without knowing in advance how much solving/simplifying is going to
take place. Now I would really like to understand the exact algorithms used by
REWRITE_TAC, SIMP_TAC and MESON_TAC, and John posted that Tobias's paper
explains REWRITE_TAC, but I contend that there is little practical value to
such knowledge. It would just be nice to know. As long as we're using
complicated solve/simplify tools, we're not going to easily be able to
calculate in advance whether they will work. And this problem will only get
worse over time, as we develop even better solve/simplify tools.
The problem with my use of REWRITE_TAC[DIST_SYM] is that I didn't intend
maximal simplification. I got one out of three possible rewrites, and said,
"Hey, that's just what I wanted, I'll keep it!" So my error was using a
powerful simplification tool and intending that it didn't work very well.
That's gotta be bad coding.
Do you mean you don't know the technical differences between them
[REWRITE_TAC, MESON_TAC and SIMP_TAC]? or that you know them but
don't necessarily know which impact it has on their behaviour? Or
that you are really trying them completely randomly?
There's a lot I don't know. I know that MESON_TAC is a FOL prover, so will
fail if it doesn't solve the goal, while REWRITE_TAC and SIMP_TAC are
simplifiers, which may solve the goal. I think that SIMP_TAC is in all ways
more powerful than REWRITE_TAC, except that it will hang more often (trying to
simplify farther), so I try to use REWRITE_TAC instead of SIMP_TAC. I used to
think that SIMP_TAC was in all ways more powerful than MESON_TAC, but I know
now that this isn't true, from my in-progress (pushing 2800 lines) readable.ml
port RichterHilbertAxiomGeometry/Topology.ml of John's 20,000 line
Multivariate/topology.ml. I'm quite pleased to know this, BTW, that MESON_TAC
is actually better at FOL than SIMP_TAC. Michael N explained here that
MESON_TAC is not very good at equational reasoning, but that's what REWRITE_TAC
and SIMP_TAC are good at, so we ought to use MESON_TAC and REWRITE/SIMP_TAC
together. John of course understands the difference between MESON_TAC and
REWRITE/SIMP_TAC very well, and when he wrote the code he might well have known
what would work, but I can't just use his choices, because I have extra
assumptions. Let's look at one of John's theorems
let OPEN_IN_SUBTOPOLOGY_UNION = prove
(`!top s t u:A->bool.
open_in (subtopology top t) s /\ open_in (subtopology top u) s
==> open_in (subtopology top (t UNION u)) s`,
REPEAT GEN_TAC THEN REWRITE_TAC[OPEN_IN_SUBTOPOLOGY] THEN
DISCH_THEN(CONJUNCTS_THEN2
(X_CHOOSE_THEN `s':A->bool` STRIP_ASSUME_TAC)
(X_CHOOSE_THEN `t':A->bool` STRIP_ASSUME_TAC)) THEN
EXISTS_TAC `s' INTER t':A->bool` THEN ASM_SIMP_TAC[OPEN_IN_INTER] THEN
ASM SET_TAC[]);;
In my port, I had to change REWRITE_TAC to SIMP_TAC (simplify);
needs "RichterHilbertAxiomGeometry/Topology.ml";;
let OpenInSubtopologyUnion = theorem `;
∀α s t u. t ⊂ topspace α ∧ u ⊂ topspace α ⇒
open_in (subtopology α t) s ∧ open_in (subtopology α u) s
⇒ open_in (subtopology α (t ∪ u)) s
proof
intro_TAC ∀α s t u, Ht Hu;
simplify Ht Hu UNION_SUBSET OpenInSubtopology;
intro_TAC sOpenSub_t sOpenSub_u;
consider a b such that
open_in α a ∧ s = a ∩ t ∧
open_in α b ∧ s = b ∩ u [abExist] by fol sOpenSub_t sOpenSub_u;
exists_TAC a ∩ b;
set MESON [abExist; OPEN_IN_INTER] [open_in α (a ∩ b)] abExist;
qed;
`;;
and it fails if I change it to back to REWRITE_TAC (rewrite):
let OpenInSubtopologyUnion = theorem `;
∀α s t u. t ⊂ topspace α ∧ u ⊂ topspace α ⇒
open_in (subtopology α t) s ∧ open_in (subtopology α u) s
⇒ open_in (subtopology α (t ∪ u)) s
proof
intro_TAC ∀α s t u, Ht Hu;
rewrite Ht Hu UNION_SUBSET OpenInSubtopology;
intro_TAC sOpenSub_t sOpenSub_u;
consider a b such that
open_in α a ∧ s = a ∩ t ∧
open_in α b ∧ s = b ∩ u [abExist] by fol sOpenSub_t sOpenSub_u;
exists_TAC a ∩ b;
set MESON [abExist; OPEN_IN_INTER] [open_in α (a ∩ b)] abExist;
qed;
`;;
Warning: inventing type variables
0..0..0..0..0..1..2..3..4..5..6..7..8..9..10..11..12..13..14..15..16..17..18..23..28..33..38..43..48..53..58..63..76..89..102..115..128..141..154..167..180..203..226..249..272..295..318..341..364..387..420..Exception:
Failure("solve_goal: Too deep").
The reason is that I'm not just rewriting with OpenInSubtopology:
OpenInSubtopology
|- ∀α u s. u ⊂ topspace α
⇒ (open_in (subtopology α u) s ⇔ ∃t. open_in α t ∧ s = t ∩ u)
OpenInSubtopology needs an antecedent, which in our case is
t ∪ u ⊂ topspace α
and I know from experience that SIMP_TAC will compute this antecedent using the
assumptions
Ht & Hu and the theorem UNION_SUBSET.
If you go through my code and randomly permute rewrite, simplify and fol, you
might be surprised at what does and doesn't work. Look at the tail end of my
file Topology.ml, where I'm giving mostly 1-line proofs of John's Euclidean
theorems from the general topology theorems I proved above. Most of the proofs
start
by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ...
but sometimes I can change that to
by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN ...
and sometimes I need a longer proof. Here I can see why I need a longer proof:
let CLOSURE_INTERIOR = theorem `;
∀s. closure s = UNIV ━ interior (UNIV ━ s)
proof
rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosureInterior;
qed;
`;;
I'm using both TOPSPACE_EUCLIDEAN and its GSYM. Only MESON_TAC can do that.
Here's a 2-line proof:
let INTERIOR_EQ = theorem `;
∀s. interior s = s ⇔ open s
proof
simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq;
fol;
qed;
`;;
Neither SIMP_TAC nor MESON_TAC can prove this by themselves, and I don't know
why. I don't feel that I need to know. That's the point of powerful tools, to
do things I can't do in my head. I can't even in my head figure out which of
the two powerful tools will work, or whether they're both needed.
--
Best,
Bill
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
