Dear Bill,
The "types" that you're talking about in quotation marks are ML types. I
guess you quote them to distinguish them from HOL types. Indeed, they are
meta-language types (guess what ML stands for).
Your example with MP_TAC o SPEC etc. looks good.
To learn more about this stuff I tentatively suggest Larry Paulson's "ML
for the Working Programmer". Others may have better suggestions.
Ramana
On Fri, Jan 4, 2013 at 6:47 PM, Bill Richter
<[email protected]>wrote:
> 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
>
------------------------------------------------------------------------------
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
