Re: [Hol-info] Formalizing logical puzzles

[Marco Maggesi]

2018-06-26 20:11 GMT+02:00 Marco Maggesi :

> # REWRITE_CONV[PORTIA; EXISTS_BOOL_THM]
>   `?ig is. (ig <=> ~pg) /\ (is <=> (ig <=> ~is))`;;
>
> val it : thm = |- (?ig is. (ig <=> ~pg) /\ (is <=> ig <=> ~is)) <=> pg
>

​​Sorry, I made a mistake (thm PORTIA in the rewrite).  Here is the
corrected version:

# REWRITE_CONV[EXISTS_BOOL_THM]
​​
`?ig is. (ig <=> ~pg) /\ (is <=> (ig <=> ~is))`;;

val it : thm = |- (?ig is. (ig <=> ~pg) /\ (is <=> ig <=> ~is)) <=> pg
​
--
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

Re: [Hol-info] Question about Type (:M+N) in HOL Light

[Marco Maggesi]

Hello,

when `:N` is an infinite type, `dimindex(:N)` is by definition 1.
Then, if either `:M` or `:N` is infinite, we have
dimindex(:M+N) = 1
while
dimindex(:M) + dimindex(:N) >= 2
It follows that your relation
dimindex (:M+N) = dimindex(:M)+dimindex(:N)
holds only if `:M` and `:N` are both finite types.

I believe that the type `:(M,N)finite_sum` has been introduced precisely to
get around this problem.

Marco


2018-03-16 2:49 GMT+01:00 liliminga :

>
> Hi, everyone.
> I know the type  :(M,N)finite_sum in library "Definition of finite
> Cartesian product types".  What is the difference between (:M+N) and
>  :(M,N)finite_sum? Is there the theorem |- dimindex (:M+N) =
> dimindex(:M)+dimindex(:N) in the existing library?
> Thank you very much.
> Best regards,
> Liming
>
> 2018-03-16
> --
> liliminga
>
>
>
>
> 
> --
> 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

Re: [Hol-info] 2-vector zero

[Marco Maggesi]

Put explicit type annotation: `vec 0:real^2` and `vector[ ... ] : real^2`
etc.
For the moment there is no other solution.
I have a hack that modifies the parser so that HOL Light infers the right
`:N` for `vector [...]` by "counting" the number of elements in the list.
As soon as I have time to polish it I will post the code to the list.
M.


2018-01-19 23:34 GMT+01:00 Michael Beeson :

> vec(0)  has type real^N with variable N.
> So ISPEC and ISPECL  can't substitute it for a bound variable of type
> real^2.
> I need a 2-vector of zeroes instead.
>
> I tried vector[&0,&0],  but that ALSO has type real^N.
> How can I create a zero vector of type real^2?
>
>
>
> 
> --
> 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

Re: [Hol-info] matrices

[Marco Maggesi]

Hi,

the key theorem here is MATRIX_VECTOR_MUL_COMPONENT.

Here is a proof of your statement:

let MATRIXTWO_MUL_COMPONENT = prove
 (`!A:real^2^2 x:real^2.
 (A**x)$1 = A$1$1 * x$1 + A$1$2 * x$2 /\
 (A**x)$2 = A$2$1 * x$1 + A$2$2 * x$2`,
  SIMP_TAC[MATRIX_VECTOR_MUL_COMPONENT;
   DIMINDEX_2; LE_REFL; ARITH_RULE `1 <= 2`] THEN
  REWRITE_TAC[DOT_2]);;

Hope it helps,
Marco


2018-01-14 8:11 GMT+01:00 Michael Beeson :

