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, 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?
--
Best,
Bill
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
