[Hol-info] Sources for "Formal verification of floating point trigonometric functions"

[Heiko Becker]

Hello everyone,

The paper "Formal verification of floating point trigonometric 
functions" by John Harrison from TPHOLs'97  gives a formal proof of 
sturm's theorem and how to apply it to find roots of a polynomial in 
HOL. I am trying to find the accompanying formal development as the 
proof (and use) of Sturm's theorem is of special interest to me.


I tried searching the HOL-Light repository at 
https://github.com/jrh13/hol-light  
and the HOL4 sources but could not find any mention of sturm's theorem.


Does someone have a pointer to where I could find the sources of the 
development?


Thank you and best regards,

Heiko



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

Re: [Hol-info] John Harrison's Book HOL Light

[Heiko Becker]

Hi William,

I assume that you want to run an interactive session of HOL-light, 
right? What worked quite nice for me is using the hol-light.el bindings 
for emacs (https://github.com/gilith/hol-light-emacs 
). There seems to also be a 
vi mode (https://www.cs.ru.nl/~freek/step/step.tar.gz 
), but I have never used 
it before. I just found it here: 
https://sourceforge.net/p/hol/mailman/hol-info/thread/CAMej%3D27hGGcVYxfMBf-F4b3sZsH-dYu1djYs3vddcc8GzsMv%3DA%40mail.gmail.com/#msg34592229 



With those proof modes you can edit your proof script on one side of the 
screen and send the things you are typing to an interactive session that 
is run for you.  I hope that is what you were looking for.


Cheers,

Heiko

On 11.03.21 06:25, William Mitchell Jr wrote:

Hi,

I downloaded the code and  #use "init.ml ";; runs 
without errors.

But how do I make OCaml's utop interactive with all of the .ml files?

Much Thanks,
William Mitchell



___
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

[Hol-info] Verification internships at MPI institutes (Application, deadline 31st December)

[Heiko Becker]

Hi all,

The Max Planck Institutes for Informatics (Saarbruecken), Software 
Systems (Saarbruecken and Kaiserslautern), and Security and Privacy  
(Bochum) offer research internships in all areas of Computer Science. An 
internship at a Max Planck Institute is a way to pursue world-class  
research in computer science! Our internships are also an excellent way 
to explore research or  new research areas for the first time.


Internships are open to exceptional Bachelor, Master, and Doctoral 
students worldwide, as well as exceptional individuals from industry  
interested in gaining academic research experience in computer science.  
Intern positions are limited and admissions are very competitive.


Max Planck Institutes offer an internationally renowned research 
community, with world-class faculty across the full spectrum of Computer 
Science. A larger description of the program can be found at the end of 
the mail, and on the official website 
https://www.cis.mpg.de/internships/#csresearchareas



If you are especially interested in theorem proving in HOL4 or the 
CakeML compiler, please consider applying for an internship with Eva 
Darulova.


More information on our website at
https://www.cis.mpg.de/internships/#csresearchareas

Regards,

Heiko




Computer Science Internships at Several Max Planck Institutes

Several Max Planck Institutes in Germany invite applications for
research internships in Computer Science from exceptional university
students at all levels (Bachelors, Masters and PhD). Interns tackle
new and challenging research problems in close collaboration with
faculty and graduate students at the institute.  Successful
internships often result in coauthored publications at top academic
conferences.

A Max Planck CS internship is an excellent way for Bachelor's and
Master's students to start or extend their research experience and
embark on a research career! Students looking for Bachelor's or
Master's thesis projects may also apply. We particularly welcome
applications from women and individuals belonging to groups that are
underrepresented in science and technology.

Eligibility
---

The eligibility criteria for an internship are an exceptional academic
record and knowledge of Computer Science equivalent to the first three
years of a standard university Bachelor's (undergraduate) program in
CS. Internship projects are individually customized to suit the
existing knowledge and experience of every intern. Intern positions
are limited and admissions are very competitive.

Period and Duration of Internships
--

Internships are typically 12-14 weeks long and held during the summer
months (May-August), but internships at other times or those of longer
duration are possible.

Funding
---

All interns receive a monthly stipend, free (shared) housing, and
travel to and from the institute hosting the internship.

Application Deadlines for 2021
--

- Early Deadline: 31 December, 2020 (for internships starting in May or 
June 2021)
- Late Deadline: 31 January, 2021 (for internships starting in July or 
August 2021)


For an internship starting at any other time of the year, apply at
least 4 months before your intended started date.

How to Apply


Internship applications must be submitted online at
https://cis.mpg.de/internships

To apply, you will need to provide your CV, transcripts, contact
information for at least one reference, and an optional motivation
letter. You can also optionally indicate faculty members at the
participating institutes (see below) with whom you would like to work
and the period during which you would like to intern.

