Re: [Hol-info] Difference between sets formats

[Thomas Tuerk]

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 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] Transform under binders

[Thomas Tuerk]

Hi Haitao,

it all depends on what exactly you want to do. Sometimes it is as easy
as using GSYM instead of SYM. Of you can use something like DEPTH_CONV
or ONCE_DEPTH_CONV. That's how GSYM is defined in terms of SYM. Or you
could use something more specialised like STRIP_BINDER_CONV or
STRIP_QUANT_CONV. Notice that these are all conversionen, so you wrap
the whole thing in CONV_RULE.

Best

Thomas


On 28.02.19 09:38, Haitao Zhang wrote:
> Rules like SYM do not work with top level binders. What is the
> recommended way to use them with binders without having to stack up
> SPEC and GEN?
>
> Thanks,
> Haitao
>
>
> ___
> 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] Exception raised while using HOL in hol-mode

[Thomas Tuerk]

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 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] conflicts auto-resolved by Define?

[Thomas Tuerk]

Hi Chun, Waqar,

"Define" does indeed give priority to earlier clauses. Under the hood
pattern compilation takes place. So what is actually is going on for

> val extreal_add_def = Define`
>   (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>   (extreal_add PosInf a = PosInf) /\
>   (extreal_add a PosInf = PosInf) /\
>   (extreal_add NegInf b = NegInf) /\
>   (extreal_add c NegInf = NegInf)`;

Is similar to what would happen for

val extreal_add_def = Define`
  (extreal_add a b = case (a, b) of
 (Normal x, Normal y) => (Normal (x + y))
   | (PosInf, _) => PosInf
   | (_, PosInf) => PosInf
   | (NegInf, _) => NegInf
   | (_, NegInf) => NegInf

In both cases, the pattern match (case-expression) is compiled to a
decision tree using various heuristics. This tree contains implicitly a
complete list of distinct patterns.
Distinct means that the patterns don't overlap. Complete means that they
cover every possible value. For case-expressions you get the decision
tree itself back. For top-level pattern matches you get a list of
non-overlapping patterns back that are used for the returned definition
theorem. If you look at the result of the original definition, you will
see that the actual definition theorem is

  |- !y x v5 v3 v2 a.
  (extreal_add (Normal x) (Normal y) = Normal (x + y)) /\
  (extreal_add PosInf a = PosInf) /\
  (extreal_add NegInf PosInf = PosInf) /\
  (extreal_add (Normal v2) PosInf = PosInf) /\
  (extreal_add NegInf NegInf = NegInf) /\
  (extreal_add NegInf (Normal v5) = NegInf) /\
  (extreal_add (Normal v3) NegInf = NegInf)

Here you see that the original clauses disappeared. Instead patterns
from resulting from this pattern compilation are used. Notice that
similar to SML and other functional languages, Define gives precedence
to earlier clauses.

Most case-expressions are simple and pattern compilation is not an
issue. However, for more complicated cases it can be hard to predict
what the results will be. If you are interested, I recommend having a
look at section 6.4 of the description manual. I personally try not to
use non-trivial definitions directly, but use the theorems produced by
Define to prove simple, manually stated sanity check lemmata. I believe
this makes proofs more robust and helps me detect problems with my
definitions earlier.

Best

Thomas


On 05.08.2018 18:09, Waqar Ahmad via hol-info wrote:
> Hi Chun,
>
> I'm not sure about your potential conflict question but we are now
> using an improved definition of "extreal_add_def" 
>
> val extreal_add_def = Define`
>    (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>    (extreal_add (Normal _) a = a) /\ 
>    (extreal_add b (Normal _) = b) /\
>    (extreal_add NegInf NegInf = NegInf) /\
>    (extreal_add PosInf PosInf = PosInf)`;
>
> This will rule out the possibility of PosInf + a= PosInf... We do have
> a plan to update the probability theory to the latest version in the
> near future (Speaking on the behalf of original authors). 
>
>
>
> On Sun, Aug 5, 2018 at 11:14 AM Chun Tian  > wrote:
>
> Hi,
>
> the version of “extreal” (extended real numbers) in latest HOL4
> has a wrong definition for sum:
>
> val _ = Hol_datatype`extreal = NegInf | PosInf | Normal of real`;
>
> val extreal_add_def = Define`
>   (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>   (extreal_add PosInf a = PosInf) /\
>   (extreal_add a PosInf = PosInf) /\
>   (extreal_add NegInf b = NegInf) /\
>   (extreal_add c NegInf = NegInf)`;
>
> according to this definition, one could prove the wrong statement
> ``PosInf + NegInf = NegInf + PosInf = PosInf``, e.g.
>
>> PROVE [extreal_add_def] ``extreal_add PosInf NegInf = PosInf``;
> Meson search level: ..
> val it = ⊢ PosInf + NegInf = PosInf: thm
>
> P. S. the original authors have fixed this issue in their latest
> version of probability theories, which I’m now working on merging
> them into HOL4.
>
> What I don’t quite understand here is, shouldn’t one also prove
> that ``PosInf + NegInf = NegInf + PosInf = NegInf``, as the last
> two lines of extreal_add_def stated, but it turns out that this is
> not true (PROVE command doesn’t return):
>
>> PROVE [extreal_add_def] ``extreal_add NegInf PosInf = NegInf``;
> Meson search level: .Exception- Interrupt raised
>
> of course it can’t be proved, because otherwise it means ``PosInf
> = NegInf``, contradicting the axioms generated by Hol_datatype,
> then the whole logic would be inconsistent.
>
> But given the fact that above definition can be directly accepted
> by Define command, does HOL internally resolve potential conflicts
> by putting a priority on each sub-clauses based on their
> appearance order?
>
> Regards,
>
> Chun Tian
>
> 
> 

Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem?

[Thomas Tuerk]

Hi Chun,

the easiest way is using alpha-equivalence. If you really just want to
rename vars, you can state the new form explicitly and use
apha-equivalence via e.g. ALPHA directly. Tools like METIS_TAC should in
theory be able to do it, but in practice try to do too much and
therefore time out, I fear.

There are also tools for renaming bound vars. "rename_bvar" for example
is a conversion for renaming an outermost bound var.

Variables at subpositions can also be renamed using the quantifier
heuristics lib (see, e.g. INST_QUANT_CONV)

Vaguely related are tools for renaming free vars during a tactical
proof. There are various related tactics for this, e.g. RENAME_TAC.
However, since these deal with free vars during a proof, this does not
fit really here.


So, there are plenty of options. Looking at your description, I expect
using ALPHA is the easiest and fasted possibility for your problem. I
would use something like

fun ALPHA_RULE t thm = let
  val t0 = concl thm
  val thm1 = ALPHA t0 t
  val thm2 = EQ_MP thm1 thm
in
  thm2
end


val t0 = ``?A.  A  \/ !B  C. ?D.  D  B  C``
val t  = ``?A'. A' \/ !B' C. ?DD. DD B' C``

val thm0 = METIS_PROVE [] t0
val thm = ALPHA_RULE t thm0

Best

Thomas



On 03.08.2018 14:34, Chun Tian (binghe) wrote:
> Hi,
>
> suppose I have proved (or generated) a theorem like this:
>
>  ⊢ ∀a0 a1.
>  a0 ∼ a1 ⇔
>  ∀u.
>  (∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
>  ∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2
>
> but I don’t like the variables names (a0, a1, E1, E2), I want a new theorem, 
> essentially the same one, but with variables names same as in text book:
>
> ⊢ ∀P Q.
>  P ∼ Q ⇔
>  ∀u.
>  (∀P'. P --u-> P' ⇒ ∃Q'. Q --u-> Q' ∧ P' ∼ Q') ∧
>  ∀Q'. Q --u-> Q' ⇒ ∃P'. P --u-> P' ∧ P' ∼ Q’
>
> if I understood HOL correctly, it is impossible to directly modify any 
> theorem (as first-class object), replacing its bound variables with different 
> names (if not conflicting others).
>
> Actually, changing the outside universal quantifiers is easy, as I just need 
> to do a SPEC with new variables, then GEN them. On the other side, I don’t 
> see any automatic way to replace inner variables.   I also tried to prove the 
> new theorem by PROVE_TAC or METIS_TAC with the old theorem, sometimes the 
> theorem can be directly proved, but most of time it fails, I think because of 
>  those existential quantifiers.
>
> Does anyone have such experiences? (it’s a painful process to go over all 
> proofs again, fixing almost every step with different variable names)
>
> Regards,
>
> Chun Tian
>
>
>
> --
> 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] INST on a theorem

[Thomas Tuerk]

Hi,

hard to say, why it does not work without further details. However, one
guess is that types do not match. I would recommend showing the types
when printing the theorem. I expect that P might be of type `'a ->
bool`. In this case you need to instantiate 'a to string first.

Best

Thomas


On 23.07.2018 18:10, Dylan Melville wrote:
> I have a theorem called EX which returns true when a value is an
> element of a list. It is defined as:
>
> thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t)
>
> I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t`
> being a long list of strings which contains “T”.  Unfortunately my
> attempts to use INST on this theorem haven’t worked. Why doesn’t the
> following work?
>
> INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;;
>
> Thank you.
>
> -Dylan Melville (McMaster University)
>
>
> --
> 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] Adding abstraction to terms

[Thomas Tuerk]

Hi Dylan,

I'm not aware of such a "tactical". In fact, I'm uncertain what you are
looking for. A tactical is a SML function used to build tactics. An
example is "REPEAT". It is of type "tactic -> tactic". Given a tactic,
it returns another tactic that applies the argument tactic repeatedly.

I guess (please correct me if I'm wrong) that you look for something
like "aconv". Given two terms you want to check whether they are "equal
with an added abstraction". So I guess you want something like

"aebconv" of type  "term -> term -> bool" with the following example
behaviours

aebconv ``( f:(num->bool) ) n`` ``(\x:num. f:(num->bool) x) n`` returns true
aebconv ``f:(num->bool)`` ``(\x:num. f:(num->bool) x)`` returns true
aebconv returns false if they are not equal.

Notice, that I added a missing argument 'x' inside the lambda in both
cases. Your original theorems have this typo in.

Is this the kind of function you are looking for? In this case, what you
are looking for is equivalence up to beta- and eta-reduction. "aconv"
checks for alpha-equivalence, i.e. equivalence up to names. I'm not
aware of any function that checks equivalence up to beta- and
eta-reduction. You could do the reductions and then check the results
for alpha-equivalence. There is "beta_conv" and "eta_conv" that do
one-top-level step of such conversions. They are both very basic
conversions. I.e. given a term t, they try to change it at top-level and
return if they succeed a theorem of form |- t = t'. You could apply
these repeatedly (DEPTH_CONV) and compare the results with aconv. These
names are the ones used by HOL 4, I believe for HOL light they are the
same. I have not checked though.

Or are you interested in a proof of the equality? This would be in the
logic and the statement would actually say that both sides are equal,
not that they have the same beta- and eta-normal form.

If you tell me more about what you want to do, I can perhaps help better.

Best

Thomas Tuerk


On 06.07.2018 19:01, Dylan Melville wrote:
> Is there a tactical that shows that a term is equal to the same term with an 
> added abstraction, for example:
>
> |- ( f:(num->bool) ) n <=> (\x:num. f:(num->bool) ) n
>
> Or even more simply
>
> |- f:(num->bool) <=> (\x:num. f:(num->bool) )
> --
> 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] Loops in HOL4

[Thomas Tuerk]

Dear Shang,

reading your question, I was wondering, whether you really want to use a
WHILE loop. Usually you would rather use recursion in HOL. In higher
order logic you don't have a state that you can modify. Of course you
can mimic a state by passing it around explicitly. This is what the
WHILE function does. If you are new to HOL and have not done much
functional programming before, I recommend learning functional
programming first. Prof. Larry Paulson's book "ML for the working
programmer" is available online and a very good introduction
http://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html.

I'm also uncertain what you want to do exactly, but for me it sounds
like a combination of standard list functions like MAP, TAKE or FOLDL
might be what you really want. In HOL you talk about the value of
things, you don't have a global state to manipulate and there is nothing
like execution or an execution order. So - while it is a common thing to
say and people do it very frequently as a shortcut - strictly speaking
"removing the first n items of a list" is not something you can do. You
cannot modify an existing list. You talk about the first n elements of a
list (TAKE) or about the list you get by removing the first n elements
(DROP), but you don't have a concept of execution there and the original
list does not change. You talk about values and pass different lists
around explicitly. Similarly things like "operate on them" sounds like
doing something that modifies the global state (like e.g. printing
them). This is just nothing you can do in HOL. Timing is meaningless as
well. So things like first do something then "continue" to do something
else is meaningless. You talk about the value of a function, not how you
compute that value.

Best

Thomas


On 05.06.2018 04:23, 尚亚龙 wrote:
> Hi Waqar,
>
>
> First of all thanks for the reply. Your answer is very helpful to me. 
>
> What I want to achieve is to remove the first n items of the list each
> time and operate on them, 
>
> and then continue to perform the same operation on the rest of the
> list until the list is empty. 
>
> So after reading your reply, this problem can be solved. 
>
>
> thank you
>
>
> Shang
>
>
> -原始邮件-
> *发件人:*"Waqar Ahmad" <12phdwah...@seecs.edu.pk>
> *发送时间:*2018-06-05 07:43:50 (星期二)
> *收件人:* "尚亚龙" <2016210...@mail.buct.edu.cn>
> *抄送:* hol-info 
> *主题:* Re: [Hol-info] Loops in HOL4
>
> I'm not sure what actually you desired with WHILE function but I
> can explain its functioning that might help you to define your
> function.
>
> For instance, you can define a function that continue traversing
> over a list until "P h" is true otherwise return the remaining
> part of the list.
>
> !P L. dropWhile_new P L = WHILE (\a. P (HD a)) TL L
>
> a trivial example could be
>
> val dropWhile_eq = store_thm("dropWhile_eq",
>   ``ALL_DISTINCT [a;b;c] ==> (dropWhile_new ($=a) [a;b;c] = [b;c])``,
> rw[dropWhile_new_def]
> \\ once_rewrite_tac[WHILE]
> \\ rw[]
> \\ once_rewrite_tac[WHILE]
> \\ rw[]);
>
> I hope this helps
>
>
> On Mon, Jun 4, 2018 at 10:08 AM, 尚亚龙 <2016210...@mail.buct.edu.cn
> > wrote:
>
> Hi everyone,
>  
>   
> I'm just beginning to learn HOL4. And I have a question.
>
>
>
> The problem is as follows: I have a list 'a',
>  
> I want to use a loop to retrieve the number of 'num' in a each
> time until the list is empty, 
>
> and I see WHILE theorems can be used in the HOL library, but I
> can not succeed, 
>
> So I would like to ask how to implement the WHILE theorem,
>  
> if you can, please attach an example to explain. Thank you!
>
>
>
> Shang
>
> 
> --
> 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
> 
>
>
>
>
> -- 
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>
>
>
> --
> 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
> 

Re: [Hol-info] Poly/ML debugging facility does not work in HOL4

[Thomas Tuerk]

I'm also not using the Poly/ML debugger and don't think this has high
priority. I was just curious and tried it with an old version I had
lying around. With Poly/ML 5.6 and revision
15e37a5df6ea4b6680e57420257ba30b2e45ceac from 12 July 2017 it did still
work. With the same Poly/ML and a current version
689b9eb3eccdebc314664a6e583c8d8bc76c0591 I get the behavior described by
Mario.

Thomas


On 20.04.2018 06:02, michael.norr...@data61.csiro.au wrote:
> I've never used the Poly/ML debugger. The HOL4 REPL is a custom piece of code 
> (handling the lexing of “...” forms, for example), so I guess this interferes 
> with what the debugger wants to do.  If you wanted to use the debugger, you 
> might be able to get things to work by manually use-ing the HOL SML sources 
> into the standard poly REPL.
>
> Michael
>
> On 20/4/18, 02:44, "Mario Xerxes Castelán Castro"  
> wrote:
>
> Hello.
> 
> When I tried to use the Poly/ML debugger as described in
> 
> breakpoints do not work. “breakIn” does not raise an exception, but when
> applying the exception, the debugger is not entered. I check this within
> the HOL mode for Emacs, running “hol.bare” from the command like and
> running “poly” from the command line (to confirm that debugging works as
> intended without HOL). Only the later (Poly/ML without HOL4) worked.
> 
> Is there a way to use the debugger from within HOL4?
> 
> Thanks.
> 
> -- 
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> 
> 
>
> --
> 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] "Gordon Computer"

