Hello Bill,
On 02/01/2013 06:22, Bill Richter wrote:
> Thanks, Petros, but I don't see how SUBGOAL_TAC is any better than
> SUBGOAL_THEN at avoiding the one-step-forward-one-step-back awkwardness of
> MP_TAC/DISCH_THEN ASSUME_TAC/FIRST_X_ASSUM that John's cases and the
> modification bcases have.
Only indirectly, I guess, since the ASSUME_TAC or MP_TAC step is
implicit in SUBGOAL_TAC.
> BTW how does HOL and Informatics fit together?
How do they not? :)
They are connected in so many ways...
>
> but as you say that won't work unless I can calculate how my disjuncts I'll
> get. There must be a function that calculates that. In the first bcases
> below, it's 2, and it's 3 for the second. I also don't know how to print a
> variable number of ALL_TACs. I thought maybe I could try
> SUBGOAL_THEN t ALL_TAC THENL [SUBGOAL_THEN t ALL_TAC; ALL_TAC]
> so the top 3 goals in the goalstack would be (for g the original top goal)
> t, t, and g
> But that won't fly, because
> MP_TAC is a thm_tactic, and ALL_TAC is just a tactic. I that the correct
> usage? And that's the difference between SUBGOAL_THEN and SUBGOAL_TAC,
> whether you use a thm_tactic or a tactic? BTW how do I learn the typed LC or
> whatever that explains how tactics and thm_tactics actually work? The HOL
> Light tutorial I think is actually a pretty good way to learn how to write
> tactics proofs, if you read the whole tutorial from beginning to end, dipping
> into the reference manual (and posting here!) when you get stuck, but I don't
> think it explains the theory of tactics proofs. Maybe I missed it.
>
I am not exactly sure what you are trying to accomplish here.
I'll try to explain a few things as simply and as best I can:
A thm_tactic roughly corresponds to a forward reasoning step, whereas a
tactic roughly corresponds to a backwards step.
A thm_tactic expects a theorem (often one of the assumptions) as an
argument, and does something with it (its conclusion to be more precise).
That's why SUBGOAL_THEN requires a thm_tactic. You provide a SUBGOAL and
THEN the thm_tactic does something to/with it.
Same goes for DISCH_THEN. It DISCHarges an antecedent (which is now an
assumption/theorem) and THEN uses a thm_tactic on it.
eg. MP_TAC adds it as an antecedent to the goal, while ASSUME_TAC adds
it as an assumption.
(Note how DISCH_TAC is *roughly* equivalent to DISCH_THEN ASSUME_TAC.)
Examples:
e (MP_TAC LT_0);; (* adds `!n. 0 < SUC n` as an antecedent to the goal *)
e (ASSUME_TAC LT_0);; (* adds `!n. 0 < SUC n` as an assumption *)
e (FIRST_ASSUM MP_TAC);; (* adds the first assumption as an antecedent -
the opposite of DISCH_TAC *)
Tactics (traditionally and usually) apply their effects to the goal.
The difference between SUBGOAL_THEN and SUBGOAL_TAC is deeper than this.
Both of them introduce two new subgoals:
Subgoal (A) is your original subgoal, where your newly introduced t is
also available.
Subgoal (B) is a new subgoal where you need to prove t with your
original assumptions.
** The thm_tactic given to SUBGOAL_THEN is applied to t in subgoal (A).
ie. it allows you to take an extra step in your original subgoal using
t. This step can be as simple as introducing t as an assumption
(ASSUME_TAC) or an antecedent (MP_TAC), or more complicated:
eg. from a previous email:
eliminatean existential quantifier from t and then add the result as an
assumption:
SUBGOAL_THEN t (X_CHOOSE_THEN `foo:bar` ASSUME_TAC)
** The tactic given to SUBGOAL_TAC is applied to subgoal (B).
ie. the tactic given to SUBGOAL_TAC works towards (and possibly proves)
t. If the tactic can completely prove t, subgoal (B) will be eliminated
in the same step and not appear to the user at all. The difference here
is that you do not (immediately) control what happens to t in (A),
except only through its new label in subsequent steps. (Depending on
your style and what you want to do this may be a good or a bad thing.)
Note that "SUBGOAL_TAC tm s [p]" is defined as:
SUBGOAL_THEN tm (LABEL_TAC s) THENL [p; ALL_TAC]
What you are trying to do:
SUBGOAL_THEN t ALL_TAC ...
is like saying: "introduce subgoal t then do nothing (ALL_TAC)".
You need to provide a thm_tactic so that you do "something" with t (as
trivial or as complicated this "something" is).
That being said (and in hope that this will not confuse you further),
you can use a tactic as a thm_tactic if that is what you *really* need.
For example if you want to use t once to simplify your goal (and then
throw t away) you can do this:
SUBGOAL_THEN t (fun t -> SIMP_TAC[t])
Note that t will *not* appear in the new subgoal (as you have not added
it as an assumption or as an antecedent). Of course you can do both if
you so desire:
SUBGOAL_THEN t (fun t -> SIMP_TAC[t] THEN ASSUME_TAC t)
Now, just to give you a more concrete idea of what I meant in the
previous email in the context of the "cases" tactic from p.78 of the
tutorial you've been looking at:
let cases (lab,t) tac =
SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
is equivalent to:
let cases (lab,t) tac =
SUBGOAL_TAC lab t [tac] THEN
REMOVE_THEN lab (REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
(but this is not as clean as the original - it only makes the MP_TAC
step implicit)
as well as equivalent to:
let cases (lab,t) tac =
(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab)) (prove (t,tac));;
which I think is closer to what you are looking for.
(As a side note, the original "cases" can be modified so that it is not
important if tac proves t completely or not, whereas this is not
possible with the two alternatives. This is why I noted in the last
email that it is assumed that tac proves t.)
Hope I have helped and not complicated things for you any further!
Regards,
Petros
--
Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: [email protected]
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122712
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
