Thanks, Vince! I didn't know this:
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.
But I should have known this, because there are 4 different kinds of terms,
each having a type, and the simplest kind of term is a variable. So a variable
is not just a symbol. Thanks.
(note thus that if two variables have the same name but different
types, then they are different; this is really counter intuitive)
So what I want is a dialect of HOL Light where this seems not to be true, but
instead:
If x is a variable (which of course has a type, say alpha), then any other
occurrence of the symbol x in the scope of the first x will then inherit the
type alpha. So there will be no need to give the second x a type annotation,
and it will be an error to give x a different type annotation than alpha. This
is the way Freek's miz3.ml works. Do you like this idea? Do you instead think
that it's an important ability for the same symbol x to have different types at
different places and so be different variables?
My plan to make this work is
1) to use strings as in my modification of quotexpander I posted here
2) understand tactics.ml.
I don't think anything else is needed. I don't mind mining miz3.ml for good
ideas, but I don't think it will be necessary to understand miz3.ml. My guess
is that using strings will simplify matters that were difficult with Freek's
preterms.
> (`!u v w:real^2. ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w = u`,
> INTRO_TAC "!u v w; H1" [...]
> 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").
Sorry for my "set theory" terminology, which I see isn't the way HOL Light
describes INTRO_TAC:
# help "INTRO_TAC";;
INTRO_TAC : string -> tactic
Given a string s, INTRO_TAC s breaks down outer universal quantifiers
and implications in the goal, fixing variables [...]
I guess I don't know what "fix" means. I know what it looks like to me: The
symbols u, v, w were already typed real^2 in the goal
`!u v w:real^2. ~collinear {vec 0,v,w} ==> ? s t. s % v + t % w = u`
so u, v, w are already variables. But these variables right now don't have any
scope outside the goal. Evaluating
INTRO_TAC "!u v w; H1"
then gives scope to these variables u, v, w which extends at least as far as
the next line:
> 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 the v, w that occur in the term
`~(v$1 * w$2 - (w:real^2)$1 * (v:real^2)$2 = &0)`
must be equal to to the v, w above that has the scope, as long as the type of
the new v, w is also real^2.
What I don't understand is how HOL Light realizes that the new u, v is the same
as the old u, v. Really I suppose I mean I don't understand how HOL Light
still remembers about the old v, w. There should be an environment which keeps
track of the fixed variables and their scope. How is that handled in HOL
Light? Are you saying that Ocaml handles the environment?
--
Best,
Bill
------------------------------------------------------------------------------
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