Which MPIs participate? Where will the internships be?
--

The internship is held at one of the participating institutes. The
participating institutes are:

- Max Planck Institute for Informatics (Saabruecken)

- Max Planck Institute for Software Systems (Kaiserslautern and
  Saarbruecken)

- Max Planck Institute for Security & Privacy (Bochum)

We understand that travel restrictions due to the ongoing COVID-19
pandemic may prevent interns from traveling to Germany right now. In
such a case, after an intern is selected, the intern and the mentor
may agree mutually to complete the internship remotely. The intern
will still be paid the monthly stipend.

Further Details? Questions?
---

Further details of the internship program, including answers to
frequently asked questions (FAQs), can be found at
https://cis.mpg.de/internships.



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

Re: [Hol-info] How to prove basic equivalency of rational?

[Heiko Becker]

Hello,

I am not an expert on ratTheory itself but I briefly looked at your 
goal. To me it feels like `1/10:rat = 10/100` is the wrong goal to prove.
Looking at the documentation of ratTheory some theorems use `rat_equiv` 
instead. If I restate your goal as


`rat_equiv (abs_frac (1,10)) (abs_frac (10,100))`

it can be proven by

fs[rat_equiv_def, NMR, DNM]

My guess is that your goal is not provable because `1/10` and `10/100` 
represent different rational "objects" though they are equivalent (as 
captured by `rat_equiv`).
But I am not sure about this. Maybe someone more experienced can comment 
on this.



Best regards,

Heiko


On 1/14/19 6:24 AM, Xero Essential wrote:

Hi, every expert.

    Maybe I'm a little new to the HOL4 libraries.

    But, how could I prove the basic equivalency of rational like `1q 
/ 10 = 10 / 100`?
    The documentation is little and I have searched all the source, 
but related conversions and tactics like `RAT_EQ_TAC` are all failed 
and throw an empty error.
    I looked the source about `RAT_EQ_TAC`, which something about  
`abs_rat`, and then I become confused.


    Sorry for my bothering, and hope the suggestion.

Thanks.
Qiyuan Xu.


___
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] Applying a theorem to a specific subgoal

[Heiko Becker]

Hello Dylan,

There are two ways (I know of) to easily work on subgoals:

1) You use the >- symbol and not \\ or THEN as it only applies to the 
first subgoal


2) You use THENL an give it a list of tactics, where the i-th element 
the list is applied to subgoal i.


Personally, I would recommend using ">-".

Best regards,

Heiko


On 08/08/2018 07:24 AM, Dylan Melville wrote:

When a goal is separated into multiple subgoals during a proof of the form

# prove(thm,tactic);;


Where the last tactic is something like

REPEAT CONJ_TAC

Is there a way to specify that the next tactic should be applied to a specific 
subgoal? In the proof I’m working on, it was applied to all subgoals.


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

[Heiko Becker]

Hello,

On 06/28/2018 11:44 PM, Dylan Melville wrote:

Also, the version Im using is HOL - Light


On Jun 28, 2018, at 5:38 PM, Dylan Melville  wrote:

Is there a tactic for splitting conjoined assumptions into separate assumptions?


In HOL-Light you can try using CONJ_PAIR[1] for an assumption of the 
form A /\ B and CONJUNCTS[2] for finitely many conjuncts. These can then 
be added back using ASSUME_TAC.


Alternatively you can use CONJUNCTS_THEN[3] in combination with ASSUME_TAC.


Hope this helps.

Best regards,


Heiko


[1]: http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJ_PAIR.html

[2]: http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_UPPERCASE.html

[3]:http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_THEN.html


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

[Hol-info] Using polyscripter with user-written theories

[Heiko Becker]

Hello everyone,


I am trying to use the polyscripter tool to generate some nice output 
from my HOL4 definitions.


In my directory, I have a file aScript.sml with theorem b_def being 
produced. After compiling with Holmake, I have the files aTheory.sml and 
aTheory.sig, where aTheory.sig contains the theorem b_def as expected.


I am trying to produce a pretty-printed version of b_def in a file c.txt 
that contains the following two lines:


  >>__ open aTheory

  ##thm b_def

However, running $HOL_DIR/Manual/Tools/polyscripter < c.txt gives me an 
error in the line with open aTheory, that aTheory has not been declared.


Putting

>>  OS.FileSys.getDir()

will print the working directory I am in at the moment.


Can someone explain to me how to set up my files such that I can 
reference other theories using polyscripter?



Thanks in advance,


Heiko


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

[Hol-info] Share list of terms with later theories

[Heiko Becker]

Hello everyone,

