On 04/21/2013 01:12 AM, Bill Richter wrote:
> Here's a simpler version of the type-inference question I've been asking, and
> this I suspect does not involve the parser. Suppose we have a free variable
> in a term that's in the scope of a variable binding. As Petros explained to
> me here some time ago, this variable's type must be either annotated in the
> term, or else follow from type inference using only the term itself. Vince
> explained to me why this extra typing is needed. But having correctly typed
> the variable, I have a beginner's question:
>
> Why does the variable receive its correct value?
>
> Here's the first example of this in Examples/inverse_bug_puzzle_tac.ml:
>
> let Noncollinear_2Span = prove
> (`!u v w:real^2. ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w = u`,
> INTRO_TAC "!u v w; H1" THEN
> SUBGOAL_TAC "H1'" `~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 = &0)`
> [HYP MESON_TAC "H1" [COLLINEAR_3_2Dzero; REAL_SUB_0]] THEN [...]);;
>
> So in the SUBGOAL_TAC expression, v and w need type annotations. But then
> they received the value given by INTRO_TAC. That is, the statement of the
> theorem is "for all u, v, w...", and INTRO_TAC then fixes arbitrary real^2
> vectors u, v, w,
I'm not sure what you mean by "INTRO_TAC then *fixes* arbitrary".
In this particular example, INTRO_TAC is just the same as GEN_TAC THEN
GEN_TAC THEN GEN_TAC THEN DISCH_THEN (LABEL_TAC "H1").
> for which we're to prove
> ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w = u.
> How does HOL Light know that the v and w of the SUBGOAL_TAC command are the
> same v and w that were fixed by INTRO_TAC?
Mathematically, a variable is the pair of a name and a type, so if two
variables have the same name and the same type then they're just the
same variable.
(note thus that if two variables have the same name but different types,
then they are different; this is really counter intuitive)
--
Vincent Aravantinos
Postdoctoral Fellow, Concordia University, Hardware Verification Group
http://users.encs.concordia.ca/~vincent
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
