Hi Bill,
you're right. Indeed, part of the idea of automation tools is to
actually remove the burden of knowing precisely what's going on inside.
But they're not perfect so in practice, it turns out to actually be
useful to know about them. So knowing about the algorithms behind them
is still useful - but not necessary. I learnt about REWRITE_TAC and
SIMP_TAC simply by browsing HOL Light sources. Not saying it's the best
way but it brings a lot (REWRITE_TAC is relatively simple, if you need a
starting point).
In case you need heuristics to know which tactic to use in which
circumstences (they're heuristics, meaning they don't work all the time
;-) ):
- if you only make use of theorems of the form "!xyz. l = r", use
REWRITE_TAC
- if you also have theorems of the form "!xyz. p ==> l = r", use
SIMP_TAC (in which case you should also provide theorems allowing to
prove p)
- if you have existentials or disjunctions in the theorems you want to
use or in the goal, use MESON_TAC
- if you have quantifications over functions, REWRITE_TAC/SIMP_TAC *can*
still do better than MESON_TAC (but this is very tricky to know in
advance, hence - I guess - the final situation in your email).
- of course there is the obvious but essential point that MESON_TAC can
only be used to conclude a goal, and not to make progress in it (as you
pointed out already)
- REWRITE_TAC is faster than SIMP_TAC which is faster than MESON_TAC;
that's because each achieves a more complex reasoning than the other.
In theory, one could actually combine the power of REWRITE_TAC and
SIMP_TAC while preserving the efficiency, by defining a tactic that
would just inspect the input theorems, and, if a theorem of the form
"!xyz. p ==> l = r" is present, call SIMP_TAC, and otherwise call
REWRITE_TAC. Maybe this is done in HOL4 already, dunno. The only
obstacle I see right now is that is that theorems of form "!xyz. p ==> l
= r" are still useful to REWRITE_TAC since they are interpreted as
"!xyz. (p ==> l = r) = T". I don't know which impact it would have in
practice though.
Regarding your last theorem, yeah it's a bit tricky... Note that you can
simply do this however:
let INTERIOR_EQ = theorem `;
∀s. interior s = s ⇔ open s
proof
simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq
EQ_SYM_EQ;
qed;
`;;
Cheers,
V.
On 18.02.2014 06:00, Bill Richter wrote:
> 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.
>
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH <www.fortiss.org/en>
T +49 (0)89 360 35 22 33 | Fx +49 (0)89 360 35 22 50
Guerickestrasse 25 | 80805 Munich | Germany
------------------------------------------------------------------------------
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