suppose I have a custom tactic that depends on a list of terms and I 
want to keep adding elements to the list throughout my development.
I tried to achieve this using a :term list ref on the ML level. However, 
it is the case that if I add some term in theory A and inspect the list 
in theory B, where A is in the theory graph before B, all elements added 
in A are not in the list anymore.


Can someone give me a hint on why this is the case or tell me a better 
way to "share" a list of terms from a theory with theories depending on it?


Cheers,

Heiko

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

[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 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] Changing thms used by computeLib

[Heiko Becker]

Hello Ramana,

yes, the Mk_comb error occurs non-deterministic. Is there a temporary 
workaround for this, that I could make use of?


Cheers,

Heiko

On 10/05/2017 12:43 PM, Ramana Kumar wrote:

Hi Heiko,

Does it fail every time when you try to run the proofs 
non-interactively (with Holmake)?


I suspect the "Mk_comb" error, if it is non-deterministic, has to do 
with pointer equality problems, which are in the middle of being fixed.


Cheers,
Ramana

On 5 October 2017 at 13:22, Heiko Becker <hbec...@mpi-sws.org 
<mailto:hbec...@mpi-sws.org>> wrote:


Hello,

I have some proofs that I could previously solve by running
EVAL_TAC, after modifying computeLib.the_compset with


val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]


As it turns out, the proofs still run fine when interactively run
in an HOL4 emacs session, but the proofs fail when run on the
command line.

The failure either is