[Thomas Tuerk]

Sorry, I copied my reply to another thread in the wrong message. Please
ignore it. Thomas


On 07.04.2018 08:43, Thomas Tuerk wrote:
>
> Hi,
>
> higher order matching is decidable, but has a very high complexity.
> (see e.g. "An introduction to decidability of higher-order matching",
> Colin Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher
> order unification is undecidable, but matching is decidable. As I
> understand it, HOL supports higher-order patterns for higher-order
> matching. This has polynomial complexity. In case you use anything
> else than a higher-order pattern (slightly extended), all bets are
> off. It might work or fail.
>
> I can't remember, where I got this belief that HOL supports
> higher-order patterns. Looking for some reference, I could not find
> much documentation either, but Section 7.5.4.4 in the description
> manual seems to hint in this direction
>
>> The simplifier uses a special form of higher-order matching. If a
>> pattern includes a
>> variable of some function type (f say), and that variable is applied
>> to an argument a
>> that includes no variables except those that are bound by an
>> abstraction at a higher
>> scope, then the combined term f (a) will match any term of the
>> appropriate type as long
>> as the only occurrences of the bound variables in a are in sub-terms
>> matching a.
>>
>
> A higher-order pattern means that in your term, all arguments of free
> variables are distinct _bound_ variables.
> In your first example, both "f" and "x" are free. "f x" is not a
> higher-order pattern. If you bind "x" somehow, it works:
>
> > ho_match_term [] empty_tmset ``(f :'a -> 'a) x`` ``y :'a``
> Exception-
>    HOL_ERR
>  {message = "at Term.dest_comb:\nnot a comb", origin_function =
>   "ho_match_term", origin_structure = "HolKernel"} raised
>
> > ho_match_term [] (HOLset.add (empty_tmset, ``x:'a``)) ``(f :'a ->
> 'a) x`` ``y :'a``
> val it =
>    ([{redex = “f”, residue =
>   “λx. y”}], []):
>    {redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>
> > ho_match_term [] empty_tmset ``\x. (f :'a -> 'a) x`` ``\x:'a. y :'a``
> val it =
>    ([{redex = “f”, residue =
>   “λx. y”}], []):
>    {redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>
> I believe the restriction that all arguments need to be variables can
> be lifted. So matching against "f (x+1) y" does work, if "x" and "y"
> are distinct bound vars. However, "x+1" really has to occur literally.
> This kind of higher order matching is what you normally need for
> rewriting and it is efficiently implementable.
>
> As for your example which returns an invalid solution:
>
>>> ho_match_term [] empty_tmset “(λx :'a. t :'a)” “(λx :'a. x)”;
>> val it =
>>([{redex = “t”, residue = “x”}], []):
>>{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>>
>
> Yes, ho_match_term can produce wrong results, in case no solution
> exists. I'm not sure whether this is deliberate or a bug. In any case,
> it does not effect rewriting and other tools, because it is caught later.
>
> Best
>
> Thomas
>
>
> On 07.04.2018 08:23, michael.norr...@data61.csiro.au wrote:
>>
>> Thanks for digging out this material Larry!  I’d be very happy to see
>> it added to our examples directory.
>>
>>  
>>
>> Ramana, let me know if you want to make the initial commits.  I
>> suggest we can have an examples/hardware with an appropriate README.
>>
>>  
>>
>> Best,
>>
>> Michael
>>
>>  
>>
>> *From: *Lawrence Paulson <l...@cam.ac.uk>
>> *Date: *Friday, 6 April 2018 at 21:27
>> *To: *Ramana Kumar <ramana.ku...@cl.cam.ac.uk>, HOL-info list
>> <hol-info@lists.sourceforge.net>
>> *Subject: *Re: [Hol-info] "Gordon Computer"
>>
>>  
>>
>> I am not sure who is in charge of HOL4 these days. Would it be
>> possible to add this as an example to HOL4? If people are interested,
>> I found many other examples. Here are just two of them:
>>
>>  
>>
>> * the specification and verification of some CMOS adders
>>
>> * Transistor Implementation of a n-bit Counter
>>
>>  
>>
>> I also found Mike's original computer, which is a slightly larger
>> example than Tamarack.
>>
>>  
>>
>> Larry
>>
>>
>>
>> On 5 Apr 2018, at 14:31, Ramana Kumar
&

Re: [Hol-info] Higher order matching in HOL4

[Thomas Tuerk]

Hi,

higher order matching is decidable, but has a very high complexity. (see
e.g. "An introduction to decidability of higher-order matching", Colin
Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order
unification is undecidable, but matching is decidable. As I understand
it, HOL supports higher-order patterns for higher-order matching. This
has polynomial complexity. In case you use anything else than a
higher-order pattern (slightly extended), all bets are off. It might
work or fail.

I can't remember, where I got this belief that HOL supports higher-order
patterns. Looking for some reference, I could not find much
documentation either, but Section 7.5.4.4 in the description manual
seems to hint in this direction

> The simplifier uses a special form of higher-order matching. If a
> pattern includes a
> variable of some function type (f say), and that variable is applied
> to an argument a
> that includes no variables except those that are bound by an
> abstraction at a higher
> scope, then the combined term f (a) will match any term of the
> appropriate type as long
> as the only occurrences of the bound variables in a are in sub-terms
> matching a.
>

A higher-order pattern means that in your term, all arguments of free
variables are distinct _bound_ variables.
In your first example, both "f" and "x" are free. "f x" is not a
higher-order pattern. If you bind "x" somehow, it works:

> ho_match_term [] empty_tmset ``(f :'a -> 'a) x`` ``y :'a``
Exception-
   HOL_ERR
 {message = "at Term.dest_comb:\nnot a comb", origin_function =
  "ho_match_term", origin_structure = "HolKernel"} raised

> ho_match_term [] (HOLset.add (empty_tmset, ``x:'a``)) ``(f :'a -> 'a)
x`` ``y :'a``
val it =
   ([{redex = “f”, residue =
  “λx. y”}], []):
   {redex: term, residue: term} list * (hol_type, hol_type) Lib.subst

> ho_match_term [] empty_tmset ``\x. (f :'a -> 'a) x`` ``\x:'a. y :'a``
val it =
   ([{redex = “f”, residue =
  “λx. y”}], []):
   {redex: term, residue: term} list * (hol_type, hol_type) Lib.subst

I believe the restriction that all arguments need to be variables can be
lifted. So matching against "f (x+1) y" does work, if "x" and "y" are
distinct bound vars. However, "x+1" really has to occur literally. This
kind of higher order matching is what you normally need for rewriting
and it is efficiently implementable.

As for your example which returns an invalid solution:

>> ho_match_term [] empty_tmset “(λx :'a. t :'a)” “(λx :'a. x)”;
> val it =
>([{redex = “t”, residue = “x”}], []):
>{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>

Yes, ho_match_term can produce wrong results, in case no solution
exists. I'm not sure whether this is deliberate or a bug. In any case,
it does not effect rewriting and other tools, because it is caught later.

Best

Thomas


On 06.04.2018 18:28, Mario Xerxes Castelán Castro wrote:
> Hello.
>
> What variant of higher order matching is “ho_match_term” supposed to
> perform?. This function is undocumented, despite being at the core of
> the simplifier, and there are many variants of higher order unification
> described in the literature (unlike first order unification), so it is
> unclear what it is supposed to do. The general case is undecidable and
> there are no most general solutions[1].
>
> At first I thought that it was second order matching, but it does not
> solve a simple second order matching problem:
>
>> ho_match_term [] empty_tmset “(f :'a -> 'a) x” “y :'a”;
> Exception-
>HOL_ERR
>  {message = "at Term.dest_comb:\nnot a comb", origin_function =
>   "ho_match_term", origin_structure = "HolKernel"} raised
>
> A second order solution is f := «λz. y». Another one is x := «y». f :=
> «λx. x». Next is a case where “ho_match_term” gives an anomalous answer;
> the substitution returned is not a solution in the sense of [1] (because
> alpha-renaming would occur to avoid capture of “x”):
>
>> ho_match_term [] empty_tmset “(λx :'a. t :'a)” “(λx :'a. x)”;
> val it =
>([{redex = “t”, residue = “x”}], []):
>{redex: term, residue: term} list * (hol_type, hol_type) Lib.subst
>
> I am asking this because:
>
> * I would find useful to use some notion of “higher order rewriting” in
> custom tactics and while “ho_match_term” empirically seems to work, it
> does not seem a good idea to use it if I do not really know what it is
> doing.
>
> * Since “ho_match_term” is used by several tacticals, I am concerned
> that the informal specification that “ho_match_term” was written for
> does not matches the expectation of the authors of those tacticals
> (e.g.: the simplifier of simpLib, metis). This is a possible source of
> errors (“bugs”).
>
> Thanks.
>
> [1] “Handbook of Automated Reasoning, vol. II”, A. Robinson, A.
> Voronkov, 2001, Chapter 16 “Higher-Order Unification and Matching”.
>
>
>
> --
> Check out the vibrant tech community on one 

Re: [Hol-info] HOL Help for Axiom.

[Thomas Tuerk]

Hi,

just too clarify. Axioms and oracles are different things in HOL 4. In
the context of HOL 4, an "oracle" usually refers to external proof tool
which is trusted by HOL. Its results are "imported" using HOL's "oracle
mechanism" (mk_oracle_thm and related). Oracles are __not__ axiom
schemata. Axioms are only used to make your logic stronger, i.e. (2). Of
course, in a theorem prover you can abuse axioms to do (1). However,
even if you do it, you would not call it introducing new axioms.
However, usually theorem provers provide a different mechanism for (1).
In HOL 4 the oracle mechanism is used for (1). Things like
"boosLib.cheat" are implemented with it.

Best

Thomas


On 12.03.2018 18:41, Mario Xerxes Castelán Castro wrote:
> There are 2 reasons for adding new axioms and axiom schemata (oracles):
>
> (1) To save the work for proving something provable or constructible
> (e.g.: one could assume the axioms for the real numbers instead of
> constructing the reals; although in this case, the library includes a
> construction of the reals)
>
> (2) Because the axiom is not provable from within the logic, i.e.: you
> want to make the theory stronger.
>
> In case (1), maybe the axiom you needs are already proved or available
> as a theory. You will have to search for it. Check the theory tree
>
> In case (2), you can add a new axiom (refer to Thomas message) or state
> your theorems as an implication, where the antecedent suffices to encode
> your new axioms or axiom schemata.
>
>
>
> --
> 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] HOL Help for Axiom.

[Thomas Tuerk]

Dear Sana,

it is easily possible to define own axioms and inference rules. However,
it very easily leads to inconsistencies and is usually not advisable
expect if you really know what you are doing. In most cases the
definitional extension principles provided by HOL suffice and are much
safer to use (see https://hol-theorem-prover.org/hol-course.pdf, slide
121 onwards).

HOL distinguishes between new axioms
(https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Theory.new_axiom.html)
and oracles
(https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Thm.mk_oracle_thm.html).
"new_axiom" and "mk_oracle_thm" both introduce new theorems without
requiring a proof. They are therefore very similar. However, "new_axiom"
is intended to be used for extending the logic of HOL, while
"mk_oracle_thm" is used to introduce theorems that could be proved in
the existing logic but for which you don't have a proof. A typical
example is that you trust the results of some oracle like an external
sat solver. From a pragmatic point of view, it is hard to keep track of
what depends on a new axiom, while it is thanks to tags easy to keep
track of what depends on an oracle theorem. New inference rules can be
coded as ML functions using "mk_oracle_thm".

So, it is easy to define own inference rules and axioms. However, it is
usually not necessary. You can introduce inconsistencies when doing it
and might have a harder time convincing reviewers that your development
is sensible. I would therefore check double, whether tools like
"new_specification"
(https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/Docfiles/HTML/Definition.new_specification.html)
are not more useful for your purposes.

Best

Thomas


On 12.03.2018 08:54, Sana Imtiaz via hol-info wrote:
> Hey.
> Hope you are fine. I am doing MS from National University of Science
> and Technology Islamabad. I need your help as i am working with HOL
> environment. Is it possible to define an *Inference Rule* or *Axiom*
> by myself? Kindly please guide me in this matter. 
>
> Waiting for your kind response. Thank you.
>
> Regards,
> Sana Imtiaz
> MSIT-16
> NUST 
>
>
> --
> 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] Simplifying expressions like «P ∧ P ∧ Q»

[Thomas Tuerk]

Hi,

the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
description manual). AC normalisation would sort multiple occurrences of
the same operant next to each other. Therefore these multiple
occurrences can then be removed by providing 2 idempotency rewrite rules:

f x x = x

f x (f x y) = f x y

This provides a very high level simple way to do what you want, I believe.

If you want something lower level, more efficient with finer control,
you could use "sort" from structure "AC_Sort". It provides a conversion
that does what you want if instantiated properly. However, I never used
it myself, so I don't have first hand experience with it.

There is also the structure "AC" from refute. However, I believe in
contrast to "AC_Sort", there is no direct support for idempotency in "AC".

Cheers

Thomas


On 21.02.2018 18:34, Mario Xerxes Castelán Castro wrote:
> Hello.
>
> Is there an existing tactic for removing multiple appearances of an
> operand under an operator «f» that has the property «f x x = x» and is
> associative-commutative? For example, conjunction and disjunction.
>
> If not, I can write one for HOL4, but I do not want to duplicate
> existing work.
>
> Thanks.
>
>
>
> --
> 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] Using polyscripter with user-written theories

[Thomas Tuerk]

Hi Heiko,

you need to load the theory before you can open it. Usually you don't
need to take care of it yourself, because tools like Holmake or the
emacs mode take care of it for you. However, for polyscripter you need a
line like

>>__ load "aTheory"

before you can open it. Often you want to load multiple theories, so
"map load [...]" is useful.

However, if you just add this line, it is quite likely that loading will
fail, because the file "aTheory.ui" cannot be found. For files not in
the current directory, you need to manually extend the loadpath via
something like

>>__ loadPath := newdir :: !loadPath;

As an example let's say you want to use "latticeTheory" from
"examples/separationLogic/src/". Then you need to build
"latticeTheory.ui" (usually by running Holmake in that directory). Then
you add

>>__ loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src/") ::
!loadPath;
>>__ map load ["latticeTheory"]
>>__ open latticeTheory

>>- OPTION_SELECT_def

Cheers

Thomas

P.S.: I was wondering, whether you have had a look at the munger. It is
usually the one used to print existing definitions in Latex files.


On 14.02.2018 13:17, Heiko Becker wrote:
> 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


--
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] Dependency on absolute paths remaining the same

[Thomas Tuerk]

No, that's not at all what I suggest and I would not work this way. All
I say is that you can keep multiple source trees around without trouble.
Use this how you see fit. You need to know what your needs are and
choose an appropriate workflow. All I tried to do was point out some
options. Relocation is another one, of course.

I do the following, which fits my needs. Yours might be quite different:
I only keep fixed versions needed for certain external (not in HOL
examples dir) projects and a more or less up-to-date development version
around. I do not tend to switch the symbolic link, just when switching
projects, but select the HOL I want to use manually for every full
rebuild. Only if I know I will mainly use a certain HOL version mostly
for some time, I switch the default.

I do updates directly on the development version and never had trouble,
since it tends to take much less than 30 min on my machine (if I don't
build many examples). I can easily schedule this for a time slot when I
don't need HOL (e.g. lunch-time or during a meeting) and not be
interrupted in my work. Even if I want to update while working with HOL,
this is usually not an issue. While HOL rebuilds, I can continue working
interactively on some proof, I just cannot restart or load additional
theories / libs. This is for me usually not an issue for the about 5-10
min it takes on my machine.

Best

Thomas


On 04.02.2018 19:03, Mario Xerxes Castelán Castro wrote:
> If I understand correctly, your overall suggestion is
>
> * Have a symbolic link S that points to either A or B, where A and B are
> HOL4 source+build trees. My Emacs init file should point to hol-mode
> within S.
>
> * If I am working, and S points to A, then update and re-build B
> (vice-versa if S points to B). Switch S to point to B when convenient
> (now the roles of A and B are swapped).
>
> Is this correct?
>
> Thanks.
>
> On 04/02/18 11:56, Thomas Tuerk wrote:
>> Hi,
>>
>> for this workflow, you don't need to change the absolute location. You
>> can just choose which of the multiple installed HOL versions to use.
>> Keep the installation in the same place and just choose which one to use
>> when. The only trouble with this is that you have to rebuild your own
>> development manually and completely to switch versions. This usually
>> happens and is advisable anyhow.
>>
>> So, I do the following:
>>
>> Have multiple HOL directories around, e.g.:
>>
>> - HOL-stable
>> - HOL-version1
>> - HOL-version2
>> - symbolic link HOL -> whichever is my default version
>>
>> I use the emacs mode and use the files from the symbolic link for the
>> emacs mode. If I want to switch the default versions (I need multiple
>> ones for different projects and sometimes work several days mainly with
>> one project), I change the symbolic link. However, in your case you have
>> to rebuild your whole own development after such a change, since
>> otherwise it remembers which HOL it was build with and uses this one
>> (which might be desirable sometimes).
>>
>> By the way, the ~30 min rebuild time are just for a fresh build on a not
>> too fast machine. Very often nothing changed in parts that appear early
>> in the build-chain, rebuilding the development version is much faster.
>> Even if it takes 30 min, I tend to schedule it for my lunch break and
>> have usually not much trouble.
>>
>> Cheers
>>
>> Thomas
>>
>>
>> On 04.02.2018 18:31, Mario Xerxes Castelán Castro wrote:
>>> On 04/02/18 11:26, Ramana Kumar wrote:
>>>> Yes, to do that you need to use --relocbuild, since any executables (heaps)
>>>> need to be rebuilt if the path changes.
>>>>
>>>> Steps:
>>>> 1. Copy your HOL directory to the new location, omitting any files that
>>>> match the patterns in tools-poly/rebuild-excludes.txt
>>>> 2. Run poly --script tools/smart-configure.sml in the new location
>>>> 3. Run bin/build --relocbuild in the new location
>>> Thanks, do I need to do this every time the absolute path changes?
>>>
>>> I try to use the development version, but since it takes around 1700 s
>>> to complete the build, I only update occasionally. I intended to
>>> schedule building an updated development version while I work with an
>>> already-built version. Once it is done building and I finish my work
>>> session, then move the new build into the place where my working build
>>> is. Is this possible without having to re-build heaps after moving?
>>>
>>> Thanks.
>>>
>>>
>>>
>>> 

Re: [Hol-info] Dependency on absolute paths remaining the same

[Thomas Tuerk]

Hi,

for this workflow, you don't need to change the absolute location. You
can just choose which of the multiple installed HOL versions to use.
Keep the installation in the same place and just choose which one to use
when. The only trouble with this is that you have to rebuild your own
development manually and completely to switch versions. This usually
happens and is advisable anyhow.

So, I do the following:

Have multiple HOL directories around, e.g.:

- HOL-stable
- HOL-version1
- HOL-version2
- symbolic link HOL -> whichever is my default version

I use the emacs mode and use the files from the symbolic link for the
emacs mode. If I want to switch the default versions (I need multiple
ones for different projects and sometimes work several days mainly with
one project), I change the symbolic link. However, in your case you have
to rebuild your whole own development after such a change, since
otherwise it remembers which HOL it was build with and uses this one
(which might be desirable sometimes).

By the way, the ~30 min rebuild time are just for a fresh build on a not
too fast machine. Very often nothing changed in parts that appear early
in the build-chain, rebuilding the development version is much faster.
Even if it takes 30 min, I tend to schedule it for my lunch break and
have usually not much trouble.

Cheers

Thomas


On 04.02.2018 18:31, Mario Xerxes Castelán Castro wrote:
> On 04/02/18 11:26, Ramana Kumar wrote:
>> Yes, to do that you need to use --relocbuild, since any executables (heaps)
>> need to be rebuilt if the path changes.
>>
>> Steps:
>> 1. Copy your HOL directory to the new location, omitting any files that
>> match the patterns in tools-poly/rebuild-excludes.txt
>> 2. Run poly --script tools/smart-configure.sml in the new location
>> 3. Run bin/build --relocbuild in the new location
> Thanks, do I need to do this every time the absolute path changes?
>
> I try to use the development version, but since it takes around 1700 s
> to complete the build, I only update occasionally. I intended to
> schedule building an updated development version while I work with an
> already-built version. Once it is done building and I finish my work
> session, then move the new build into the place where my working build
> is. Is this possible without having to re-build heaps after moving?
>
> Thanks.
>
>
>
> --
> 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] How can I instantiate the variable which constrained by the existential quantifier in the parentheses？

[Thomas Tuerk]

Hi Liu,

you can't instantiate such a variable. The existential quantifier in
your formula is morally a universal one.

(?x. P x) ==> Q

is equivalent to

!x. (P x ==> Q)

Let's make an example and instantiate P and Q as follows:

P x := (x = 5)
Q := F

Then (?x. P x) ==> Q does not hold. "?x. P x" is true (witness x = 5)
and Q is F, so we get T ==> F, which is F.

If we were allowed to instantiate x, we could have with x := 6 the proof
obligation (6 = 5) ==> F, which can be shown. So, this shows that
instantiating such existential quantifiers is not a valid operation.

Technically speaking, the existential quantifier in your formula occurs
at odd negation level and is therefore really a universal one.

Cheers

Thomas

On 19.12.2017 12:21, Liu Gengyang wrote:
> Hi，
>
> How can I instantiate the variable which constrained by the
> existential quantifier in the parentheses(i.e. (?x. _) ==> _,
> replacing x with a specific value.)? For example,
>
> (?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)
>
> Now I want to instantiate `l` using `[]` ,which tactic or lemma I
> could use(I know I can use simplify tactics here, but that not I
> wanted.)? I have seen the proof process of APPEND_EQ_APPEND, but it
> didn't instantiate `l`.
>
> Regards,
>
> Liu
>
>
> --
> 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] A problem of derivation

[Thomas Tuerk]

Hi Liu,

rewriting applies the provided equations left to write.  So if if have

(A = A') /\ (B = B') ==> (f A B)

The simplifier (with std_ss) uses the precondition (A = A') /\ (B = B')
as context and adds the rewrite rules

A -> A'
B -> B'

where "->" is an ad-hoc notation for "=" but only applied in this
direction. It then uses these rules to rewrite

f A B

to

f A' B'.

So, for your example: 

``!a b c d.(sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\
(sqrt(a pow 2 + b pow 2) pow 2 = a pow 2 + b pow 2) /\ sqrt(c pow 2 + d
pow 2) pow 2 ≤ sqrt(a pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤ a
pow 2 + b pow 2``

the equations are in the wrong direction to be used as rewrites for the
conclusion. They could be used on the 3rd conjunct (which you probably
expected). However, the 3rd conjunct is not simplified with the other
conjuncts. They are not used as context by std_ss. So, if you write

``!a b c d. (sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\
(sqrt(a pow 2 + b pow 2) pow 2 = a pow 2 + b pow 2) ==> sqrt(c pow 2 + d
pow 2) pow 2 ≤ sqrt(a pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤ a
pow 2 + b pow 2``

(notice /\ replaced by ==>) it works and is semantically equivalent.

Your simplified example

!a b c d e f. (a = b + e) /\ (c = d + f) /\ a <= c ==> b + e <= d + f

works, because a and c are quantified variables, which are removed by
quantifier instantiation. If you strip away the quantifiers, it stops
working.

I recommend using STRIP_TAC and REV_FULL_SIMP_TAC.

Cheers

Thomas


On 09.11.2017 04:02, Liu Gengyang wrote:
> Hi,
>
> I want to prove the goal:
>
> !a b c d.(sqrt(c pow 2 + d pow 2) pow 2 = c pow 2 + d pow 2) /\
> (sqrt(a pow 2 + b pow 2) pow 2 = a pow 2 + b pow 2) /\ sqrt(c pow 2 +
> d pow 2) pow 2 ≤ sqrt(a pow 2 + b pow 2) pow 2 ==> c pow 2 + d pow 2 ≤
> a pow 2 + b pow 2
>
> In theory this goal can be proved by FULL_SIMP_TAC, but failed.
> However, the goal as below who have the same structure can be proved
> by FULL_SIMP_TAC.
>
> !a b c d e f.(a = b + e) /\ (c = d + f) /\ a <= c ==> b + e <= d + f
>
> What's the problem with the first goal, how can I prove it?
>
> P.S. The origin goal is:
>
> !a b c d.sqrt(a pow 2 + b pow 2) >= sqrt(c pow 2 + d pow 2) ==> a * a
> + b * b >= c * c + d * d
>
> RW_TAC std_ss [] >>
>
> `0 <= c pow 2 + d pow 2` by RW_TAC std_ss
> [realTheory.REAL_LE_POW2,realTheory.REAL_LE_ADD] >>
>
> `0 <= a pow 2 + b pow 2` by RW_TAC std_ss
> [realTheory.REAL_LE_POW2,realTheory.REAL_LE_ADD] >>
>
> `0 <= sqrt (c pow 2 + d pow 2)` by RW_TAC std_ss
> [transcTheory.SQRT_POS_LE] >>
>
> `0 <= sqrt (a pow 2 + b pow 2)` by RW_TAC std_ss
> [transcTheory.SQRT_POS_LE] >>
>
> `sqrt (c pow 2 + d pow 2) pow 2 <= sqrt (a pow 2 + b pow 2) pow 2` by
> FULL_SIMP_TAC std_ss [realTheory.real_ge,realTheory.POW_LE] >>
>
> FULL_SIMP_TAC std_ss [GSYM transcTheory.SQRT_POW2] >>(*Here is the
> problem.*)
>
> Regards,
>
> Liu
>
>
> --
> 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] Question on rewriting with assumptions

[Thomas Tuerk]

Hi Mario,

I believe, there is nothing bad about using inline functions (i.e. a
lambda) per se. If I understood correctly, you are currently using the
following from

`some goal` by (
   tactic_goal
) >>
POP_ASSM (fn thm => REWRITE_TAC[thm])

A slightly more elegant way might be (it's all a matter of opinion :-))

Q.SUBGOAL_THEN `some_goal` (fn thm => REWRITE_TAC[thm]) >- (
  tactic_goal
)

However, this keeps the inline function. I don't know of a SUBST1_TAC
like function. However, it is easy to define. You could use REWR_CONV
(or it's higher order corresponding function) and combine it with
tacticals. You would end up with something like

fun REWRITE1_TAC thm = CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV thm)))

Depending on your circumstances, ONCE_ASM_REWRITE_TAC or similar
existing tactics might do the trick for you as well.

Cheers

Thomas Tuerk


On 25.09.2017 20:03, Mario Castelán Castro wrote:
> Hello.
>
> Suppose that in a tactic-based proof I have just proved with “by” a
> lemma of the form “P = Q”, where “P” can be matched against a proper
> subterm of the goal. I want to use this lemma to rewrite the respective
> subterm of the goal. What is the preferred approach to do this?
>
> The obvious approach is “POP_ASSUM (fn thm => REWRITE_TAC [thm])” (or
> another rewriter in place of “REWRITE_TAC”). But I feel that embedding a
> lambda expression in a proof is an inelegant approach.
>
> I am aware that “ASM_REWRITE_TAC” or “FULL_SIMP_TAC” can be used in some
> of these cases, but sometimes there are assumptions that would lead to
> an undesired rewriting.
>
> Is there something like “SUBST1_TAC” that does matching?
>
> Thanks.
>
>
>
> --
> 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] How to reduce these lambda equations to F?

[Thomas Tuerk]

Hi Chun,

via a subgoal, you can introduce an assumption for a concrete argument.
This should be what you need. I'm thinking of something like

First show that a CCS q exists with "q <> p"

`?q. q <> p` by ...

Then use this new q as an argument)

`(\t. t) q = (\t. p) q` by PROVE_TAC[]

Now you are done by BETA reduction and contradicting assumptions.

Best

Thomas



On 04.08.2017 20:22, Chun Tian (binghe) wrote:
> Hi,
>
> This is the first time I met the following goal, in which one of the 
> assumptions should be able to reduce to F (then the goal is resolved):
>
> R (λt. t)
> 
>   4.  (λt. t) = (λt. prefix (label l) t)
>
> The lambda function has the type of ``CCS -> CCS``, which CCS is my datatype 
> defined by HOL’s Define command.  “prefix” is an constructor of CCS datatype. 
>I *know* the equation doesn’t hold, because the whatever input arguments, 
> the resulting CCS on both side must have different “size”, simply because one 
> is the sub-expression of the other.   But how can I actually reduce it to F?
>
> The other case is a little different:
>
> R (λt. t)
> 
>   4.  (λt. t) = (λt. p)
>
> The assumption "(λt. t) = (λt. p)” hold for only one case: when input of 
> lambda function is exactly “p”.  For all other cases the left side doesn’t 
> equal to the right side.  But from the view of two functions, they’re 
> obviously not identical. But how can I actually reduce it to F?
>
> Regards,
>
> Chun Tian
>
>
>
> --
> 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] Counting Subgoals in a Proof

[Thomas Tuerk]

Hi Matthias,

I'm not aware of an easy way. Moreover, for me it is unclear how to
count subgoals. I could well imagine that one wants to count only
"interesting ones", i.e. ignore trivial ones like "Cases_on `x:num` >>
ASM_REWRITE_TAC[...]", where the case for "0" is automatically discarded.

One idea would be to define a tactic for counting, i.e. something like


val subgoal_counter = ref 0;
fun COUNT_TAC (asm, g) = (subgoal_counter := !subgoal_counter + 1;
ALL_TAC (asm, g))


You can then add it at the places, where you want counting to happen,
e.g. after a "REPEAT CASE_TAC". Add some stuff for resetting the counter
and printing it, e.g. by a tactical like


fun PRINT_COUNT tac (asm, g) = let
  val _ = subgoal_counter := 0;
  val res = tac (asm, g);
  val _ = print ("\n\nCOUNTER: "^(int_to_string (!subgoal_counter))^"\n\n");
in res end; 

And you have some basic infrastructure. Very hackish, but probably
working, flexible and not too much work.

Cheers

Thomas



On 11.07.2017 12:34, Matthias Stockmayer wrote:
> Hi,
>
> I'm working on a proof that produces many subgoals due to a rather
> complex case-splitting structure. To see, if some changes to the proof
> increase or decrease the complexity, I'd like to know how many
> subgoals are produced and solved in the whole proof.
>
> So, is there any way to find out the number of subgoals, without
> manually stepping through the proof and counting?
>
> I know I can use the running time of the proof to compare different
> approaches, but I'm not sure how accurate this will be.
>
>
> With regards,
>
> Matthias
>
>
>
> --
>
> 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] REWRITE_CONV fails

[Thomas Tuerk]

Hi,

I always understood "fail" as raising "HOL_ERR". However, I might be
wrong there.

There is QCONV. If a conversion raises UNCHANGED, it calls REFL. So

QCONV (REWRITE_CONV thms)

is what you are after, I believe.

Thomas


On 05.05.2017 22:09, Chun Tian (binghe) wrote:
> Hi,
>
> The HOL System REFERENCE said, REWRITE_CONV "Does not fail, but may diverge 
> if the sequence of rewrites is non-terminating.”, but I found this is not 
> true (any more):
>
>> REWRITE_CONV [ASSUME ``A = B``] ``A``;
> val it =
> [.] |- A = B:
>thm
>> REWRITE_CONV [ASSUME ``A = B``] ``C``;
> Exception- UNCHANGED raised
>
> What I wanted is a theorem ``C = C`` in this case.
>
> Further more,
>
>> REWRITE_CONV [] ``F``
> Exception- UNCHANGED raised
>
> which used to return a theorem ``F = F`` in HOL88:
>
> #REWRITE_CONV [] "F";;
> |- F = F
>
> Is there a way I could get the desired (old) behavior?
>
> Regards,
>
> Chun Tian
>
>
>
> --
> 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] What tactic I should use?

[Thomas Tuerk]

Hi Dwi,

I would expect that a

ASM_REWRITE_TAC[]

does the trick. It would take the assumptions as a rewrite and use it to
simplify the goal. In this case, it should simplify the goal to "!s0.
Next s0 x = Next s0 x"  which is solved thanks to reflexivity. A problem
might be free type variables, i.e. that the type of "x" in the
assumption and "Next s0 x" in the goal don't match. This seems not to be
the case in your example, though. I recommend reading up on REWRITE_TAC
and ASM_REWRITE_TAC, as well as ASM_SIMP_TAC and similar stuff in the
description and reference manuals.

Cheers

Thomas


On 25.04.2017 09:24, Dwi Teguh Priyantini wrote:
> Hi,
>
> I have a question,
> What tactic I should use to solve this problem?
>
> !s0. flipslv (flipslv (Next s0 x)) = Next s0 x
> --
> x. flipslv (flipslv x) = x
>
> The flipslv function is just simply reverses x which is a slv datatype.
>
> The datatype declaration is written as bellow:
> val _ = Hol_datatype`
>slv = Single of stdl
> | Next of stdl => slv
> `;
>
> And I also have this definitions before:
> val flipnext_def = Define `(flipnext (Next a b) c = flipnext b (Next a 
> c))
>   /\ (flipnext (Single a) c = Next a c)`;
>
> val flipslv_def = Define `(flipslv (Next a b) = flipnext b (Single a))
>   /\ (flipslv (Single a) = (Single a))`;
>
>
> I think the pattern has matched (by replace "x" with "Next s0 x"), but I 
> don't know how to do. Could anyone help me?
> Thank you.
>
>


--
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] How to instantiate record datatype?

[Thomas Tuerk]

Hi Liu,

I don't know EXTENCE_TAC. I would have used EXISTS_TAC. This shound not
depend on whether "a" is a record type or not. So something like:

Q.EXISTS_TAC `EL n A`

It might be worth looking at REFINE_TAC to partially instantiate the
record and quantifier heuristics (QI_ss) to split the quantifier
automatically and introduce a record.

Cheers

Thomas


On 17.04.2017 08:54, Liu Gengyang wrote:
> Hi,
>
> I have a question as follow:
>
> load "realLib";
> open listTheory;
>
> Datatype `coordinate = <|x_axis: real; y_axis: real; z_axis: real|>`;
> val A = ``A: coordinate list``;
>
> g `^A <> [] ==> !n. ?a. a.x_axis <= (EL n A).x_axis`;
>
> - e(RW_TAC list_ss []);
> OK..
> 1 subgoal:
> > val it =
>
> ?a. a.x_axis <= (EL n A).x_axis
> 
>   A <> []
>  : proof
>
> Now I want to use EXTENCE_TAC to instantiate "a", but I don't know how
> to do it, because "a" is a record type. Could anyone help me?
>
> Thanks,
>
> Liu
>
>
> --
> 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] How to eliminate existential quantifier in a goal about list?

[Thomas Tuerk]

Hi Liu,

you have realLib open. "0" can be parsed as either a real or a num.
That's why you get the warning that two resolutions are possible. The
"EXISTS_TAC ``0``" fails, because ``0`` is parsed as a real, while you
need a num. An explicit type annotation does the trick: So use

e (EXISTS_TAC ``0:num``);

Cheers

Thomas


--
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] Questions about RTC (reflexive transitive closure)

