Thanks, Ramana! That's very helpful, clarifying DISCH_TAC and explaining
To keep things really simple: thm_tactic is just an abbreviation
for (thm -> tactic). That is, a thm_tactic is any function that
takes a theorem and returns a tactic.
Great, I didn't know how to parse the phrase thm_tactic!
E.g. with FIRST_ASSUM ttac, you can think of ttac as being a
theorem-parameterised tactic; then FIRST_ASSUM says to provide the
first assumption in the current goal as the theorem that makes ttac
into a tactic.
OK, I was using it that way in monkey-see-monkey-do fashion, but I didn't see
that with ttac having an actual meaning. I didn't realize this was incorrect,
as you next explain:
Sorry, I got the semantics of FIRST_ASSUM wrong: it's more subtle
(but irrelevant to the point I was making); it says to provide the
first assumption that makes the resulting tactic succeed (i.e. it
will backtrack and try each assumption in turn until the
constructed tactic doesn't fail).
Thanks! I did wonder why the term FIRST was used: I would have said
LAST_ASSUM, as the assumption number I always use is the highest number, not
the lowest. Let's go through an example I just wrote, a proof of the
LABEL_TAC manual exercise that doesn't use LABEL_TAC:
g `(!x y. x <<= y /\ y <<= x ==> x = y) /\
(!s. ~(s = {}) ==> ?a:A. a IN s /\ !x. x IN s ==> a <<= x)
==> (!x y. x <<= y \/ y <<= x) /\
(!x y z. x <<= y /\ y <<= z ==> x <<= z)`;;
e(REPEAT STRIP_TAC);;
e(FIRST_ASSUM (MP_TAC o SPEC `{x:A,y:A}`) THEN ASM SET_TAC[]);;
e(FIRST_ASSUM (MP_TAC o SPEC `{x:A,y:A,z:A}`) THEN ASM SET_TAC[]);;
Please check if I got this right. I still have trouble with SPEC and
composition. I see the "types" are
FIRST_ASSUM : thm_tactic -> tactic
SPEC : term -> thm -> thm
MP_TAC : thm_tactic
Thus SPEC `{x:A,y:A}` is a function of "type" :thm -> thm, and MP_TAC is a
thm_tactic, meaning it's a function of "type"
:thm -> tactic,
so composing them we see that (MP_TAC o SPEC `{x:A,y:A}`) is a function of
"type"
:thm -> tactic, i.e. it's a thm_tactic, and so the right "type" argument for
FIRST_ASSUM, which hands over the first assumption (that works!) to our
thm_tactic, and that means we're evaluating
(MP_TAC o SPEC `{x:A,y:A}`) `!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a
<<= x))`
=
MP_TAC `({x:A,y:A} = {}) ==> (?a. a IN {x:A,y:A} /\ (!x. x IN {x:A,y:A} ==> a
<<= x))`
=
`({x:A,y:A} = {}) ==> (?a. a IN {x:A,y:A} /\ (!x. x IN {x:A,y:A} ==> a <<= x))
==> x <<= y \/ y <<= x`
So MP_TAC applied to its thm argument `t` is a tactic, meaning it did
something: it changed the goal `g` to
`t ==> g`.
So i.e. something that does something with a thm. Now I see the "type"
SET_TAC : thm list -> tactic
which I think means that SET_TAC[] is a tactic, but the ASM means to use the
list of theorems in the assumption list, which is
0 [`!x y. x <<= y /\ y <<= x ==> x = y`]
1 [`!s. ~(s = {}) ==> (?a. a IN s /\ (!x. x IN s ==> a <<= x))`]
to get a tactic, and this tactic uses SET_RULE to prove the new goal `t ==> g`,
and it does!
Wow, this is great, Ramana, I never had any idea what was actually going on.
How do I learn more about this?
Petros, this sounds really cool, but I have only the vaguest idea what you
mean:
HOL systems are commonly used in informatics for software and hardware
verification. For example, (as far as I can tell) this is the kind of
thing John is working on at Intel.
For my research, as another example, I am using an embedding of Linear
Logic to specify and reason about services/processes and their
compositions/workflows in HOL Light.
Please say more. I'm no expert, but I think one of the things John does at
Intel is formalize theorems for them, floating point theorems about the
algorithms the chips use that are very difficult for humans to check, perhaps
using clever stunts with fast fourier transforms? So that would be actual math
that John's doing. I'm having a hard time understanding what else we can use
HOL for besides mathematical proofs.
--
Best,
Bill
------------------------------------------------------------------------------
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