> I've been reading the treatment of matrices in vectors.ml.   I only need
> two by two matrices for now.I don't find a procedure MATRIX_ARITH
> analogous to VECTOR_ARITH or REAL_ARITH.  Is there anything like that?
> Here's a sample I would like to use it on.
>
> let MATRIXTWO_MUL_COMPONENT = prove
> ( `!A:real^2^2 x:real^2.
>   (A**x)$1 = A$1$1 * x$1 + A$1$2 * x$2 /\
>   (A**x)$2 = A$2$1 * x$1 + A$2$2 * x$2`,
>
>     I don't know how to prove it.  Can anyone help?
> BTW,  I am very thankful to all those who have helped me on this list so
> far.
>
> Michael Beeson
>
> 
> --
> 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

Re: [Hol-info] SPEC and ISPEC

[Marco Maggesi]

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 :

> 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
>
>

Re: [Hol-info] REWRITE_RULE

[Marco Maggesi]

Hello,

2018-01-08 18:08 GMT+01:00 Michael Beeson :

> Falling script can be run after loading vectors.ml
>
>
> # let lemma300 = VECTOR_ARITH `!x:real^2 y:real^2 z:real^2.  (x + y = z)
> <=> (y = z-x)`;;
>
> val lemma300 : thm = |- !x y z. x + y = z <=> y = z - x
>
> # let test = ASSUME  `!a:real^2 b:real^2 c:real^2 d:real^2 . tarea(d,a,b)
> + tarea(c,a,d) = tarea(a,b,c)`;;
>

​The problem is in the previous line.  The type of + is inferred by
overloading.
Hence you need a type annotation to force the inference
`(+):real^2->real^2->real^2.

For instance (notice the annotation :real^2 added at the end):

let test = ASSUME  `!a:real^2 b:real^2 c:real^2 d:real^2.
  tarea(d,a,b) + tarea(c,a,d) = tarea(a,b,c):real^2`;;

Now the rewrite works as expected:

REWRITE_RULE[lemma300] test;;
​val it : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
  |- !a b c d. tarea (c,a,d) = tarea (a,b,c) - tarea (d,a,b)

​Marco​



> val test : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
>   |- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> # REWRITE_RULE[lemma300] test;;
>
> val it : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
>   |- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> #
>
>
> I was expecting
>
> tarea(c,a,d) = tarea(a,b,c)-tarea(d,a,b) in the conclusion
>
> (and maybe in the assumptions too).  Note that no type variables
>
> are involved, so whatever the problem is here,  it has nothing to do
>
> with type variables.
>
>
>
>
>
> 
> --
> 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

Re: [Hol-info] Rewriting and Types in HOL-Light

[Marco Maggesi]

Dear Heiko,

I see two main problem in your proof:

1. When you open the subgoal, you have to be sure about the types of your
terms.  I.e., here you have to add the annotation :num beside v or v2:

e (SUBGOAL_TAC "v_eq_v2" `v:num = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN
ONCE_REWRITE_TAC[injectivity "exp"]]);;

2. About your proof strategy, you surely want to make use of injectivity
and distinctness of constructors.  This is what I would do in this case:

g `!eps env v val.
   eval_exp eps env (Var v) val ==> val = env v`;;
e (REPEAT GEN_TAC);;
e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
(* Use distinctness of constructors. *)
e (REWRITE_TAC[distinctness "exp"]);;
(* Use injectivity of constructors. *)
e (REWRITE_TAC[injectivity "exp"]);;
(* Now you can easy conclude with MESON_TAC, or, if you wish, with. *)
e (DISCH_THEN STRUCT_CASES_TAC);;
e REFL_TAC;;

Marco




2016-07-05 12:02 GMT+02:00 Heiko Becker :

> Hello everyone,
>
> I have another question on HOL-Light. This time I am stuck with some
> rewriting in a proof.
>
> I have defined an inductive type and want to prove an "inversion" lemma
> for it:
>
> g `!eps env v val.
>eval_exp eps env (Var v) val ==> val = env v`;;
>
> I have been able to do the proof until I arrive at a subgoal which I
> think is easy to proof but I cannot find the appropriate tactic to do it:
>
> val it : xgoalstack = 1 subgoal (4 total)
>
>0 [`val = env v2`] (val_eq)
>1 [`v = v2`]
>
> `v = v2`
>
> The script I used is:
>
> e (ONCE_REWRITE_TAC[eval_exp_CASES]);;
> e (INTRO_TAC "!eps env v val; cases");;
> e (REMOVE_THEN "cases" (DESTRUCT_TAC "var | const | bin"));;
> (* Var case *)
> e (REMOVE_THEN "var" (DESTRUCT_TAC "@v2. var_eq val_eq"));;
> e (SUBGOAL_TAC "v_eq_v2" `v = v2` [REMOVE_THEN "var_eq" (MP_TAC) THEN
> ONCE_REWRITE_TAC[injectivity "exp"]]);;
> e (DISCH_TAC);;
> e (EXPAND_TAC "v2");;
> e (ONCE_REWRITE_TAC[ASSUME `v = v2`]);
>
> Since the last two tactics do not change the goal in any way my
> questions in this case are:
>
> 1) How can I use the assumption 1 and rewrite it inside my goal?
>
> 2) Is there an easier way of closing the proof, since I already derived
> the goal I have?
>
> 3) (A little unrelated) Can I make HOL-Light annotate all terms in my
> goal with their derived type?
>
> I have added my formalization below.
>
>
> Thank you (once again) in advance.
>
> Best regards,
>
> Heiko
>
>
> 
>
> let binop_IND, binop_REC = define_type
>"binop = Plus | Sub | Mult | Div ";;
> (*
>Define an evaluation function for binary operators.
> *)
> let eval_binop = new_recursive_definition binop_REC
>`(eval_binop Plus v1 v2 = v1 + v2) /\
>(eval_binop Sub v1 v2 = v1 - v2) /\
>(eval_binop Mult v1 v2 = v1 * v2) /\
>(eval_binop Div v1 v2 = v1 / v2)`;;
>
> let exp_IND, exp_REC= define_type
>"exp = Var num
>| Const V
>| Binop binop exp exp";;
>
> let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;;
> new_type_abbrev ("env_ty",`:num->real`);;
>
> let eval_exp_RULES, eval_exp_IND, eval_exp_CASES = new_inductive_definition
>`(!eps env v.
>eval_exp eps env (Var v) (env v)) /\
>(!eps env n delta.
>   abs delta <= eps ==>
>   eval_exp eps env (Const n) (perturb n delta)) /\
>(!eps env b e1 e2 v1 v2 delta.
>   eval_exp eps env e1 v1 /\
>   eval_exp eps env e2 v2 /\
>   abs delta <= eps ==>
>   eval_exp eps env (Binop b e1 e2) (perturb (eval_binop b v1 v2)
> delta))`;;
>
>
>
> --
> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] On the wondering of detection of constructive proofs

[Marco Maggesi]

[I forgot to replay to the list ...]

Hi Robert,

in HOL Light you can use ITAUT (or ITAUT_TAC).
The documentation (https://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/ITAUT.html)
says:

Normally, first-order reasoning should be performed by MESON[], which is
much more powerful, complete for all classical logic, and handles equality.
The function ITAUT is mainly for ``bootstrapping'' purposes. Nevertheless
it may sometimes be intellectually interesting to see that certain logical
formulas are provable intuitionistically.


2015-06-08 19:40 GMT+02:00 Robert White ai.robert.wangsh...@gmail.com:

 Dear all,

 I wonder how I can detect if there law of excluded middle or double
 negation elimination used in a proof. Basically, I am trying to find out if
 a proof is classical or constructive.

 Since when I use TAUT or other rewriting functions I won't get a direct
 idea if it is classical or constructive. I wonder if there is anyway I can
 find out.

 Thanks a lot.

 --

 Regards,
 Robert White http://www.dptinfo.ens-cachan.fr/~swang/(Shuai Wang)
 INRIA Deducteam https://www.rocq.inria.fr/deducteam/
 [Moving to ILLC of UvA from this Sep. ]
 [New email address will be shuai.w...@student.uva.nl]



 --

 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info


--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Theory loading conflict

[Marco Maggesi]

Dear Adnan,

the expected way to use Multivariate/cauchy.ml is by loading the file
Multivariate/make_complex.ml which in turn loads all the dependencies in
the appropriate order (including cauchy.ml).

You also must be warned that loading complex analysis may take a while (say
30 minutes, but obviously it depends on your setting).

Hope it helps,
Marco


2015-02-13 9:32 GMT+01:00 Adnan Rashid adnan.ras...@seecs.edu.pk:

 ​​Dear all,

 I am using Hol-light on Ubuntu 14.04. I am facing theory loading conflict.
 I am loading only two theories in alternative sequences but in both cases I
 am having problems.  The theories are *Multivariate/cauchy.ml
 http://cauchy.ml* and *Library/poly.ml http://poly.ml*.
 ​
 In the first case, when I load cauchy theory first, it ends up with the
 following error:


 ---

 File /home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml,
 line 12911, characters 35-58:
 Error: Unbound value REAL_LOG_CONVEX_ON_SING
 Error in included file
 /home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
 val it : unit = ()


 ---

 After this, I load the poly theory which also ends up with the following
 error:


 ---

 File /home/user/hol-light-workbench/hol-light/Library/poly.ml, line
 173, characters 51-61:
 Error: Unbound value DIFF_CONST
 Error in included file /home/user/hol-light-workbench/hol-light/Library/
 poly.ml
 val it : unit = ()


 ---

 In this sequence of loading theories,  it does not recognize the theorems
 when entered in shell.
 e.g.

 *REAL_CONTINUOUS_ATREAL_WITHINREALError: Unbound value
 REAL_CONTINUOUS_ATREAL_WITHINREAL​*

 Where as, in the second case, when I load poly theory first, it ends up
 fine. Next, when I load the cauchy theory, it ends up with the following
 error:


 -

 Error in included file
 /home/user/hol-light-workbench/hol-light/Multivariate/realanalysis.ml
 - : unit = ()
 File /home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml,
 line 23, characters 45-64:
 Error: Unbound value OPEN_CONTAINS_CBALL
 Error in included file
 /home/user/hol-light-workbench/hol-light/Multivariate/moretop.ml
 - : unit = ()
 - : unit = ()
 - : unit = ()
 Exception:
 Failure
  typechecking error (initial type assignment): f cannot have type
 real-(_-bool)-bool and real-real simultaneously.
 Error in included file
 /home/user/hol-light-workbench/hol-light/Multivariate/cauchy.ml
 val it : unit = ()


 --

 In this case, when I write a goal involving exponential (exp) function, it
 gives error* Exception: Noparse* else it works fine.

 If I try only cauchy theory without loading poly theory, it results no
 error when using exp function, which, to me, shows that *Noparse* error
 is not due to brackets.

 Thanks in advance.



 --
 Dive into the World of Parallel Programming. The Go Parallel Website,
 sponsored by Intel and developed in partnership with Slashdot Media, is
 your
 hub for all things parallel software development, from weekly thought
 leadership blogs to news, videos, case studies, tutorials and more. Take a
 look and join the conversation now. http://goparallel.sourceforge.net/
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info


--
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Instrumenting the HOL light core

[Marco Maggesi]

Hi Mario,

you might be interested in the Proof Recording mechanism.  Look into the
subdirectory Proofrecording in HOL Light distribution.  It has already been
employed for exporting theorems from HOL Light to Coq.  Beside the README
in the above directory, you may find
other​​
 information in the paper of Chantal Keller and Benjamin Werner
​ ​
​
Importing HOL Light into Coq
​​.

Hope it can be useful,
Marco

2014-10-11 4:34 GMT+02:00 Mario Carneiro di.g...@gmail.com:

 Hello,

 I'm interested in examining the core axiom functions of HOL so that I can
 produce diagnostic information on the actual proof process as the program
 runs. What is the best way to do this? I remember hearing somewhere that
 someone made a program to convert HOL light proofs into something
 understandable by an automated prover, and I am trying to something similar
 (I want to translate HOL proofs into another language), so I'm curious if
 there is an already established method for getting this sort of data out of
 the core.

 Mario Carneiro


 --
 Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
 Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
 Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
 Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
 http://p.sf.net/sfu/Zoho
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info


--
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://p.sf.net/sfu/Zoho___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

[Marco Maggesi]

Hi Nela,

I use the Nix package manager (http://nixos.org/nix/) and it works well for
me.  I use Nix both on Max and on Linux.  It is nice because it makes the
installation of HOL Light completely independent from the versions of
ocaml, camlp5 (or any other software indeed) installed in your machine.

If you want to try, here is what you have to do:

1. Install Nix.  Follow the instructions from the nix manual (
http://nixos.org/nix/manual).  Basically you have to type the following
four commands in a terminal:

  ​
$ bash (curl https://nixos.org/nix/install)
  source /usr/local/etc/profile.d/nix.sh
​​
​​
nix-channel --add http://nixos.org/channels/nixpkgs-unstable
  ​nix-channel --update​
​​
​2​
.
​Then you can install HOL Light with a single command (no need to install
OCaml or Camlp5)

​  ​
nix-env -i hol_light

​For more serious work you probably need to use checkpointing which is
available only on Linux.  For this I use a NixOS (http://nixos.org)
VirtualBox appliance.  Do not esitate to ask for more details if you are
interested.

Best,
Marco


2014-09-17 5:50 GMT+02:00 Mark Adams m...@proof-technologies.com:

 Hi Nela,

 There have been various problems over the years, but I get no problems with
 recent versions of HOL Light (downloaded since May 2014, including SVN
 version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
 running on Fedora 17.

 Do you know the HOL Light SVN version (or otherwise, what date did you
 download)?

 And can you please check your OCaml and Camlp5 versions by executing the
 following from the same terminal window from which you are trying the HOL
 Light make?:
ocaml -version
camlp5 -v

 Mark.

 on 16/9/14 4:45 PM, Nela Cicmil nela.cic...@dpag.ox.ac.uk wrote:

  Dear HOL Light users,
 
  Would anyone be able to please advise me on how to install HOL Light on
 my
  Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.
 
  My trouble is that I can't seem to get compatible versions of Ocaml,
 camlp5
  and HOL Light installed on my system, mainly because the Ocaml version
 that
  comes with OPAM, v 4.01.0, seems to be too recent to run with the
 slighter
  older camlp5 versions compatible with HOL Light.
 
  Has anyone recently installed HOL Light on a Mac, and has advice on which
  versions of Ocaml and camlp5 to install, and which procedure to use to
  install them? In particular, is it possible to install an older version
 of
  Ocaml, e.g. v 3.12, using OPAM?
 
  The specific issues I've encountered are detailed below. Any advice would
 be
  much appreciated.
 
  Thank you,
 
  Best wishes,
  Nela
  
  Nela Cicmil, D.Phil
  Dept. Physiology, Anatomy  Genetics,
  University of Oxford
  
 
  After various attempts to install Ocaml on the Mac, I installed (using
  homebrew) the latest version of OPAM, which comes with Ocaml version
 4.01.0.
  On basic testing at the terminal, Ocaml seemed to be working fine. I then
  installed camlp5 version 6.11, using ./configure --transitional mode, and
  that seemed to be running fine as well. When I then attempted to install
 HOL
  Light, using the svn checkout http://hol-light.googlecode.com/svn/trunk/
  hol_light procedure, and got the following error on make:
 
  File pa_j.ml, line 112, characters 72-74:
  Error: This expression has type (string * MLast.ctyp) list
  but an expression was expected of type
  ('a * MLast.ctyp) list Ploc.vala
  make: *** [pa_j.cmo] Error 2
 
  - On reading various previous posts, it seemed that the latest versions
 of
  camlp5 could be at fault. I attempted to install older versions of
 camlp5,
  version 6.02.0 and 5.15, but I got the following error on ./configure
  --transitional:
 
  Sorry: the compatibility with ocaml version 4.01.0
  is not yet implemented. Please report.
  Information: directory ocaml_stuff/4.01.0 is missing.
  Configuration failed.
 
  - With campl5 version 6.06 it's the following error (I'm not sure what
 the
  preprocessor is here):
 
  Fatal error: OCaml and preprocessor have incompatible versions
  Fatal error: exception Misc.Fatal_error
  make[2]: *** [versdep.cmo] Error 2
  make[1]: *** [core] Error 2
  make: *** [world.opt] Error 2
 
  - So then I attempted to install an earlier version of Ocaml, version
  3.12.1, in the hope that it would be compatible with the earlier versions
 of
  camlp5. This did not seem possible with OPAM so I downloaded the original
  source distribution tar.gz from http://ocaml.org/releases/3.12.1.html. I
  believe my system has the necessary dependencies in the form of Xcode
 5.11,
  gcc and gnumake running. However, the make world installation command
  exits on the following error:
 
  make coldstart
  cd byterun; make all
  gcc -DCAML_NAME_SPACE -O -fno-defer-pop -no-cpp-precomp -Wall
  -D_FILE_OFFSET_BITS=64 -D_REENTRANT-c -o interp.o interp.c
  clang: error: unknown argument: '-fno-defer-pop'
  [-Wunused-command-line-argument-hard-error-in-future]
  clang: note: this will be a hard error (cannot be downgraded 

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

[Marco Maggesi]

2014-09-17 14:14 GMT+02:00 Nela Cicmil nela.cic...@dpag.ox.ac.uk:

 and all seemed to complete without errors. My question is, if HOL Light is
 now installed on my machine, what's the best way to run it?


​Sorry, I forgot to say.  As you already found yourself, you have to use
the command

hol_light

which starts ocaml and loads hol.ml automatically.

You have to wait a few minutes while the full system loads (people use
checkpointing precisely to avoid this step).  Don't care about the long
list of messages and warnings, all should be OK.  At the end you get
something like:

File
/nix/store/0cgxqn0x9nz0i6l5ysnf9ak0rqkh0v7y-hol_light-189/lib/hol_light/
help.ml, line 116, characters 25-57:

Warning 3: deprecated feature: operator (); you should use () instead

Camlp5 parsing version 6.11


#

then you can type our commands: e.g.

# ARITH_RULE `1 + 1 = 2`;;
val it : thm =

|- 1 + 1 = 2


Small suggestion: since the ocaml toplevel do not have line editing
features, you may want to use rlwrap:


nix-env -i rlwrap


then invoke hol as


rlwrap hol_light


Hope it helps and keep asking if all this is not clear,

Marco
--
Want excitement?
Manually upgrade your production database.
When you want reliability, choose Perforce
Perforce version control. Predictably reliable.
http://pubads.g.doubleclick.net/gampad/clk?id=157508191iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Help on HOL Light (possible problems with the installation)

[Marco Maggesi]

Hi Alfio,

you should be able to fix your problem by using a customized OCaml  
toplevel

with the num library preloaded.
Try this:

cd hol_light
ocamlmktop -o ocamlnum nums.cma
./ocamlnum
#use hol.ml;;

This is explained at the very end in the README of the HOL Light  
distribution.


Hope it helps,
Marco

On Dec 30, 2008, at 3:29 AM, Alfio Ricardo de B Martini wrote:


Hi People,

I am new member to the list (since a few minutes ago) and I am  
struggling to install correctly
the HOL Light system (in a cygwin environment). Actually the  
installation and building is pretty straightforward (as
described in the tutorial), but when I load the HOL system from the  
ocaml top level, there are a number of errors during
the loading of the several files. As a consequence,  I am only able  
to use the pure ML
language (the top level). I attach part of the messages printed in  
the cygwin bash shell below.

Can you help me on this?

Many thanks!
-

bash-3.2$ cd hol_light

bash-3.2$ ocaml

Objective Caml version 3.08.2

# #use hol.ml;;


[...]

File /home/hol_light/sys.ml, line 31, characters 0-34:

Warning: this pattern-matching is not exhaustive.

Here is an example of a value that is not matched:

false

- : bool - bool = fun

Cannot load required shared library dllnums.

Reason: dynamic loading not supported on this platform.

Reference to undefined global `Num'

Error in included file /home/hol_light/sys.ml

- : unit = ()
--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info