Hello,
this is what I would write to make your example work.
(* Here the types of x and y cannot be inferred, so an explicit type
annotation is needed. *)
let cross2 = new_definition
`(x:real^2) cross2 (y:real^2) = x$1* y$2 - x$2 *y$1`;;
(* Here all the types are inferred from the type of `cross2`. No type
annotation is needed. *)
let crossanticommutative = prove
(`!a b. --(b cross2 a) = a cross2 b `,
REPEAT GEN_TAC THEN
REWRITE_TAC[cross2; VECTOR_MUL_COMPONENT] THEN
CONV_TAC REAL_RING);;
(* Now we can specialize the theorem. No type instantiation is needed. *)
(* However, a type annotation is needed to constrain the variable A. *)
SPEC `A:real^2` crossanticommutative;;
As a rule of thumb, if something goes wrong and you cannot understand why,
one thing that you can do is looking for
"Warning: inventing type variables"
and add type annotation until the warning disappear.
Of course, inspecting types can also be very helpful.
For this, beside the functions suggested by Heiko, a cheap way to print the
types assigned to each variable is:
(map dest_var o variables) tm
for a term tm or
(map dest_var o variables o concl) th
for a theorem th. E.g.:
# (map dest_var o variables o concl) cross2;;
val it : (string * hol_type) list = [("y", `:real^2`); ("x", `:real^2`)]
Hope it helps to clarify,
Marco
2018-01-05 10:38 GMT+01:00 Heiko Becker <hbec...@mpi-sws.org>:
> Hello Michael,
>
> I remember from my last time I used hol-light that the following code from
> the flyspeck project was quite helpful:
>
> (**
> Add printers to HOL-Light to be able to print terms annotated with their
> terms.
> Snippet obtained from HOL-Light mailing list.
> https://sourceforge.net/p/hol/mailman/message/35203735/
> Code taken from the Flyspeck project.
> **)
> let print_varandtype fmt tm =
> let hop,args = strip_comb tm in
> let s = name_of hop
> and ty = type_of hop in
> if is_var hop & args = [] then
> (pp_print_string fmt "(";
> pp_print_string fmt s;
> pp_print_string fmt ":";
> pp_print_type fmt ty;
> pp_print_string fmt ")")
> else fail() ;;
>
> let show_types,hide_types =
> (fun () -> install_user_printer ("Show Types",print_varandtype)),
> (fun () -> try delete_user_printer "Show Types"
> with Failure _ -> failwith ("hide_types: "^
> "Types are already
> hidden."));;
>
> Running it with your example, I get the following output for your theorem:
>
> val crossanticommutative : thm =
> |- !(a:real^?219759) (b:real^?219758).
> --((b:real^?219758) cross2 (a:real^?219759)) =
> (a:real^?219759) cross2 (b:real^?219758)
>
> Consequently
>
> ISPEC `A:real^N` crossanticommutative
>
> works:
>
> val it : thm =
> |- !(b:real^?219758). --((b:real^?219758) cross2 (A:real^N)) =
> (A:real^N) cross2 (b:real^?219758)
>
>
> I hope my answer is helpful, please ask for clarifications if necessary.
>
>
> Best regards,
>
> Heiko
>
> On 01/05/2018 06:11 AM, Michael Beeson wrote:
>
> Could someone please help me get the following to work?
>
> parse_as_infix("cross2",(20,"right"));;
> needs "/Users/beeson/Dropbox/Provers/HOL-Light/Multivariate/vectors.ml";;
>
>
>
> (* Properties of scalar cross product *)
>
> let cross2 = new_definition
> ` x cross2 y = x$1* y$2 - x$2 *y$1`;;
>
> let crossanticommutative = prove(
> `!a b. --( b cross2 a) = a cross2 b `,
> (REPEAT GEN_TAC)THEN
> REWRITE_TAC[cross2;VECTOR_MUL_COMPONENT] THEN
> (CONV_TAC REAL_RING)
> );; # This works fine.
>
> SPEC `A` crossanticommutative;; # doesn't work, Exception: Failure
> "SPEC".
>
> ISPEC `A` crossanticommutative;; # doesn't work, Exception: Failure
> "ISPEC can't type-instantiate input theorem".
>
> SPEC `A:R^N` crossanticommutative;; #doesn't work, also not with ISPEC.
>
> I believe the types of a and b in crossanticommutative are
> real^N, where N is a system-generated type variable, but maybe not, in
> view of the failure message for ISPEC.
>
> since
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
>
> _______________________________________________
> hol-info mailing
> listhol-info@lists.sourceforge.nethttps://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