HOL_ERR {message = "", origin_function = "Mk_comb",
origin_structure = "T$
m"}
 Uncaught exception: HOL_ERR {message = "", origin_function =
"Mk_comb", origin_structure = "Thm"}

or

 (∀k.
k = 1 ∨ k = 0 ⇒
lookup k (BS (BN LN (LS ())) () (LS ())) =
lookup k (BS LN () (LS (

Previously it sufficed to have a file myComputeLib.sml declaring
the structure myComputeLib and adding the two val statements above
there and loading that file when doing the proof with "open". When
trying to debug this issue, I moved the val statements in a
separate tactic, declaring

  val my_eval_tac =
 let
   val _ = computeLib.del_funs [sptreeTheory.subspt_def]
   val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]
 in
  EVAL_TAC
 end;


but that did not solve my problem either.

Can someone help me resolve this or give me a hint on how to debug
this issue?

Thanks,

Heiko



--
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 <mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
<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

[Hol-info] Changing thms used by computeLib

[Heiko Becker]

Hello,

I have some proofs that I could previously solve by running EVAL_TAC, 
after modifying computeLib.the_compset with



val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, 
sptreeTheory.subspt_eq]



As it turns out, the proofs still run fine when interactively run in an 
HOL4 emacs session, but the proofs fail when run on the command line.


The failure either is

HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
m"}
 Uncaught exception: HOL_ERR {message = "", origin_function = 
"Mk_comb", origin_structure = "Thm"}


or

 (∀k.
k = 1 ∨ k = 0 ⇒
lookup k (BS (BN LN (LS ())) () (LS ())) =
lookup k (BS LN () (LS (

Previously it sufficed to have a file myComputeLib.sml declaring the 
structure myComputeLib and adding the two val statements above there and 
loading that file when doing the proof with "open". When trying to debug 
this issue, I moved the val statements in a separate tactic, declaring


  val my_eval_tac =
 let
   val _ = computeLib.del_funs [sptreeTheory.subspt_def]
   val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, 
sptreeTheory.subspt_eq]

 in
  EVAL_TAC
 end;


but that did not solve my problem either.

Can someone help me resolve this or give me a hint on how to debug this 
issue?


Thanks,

Heiko


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

[Hol-info] Instantiating type variables

[Heiko Becker]

Hello everyone,

I am trying to prove a theorem using the IEEE floating-point 
formalizations of HOL4. In a proof, I need to apply the lemma 
lift_ieeeTheory.float_add_relative. However neither match_mp_tac nor 
irule are able to unify the lemma with the conclusion I want to show.


I tried instantiating variables by hand to see what happens. Trying the 
below code fails with an error complaining about mismatched types in the 
conclusion:


SPEC ``(fp64_to_float v):(52, 11) float``  float_add_relative


Can someone tell me what I a doing wrong in this case, since (52,11) 
float should be unifiable with (τ, χ) float.




Thanks,

Heiko




--
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] Handling existentials in conclusions

[Heiko Becker]

Thanks. That looks like the thing I need to get my proofs to be shorter.


On 08/30/2017 02:06 PM, michael.norr...@data61.csiro.au wrote:

I don’t know of anything that does exactly this, and it does look like an 
appealing thing to have.  An easy implementation (tested as per attachment) 
would be something like

   fun prove_hyp_tac th =
  SUBGOAL_THEN (lhand (concl th)) (fn hyp => STRIP_ASSUME_TAC (MP th hyp))

You would then get your effect with

   qspecl_then [`param1`, `param2`, `param3`] prove_hyp_tac test

You presumably have to provide the params to the theorem so that you get the 
right instantiation and a concrete P to prove.

Screen shot shows it in action.  Let me know if that’s not what you meant.

Michael

On 30/8/17, 21:40, "Heiko Becker" <hbec...@mpi-sws.org> wrote:

 Hello everyone,
 
 I have a question on how to prove a theorem relying on lemmas with

 existentials in their conclusion:
 
 Take an arbitrary theorem of the form
 
  val test = Q.prove (``!P Q R. P ==> ?m. Q m /\ R m``, cheat)
 
 where P may be arbitrarily complex.
 
 If I want to use the aforementioned theorem in another proof obtaining

 its conclusion as an additional hypothesis, the only way I can currently
 handle this is by writing the conclusion down explicitly and then
 discharging the proof with "by":
 
`?m. Q m /\ R m` by (irule test \\ ...)
 
 
 In Coq, I could just say
 
destruct test as ...
 
 which would generate a subgoal for the P occurring on the left side of

 the arrow.
 
 Is there a way of having similar behavior in HOL4, or at least to

 improve upon writing it all by hand?
 
 
 Thanks,
 
 Heiko
 
 --

 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


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

[Hol-info] Handling existentials in conclusions

[Heiko Becker]

Hello everyone,

I have a question on how to prove a theorem relying on lemmas with 
existentials in their conclusion:


Take an arbitrary theorem of the form

val test = Q.prove (``!P Q R. P ==> ?m. Q m /\ R m``, cheat)

where P may be arbitrarily complex.

If I want to use the aforementioned theorem in another proof obtaining 
its conclusion as an additional hypothesis, the only way I can currently 
handle this is by writing the conclusion down explicitly and then 
discharging the proof with "by":


  `?m. Q m /\ R m` by (irule test \\ ...)


In Coq, I could just say

  destruct test as ...

which would generate a subgoal for the P occurring on the left side of 
the arrow.


Is there a way of having similar behavior in HOL4, or at least to 
improve upon writing it all by hand?



Thanks,

Heiko

--
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] Strange tactics bug when using match_mp_tac

[Heiko Becker]

On 08/23/2017 09:03 AM, michael.norr...@data61.csiro.au wrote:

You are being caught by the fact that match_mp_tac thm can throw an exception 
before the tactic is ever applied to a goal.  In particular, if the theorem 
passed to match_mp_tac is not an implication an exception is thrown immediately.

You can fix this by handling that possible exception:

fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm handle HOL_ERR 
_ => ALL_TAC)
Thank you for the fix. With this I could come up with a solution that I 
find ok for the moment:


val my_match_mp_tac = (fn thm => (fn gs => match_mp_tac thm gs))

This allows to at least not have the HOL_ERR handling, but I guess it 
depends what one finds nicer.

This arguably a poor design for match_mp_tac, and should perhaps be changed.


Looking at the definition of MATCH_MP_TAC, I found a pretty easy fix, 
that should remove this behavior, thus I opened Pull Request #455 
.


Cheers,

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

[Hol-info] Strange tactics bug when using match_mp_tac

[Heiko Becker]

Hello everyone,

while working on some custom tactics, I noticed some strange behavior 
related to combining tactics with match_mp_tac and the ORELSE tactical:


I am trying to write a tactic takes a theorem and first tries out 
whether it is already a proof of the current goal with ACCEPT_TAC.
If this does not succeed, the tactic should try matching the theorem 
with match_mp_tac.


Here is what I have come up with:

fun simple_apply thm = (ACCEPT_TAC thm) ORELSE (match_mp_tac thm);

I have defined a test tactic, to see whether ACCEPT_TAC works as I 
expect it to work:


fun dumb_apply thm = (ACCEPT_TAC thm) ORELSE (FAIL_TAC "Unreachable");

Strangely the simple_apply tactic does not work in cases, where the 
dumb_apply tactic works:


val test_thm = Q.prove (
  ` !(n:num) (P:num -> bool).
   P n ==>
   P n`,
  rpt gen_tac
  DISCH_THEN ASSUME_TAC
  qpat_x_assum `P n` (fn thm => simple_apply thm) (* Fails with "No 
parse of quotation leads to success" *)

  qpat_x_assum `P n` (fn thm => dumb_apply thm)  (* Proves the goal *)
  );


Can someone explain to me what I did wrong with the simple_apply tactic?


Thanks,


Heiko

--
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] deactivate newline-and-indent for sml-mode

[Heiko Becker]

Hello,


thanks for looking into this issue. It works perfectly fine now.


On 01/26/2017 10:25 PM, Chun Tian (binghe) wrote:
> I took a look into sml-mode.el and the documentation [1], it seems that the 
> following Emacs configuration could disable the auto-indent triggered by 
> return key:
>
> (defun my-sml-mode-hook ()
>"Local defaults for SML mode"
>(setq electric-indent-chars '()))
>
> (add-hook 'sml-mode-hook 'my-sml-mode-hook)
>
> P. S. You can only see the effect for newly opened SML code files. (or just 
> restart Emacs)
>
> [1] http://www.smlnj.org/doc/Emacs/sml-mode.html
>
>> Il giorno 26 gen 2017, alle ore 09:43, Heiko Becker 
>> <s9hhb...@stud.uni-saarland.de> ha scritto:
>>
>> Hello everyone,
>>
>> I am currently running into some technical "difficulties" with using HOL4:
>>
>> I found that the emacs sml-mode binds the return key to
>> "newline-and-indent" and I cannot find a way to remove this binding.
>> Problem being that emacs keeps indenting my tactic proofs totally weird,
>> so I would favour being able to indent only on my own.
>>
>> So far, I tried deactivating it similar to what worked for removing
>> tab-indentation
>>
>>(setq default-tab-width 4)
>>(setq-default indent-tabs-mode nil)
>>(global-set-key (kbd "TAB") 'self-insert-command)
>>
>> by setting
>>
>>(global-set-key (kbd "RET") 'newline)
>>
>>
>> Unfortunately this does not work. Can someone help me with this issue
>> with some elisp?
>>
>>
>> Thanks in advance.
>>
>> Best regards,
>>
>> Heiko
>>
>>
>> --
>> 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] deactivate newline-and-indent for sml-mode

[Heiko Becker]

Hello,


thanks for the replies, Magnus and Thomas.

Unfortunately I am already using (electric-indent-mode -1) for SML mode, 
and it does not seem to fix the problem and I do not want to turn off 
auto-indent globally.

I suspect that this may be due to me using the spacemacs configuration, 
so I will check whether there is a fix on this site.

Cheers,

Heiko


On 01/26/2017 12:52 PM, Thomas Tuerk wrote:
> Hello Heiko,
>
> I have the same issue. I just deactivated electric indent mode. So, its
> not a proper solution, but for me it does the trick.
>
> (electric-indent-mode -1)
>
> Best
>
> Thomas Tuerk
>
>
> On 26.01.2017 09:43, Heiko Becker wrote:
>> Hello everyone,
>>
>> I am currently running into some technical "difficulties" with using HOL4:
>>
>> I found that the emacs sml-mode binds the return key to
>> "newline-and-indent" and I cannot find a way to remove this binding.
>> Problem being that emacs keeps indenting my tactic proofs totally weird,
>> so I would favour being able to indent only on my own.
>>
>> So far, I tried deactivating it similar to what worked for removing
>> tab-indentation
>>
>> (setq default-tab-width 4)
>> (setq-default indent-tabs-mode nil)
>> (global-set-key (kbd "TAB") 'self-insert-command)
>>
>> by setting
>>
>> (global-set-key (kbd "RET") 'newline)
>>
>>
>> Unfortunately this does not work. Can someone help me with this issue
>> with some elisp?
>>
>>
>> Thanks in advance.
>>
>> Best regards,
>>
>> Heiko
>>
>>
>> --
>> 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


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

[Hol-info] Evaluation in HOL-Light

[Heiko Becker]

Hello everyone,

suppose I want to evaluate the definition

let factorial = define `(fact (0) = 1)
   /\ (fact (SUC n) = SUC n * fact (n))`;;

in the term

`fact 10`

in HOL-Light.

Do I need to use Conversions to do this or is there a simpler way like
Coq's "Eval compute" or HOL4's "EVAL"?


As a context, I have constructed a function that computes a boolean
result by structural recursion in HOL-Light that can be used as a
certificate checker for a static analysis.

The problem is that currently the certificate checking is very slow
since I am using only rewrite conversions.


Best regards,

Heiko


--
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] Deriving Contradictions

[Heiko Becker]

Hello Petros,

thank you for your fast answer.

Your tactic worked perfectly.


Regards,

Heiko


On 07/04/2016 03:20 PM, Petros Papapanagiotou wrote:
> Hello Heiko,
>
> Try:
>  e (REWRITE_TAC[distinctness "test"]);;
>
> HOL Light automatically produces distinctness theorems for inductive 
> types, accessed through the "distinctness" function.
>
>
> Regards,
> Petros
>
>
> On 04/07/2016 13:36, Heiko Becker wrote:
>> On 07/04/2016 02:34 PM, Heiko Becker wrote:
>>
>>> Hello everyone,
>>>
>>>
>>> suppose I have an inductive type as follows:
>>>
>>> let test_IND, test_CASES =
>>>define_type
>>>  "test = Foo num
>>>|Bar int ";;
>>>
>>> Can someone explain to me how I can derive a contradiction given
>>> equality as in the goal below?
>>>
>>> g `Foo 1 = Bar (&1) ==> F`;;
>>>
>>> Thanks in advance.
>>>
>>> Best regards,
>>>
>>>
>>> Heiko
>>>
>> Forgot to add:
>> I want to do the proof in HOL-Light. Sorry the double post.
>>
>> Best regards.
>>
>> --
>>  
>>
>> 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] Deriving Contradictions

[Heiko Becker]

On 07/04/2016 02:34 PM, Heiko Becker wrote:

> Hello everyone,
>
>
> suppose I have an inductive type as follows:
>
> let test_IND, test_CASES =
>   define_type
> "test = Foo num
>   |Bar int ";;
>
> Can someone explain to me how I can derive a contradiction given 
> equality as in the goal below?
>
> g `Foo 1 = Bar (&1) ==> F`;;
>
> Thanks in advance.
>
> Best regards,
>
>
> Heiko
>

Forgot to add:
I want to do the proof in HOL-Light. Sorry the double post.

Best regards.

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

[Hol-info] Deriving Contradictions

[Heiko Becker]

Hello everyone,


suppose I have an inductive type as follows:

let test_IND, test_CASES =
   define_type
 "test = Foo num
   |Bar int ";;

Can someone explain to me how I can derive a contradiction given 
equality as in the goal below?

g `Foo 1 = Bar (&1) ==> F`;;

Thanks in advance.

Best regards,


Heiko


--
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] Fwd: Re: HOL-Light Beginner Questions

[Heiko Becker]

Am 17.06.2016 4:04 nachm. schrieb "Mark Adams" <m...@proof-technologies.com
>:
>
> I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see the
HOL Light reference manual entry for 'new_inductive_definition').  So I
think you should get what you intend by transforming it to something
logically equivalent, i.e. change "A ==> B ==> C" to "A /\ B ==> C".  The
error messages could be much better here.
>
> Mark.
>

Thank you. That was exactly the problem I had.

Heiko

>
> On 17/06/2016 10:51, Heiko Becker wrote:
>>
>> Hello,
>>
>>
>> On 06/16/2016 01:45 PM, Mark Adams wrote:
>>>
>>> Hi Heiko,
>>>
>>> That's strange, your corrected version goes through fine on my
computer.  Do you still get the same problem if you restart HOL Light and
enter the corrected script?  What version of HOL Light are you using?
>>>
>>> Mark.
>>>
>>>
>>
>>
>> It turns out, that I accidentally loaded both commands. The sstep
definition and the next one. And the failure came from the next one. But I
am unable to fix it currently:
>>
>> let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition
>>   `(!(x:num) (e:exp) (s1:cmd) (s2:cmd) (env:num->real) (v:real).
>>   exp_eval e env = v ==>
>>   bstep s1 (upd_env x v env) s2 ==>
>>   bstep (Ass x e s1) env s2) /\
>>   (!(c:bexp) (s1:cmd) (s2:cmd) (t:cmd) (env:num->real).
>>   bval c env = T ==>
>>   bstep s1 env s2 ==>
>>   bstep (Ite c s1 t) env s2) /\
>>   (!(c:bexp) (s:cmd) (t1:cmd) (t2:cmd) (env:num->real).
>>   bval c env = F ==>
>>   bstep t1 env t2 ==>
>>   bstep (Ite c s t1) env t2)`;;
>> Exception: Failure "dest_var: not a variable".
>>
>> I have tried removing some parts of the definition to see if I have an
undefined variable lying around but could not arrive at some obvious
failure.
>>
>> Best regards,
>>
>> Heiko
>>
>>>
>>> On 16/06/2016 10:01, Heiko Becker wrote:
>>>>
>>>>
>>>>
>>>>  Forwarded Message 
>>>> Subject:
>>>> Re: [Hol-info] HOL-Light Beginner Questions
>>>> Date:
>>>> Thu, 16 Jun 2016 10:59:44 +0200
>>>> From:
>>>> Heiko Becker <heikobecke...@gmail.com>
>>>> To:
>>>> Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
>>>> CC:
>>>> hol-info <hol-info@lists.sourceforge.net>
>>>>
>>>>
>>>>
>>>> On 06/16/2016 01:57 AM, Ramana Kumar wrote:
>>>>>
>>>>> I expect it could be because the Boolean constants are spelled "T"
and "F" rather than "true" and "false" in the logic, so the latter are
being treated as free variables.
>>>>>
>>>>
>>>>
>>>> Thank you for your explanation. I am getting closer to getting my
definition working.
>>>> I have changed it as follows:
>>>>
>>>> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
>>>>   `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s
(upd_env x v env)) /\
>>>>   (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
>>>>   (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;
>>>>
>>>> But now HOL-Light complains about some construct not being a variable:
>>>> Exception: Failure "dest_var: not a variable".
>>>>
>>>> Can you maybe help me again?
>>>>
>>>> Best regards,
>>>>
>>>> Heiko
>>>>
>>>>> On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com>
wrote:
>>>>>>
>>>>>>
>>>>>> My formalization:
>>>>>>
>>>>>> let exp_INDUCT, exp_REC= define_type
>>>>>>"exp = Var num
>>>>>>| Const real
>>>>>>| Plus exp exp
>>>>>>| Sub exp exp
>>>>>>| Mult exp exp
>>>>>>| Div exp exp";;
>>>>>>
>>>>>> let exp_eval_SIMPS = define
>>>>>>`(exp_eval (Var x) E = E x) /\
>>>>>>(exp_eval (Const r) E = r) /\
>&g

Re: [Hol-info] HOL-Light Beginner Questions

[Heiko Becker]

On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants are spelled "T" and 
"F" rather than "true" and "false" in the logic, so the latter are 
being treated as free variables.




Thank you for your explanation. I am getting closer to getting my 
definition working.

I have changed it as follows:

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
  `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s 
(upd_env x v env)) /\

  (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
  (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;

But now HOL-Light complains about some construct not being a variable:
Exception: Failure "dest_var: not a variable".

Can you maybe help me again?

Best regards,

Heiko

On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com 
<mailto:heikobecke...@gmail.com>> wrote:



My formalization:

let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const real
   | Plus exp exp
   | Sub exp exp
   | Mult exp exp
   | Div exp exp";;

let exp_eval_SIMPS = define
   `(exp_eval (Var x) E = E x) /\
   (exp_eval (Const r) E = r) /\
   (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
   (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
   (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
   (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;

let bexp_INDUCT, bexp_REC = define_type
   "bexp = leq exp exp
 | less exp exp";;

let bval_SIMPS = define
   `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval
e2 E)) /\
   (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;

let cmd_INDUCT, cmd_REC = define_type
   "cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;

let upd_env_simps1 = define
   `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v
else E
y)`;;

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
   `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s
(upd_env x v
E)) /\
   (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
   (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;


When loading the sstep definitions I get the following failure:
 Exception: Failure "new_definition: term not closed".



--
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] Fwd: Re: HOL-Light Beginner Questions

[Heiko Becker]

Hello,


On 06/16/2016 01:45 PM, Mark Adams wrote:


Hi Heiko,

That's strange, your corrected version goes through fine on my 
computer.  Do you still get the same problem if you restart HOL Light 
and enter the corrected script?  What version of HOL Light are you using?


Mark.



It turns out, that I accidentally loaded both commands. The sstep 
definition and the next one. And the failure came from the next one. But 
I am unable to fix it currently:


let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition
  `(!(x:num) (e:exp) (s1:cmd) (s2:cmd) (env:num->real) (v:real).
  exp_eval e env = v ==>
  bstep s1 (upd_env x v env) s2 ==>
  bstep (Ass x e s1) env s2) /\
  (!(c:bexp) (s1:cmd) (s2:cmd) (t:cmd) (env:num->real).
  bval c env = T ==>
  bstep s1 env s2 ==>
  bstep (Ite c s1 t) env s2) /\
  (!(c:bexp) (s:cmd) (t1:cmd) (t2:cmd) (env:num->real).
  bval c env = F ==>
  bstep t1 env t2 ==>
  bstep (Ite c s t1) env t2)`;;
Exception: Failure "dest_var: not a variable".

I have tried removing some parts of the definition to see if I have an 
undefined variable lying around but could not arrive at some obvious 
failure.


Best regards,

Heiko



On 16/06/2016 10:01, Heiko Becker wrote:


 Forwarded Message 
Subject:Re: [Hol-info] HOL-Light Beginner Questions
Date:   Thu, 16 Jun 2016 10:59:44 +0200
From:   Heiko Becker <heikobecke...@gmail.com>
To: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
CC: hol-info <hol-info@lists.sourceforge.net>




On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants are spelled "T" 
and "F" rather than "true" and "false" in the logic, so the latter 
are being treated as free variables.


Thank you for your explanation. I am getting closer to getting my 
definition working.

I have changed it as follows:

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
  `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s 
(upd_env x v env)) /\

  (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
  (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;

But now HOL-Light complains about some construct not being a variable:
Exception: Failure "dest_var: not a variable".

Can you maybe help me again?

Best regards,

Heiko

On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com 
<mailto:heikobecke...@gmail.com>> wrote:



My formalization:

let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const real
   | Plus exp exp
   | Sub exp exp
   | Mult exp exp
   | Div exp exp";;

let exp_eval_SIMPS = define
   `(exp_eval (Var x) E = E x) /\
   (exp_eval (Const r) E = r) /\
   (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
   (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
   (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
   (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;

let bexp_INDUCT, bexp_REC = define_type
   "bexp = leq exp exp
 | less exp exp";;

let bval_SIMPS = define
   `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <=
(exp_eval e2 E)) /\
   (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;

let cmd_INDUCT, cmd_REC = define_type
   "cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;

let upd_env_simps1 = define
   `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v
else E
y)`;;

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
   `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s
(upd_env x v
E)) /\
   (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
   (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;


When loading the sstep definitions I get the following failure:
 Exception: Failure "new_definition: term not closed".



Forwarding my message. Send from wrong mail account intially.


--
What NetFlow Analyzer can do for you? Monitors network bandwidth and 
traffic
patterns at an interface-level. Reveals which users, apps, and 
protocols are

consuming the most bandwidth. Provides multi-vendor support for NetFlow,
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning
reports. 
http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381


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


---

[Hol-info] Fwd: Re: HOL-Light Beginner Questions

[Heiko Becker]

 Forwarded Message 
Subject:Re: [Hol-info] HOL-Light Beginner Questions
Date:   Thu, 16 Jun 2016 10:59:44 +0200
From:   Heiko Becker <heikobecke...@gmail.com>
To: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
CC: hol-info <hol-info@lists.sourceforge.net>




On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants are spelled "T" and 
"F" rather than "true" and "false" in the logic, so the latter are 
being treated as free variables.




Thank you for your explanation. I am getting closer to getting my 
definition working.

I have changed it as follows:

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
  `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s 
(upd_env x v env)) /\

  (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
  (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;

But now HOL-Light complains about some construct not being a variable:
Exception: Failure "dest_var: not a variable".

Can you maybe help me again?

Best regards,

Heiko

On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com 
<mailto:heikobecke...@gmail.com>> wrote:



My formalization:

let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const real
   | Plus exp exp
   | Sub exp exp
   | Mult exp exp
   | Div exp exp";;

let exp_eval_SIMPS = define
   `(exp_eval (Var x) E = E x) /\
   (exp_eval (Const r) E = r) /\
   (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
   (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
   (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
   (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;

let bexp_INDUCT, bexp_REC = define_type
   "bexp = leq exp exp
 | less exp exp";;

let bval_SIMPS = define
   `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval
e2 E)) /\
   (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;

let cmd_INDUCT, cmd_REC = define_type
   "cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;

let upd_env_simps1 = define
   `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v
else E
y)`;;

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
   `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s
(upd_env x v
E)) /\
   (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
   (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;


When loading the sstep definitions I get the following failure:
 Exception: Failure "new_definition: term not closed".



Forwarding my message. Send from wrong mail account intially.

--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL-Light Beginner Questions

[Heiko Becker]

Hello everyone,

I am currently learning HOL-Light and therefore working through the 
tutorial from the official page.[1]
To get a feeling for the inductive definitions, I started a 
formalization similar to the semantics on page 109.
My problem is that when I try to define some small step semantics I get 
a failure saying that I have some unbound free variables, but I cannot 
resolve this failure.

My formalization:

let exp_INDUCT, exp_REC= define_type
   "exp = Var num
   | Const real
   | Plus exp exp
   | Sub exp exp
   | Mult exp exp
   | Div exp exp";;

let exp_eval_SIMPS = define
   `(exp_eval (Var x) E = E x) /\
   (exp_eval (Const r) E = r) /\
   (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
   (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
   (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
   (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;

let bexp_INDUCT, bexp_REC = define_type
   "bexp = leq exp exp
 | less exp exp";;

let bval_SIMPS = define
   `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\
   (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;

let cmd_INDUCT, cmd_REC = define_type
   "cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;

let upd_env_simps1 = define
   `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E 
y)`;;

let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
   `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v 
E)) /\
   (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
   (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;


When loading the sstep definitions I get the following failure:
 Exception: Failure "new_definition: term not closed".


Can someone maybe help me figuring out where this failure comes from?

Thanks in advance.

Best regards,

Heiko

---
[1]: https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf

--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity planning
reports. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info