Re: [Hol-info] Difference between sets formats
Dear Thomas,
Thank you so much for your elaborated reply.
I will go through Section 5.5.1.1 that you referred to
Thanks again!
Yassmeen
On Fri, Oct 25, 2019 at 1:22 PM Thomas Tuerk
wrote:
> Dear Yassmeen,
>
> set comprehensions in HOL are a bit cryptic. They are explained in Section
> 5.5.1.1 of the Description manual. In short, something like {t | p} is
> syntactic sugar that is turned by the parser into GSPEC(\(x1 ,...,xn).
> (t,p)). The trick is figuring out, which variables x1, ... xn to use. There
> are rules for that, which for non-trivial cases gives sometimes unexpected
> results. See excerpt from Sec. 5.5.1.1 below. For making it unambiguous,
> there is also the form {t | (x1, ..., xn) | p} where the variables are
> given explicitly. For complicated sets, I would always use the explicit
> form and I would not be surprised if L is free in one of the forms below
> and free in the other. In my opinion the syntax {t | p} should only be used
> in trivial cases, because it can easily lead to human readers
> misunderstanding the meaning otherwise. I for one are confused by
> complicated examples like the comprehensions you use. I need essentially to
> run the parser and look at the result before knowing what the meaning is.
> The following trace might be useful to show more information when
> pretty-printing the parsed comprehensions:
>
> set_trace "pp_unambiguous_comprehensions" 1
>
>
> Excerpt from Section 5.5.1.1
>
> The normal interpretation of { t | p } is the set of all ts such that
> p. In HOL , such syntax parses to: GSPEC(\(x 1 ,...,x n ).(t,p)) where x 1
> , ... , x n are those
> free variables that occur in both t and p if both have at least one free
> variable. If t or p
> has no free variables, then x 1 , ... , x n are taken to be the free
> variables of the other term.
> If both terms have free variables, but there is no overlap, then an error
> results. The
> order in which the variables are listed in the variable structure of the
> paired abstraction
> is an unspecified function of the structure of t (it is approximately left
> to right).
>
> I hope this helps.
>
> Thomas
>
>
> On 25.10.19 18:05, Yassmeen Derhalli wrote:
>
> Hi,
> I have this proof goal, where I need to prove that two sets are equal.
>
> {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
> a |
> a IN if j IN L then s3 j else s4 j} =
> {{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
> a IN if j IN L then s3 j else s4 j}
>
> I have two questions regarding this proof, first, what is the difference
> between the first format when we use "|a | a IN" (the left side of the
> goal) and the second format "...|a IN..." (the right side of the goal)?
> Secondly, are these sets equal? because it seems that HOL treats set L in
> the right side of the goal as a dummy variable of the set.
> I need help in clarifying the difference between both formats and some
> clues about how to proceed with the proof if the sets are equal.
>
> Best Regards,
> Yassmeen Elderhalli
>
>
> ___
> hol-info mailing
> listhol-info@lists.sourceforge.nethttps://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] Difference between sets formats
Hi,
I have this proof goal, where I need to prove that two sets are equal.
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a |
a IN if j IN L then s3 j else s4 j} =
{{f i | i IN if a IN {b | b IN L} then s1 a else s2 a} |
a IN if j IN L then s3 j else s4 j}
I have two questions regarding this proof, first, what is the difference
between the first format when we use "|a | a IN" (the left side of the
goal) and the second format "...|a IN..." (the right side of the goal)?
Secondly, are these sets equal? because it seems that HOL treats set L in
the right side of the goal as a dummy variable of the set.
I need help in clarifying the difference between both formats and some
clues about how to proceed with the proof if the sets are equal.
Best Regards,
Yassmeen Elderhalli
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] Exception raised while using HOL in hol-mode
Hi,
thank you for your reply.
I am using an oracle virtual machine on my laptop
running ubuntu-16.04.4-desktop-i386. I have been using this machine for
about three months now, and I have not had any problem until yesterday.
Best Regards,
Yassmeen
On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk
wrote:
> Hi,
>
> I believe this is due to how hol-mode copies input from emacs buffers to
> HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff. (
> https://github.com/HOL-Theorem-Prover/HOL/blob/
> master/tools/hol-mode.src#L800). If a chunk of text you want to send
> exceeds a certain size, it is written to a temp-file instead and "use
> tempfile" is send to HOL. I fear this is going wrong for some reason.
> hol-mode tries to write the chunk of text to the file "/tmp/hol2207zVM" and
> then sends "use "/tmp/hol2207zVM" to HOL. However, for some reason HOL
> cannot find this file. This results in the error message you posted.
>
> How to fix it is a good question. I have seen this error before when
> working remotely with HOL. When using HOL via ssh or in some virtual
> environment like a docker container, I had the problem before that the
> communication with HOL worked just fine, but HOL and emacs saw different
> "/tmp" directories (e.g. the ones on the local and remote machine). Are you
> using anything like this? What environment are you running HOL in?
>
> Best
>
> Thomas
>
>
>
> On 20.09.2018 17:40, Yassmeen Derhalli wrote:
>
> Hi,
>
> Sorry for sending this email again, but it seems that there was a problem
> with the first email
>
> I am using HOL4, yesterday I started receiving this error message
>
> Exception raised Io {cause = SysErr ("No such file or directory", SOME
> ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"}
>
> I am using HOL4 in the hol-mode, but when I use HOL directly using the
> shell, my script runs fine, this only happens in the hol-mode, any clue why
> this could happen and how can I fix it?
>
> thanks
>
>
>
>
>
> ___
> hol-info mailing
> listhol-info@lists.sourceforge.nethttps://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 mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Exception raised while using HOL in hol-mode
Hi,
Sorry for sending this email again, but it seems that there was a problem
with the first email
I am using HOL4, yesterday I started receiving this error message
Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"}
I am using HOL4 in the hol-mode, but when I use HOL directly using the
shell, my script runs fine, this only happens in the hol-mode, any clue why
this could happen and how can I fix it?
thanks
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] (no subject)
Hi, I am using HOL4 in hol-mode, yesterday I started receiving this error message ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
