Hi Bill,
> Why don't we try to prove your precedence order is correct for HOL Light.
> Don't we just have to understand parser.ml?
Yes, but that's easier said than done! Parsers can be subtle things.
> I just realized I don't need type annotations if use tactics:
>
> let CartesianProduct = new_definition
> `! X Y. X times Y = {x,y | x IN X /\ y IN Y}`;;
>
> let IN_CartesianProduct = prove
> (`! X Y x y. x,y IN X times Y <=> x IN X /\ y IN Y`,
> REWRITE_TAC[IN_ELIM_THM; CartesianProduct] THEN MESON_TAC[PAIR_EQ]);;
The term defining CartesianProduct has a type variable (automatically
generated). It's good practice to explicitly type-annotate your terms with
any type varaibles, rather than to get HOL Light to generate type variables
for you. As you say, it helps readability.
Your proof above works because you don't need to supply term quotations that
involve the generated type variable. If such term quotations were needed,
then you would have to annotate them with the nasty generated type variable
name.
> However, that doesn't work in miz3!!! I get the error #6 underspecified
> types hol with
> ....
> So miz3 is doing something funny.
I don't know about miz3, but I'm guessing it doesn't allow type variables to
be generated.
> Milner type inference surely tells us that no type annotations were needed
above.
Milner type inference tells us that type annotations are never needed! It
always either fails (because the term is ill-typed) or succeeds with the
most general types possible (generating type variables that are not
explicitly supplied in type annotations).
> Here's a place where my type inference intuition doesn't work, and I get
the
> error
> Exception: Failure "typechecking error (initial type assignment)":
>
> parse_as_infix("-bb-->",(13,"right"));;
>
> let FunctionbbSpace = new_definition
> `! s t. s -bb--> t = {f | (! x. x IN s ==> f x IN t) /\
> ! x. x NOTIN s ==> f x = @y. T}`;;
>
> HOL Light seems to insist on the type annotation f: A->B. But I can't see
> why. A and B just mean arbitrary types. The sub-term x IN s shows that s
> has type A->bool and x has type A, for some type A. and the sub-term f x
> IN t shows that t has type B->bool and f x has type B, for some type B.
> Thus f has type A->B. What am I missing?
Your reasoning is correct, but I don't know the full theory context in which
this exists. Crucially, has 'NOTIN' been declared as an infix? (whether it
is has been declared/defined as a constant is actually not important for the
purposes of type inference)
Mark.
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