[Thomas Tuerk]

Hi Chun,

learning Holyhammer is also on my TODO list.

One minor trick. I often look at the theory signature instead of the
Script-file. So I read "relationTheory.sig". For the theories comming
with HOL, the signature is available in the HTML help. For my own
theories, I just open the "*Theory.sig" file.

https://hol-theorem-prover.org/kananaskis-10-helpdocs/help/src-sml/htmlsigs/relationTheory.html#LinearOrder-val

Best

Thomas


On 07.04.2017 13:07, Chun Tian (binghe) wrote:
> Thanks again, this is really convenient.
>
> Actually a large piece of my time was spent on reading HOL's
> relationScript.sml and other scripts that I needed, I try to find
> useful theorems by their name (otherwise I couldn't know RTC_CASES*,
> RTC_INDUCT, RTC_SINGLE, etc.), but maybe the scripts are too long, I
> don't know how to I missed RTC_INDUCT_RIGHT1, etc.)
>
> I hope one day I could learn to use the Holyhammer ...
>
> Regards,
>
> Chun
>
>
> On 7 April 2017 at 12:57, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi Chun,
>
> by the way. I always find DB.match and DB.find very helpful. You
> can for example try
>
> DB.print_match [] ``RTC``
> DB.print_match [] ``RTC _ x x``
> DB.print_find "RTC"
>
> to find interesting theorems about RTC.
>
> Cheers
>
> Thomas
>
>
> On 07.04.2017 12:51, Chun Tian (binghe) wrote:
>> Hi Thomas,
>>
>> Thank you very much!! Obviously I didn't know those RTC_ALT* and
>> RTC_RIGHT* series of theorems before. Now I can prove something new:)
>>
>> Best regards,
>>
>> Chun
>>
>>
>> On 7 April 2017 at 12:08, Thomas Tuerk <tho...@tuerk-brechen.de
>> <mailto:tho...@tuerk-brechen.de>> wrote:
>>
>> Hi,
>>
>> 1) They are the same. You can easily proof with induction
>> (see below).
>>
>> 2) Yes you can prove it. You would also do it via some kind
>> of induction proof. However there is no need, since it is
>> already present in the relationTheory as  RTC_INDUCT_RIGHT1.
>>
>> Cheers
>>
>> Thomas
>>
>>
>>
>> open relationTheory
>>
>> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
>> (!x. RTC1 R x x) /\
>> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>>
>> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
>> (!x. RTC2 R x x) /\
>> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>>
>> val RTC1_ALT_DEF = prove (``RTC1 = RTC``,
>>
>>   `!R. (!x y. RTC1 R x y ==> RTC R x y) /\
>>(!x y. RTC R x y ==> RTC1 R x y)` suffices_by (
>>  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
>>   THEN
>>
>>   GEN_TAC THEN CONJ_TAC THENL [
>> Induct_on `RTC1` THEN
>> METIS_TAC [RTC_RULES],
>>
>> MATCH_MP_TAC RTC_INDUCT THEN
>> METIS_TAC[RTC1_rules]
>>   ]);
>>
>>
>> val RTC2_ALT_DEF = prove (``RTC2 = RTC``,
>>
>>   `!R. (!x y. RTC2 R x y ==> RTC R x y) /\
>>(!x y. RTC R x y ==> RTC2 R x y)` suffices_by (
>>  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
>>   THEN
>>
>>   GEN_TAC THEN CONJ_TAC THENL [
>> Induct_on `RTC2` THEN
>> METIS_TAC [RTC_RULES_RIGHT1],
>>
>> MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
>> METIS_TAC[RTC2_rules]
>>   ]);
>>
>>
>>
>> On 07.04.2017 11:49, Chun Tian (binghe) wrote:
>>> Hi,
>>>
>>> If I try to define RTC manually (like those in HOL tutorial,
>>> chapter 6, page 74):
>>>
>>> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
>>> (!x. RTC1 R x x) /\
>>> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>>>
>>> It seems that (maybe) I can also define the "same" relation
>>> with a different transitive rule:
>>>
>>> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
>>> (!x. RTC2 R x x) /\
>>> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>>>
>>> Here are some observations:
>>>
>>> 1. If I

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

[Thomas Tuerk]

Hi Chun,

by the way. I always find DB.match and DB.find very helpful. You can for
example try

DB.print_match [] ``RTC``
DB.print_match [] ``RTC _ x x``
DB.print_find "RTC"

to find interesting theorems about RTC.

Cheers

Thomas

On 07.04.2017 12:51, Chun Tian (binghe) wrote:
> Hi Thomas,
>
> Thank you very much!! Obviously I didn't know those RTC_ALT* and
> RTC_RIGHT* series of theorems before. Now I can prove something new:)
>
> Best regards,
>
> Chun
>
>
> On 7 April 2017 at 12:08, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi,
>
> 1) They are the same. You can easily proof with induction (see below).
>
> 2) Yes you can prove it. You would also do it via some kind of
> induction proof. However there is no need, since it is already
> present in the relationTheory as  RTC_INDUCT_RIGHT1.
>
> Cheers
>
> Thomas
>
>
>
> open relationTheory
>
> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
> (!x. RTC1 R x x) /\
> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>
> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
> (!x. RTC2 R x x) /\
> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>
> val RTC1_ALT_DEF = prove (``RTC1 = RTC``,
>
>   `!R. (!x y. RTC1 R x y ==> RTC R x y) /\
>(!x y. RTC R x y ==> RTC1 R x y)` suffices_by (
>  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
>   THEN
>
>   GEN_TAC THEN CONJ_TAC THENL [
> Induct_on `RTC1` THEN
> METIS_TAC [RTC_RULES],
>
> MATCH_MP_TAC RTC_INDUCT THEN
> METIS_TAC[RTC1_rules]
>   ]);
>
>
> val RTC2_ALT_DEF = prove (``RTC2 = RTC``,
>
>   `!R. (!x y. RTC2 R x y ==> RTC R x y) /\
>(!x y. RTC R x y ==> RTC2 R x y)` suffices_by (
>  SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
>   THEN
>
>   GEN_TAC THEN CONJ_TAC THENL [
> Induct_on `RTC2` THEN
> METIS_TAC [RTC_RULES_RIGHT1],
>
> MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
> METIS_TAC[RTC2_rules]
>   ]);
>
>
>
> On 07.04.2017 11:49, Chun Tian (binghe) wrote:
>> Hi,
>>
>> If I try to define RTC manually (like those in HOL tutorial,
>> chapter 6, page 74):
>>
>> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
>> (!x. RTC1 R x x) /\
>> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>>
>> It seems that (maybe) I can also define the "same" relation with
>> a different transitive rule:
>>
>> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
>> (!x. RTC2 R x x) /\
>> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>>
>> Here are some observations:
>>
>> 1. If I directly use the RTC definition from HOL's
>> relationTheory, above two transitive rules are both true, easily
>> provable by theorems RTC_CASES1 and RTC_CASES2 (relationTheory):
>>
>> > RTC_CASES1;
>> val it =
>>|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R x u ∧ R^* u y:
>>thm
>> > RTC_CASES2;
>> val it =
>>|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R^* x u ∧ R u y:
>>thm
>>
>>  2. The theorem RTC1_ind (generated by Hol_reln) is the same as
>> theorem RTC_INDUCT (relationTheory):
>>
>> val RTC1_ind =
>>|- ∀R RTC1'.
>>  (∀x. RTC1' x x) ∧ (∀x y z. R x y ∧ RTC1' y z ⇒ RTC1' x z) ⇒
>>  ∀a0 a1. RTC1 R a0 a1 ⇒ RTC1' a0 a1:
>>thm
>>
>> > RTC_INDUCT;
>> val it =
>>|- ∀R P.
>>  (∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒
>>  ∀x y. R^* x y ⇒ P x y:
>>thm
>>
>> Now my questions are:
>>
>> 1. Given any R, are the two relations (RTC1 R) and (RTC2 R)
>> really the same? i.e. is ``!R x y. RTC1 R x y = RTC2 R x y`` a
>> theorem? (and if so, how to prove it?)
>>
>> 2. (If the answer of last question is yes) Is it possible to
>> prove the following theorem RTC_INDUCT2 in relationTheory? (which
>> looks like RTC2_ind generated in above definition)
>>
>> val RTC_INDUCT2 = store_thm(
>>"RTC_INDUCT2",
>>   ``!R P. (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
>>   (!x (y:'a). RTC R x y ==> P x y)``,
>> cheat);
>>
>

Re: [Hol-info] Questions about RTC (reflexive transitive closure)

[Thomas Tuerk]

Hi,

1) They are the same. You can easily proof with induction (see below).

2) Yes you can prove it. You would also do it via some kind of induction
proof. However there is no need, since it is already present in the
relationTheory as  RTC_INDUCT_RIGHT1.

Cheers

Thomas



open relationTheory

val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
(!x. RTC1 R x x) /\
(!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;

val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
(!x. RTC2 R x x) /\
(!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;

val RTC1_ALT_DEF = prove (``RTC1 = RTC``,

  `!R. (!x y. RTC1 R x y ==> RTC R x y) /\
   (!x y. RTC R x y ==> RTC1 R x y)` suffices_by (
 SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
  THEN

  GEN_TAC THEN CONJ_TAC THENL [
Induct_on `RTC1` THEN
METIS_TAC [RTC_RULES],

MATCH_MP_TAC RTC_INDUCT THEN
METIS_TAC[RTC1_rules]
  ]);


val RTC2_ALT_DEF = prove (``RTC2 = RTC``,

  `!R. (!x y. RTC2 R x y ==> RTC R x y) /\
   (!x y. RTC R x y ==> RTC2 R x y)` suffices_by (
 SIMP_TAC std_ss [FUN_EQ_THM] THEN METIS_TAC[FUN_EQ_THM])
  THEN

  GEN_TAC THEN CONJ_TAC THENL [
Induct_on `RTC2` THEN
METIS_TAC [RTC_RULES_RIGHT1],

MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN
METIS_TAC[RTC2_rules]
  ]);



On 07.04.2017 11:49, Chun Tian (binghe) wrote:
> Hi,
>
> If I try to define RTC manually (like those in HOL tutorial, chapter
> 6, page 74):
>
> val (RTC1_rules, RTC1_ind, RTC1_cases) = Hol_reln `
> (!x. RTC1 R x x) /\
> (!x y z. R x y /\ RTC1 R y z ==> RTC1 R x z)`;
>
> It seems that (maybe) I can also define the "same" relation with a
> different transitive rule:
>
> val (RTC2_rules, RTC2_ind, RTC2_cases) = Hol_reln `
> (!x. RTC2 R x x) /\
> (!x y z. RTC2 R x y /\ R y z ==> RTC2 R x z)`;
>
> Here are some observations:
>
> 1. If I directly use the RTC definition from HOL's relationTheory,
> above two transitive rules are both true, easily provable by theorems
> RTC_CASES1 and RTC_CASES2 (relationTheory):
>
> > RTC_CASES1;
> val it =
>|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R x u ∧ R^* u y:
>thm
> > RTC_CASES2;
> val it =
>|- ∀R x y. R^* x y ⇔ (x = y) ∨ ∃u. R^* x u ∧ R u y:
>thm
>
>  2. The theorem RTC1_ind (generated by Hol_reln) is the same as
> theorem RTC_INDUCT (relationTheory):
>
> val RTC1_ind =
>|- ∀R RTC1'.
>  (∀x. RTC1' x x) ∧ (∀x y z. R x y ∧ RTC1' y z ⇒ RTC1' x z) ⇒
>  ∀a0 a1. RTC1 R a0 a1 ⇒ RTC1' a0 a1:
>thm
>
> > RTC_INDUCT;
> val it =
>|- ∀R P.
>  (∀x. P x x) ∧ (∀x y z. R x y ∧ P y z ⇒ P x z) ⇒
>  ∀x y. R^* x y ⇒ P x y:
>thm
>
> Now my questions are:
>
> 1. Given any R, are the two relations (RTC1 R) and (RTC2 R) really the
> same? i.e. is ``!R x y. RTC1 R x y = RTC2 R x y`` a theorem? (and if
> so, how to prove it?)
>
> 2. (If the answer of last question is yes) Is it possible to prove the
> following theorem RTC_INDUCT2 in relationTheory? (which looks like
> RTC2_ind generated in above definition)
>
> val RTC_INDUCT2 = store_thm(
>"RTC_INDUCT2",
>   ``!R P. (!x. P x x) /\ (!x y z. P x y /\ R y z ==> P x z) ==>
>   (!x (y:'a). RTC R x y ==> P x y)``,
> cheat);
>
> (and the corresponding RTC_STRONG_INDUCT2).
>
> Regards,
>
> -- 
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
>
> --
> 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] How to prove ``R = R'`` (two relations are equal) given the corresponding universally qualified form?

[Thomas Tuerk]

Hi Chun,

use functional extensionality. There are many ways to do it, one  is
using the theorem boolTheory.FUN_EQ_THM.

Best

Thomas

On 24.03.2017 21:42, Chun Tian (binghe) wrote:
> Hi again,
>
> If I have a theorem saying two (2-ary) relations are the same:
>
> |- R = R’
>
> Then I can easily prove the following theorem using REWRITE_TAC:
>
> |- !x y. R x y = R’ x y
>
> But if I had the second one first, how to prove the previous one?
>
> Regards,
>
> Chun Tian
>
>
>
>
> --
> 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

[Thomas Tuerk]

Hello,

many thanks. That does the trick and is much nicer than my hack.

@Magnus Myreen: Do you think this is worth adding to the HOL Interaction
manual?

Thank you,

Thomas Tuerk


On 26.01.2017 22:25, 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

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

[Thomas Tuerk]

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

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

Hi Chun,

TypeBase stores information about algebraic datatypes. So, you won't
find information for your inductive relations or recursive functions in
there. Use

TypeBasePure.listItems (TypeBase.theTypeBase())

to get an idea what types are currently in the TypeBase. I found the
reference to "Induct_on" in the description in section 5.6.1 on page
187. I was not aware of this feature. I looked up how it is implemented.
In "src/basicProof/BasicProvers.sml" line 259 you can see that the
TypeBase is not used. Instead, "src/IndDef/IndDefLib.sig" defines a map
"rule_induction_map" that contains these induction theorems.

If you want to get your hands on the strong induction theorem, I would
use DB.fetch, i.e.

DB.fetch "-" "R_strongind"

Cheers

Thomas


On 18.01.2017 14:34, Chun Tian (binghe) wrote:
> Sorry, one more question here: how to fetch from TypeBase the
> induction theorems generated by relation?
>
> I recall in The HOL System DESCRIPTION, section 5.6.1 (Proofs with
> Inductive Relations), it says that we can use (Induct_on `R`) or
> (Induct_on `R x y`) to do inductions on relation R, and internally it
> actually calls (HO_MATCH_MP_TAC R_strongind).  And the information is
> taken from TypeBase (I can't find a exact reference for this, but
> sometimes when I failed to call Induct_on, it said there's no such
> types in TypeBase).
>
> Still using my above example, if I try the type of my relation subF, I
> got nothing, and errors:
>
> > TypeBase.fetch ``:'a form -> 'a form -> bool``;
> val it = NONE: tyinfo option
>
> > TypeBase.induction_of ``:'a form -> 'a form -> bool``;
> Exception-
>HOL_ERR
>  {message = "unable to find \"min$fun\" in the TypeBase",
>   origin_function = "induction_of", origin_structure = "TypeBase"}
> raised
>
>
> On 18 January 2017 at 13:55, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi,
>
> glad I could be of help.
>
> I forgot to mention TypeBase. This is where such theorems about a
> type are collected. It is used by tools like the case or induct
> tactics. So, some other nice way of getting such theorems is
>
> TypeBase.fetch ``:'a form``
>
> or specialized ones via
>
> TypeBase.distinct_of ``:'a form``
> TypeBase.one_one_of ``:'a form``
> ...
>
> Best
>
>     Thomas
>
>
> On 18.01.2017 13:22, Chun Tian (binghe) wrote:
>> Hi Thomas,
>>
>> Oh my god ... I've learnt so much from each line of your reply.
>> Thank you so much!
>>
>> Best regards,
>>
>> Chun
>>
>>
>> On 18 January 2017 at 12:53, Thomas Tuerk
>> <tho...@tuerk-brechen.de> wrote:
>>
>> Hi Chun,
>>
>> you are on the right way with the cases theorem. Essentially
>> you need to rewrite once with it. Then you end up with
>>
>> ∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒
>> (A = atom a)
>>
>> Now you need to use the fact that "atom _ = dot B C" does not
>> hold. This distinctiveness is proved by the datatype package,
>> just not returned directly. It is stored in the theory. You
>> can fetch it via
>>
>> fetch "-" "form_distinct"
>>
>> The injectivity of constructors you asked for you get via
>>
>> fetch "-" "form_11"
>>
>> Just search for "form" and you get interesting stuff
>>
>> DB.print_find "form"
>>
>>
>> So your proof might look like
>>
>> -
>>
>> val form_distinct = DB.fetch "-" "form_distinct"
>>
>> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom
>> a)``,
>>
>> ONCE_REWRITE_TAC [subF_cases] THEN
>> SIMP_TAC std_ss [form_distinct])
>>
>> ---
>>
>>
>> There are other ways of accessing the generated theorems,
>> though. Most commonly used, but sometimes doing also extra
>> unwanted stuff is the stateful simpset. So something like
>>
>> SIMP_TAC (srw_ss ()) []
>>
>> does work as well.
>>
>> I personally prefer the DatatypeSimps to keep tight control
>> over what rewrites I use. This is a highly controversial
>> 

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

Hi,

glad I could be of help.

I forgot to mention TypeBase. This is where such theorems about a type
are collected. It is used by tools like the case or induct tactics. So,
some other nice way of getting such theorems is

TypeBase.fetch ``:'a form``

or specialized ones via

TypeBase.distinct_of ``:'a form``
TypeBase.one_one_of ``:'a form``
...

Best

Thomas


On 18.01.2017 13:22, Chun Tian (binghe) wrote:
> Hi Thomas,
>
> Oh my god ... I've learnt so much from each line of your reply. Thank
> you so much!
>
> Best regards,
>
> Chun
>
>
> On 18 January 2017 at 12:53, Thomas Tuerk <tho...@tuerk-brechen.de
> <mailto:tho...@tuerk-brechen.de>> wrote:
>
> Hi Chun,
>
> you are on the right way with the cases theorem. Essentially you
> need to rewrite once with it. Then you end up with
>
> ∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒ (A =
> atom a)
>
> Now you need to use the fact that "atom _ = dot B C" does not
> hold. This distinctiveness is proved by the datatype package, just
> not returned directly. It is stored in the theory. You can fetch
> it via
>
> fetch "-" "form_distinct"
>
> The injectivity of constructors you asked for you get via
>
> fetch "-" "form_11"
>
> Just search for "form" and you get interesting stuff
>
> DB.print_find "form"
>
>
> So your proof might look like
>
> -
>
> val form_distinct = DB.fetch "-" "form_distinct"
>
> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,
>
> ONCE_REWRITE_TAC [subF_cases] THEN
> SIMP_TAC std_ss [form_distinct])
>
> ---
>
>
> There are other ways of accessing the generated theorems, though.
> Most commonly used, but sometimes doing also extra unwanted stuff
> is the stateful simpset. So something like
>
> SIMP_TAC (srw_ss ()) []
>
> does work as well.
>
> I personally prefer the DatatypeSimps to keep tight control over
> what rewrites I use. This is a highly controversial personal taste
> though.
>
> So, I either use the version above or
>
>
> val form_ss = DatatypeSimps.type_rewrites_ss [``:'a form``]
>
> val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,
>
> ONCE_REWRITE_TAC [subF_cases] THEN
> SIMP_TAC (std_ss++form_ss) [])
>
>
> I hope this helps
>
> Thomas
>
>
> On 18.01.2017 11:58, Chun Tian (binghe) wrote:
>> Hi,
>>
>> Sorry for disturbing again, but I met new difficulties when
>> proving theorems about relations.
>>
>> Suppose I have the following simple recursive datatype and a "sub
>> formula" relation about it:
>>
>> val _ = Datatype `form = atom 'a | dot form form`;
>>
>> val (subF_rules, subF_ind, subF_cases) = Hol_reln
>>`(!(A:'a form). subF A A) /\
>> (!(A:'a form) B C. subF A B ==> subF A (dot B C)) `;
>>
>> Now I need to prove this goal: `!A a. subF A (atom a) ==> (A =
>> atom a)`.
>>
>> I have successfully proved some theorems about relations defined
>> by Hol_reln, but this one brings some difficulties that I never
>> met before.
>>
>> The main problem is, "atom" never appears in the definition of
>> Hol_reln, thus I don't have any theorem talking about it.
>>
>> But I recall the fact that, an inductive relation defines the
>> *least* relation satisfying the rules, thus anything undefined is
>> by default false.  I believe this fact has been correctly
>> captured by (and only by) subF_cases generated from above
>> Hol_reln definition:
>>
>> val subF_cases =
>>|- ∀a0 a1. subF a0 a1 ⇔ (a1 = a0) ∨ ∃B C. (a1 = dot B C) ∧
>> subF a0 B:
>>thm
>>
>> If I do cases analysis on `A`, I got a seeming good start point:
>>
>> > e (Cases_on `A:'a form`);
>> OK..
>> 2 subgoals:
>> val it =
>> ∀a. subF (dot f f0) (atom a) ⇒ (dot f f0 = atom a)
>> ∀a'. subF (atom a) (atom a') ⇒ (atom a = atom a')
>> 2 subgoals
>> : proof
>>
>> But I still don't know how to prove any of these sub-goals. I
>> have no useful theorems for rewrite or anything else.  The
>> relation rules only tells me that, forall A, (subFor A A) is
>> true, but it didn't say anything about th

Re: [Hol-info] How to prove this theorem about relations?

[Thomas Tuerk]

Hi Chun,

you are on the right way with the cases theorem. Essentially you need to
rewrite once with it. Then you end up with

∀A a.(atom a = A) ∨ (∃B C. (atom a = dot B C) ∧ subF A B) ⇒ (A = atom a)

Now you need to use the fact that "atom _ = dot B C" does not hold. This
distinctiveness is proved by the datatype package, just not returned
directly. It is stored in the theory. You can fetch it via

fetch "-" "form_distinct"

The injectivity of constructors you asked for you get via

fetch "-" "form_11"

Just search for "form" and you get interesting stuff

DB.print_find "form"


So your proof might look like

-

val form_distinct = DB.fetch "-" "form_distinct"

val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,

ONCE_REWRITE_TAC [subF_cases] THEN
SIMP_TAC std_ss [form_distinct])

---


There are other ways of accessing the generated theorems, though. Most
commonly used, but sometimes doing also extra unwanted stuff is the
stateful simpset. So something like

SIMP_TAC (srw_ss ()) []

does work as well.

I personally prefer the DatatypeSimps to keep tight control over what
rewrites I use. This is a highly controversial personal taste though.

So, I either use the version above or


val form_ss = DatatypeSimps.type_rewrites_ss [``:'a form``]

val myTHM = prove(``!A (a:'a). subF A (atom a) ==> (A = atom a)``,

ONCE_REWRITE_TAC [subF_cases] THEN
SIMP_TAC (std_ss++form_ss) [])


I hope this helps

Thomas


On 18.01.2017 11:58, Chun Tian (binghe) wrote:
> Hi,
>
> Sorry for disturbing again, but I met new difficulties when proving
> theorems about relations.
>
> Suppose I have the following simple recursive datatype and a "sub
> formula" relation about it:
>
> val _ = Datatype `form = atom 'a | dot form form`;
>
> val (subF_rules, subF_ind, subF_cases) = Hol_reln
>`(!(A:'a form). subF A A) /\
> (!(A:'a form) B C. subF A B ==> subF A (dot B C)) `;
>
> Now I need to prove this goal: `!A a. subF A (atom a) ==> (A = atom a)`.
>
> I have successfully proved some theorems about relations defined by
> Hol_reln, but this one brings some difficulties that I never met before.
>
> The main problem is, "atom" never appears in the definition of
> Hol_reln, thus I don't have any theorem talking about it.
>
> But I recall the fact that, an inductive relation defines the *least*
> relation satisfying the rules, thus anything undefined is by default
> false.  I believe this fact has been correctly captured by (and only
> by) subF_cases generated from above Hol_reln definition:
>
> val subF_cases =
>|- ∀a0 a1. subF a0 a1 ⇔ (a1 = a0) ∨ ∃B C. (a1 = dot B C) ∧ subF a0 B:
>thm
>
> If I do cases analysis on `A`, I got a seeming good start point:
>
> > e (Cases_on `A:'a form`);
> OK..
> 2 subgoals:
> val it =
> ∀a. subF (dot f f0) (atom a) ⇒ (dot f f0 = atom a)
> ∀a'. subF (atom a) (atom a') ⇒ (atom a = atom a')
> 2 subgoals
> : proof
>
> But I still don't know how to prove any of these sub-goals. I have no
> useful theorems for rewrite or anything else.  The relation rules only
> tells me that, forall A, (subFor A A) is true, but it didn't say
> anything about the other direction: (subF A B) => A = B (if A and B
> are both shapes like (atom ...)
>
> Also, I even don't know how to prove this fundamental truth about
> datatypes: ``(atom A) = (atom B) ==> A = B``, again, I have no
> theorems to use ... because the Datatype definition didn't return
> anything that I can (directly) use inside a store_thm().
>
> On the other side, Coq proves the same theorem quite simply:
>
> Lemma subAt :
>  forall (Atoms : Set) (A : Form Atoms) (at_ : Atoms),
>  subFormula A (At at_) -> A = At at_.
>  intros Atoms A at_ H.
>  inversion H.
>  reflexivity.
> Qed.
>
> Need help ...
>
> Regards,
>
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
>
> --
> 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] PAT_ASSUM doesn't remove the assumption now? (and a theorem cannot be proved in K11 any more)

[Thomas Tuerk]

Hi Chun,

PAT_ASSUM was renamed to PAT_X_ASSUM in June. See commit
fa81d70b67a61d6eddc6a517f968594c21be384d

https://github.com/HOL-Theorem-Prover/HOL/commit/fa81d70b67a61d6eddc6a517f968594c21be384d

for details and explanation. The reason was to unify naming. The X
actually indicates that the assumption is removed, while the version
without X keeps it. So in order to get your old proof working, you just
need to replace "PAT_ASSUM" with "PAT_X_ASSUM".

Best

Thomas Tuerk
On 16.01.2017 19:47, Chun Tian (binghe) wrote:
> Hi,
>
> HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches 
> the term argument, applies the theorem tactic to it, and removes this 
> assumption.” But I found it actually doesn’t remove the assumption in latest 
> Kananaskis 11.
>
> To see this, try the following goal (open listTheory first):
>
>> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> val it =
>Proof manager status: 1 proof.
> 1. Incomplete goalstack:
>  Initial goal:
>  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
> :
>proofs
>
> First I rewrite it:
>
>> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> OK..
> 1 subgoal:
> val it =
> FILTER ($= x) l = [x]
> 
>   0.  ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
>   1.  MEM x l
> :
>proof
>
> Then I want to pick the assumption 0 and specialize the quantifier with `x`:
>
>> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> <>
> OK..
> 1 subgoal:
> val it =
> ((x = h) ∨ MEM x l ⇒
>  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> (FILTER ($= x) l = [x])
> 
>   0.  ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
>   1.  MEM x l
> :
>proof
> Now you can see, the assumption 0 is still here. It’s not removed as the 
> manual said.
>
> In Kananaskis 10, the behavior is exactly the same as described in the manual:
>
> - g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
> <>
>> val it =
> Proof manager status: 1 proof.
> 1. Incomplete goalstack:
>  Initial goal:
>  ∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
>  : proofs
>
> - e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
> OK..
> 1 subgoal:
>> val it =
> FILTER ($= x) l = [x]
> 
>   0.  ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
>   1.  MEM x l
>  : proof
>
> - e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
> <>
> OK..
> 1 subgoal:
>> val it =
> ((x = h) ∨ MEM x l ⇒
>  ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
> (FILTER ($= x) l = [x])
> 
>   MEM x l
>  : proof
>
> See, the used assumption has been removed.
>
>
> Now let’s insist that, the behavior in latest Kananaskis 11 is more 
> reasonable (thus we should update the manual), because later we may be able 
> to use the assumption again for another different purpose. Now to finish the 
> proof, in Kananaskis 10 a single rewrite almost finish the job using theorem 
> FILTER_NEQ_NIL:
>
> - FILTER_NEQ_NIL;
>> val it =
> |- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x
>  : thm
> - e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> OK..
> 1 subgoal:
>> val it =
> MEM h l
> 
>   MEM h l
>  : proof
>
> Now the goal is the same as the only assumption left:
>
> - e (FIRST_ASSUM ACCEPT_TAC);
> OK..
>
> Goal proved.
>  [.] |- MEM h l
>
> Goal proved.
>  [.]
> |- ((x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
>(FILTER ($= x) l = [x])
>
> Goal proved.
>  [..] |- FILTER ($= x) l = [x]
>
> But in Kananaskis 11 the same tactical cannot prove the theorem any more:
>
>> FILTER_NEQ_NIL;
> val it =
>|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x:
>thm
>
>> e (RW_TAC std_ss [FILTER_NEQ_NIL]);
> OK..
> 1 subgoal:
> val it =
>
> FILTER ($= x) l = [x]
> 
>   0.  ∀x.
> (x = h) ∨ MEM x l ⇒
> ((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
>   1.  MEM x l
> :
>proof
>
> In fact we’re going back to previous status before PAT_ASSUM was used!  In 
> short words, the following theorem definition doesn’t work any more: (it 
&g

Re: [Hol-info] Using pattern_matches's custom syntax

[Thomas Tuerk]

Hi Armaël,

the syntax you use and that is still used in patternMatchesExamples.ML
was the one used before Michaels changes and the recent merge of the
branch you mention.

I'm not too sure myself, how to use the new one and what the new syntax
is exactly. From looking at Michael's commits and the source code, I
figured out the following. So no guarentees.

By default, the old case-expressions are used. However, the standard HOL
image used has the patternMatchesLib loaded and knows about PMATCH. For
example support for it is present in "std_ss". It just cannot parsed
with a nice syntax. It is always possible to use the full verbose syntax.

One can then enable parsing PMATCH expressions with a syntax close to
the existing decision tree matches via

patternMatchesLib.ENABLE_PMATCH_CASES ()

From this point on "case" is used to parse into PMATCH and "dtcase" to
parse into PMATCH. Pretty printing for both produces "case", though, it
seems.

Example

val t1 = ``case x of [] => 0 | _ => 1``
> val t1 =
   ``case x of [] => 0 | v2::v3 => 1``:
   term

val _ = patternMatchesLib.ENABLE_PMATCH_CASES ()

val t2 = ``case x of [] => 0 | _ => 1``
> val t2 =
   ``case x of [] => 0 | _ => 1``:
   term

val t3 = ``dtcase x of [] => 0 | _ => 1``
> val t3 =
   ``case x of [] => 0 | v2::v3 => 1``:
   term

val _ = set_trace "use pmatch_pp" 0
val _ = set_trace "pp_cases" 0

t1
> val it =
   ``list_CASE x 0 (λv2 v3. 1)``:
   term

t2
> val it =
   ``PMATCH x
[PMATCH_ROW (λ_. []) (λ_. T) (λ_. 0);
 PMATCH_ROW (λ_0. _0) (λ_0. T) (λ_0. 1)]``:
   term

t3
> val it =
   ``list_CASE x 0 (λv2 v3. 1)``:
   term


For examples on how to use the new syntax I looked at the "selftest.sml"
in the pattern match directory.

Perhaps I have time during the weekend to look into it closer and update
the syntax used by "patternMatchesExamples.ML".

Best

Thomas


(and other docu I fear) is the old one. Michael changed the syntax

On 27/07/16 15:23, Armaël Guéneau wrote:
> Hi all,
> 
> I'm trying to use the pattern_matches/ library of HOL4 (that has been merged
> relatively recently). Basically, I tried running the very first examples 
> of the
> example file (src/pattern_matches/patternMatchesExamples.ML), and it 
> seems to
> fail to parse the custom syntax for PMATCH:
> 
>``CASE x OF [ |||. (NONE, []) ~> 0 ]``
> 
> fails with the following error:
> 
>Don't expect to find a > in this position after a ~
>at line 25, character 40 and at line 25, character 39.
>Exception-
>   HOL_ERR
> {message =
>  "at line 25, character 39:\nDon't expect to find a > in this 
> position after a ~\nat line 25, character 40 and at line 25, character 
> 39.\n",
>  origin_function = "Absyn", origin_structure = "Absyn"} raised
> 
> 
> Would you have any ideas on how to enable the custom "CASE .. OF [ .. ]" 
> syntax?
> 
> Cheers,
> Armaël
> 
> --
> 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://sdm.link/zohodev2dev
> ___
> 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] How to show the function body in ML?

[Thomas Tuerk]

Hi Ada,

you can't print the definition from the ML REPL. I expect you use
PolyML. In this case look into the file "POLYML_DIR/basis/List.sml".
There you will find the following definition.

fun find _ [] = NONE
| find f (a::b) = if f a then SOME a else find f b

Best

Thomas

On 21.06.2016 11:18, Ada wrote:
> Hi,guys
> I am working with HOL4. 
> I finded a function "find" in ML Structure list,and I wanted to see
> the function body of "find". I printed :
>- find;
>> > val it = fn : string -> ((string * string) * (thm * class)) list
>The result only shows the types of the function.
>Its description in ML library is:
>[*find* p xs] applies f to each element x of xs, from left to  right
> until p(x) evaluates to true; returns SOME x if such an x  exists
> otherwise NONE.
> But,the function body or the definition of function doesn't exist.  
> Does anyone know how to show the function body ?
> Thanks!
> 
> 
> --
> 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] Is there a function that can produce random number in HOL4?

[Thomas Tuerk]

Hi Ada,

could you explain in more detail what you want? I did not get wether you
need in ML or in the logic. Moreover, I did not get the "x = ..." part.

In ML, look at the structure "Random".

In the logic such a function cannot exists, since forall f, args "f args
= f args" holds, which would be violated by a function "rand". You can
have underspecified functions though or model randomness /
nondeterminism explicitly.

Best

Thomas Tuerk

On 14/06/16 04:48, Ada wrote:
> Hi,guys
> I am working with HOL4. Now, I need a function that can produce
> random number. 
> For example, supposing  that function rand can create a random
> number, then x=rand ()/LENGTH, where x is a number between 1 and LENGTH.
> Does anyone know this?
> Thanks!
> 
> 
> --
> 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. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 

--
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. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Problem installing HOL 4

[Thomas Tuerk]

Hi Michael,

thanks. That did the trick. The new libraries were installed there, but
the old ones were still in there causing trouble. Anyhow, purging the
old ones solved the issue.

Many thanks

Thomas

On 24/05/16 07:23, Michael Norrish wrote:
> It looks to me as if you have a very old libpoly installed in /usr/local/lib 
> (or perhaps somewhere else on your LD_LIBRARY_PATH).  I'd guess that you need 
> to purge those files (and make sure that the 5.6 library files end up there 
> as well).
> 
> Michael
> 
>> On 24 May 2016, at 14:50, Thomas Tuerk <tho...@tuerk-brechen.de> wrote:
>>
>> Hi all,
>>
>> I have a problem installing HOL 4, which is puzzling me. It would be
>> great if someone had a idea how to help me.
>>
>> I wanted to update my HOL 4 installation. I had an old PolyML installed
>> and got the error message that at least version 5.5.1 is needed. So, I
>> installed the latest version 5.6 and then ran
>>
>> poly < tools/smart-configure.sml
>>
>> I got a strange error message. I also tried with versions 5.5.2, 5.5.1
>> with same effect:
>>
>> -
>> Poly/ML 5.5.1 Release
>>
>> HOL smart configuration.
>>
>> Determining configuration parameters: holdir OS poly polymllibdir
>> OS: linux
>> poly:   /usr/local/bin/poly
>> polyc:  /usr/local/bin/polyc
>> polymllibdir:   /usr/local/lib
>> holdir: /home/thtuerk/HOL
>> DOT_PATH:   /usr/bin/dot
>>
>> Configuration will begin with above values.  If they are wrong
>> press Control-C.
>>
>> Will continue in 1 seconds.
>>
>> Loading system specific functions
>> Compiling system specific functions (sml)
>> Beginning configuration.
>> Making mllex
>> Making mlyacc
>>
>> The exported object file has version 5.51 but this library supports
>> 5.10-5.50
>> Failed to make mlyacc
>> -
>>
>> Does anyone have an idea library this error message is about? I briefly
>> started debugging, but have not put much time into it yet? Has anyone
>> encountered this problem before.
>>
>> Best
>>
>> Thomas Tuerk
>>
>> --
>> Mobile security can be enabling, not merely restricting. Employees who
>> bring their own devices (BYOD) to work are irked by the imposition of MDM
>> restrictions. Mobile Device Manager Plus allows you to control only the
>> apps on BYO-devices by containerizing them, leaving personal data untouched!
>> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> 
> The information in this e-mail may be confidential and subject to legal 
> professional privilege and/or copyright. National ICT Australia Limited 
> accepts no liability for any damage caused by this email or its attachments.
> 

--
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Problem installing HOL 4

[Thomas Tuerk]

Hi all,

I have a problem installing HOL 4, which is puzzling me. It would be
great if someone had a idea how to help me.

I wanted to update my HOL 4 installation. I had an old PolyML installed
and got the error message that at least version 5.5.1 is needed. So, I
installed the latest version 5.6 and then ran

poly < tools/smart-configure.sml

I got a strange error message. I also tried with versions 5.5.2, 5.5.1
with same effect:

-
Poly/ML 5.5.1 Release

HOL smart configuration.

Determining configuration parameters: holdir OS poly polymllibdir
OS: linux
poly:   /usr/local/bin/poly
polyc:  /usr/local/bin/polyc
polymllibdir:   /usr/local/lib
holdir: /home/thtuerk/HOL
DOT_PATH:   /usr/bin/dot

Configuration will begin with above values.  If they are wrong
press Control-C.

Will continue in 1 seconds.

Loading system specific functions
Compiling system specific functions (sml)
Beginning configuration.
Making mllex
Making mlyacc

The exported object file has version 5.51 but this library supports
5.10-5.50
Failed to make mlyacc
-

Does anyone have an idea library this error message is about? I briefly
started debugging, but have not put much time into it yet? Has anyone
encountered this problem before.

Best

Thomas Tuerk

--
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Instantiating existentials under existentials

[Thomas Tuerk]

Hi,

there is "GEN_EXISTS_TAC "y" `5`" from bossLib. It is more general than
what was asked for here originally. It also knows about the usual
boolean connectives.

For example, it can instantiate also

?x. P x /\ ?z y. ... y ...

or with negation

?x. (P x /\ (!z y. ... y ...)) ==> Q x

"GEN_EXISTS_TAC" is a special case of  quantHeuristicsLib.QUANT_TAC.
This one allows _partially_ instantiating multiple variables in one go,
whereas "GEN_EXISTS_TAC" allows _completely_ instantiating_ one var.

With QUANT_TAC you can for example instantiate "l" in the following

`?x l. (HD l > x /\ P x l)`

with "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`l1`])]" to get

`?x l1. HD ((SUC x) :: (l1++l2)) /\ P x ((SUC x) :: (l1++l2))`

notice that "QUANT_TAC [("l", `(SUC x)::(l1++l2)` [`x`, `l1`])]" would
lead to

`?x x' l1. HD ((SUC x') :: (l1++l2)) /\ P x ((SUC x') :: (l1++l2))`

Best

Thomas


On 22.03.2016 04:08, Yong Kiam wrote:
> Out of curiosity:
> 
> How would one do the instantiation that Magnus doesn't need i.e.
> instantiate using (and under) and existential?
> 
> On Tue, Mar 22, 2016 at 4:12 AM, Ramana Kumar  > wrote:
> 
> Yes there is:
> CONV_TAC(RESORT_EXISTS_CONV(sort_vars["y"])) \\ qexists_tac`5`
> 
> On 22 March 2016 at 07:08, Magnus Myreen  > wrote:
> 
> Hi hol-info,
> 
> Quick question: is there a tactic for instantiating a nested
> existential based on a name? Example: for a goal such as
> 
>   ?x y z. ... y ...
> 
> I want to use a tactic foo_tac `y` `5` and get:
> 
>   ?x z. ... 5 ...
> 
> Is there such a foo_tac tactic? I suspect this functionality is
> there
> somewhere already. If not, then I'll implement it.
> 
> Note: I don't need the advanced feature of being able to instantiate
> it with `x+z+1` where the variables refer to the other existentially
> quantified variables.
> 
> Many thanks,
> Magnus
> 
> 
> --
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> 
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> 
> --
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> 
> --
> Transform Data into Opportunity.
> Accelerate data analysis in your applications with
> Intel Data Analytics Acceleration Library.
> Click to learn more.
> http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 

--
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://pubads.g.doubleclick.net/gampad/clk?id=278785351=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [SPAM] Re: some questions about the proving process in HOL4

[Thomas Tuerk]

Hi Ada,

there are many ways to do it. But essentially what you want is rewriting.

Bird's eye view:

You want to prove

``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``

STEP 1 : You show that "p" is "[]" with theorem LENGTH_NIL.
STEP 2 : You use the theorem TAKE_0 to simplify "TAKE 0 p" to "[]"
STEP 3 : You combine STEP 1 and STEP 2


There are plenty of ways to do it. Essentially, you want to use
LENGTH_NIL and TAKE_0 as rewrites. This can (rather verbosely) be done
via e.g.

val thm1 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
 REWRITE_TAC[LENGTH_NIL, TAKE_0] THEN
 REPEAT STRIP_TAC THEN
 ASM_REWRITE_TAC[])

However, a simple call to the simplifier is sufficient (it uses the
antecedent of the implication automatically and list_ss contains TAKE_0)

val thm2 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  SIMP_TAC list_ss [LENGTH_NIL])


One could also use first order automatic reasoners, but this is a bit
much here.

val thm3 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  REPEAT STRIP_TAC THEN
  `p = []` by PROVE_TAC[LENGTH_NIL] THEN
  ASM_REWRITE_TAC[TAKE_0])

val thm4 = prove (``!p. (LENGTH p = 0) ==> (TAKE 0 p = p)``,
  PROVE_TAC [TAKE_0, LENGTH_NIL])


There are plenty more ways for doing it. The core operation is rewriting
here. So, perhaps have a look at the rewrite tactics and the simplifier.

Best

Thomas Tuerk



On 15.12.2015 13:48, 康漫 wrote:
>   Hi,Ramana,Thanks for your reply!
>   after I used listTheory.LENGTH_NIL, I get that:
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_NIL);
> OK..
> 1 subgoal:
>> val it =
> first 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>  : proof
> Then Which tactic could be used to prove the goal? I tried many
> times , but it failed.
> Thanks! -Wish
> 
> 
> --
> 
> Message: 3
> Date: Tue, 15 Dec 2015 11:27:35 +0800
> From: " Ada " <ada.k...@qq.com>
> Subject: [Hol-info] [SPAM] some questions about the proving process in
> HOL4
> To: " hol-info " <hol-info@lists.sourceforge.net>
> Message-ID: <tencent_7f77ca956510ebe87ffaf...@qq.com>
> Content-Type: text/plain; charset="iso-8859-1"
> 
> Hey guys,
>  
> I am learning to use HOL4. There is  a function named "TAKE" in HOL4,
> which can get the first n elements in a list.
>  When I was proving one property of TAKE, I find an interesting thing.
> As follows:
>  - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `;
> - e (REPEAT STRIP_TAC);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
> 
>   LENGTH p = 0
>  : proof
> - e (STRIP_ASSUME_TAC listTheory.LENGTH_EQ_NUM_compute);
> OK..
> 1 subgoal:
>> val it =
>  TAKE 0 p = p
> 
>   0.  LENGTH p = 0
>   1.  !l. (LENGTH l = 0) <=> (l = [])
>   2.  !l n.
> (LENGTH l = NUMERAL (BIT1 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n) - 1) /\ (l = h::l')
>   3.  !l n.
> (LENGTH l = NUMERAL (BIT2 n)) <=>
> ?h l'. (LENGTH l' = NUMERAL (BIT1 n)) /\ (l = h::l')
>   4.  !l n1 n2.
> (LENGTH l = n1 + n2) <=>
> ?l1 l2. (LENGTH l1 = n1) /\ (LENGTH l2 = n2) /\ (l = l1 ++ l2)
>  : proof
>  The conditions of " LENGTH p = 0" and "!l. (LENGTH l = 0) <=> (l = [])"
> have already been in assumption list, so I think it is natural to get
> "p=[]", then "TAKE 0 [] = []". But I tried many times , I can't prove
> that. Could anyone prove it?
>  
>  Thanks! --Wish.
> -- next part --
> An HTML attachment was scrubbed...
> 
> --
> 
> Message: 4
> Date: Tue, 15 Dec 2015 14:34:44 +1100
> From: Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> Subject: Re: [Hol-info] [SPAM] some questions about the proving
> process in HOL4
> To: Ada <ada.k...@qq.com>
> Cc: hol-info <hol-info@lists.sourceforge.net>
> Message-ID:
> 

Re: [Hol-info] how to automatically collecting all the tactics together?

[Thomas Tuerk]

Hi,

there is also the GoalTree library. In contrast to the GoalStack one, 
expanding a tactic gets the tactic twice. Once as a string and once as a 
ML function. This allows the GoalTree to keep track of the proof 
stucture and print the tactics used for the proof using THEN, THENL, 
etc. at the end. There is a bit of support of sending the string 
automaticallz in the HolMode of emacs (I don't know about the vim 
bindings).


I prefer the wrinting my proofs manually. I believe it gives you more 
flexibility and there is better support for the GoalStack in the Emacs 
Hol Mode. However, I believe it was worth mentioning.


Best

Thomas

On 15.11.2015 11:00, Yong Kiam wrote:
See this for a better guide by Magnus: 
http://www.cl.cam.ac.uk/~mom22/HOL-interaction.pdf 



On Sun, Nov 15, 2015 at 5:55 PM, Yong Kiam > wrote:


This may not be directly relevant to your question but you could
consider developing your proofs interactively in an editor (Vim or
Emacs) and saving the scripts instead of using the HOL4 REPL
directly (see the various proof scripts in src/ and examples/).

I use the Vim bindings:
https://github.com/HOL-Theorem-Prover/HOL/tree/master/tools/vim
and others may be able to tell you more about the emacs ones.

Usual development (for me in Vim):

1) State the goal in your proof script like:

val foo = prove (``g``,

2) Highlight ``g`` and send it to the theorem prover as a goal
(h-t , h-g)

3) Start writing and trying tactics (h-e sends the tactic to the
prover, see the README for other things you could do)

val foo = prove(``g``,

fs[] >> rw[] >> blabla...

(>> is THEN, >- is THEN1)

4) On a successful proof, just save whatever you wrote in the
editor into a proof file:

val foo = prove(``g``, fs[]>>rw[]>>blabla);

This is off the top of my head, there might be a better guide for
this somewhere.

On Sun, Nov 15, 2015 at 5:39 PM, Ramana Kumar
> wrote:

Use Tactical.THEN (or lcsymtacs.>>, which is the same).

On 15 November 2015 at 09:03, shengyu shen
> wrote:

Dear all :

Supposing I have goal G and I prove it with lots of
tactics like folowing :


g `G`;
e (t1);
e (t2);
e (t3);

So after I finished proof, I need to use store_thm to
manually collecting all t1,t2,t3... to save the proven
theorem.

Is there  any way to automatically collect all these tactics?


Shen


--

___
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 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] how to prove a goal with case...of...

[Thomas Tuerk]

Hi,

if you don't like stateful tactics, you should also have a look at the
library DatatypeSimps. Moreover, it often helps me to turn off pretty
printing of case-expressions via

set_trace pp_cases 0

You need rewriting of the list_CASE and equality of chars. So, your
goal should also be solved via

SIMP_TAC std_ss [listTheory.list_case_def, stringTheory.CHR_11]

If you want it higher level use the string and list simpsets:

SIMP_TAC (list_ss++stringSimps.STRING_ss) []

or use the DatatypeSimps, which work for other types as well:

SIMP_TAC
(std_ss++stringSimps.STRING_ss++DatatypeSimps.type_rewrites_ss([``:'a
list``])) []

Thomas



On 04/11/14 04:31, Michael Norrish wrote:
 On 04/11/14 13:33, ＂f~鳓ぁぇ wrote:
 Hi,
 I want to prove a goal like this:
   `case d of u =1 |s =2|d 
 =3
 |p =4`
 Is there a tactic which can match d with the branch d and then execute 
 this
 branch.
 SIMP_TAC (srw_ss()) []

 or

 SRW_TAC[][]

 should both work on this sort of goal.

 Michael


 

 The information in this e-mail may be confidential and subject to legal 
 professional privilege and/or copyright. National ICT Australia Limited 
 accepts no liability for any damage caused by this email or its attachments.

 --
 ___
 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] list computations

[Thomas Tuerk]

Hi,

I think, it is even simpler:

SIMP_TAC list_ss [rich_listTheory.DROP_APPEND2] 

Best

Thomas

On Wed, 2013-02-27 at 22:10 +, Ramana Kumar wrote: 
 Thanks! The secret sauce seems to be EL_APPEND2, and possibly whatever
 is in lrw. (And I should use LIST_EQ_REWRITE more often too.)
 This should make a lot of my subgoal proofs much shorter :)
 
 
 
 On Wed, Feb 27, 2013 at 7:02 PM, Anthony Fox ac...@cam.ac.uk wrote:
 Note quite sure how you got to 48 lines. I think only a single
 call to SRW_TAC (or lcsymtacs.lrw) is needed.
 
 val thm = Q.prove(
`TAKE (LENGTH bvs + 1)
  (REVERSE bvs ++
   h::
   (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st))
 ++ 
DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
  (REVERSE bvs ++
 
   h::
   (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st))
 = 
TAKE (LENGTH bvs + 1)
  (REVERSE bvs ++
 
   h::
   (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st))
 ++ st`,
lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP,
 rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS,
 arithmeticTheory.PRE_SUB1]
)
 
 Anthony 
 
 On 27 Feb 2013, at 17:58, Ramana Kumar
 ramana.ku...@cl.cam.ac.uk wrote:
 
  I just wrote a fairly manual 48-line proof of the following.
  Is there some decision procedure, simpset, or tactic I could
 use to automate it that I'm not aware of?
  The theorems in srw_ss() seem not to play very well together
 on this kind of stuff.
 
  TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
 Block 3 [CodePtr a; bve]::
 (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++
 [cl0] ++ st)) ++
  DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
(REVERSE bvs ++
 Block 3 [CodePtr a; bve]::
 (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++
 [cl0] ++ st)) =
  TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
 Block 3 [CodePtr a; bve]::
 (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++
 [cl0] ++ st)) ++
  st
 
 
 
 
 --
  Everyone hates slow websites. So do we.
  Make your web apps faster with AppDynamics
  Download AppDynamics Lite for free today:
 
 
 http://p.sf.net/sfu/appdyn_d2d_feb___
  hol-info mailing list
  hol-info@lists.sourceforge.net
  https://lists.sourceforge.net/lists/listinfo/hol-info
 
 
 
 --
 Everyone hates slow websites. So do we.
 Make your web apps faster with AppDynamics
 Download AppDynamics Lite for free today:
 http://p.sf.net/sfu/appdyn_d2d_feb
 ___ hol-info mailing list 
 hol-info@lists.sourceforge.net 
 https://lists.sourceforge.net/lists/listinfo/hol-info



--
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Emacs mode for HOL4?

[Thomas Tuerk]

Hi,

the emacs code is in tools/hol_mode.el
A documentation how to install it, can be found in
Manual/Interaction.

I hope this helps,

Thomas Tuerk


Am Sonntag, den 05.02.2012, 09:26 -0800 schrieb Ian Zimmerman:
 The Kananaskis distribution contains a doc/hol-mode subdirectory with a
 quick reference chart of Emacs commands, but there seems to be no actual
 Emacs code included.  Does it exist and where might I find it?
 



--
Try before you buy = See our experts in action!
The most comprehensive online learning library for Microsoft developers
is just $99.99! Visual Studio, SharePoint, SQL - plus HTML5, CSS3, MVC3,
Metro Style Apps, more. Free future releases when you subscribe now!
http://p.sf.net/sfu/learndevnow-dev2
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info