from:"Michael.Norrish"

I was hesitant to document anything before nailing down the final form of the 
syntax.  But it's clear that a fairly radical change like this one will need 
good explanation.  

It's particularly confusing because it's a form that cannot be explained in 
terms of standard ML programming.  (Our quotation syntax has the same problem.)

Michael

On 8/1/19, 17:08, "Jeremy Dawson"  wrote:



On 8/1/19 4:49 pm, michael.norr...@data61.csiro.au wrote:
> I think you've misunderstood. 

that's true, sorry.

> Here the advantage is quite clear and valuable: in the existing system, 
you have to type the same string of symbols twice in order to avoid annoying 
maintenance issues when theorems get moved.  There's no utility in allowing 
people to write things like
> 
> val foo = save_thm("bar", ...)
> 
> and it just leads to real pain.
> 
there's certainly a discernible advantage in this particular case, I agree

> Slippery slope arguments cut no mustard.
> 
Let's hope it's not the start of one.  And do work out a way of getting 
it into the online documentation (eg, in 
HOL/help/src-sml/htmlsigs/idIndex.html)

Jeremy

___
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] HOL's new measure theory (in progress)

I look forward to the eventual PR!

Micahel

On 8/1/19, 02:33, "Chun Tian (binghe)"  wrote:

Beside, there’re two other benefits:

1) Hurd’s original elegant long proof of CARATHEODORY is now preserved in 
old_measureTheory.
2) Coble’s “dining cryptographers” work (example/diningcryptos) can also be 
fixed (in the future) under old_measureTheory and old_probabilityTheory, 
because his work also doesn’t use anything from lebesgueTheory and 
extrealTheory (also these scripts were included).

—Chun

> Il giorno 07 gen 2019, alle ore 16:19, Chun Tian (binghe) 
 ha scritto:
> 
> Hi Micheal,
> 
> thanks for your trust.  Now I’ve done the following solution for 
preserving some backwards compatibilities:
> 
> My goal is to make minimal efforts to make sure that Hurd's Miller-Rabin 
work (examples/miller) can still build after my PR.I found that, the code 
in “miller” depends only on “measureTheory” and “probabilityTheory” but 
“lebesgueTheory”.  Thus I thought maybe I can keep a minimal copy of just the 
old “measureTheory” and “probabilityTheory” with all extreal and lebesgue stuff 
removed.
> 
> This is indeed possible: 90% of the current probabilityTheory (1208 of 
1348 lines) does not use “lebesgueTheory” at all. And the only part in the 
current “measureTheory” which depends on extended reals are those related to 
“Borel” measurable sets, which is not needed by Miller-Rabin example.
> 
> The result is: I kept the old version of measureTheory and 
probabilityTheory with minimal deletions. Now they’re at 
“src/probability/old_measureScript.sml” and 
“src/probability/old_probabilityScript.sml.  And I've successfully fixed the 
Miller-Rabin example using these “old” scripts.
> 
> The fact that these two old scripts (formalizing a minimal abstract 
probabilityTheory based on real-valued measureTheory) can still support the 
Miller-Rabin example, shows that it’s worthy to keep them in latest HOL4, I 
think, unless one day someone completely ported Hurd’s code into the 
forthcoming new probabilityTheory.
> 
> The working codebase with all above ideas implemented is at my working 
branch [1]
> 
> Regards,
> 
> Chun Tian
> 
> [1] https://github.com/binghe/HOL/tree/Probability-6/
> 
>> Il giorno 07 gen 2019, alle ore 01:24, michael.norr...@data61.csiro.au 
ha scritto:
>> 
>> I am happy to let those most affected by or interested in the PR to 
discuss the best way forward, here, or on the hol-developers mailing list, or 
privately.
>> 
>> My main concern would be to minimise unnecessary backwards 
incompatibilities. As someone who introduces the most incompatibilities from 
release to release, it is clear that I don't view this as an absolute 
requirement, so I'm happy to trust the interested parties to come to an 
appropriate agreement about the right way forward.
>> 
>> Michael
>> 
>> On 5/1/19, 09:02, "Chun Tian (binghe)"  wrote:
>> 
>>   Thanks.
>> 
>>   I think it’s better to let HOL maintainers to decide if we should keep 
the old version (14,700 lines) in “examples”, e.g. “examples/old-probability”. 
I personally don’t like this idea, because the old version is always accessible 
from previous HOL releases.  And there’re still many redundant 
probability-related scripts to be cleaned up from the example folder.
>> 
>>   Comparing with the proof scripts I get from HVG’s web site, beside a 
lot of additions, I actually didn’t change any definition, and almost didn’t 
change any theorem name. I believe it should be quite easy to load HVG’s other 
proof scripts on top of my current work.
>> 
>>   So far I haven’t touched or merged anything in the following scripts:
>> 
>>   - normal_rv_hvgScript.sml
>>   - PIE_EXTREALScript.sml
>>   - lebesgue_measure_hvgScript.sml
>>   - integration_hvgScript.sml
>>   - derivative_hvgScript.sml
>> 
>>   my future plan is to merge the first 3 (or 2) scripts and abandon last 
two, as the last two must be the so-called “Gauge integral” for constructing 
Lesbegue measure.  (Now with the new carathéodory theorem and the recent ported 
“real_topologyScript.sml” in HOL4, we can easily construct Lesbegue measure)  
If their original authors (you and Qasim, e.g.) could help, that will be great! 
  We should finally work out a usable and feature-rich probability theory for 
HOL4, and let it become the standard theory library for other applications of 
future HOL4 users.
>> 
>>   In particular, If you have new theorems that can be added into my 
current version of “measureTheory”, I suggest you sending PRs to me for now. 
All your work will finally go into HOL official for sure!
>> 
>>   Regards,
>> 
>>   Chun Tian
>> 
>>> Il giorno 04 gen 2019, alle ore 22:08, Waqar Ahmad 
<12phdwah...@seecs.edu.pk> ha scritto:
>>> 
>>> Hi Chun,

Re: [Hol-info] New grammar of defining theorems?

I think you've misunderstood.  One form maps to store_thm; the other maps to 
save_thm.  In both cases the name is likely to be fresh, just as the names 
passed to store_thm and save_thm are usually fresh.  (If they're not, the 
underlying SML functions emit warning messages.)

Here the advantage is quite clear and valuable: in the existing system, you 
have to type the same string of symbols twice in order to avoid annoying 
maintenance issues when theorems get moved.  There's no utility in allowing 
people to write things like

   val foo = save_thm("bar", ...)

and it just leads to real pain. 

Slippery slope arguments cut no mustard.

Michael

On 8/1/19, 15:09, "Jeremy Dawson"  wrote:

This summary seems to make it clear that this new feature achieves very 
little, with the following costs:

- it gives users yet something else (as if there isn't already enough!) 
to lookup in the documentation, or ask questions about
- it's positively confusing, in that
"Theorem name ... " has totally different meanings, depending on which 
case applies (eg, in one case, name must already exist, in the other, it 
ought not to already exist)

This idea looks like the start of the path followed in Isabelle and Coq, 
of having a multitude of commands, some with a multitude of variants (eg 
optional arguments) with no coherent consistent grammar rules - just so 
that the user doesn't need to type a few punctuation symbols.

Jeremy

On 8/1/19 2:41 pm, Konrad Slind wrote:
> Isn't it clear just from the form?
> 
>Theorem name quote (ML)--> val name = Q.store_thm(name,quote,ML)
>Theorem name (ML)  --> val name = save_thm(name,ML)
> 
> 

___
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] New grammar of defining theorems?

You can’t/don’t want to write a regular expression to distinguish these by 
matching the entirety of the goal and tactic.

Michael

From: Konrad Slind 
Date: Tuesday, 8 January 2019 at 14:41
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] New grammar of defining theorems?

Isn't it clear just from the form?

  Theorem name quote (ML)--> val name = Q.store_thm(name,quote,ML)
  Theorem name (ML)  --> val name = save_thm(name,ML)

On Mon, Jan 7, 2019 at 8:34 PM 
mailto:michael.norr...@data61.csiro.au>> wrote:
Forward and backward give us nice terminology, thanks!  It may also be possible 
to have the quotation filter figure things out by looking for the 
left-parenthesis that is required to follow the name in the forward case.  I 
may play with that.

Michael

On 8/1/19, 12:38, "Chun Tian (binghe)" 
mailto:binghe.l...@gmail.com>> wrote:

Hmmm, well… all theorems are essentially *derived* from earlier theorems or 
axioms, thus it seems (to me) that the word “derived” still doesn’t capture the 
characterization of “save_thm” from “store_thm”.   But the word “dervied” makes 
more senses than previous “calculated” as “save_thm”’s body is mainly using 
“derived rules” instead of “tactics”. However, I see the essential difference 
is the direction in the proof: from proof goal to existing theorems, or from 
existing theorems to proof goal.

This whole mail thread is not really a technical discussion, thus whatever 
I said here must be highly subjective, however I suggest the following:

1. using keyword “forward” and “backward” to distinguish theorems built by 
“save_thm” and “store_thm”, respectively:

- Theorem(forward) name (MLcode);
- Theorem(backward) name tmquote (MLcode);

2. the keyword (backward) is optional (simply because this is the most 
case), thus backward theorems can also be expressed (if detected the tmquote 
part, somehow) in your current way:

- Theorem name tmquote (MLcode);

3. if ML’s parser is smart enough, even the keyword (forward) can be 
eliminated, because the number of arguments is different: in forward proof it 
is 2, in backward proof it is 3:

- Theorem name (MLcode);
- Theorem name tmquote (MLcode);

How much you can go with above idea, depends on how powerful the ML 
quotation code can be.

Hope this helps,

—Chun

> Il giorno 08 gen 2019, alle ore 02:10, 
michael.norr...@data61.csiro.au ha 
scritto:
>
> Indeed, they are both calculated.  In one, you state the desired 
end-state and head towards it with a tactic.  In the other, you transform 
existing theorems with rules of inference and derive a final statement (hence 
the good practice, which you mentioned, of putting the statement into a 
comment).
>
> Given that, what about
>
>   Theorem(derived) name (MLcode);
>
> ?
>
> Michael
>
> On 7/1/19, 20:31, "Chun Tian (binghe)" 
mailto:binghe.l...@gmail.com>> wrote:
>
>Hi Michael,
>
>Thanks, now I see your points: if it’s really a “lemma”, then there’s 
no need to export it, thus `Q.prove` (or `prove`) should just do the job.
>
>Among the two syntactic sugars, I personally like your first version 
(Theorem(calculated) …), because it emphasized that, a `Theorem` generated by 
`save_thm` has no differences (in use) with a `Theorem` generated by 
`store_thm`, just the word “calculated” could have a better name, as both kinds 
of theorems are essentially calculated.
>
>—Chun
>
>> Il giorno 07 gen 2019, alle ore 01:16, 
michael.norr...@data61.csiro.au ha 
scritto:
>>
>> The Theorem keyword is a prettier way of writing `store_thm`, which, as 
the name suggests, is indeed for theorems.  In other words, the choice of 
Theorem merely reflects our existing naming convention.
>>
>> If you have a lemma that shouldn’t be “stored”, then you should probably 
be using `Q.prove` (or `prove`).  The use of theory files that make theorem 
values persistent is the way in which users can distinguish important results 
that should persist (that is, “theorems”), and those that should be more 
ephemeral.
>>
>> The existing `save_thm` entrypoint has the same problem with requiring 
redundant typing of names. I’m thus tempted to invent a Theorem analogue to map 
to it.  My current feeling is to go for something like
>>
>>   Theorem(calculated) thmname (ML code);
>>
>> Or
>>
>>  Computed_Theorem thmname (ML code)
>>
>> Or …?
>>
>> Suggestions welcome.
>>
>> Michael
>>
>> From: "Chun Tian (binghe)" 
mailto:binghe.l...@gmail.com>>
>> Date: Thursday, 3 January 2019 at 23:20
>> To: Makarius mailto:makar...@sketis.net>>
>> Cc: Michael Norrish 
mailto:michael.norr...@data61.csiro.au>>, 
hol-info mailto:hol-info@lists.sourceforge.net>>
>>

Re: [Hol-info] New grammar of defining theorems?

Forward and backward give us nice terminology, thanks!  It may also be possible 
to have the quotation filter figure things out by looking for the 
left-parenthesis that is required to follow the name in the forward case.  I 
may play with that.

Michael

On 8/1/19, 12:38, "Chun Tian (binghe)"  wrote:

Hmmm, well… all theorems are essentially *derived* from earlier theorems or 
axioms, thus it seems (to me) that the word “derived” still doesn’t capture the 
characterization of “save_thm” from “store_thm”.   But the word “dervied” makes 
more senses than previous “calculated” as “save_thm”’s body is mainly using 
“derived rules” instead of “tactics”. However, I see the essential difference 
is the direction in the proof: from proof goal to existing theorems, or from 
existing theorems to proof goal.

This whole mail thread is not really a technical discussion, thus whatever 
I said here must be highly subjective, however I suggest the following:

1. using keyword “forward” and “backward” to distinguish theorems built by 
“save_thm” and “store_thm”, respectively:

- Theorem(forward) name (MLcode);
- Theorem(backward) name tmquote (MLcode);

2. the keyword (backward) is optional (simply because this is the most 
case), thus backward theorems can also be expressed (if detected the tmquote 
part, somehow) in your current way:

- Theorem name tmquote (MLcode);

3. if ML’s parser is smart enough, even the keyword (forward) can be 
eliminated, because the number of arguments is different: in forward proof it 
is 2, in backward proof it is 3:

- Theorem name (MLcode);
- Theorem name tmquote (MLcode);

How much you can go with above idea, depends on how powerful the ML 
quotation code can be.

Hope this helps,

—Chun

> Il giorno 08 gen 2019, alle ore 02:10, michael.norr...@data61.csiro.au ha 
scritto:
> 
> Indeed, they are both calculated.  In one, you state the desired 
end-state and head towards it with a tactic.  In the other, you transform 
existing theorems with rules of inference and derive a final statement (hence 
the good practice, which you mentioned, of putting the statement into a 
comment).
> 
> Given that, what about
> 
>   Theorem(derived) name (MLcode);
> 
> ?
> 
> Michael
> 
> On 7/1/19, 20:31, "Chun Tian (binghe)"  wrote:
> 
>Hi Michael,
> 
>Thanks, now I see your points: if it’s really a “lemma”, then there’s 
no need to export it, thus `Q.prove` (or `prove`) should just do the job.
> 
>Among the two syntactic sugars, I personally like your first version 
(Theorem(calculated) …), because it emphasized that, a `Theorem` generated by 
`save_thm` has no differences (in use) with a `Theorem` generated by 
`store_thm`, just the word “calculated” could have a better name, as both kinds 
of theorems are essentially calculated.
> 
>—Chun
> 
>> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au 
ha scritto:
>> 
>> The Theorem keyword is a prettier way of writing `store_thm`, which, as 
the name suggests, is indeed for theorems.  In other words, the choice of 
Theorem merely reflects our existing naming convention.
>> 
>> If you have a lemma that shouldn’t be “stored”, then you should probably 
be using `Q.prove` (or `prove`).  The use of theory files that make theorem 
values persistent is the way in which users can distinguish important results 
that should persist (that is, “theorems”), and those that should be more 
ephemeral.
>> 
>> The existing `save_thm` entrypoint has the same problem with requiring 
redundant typing of names. I’m thus tempted to invent a Theorem analogue to map 
to it.  My current feeling is to go for something like
>> 
>>   Theorem(calculated) thmname (ML code);
>> 
>> Or
>> 
>>  Computed_Theorem thmname (ML code)
>> 
>> Or …?
>> 
>> Suggestions welcome.
>> 
>> Michael
>> 
>> From: "Chun Tian (binghe)" 
>> Date: Thursday, 3 January 2019 at 23:20
>> To: Makarius 
>> Cc: Michael Norrish , hol-info 

>> Subject: Re: [Hol-info] New grammar of defining theorems?
>> 
>> So the key is to make sure that they’re not distinguished internally by 
some tools, and if some tools do, it’s their problems but HOL’s.
>> 
>> I personally don’t like the keyword “Theorem” because I think many small 
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct 
way of using these conventions should be aligned with majority math books, 
which I believe there must be some “rules” mentioned somewhere.
>> 
>> On the other side, HOL4 users always have multiple ways to build a 
theorem. For example, sometimes I perfer using “save_thm” to build theorems 
forwardly and put the statement as comments before it, sometimes multiple 
theorems were put

Re: [Hol-info] assignment

You are close.  Use MAP.

And please don’t use a mailing list to do assignments.

Michael

From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:49
To: hol-info 
Subject: [Hol-info] assignment

The following data types are defined in HOL4.

   val _ = Datatype `

 coordinate = <|

x_axis: real;

y_axis: real;

z_axis: real

 |> `;

   val _ = Datatype `

   chromosome = <|

   r: num;

   b: num;

   distance: real;

   rx: coordinate;

   path: coordinate list;

   bx: coordinate

   |> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
 val get_def = Define `
 get pop = !ch  if (Certain condition) then (ch with <| distance := 
ch.distance + 1000 |>)
   else (ch with <| distance := ch.distance |>)`;

Given a pop(:chromosome list),ch is an element in pop. For any ch, if a 
certain condition is met, the value of distance in ch is increased by 1000 on 
the basis of the original value, otherwise it is unchanged. How to achieve this?
How to write an program in SML (or Haskell, or OCaml) first,then 
formalising it in HOL? Can you give a simple example?
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] New grammar of defining theorems?

Indeed, they are both calculated.  In one, you state the desired end-state and 
head towards it with a tactic.  In the other, you transform existing theorems 
with rules of inference and derive a final statement (hence the good practice, 
which you mentioned, of putting the statement into a comment). 

Given that, what about 

   Theorem(derived) name (MLcode);

?

Michael

On 7/1/19, 20:31, "Chun Tian (binghe)"  wrote:

Hi Michael,

Thanks, now I see your points: if it’s really a “lemma”, then there’s no 
need to export it, thus `Q.prove` (or `prove`) should just do the job.

Among the two syntactic sugars, I personally like your first version 
(Theorem(calculated) …), because it emphasized that, a `Theorem` generated by 
`save_thm` has no differences (in use) with a `Theorem` generated by 
`store_thm`, just the word “calculated” could have a better name, as both kinds 
of theorems are essentially calculated.

—Chun

> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au ha 
scritto:
> 
> The Theorem keyword is a prettier way of writing `store_thm`, which, as 
the name suggests, is indeed for theorems.  In other words, the choice of 
Theorem merely reflects our existing naming convention.
> 
> If you have a lemma that shouldn’t be “stored”, then you should probably 
be using `Q.prove` (or `prove`).  The use of theory files that make theorem 
values persistent is the way in which users can distinguish important results 
that should persist (that is, “theorems”), and those that should be more 
ephemeral.
> 
> The existing `save_thm` entrypoint has the same problem with requiring 
redundant typing of names. I’m thus tempted to invent a Theorem analogue to map 
to it.  My current feeling is to go for something like
> 
>Theorem(calculated) thmname (ML code);
> 
> Or
> 
>   Computed_Theorem thmname (ML code)
> 
> Or …?
> 
> Suggestions welcome.
> 
> Michael
> 
> From: "Chun Tian (binghe)" 
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius 
> Cc: Michael Norrish , hol-info 

> Subject: Re: [Hol-info] New grammar of defining theorems?
> 
> So the key is to make sure that they’re not distinguished internally by 
some tools, and if some tools do, it’s their problems but HOL’s.
> 
> I personally don’t like the keyword “Theorem” because I think many small 
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct 
way of using these conventions should be aligned with majority math books, 
which I believe there must be some “rules” mentioned somewhere.
> 
> On the other side, HOL4 users always have multiple ways to build a 
theorem. For example, sometimes I perfer using “save_thm” to build theorems 
forwardly and put the statement as comments before it, sometimes multiple 
theorems were put into a “local” block sharing common tactics. As a result, 
HOL4 proof scripts were *not* documents but essentially raw ML programs, thus 
extremely flexible.  I may not adopt this new grammar in a complex proof script 
in which different ways of building theorems were used together.
> 
> —Chun
> 
> P. S. Coq seems to have even more synonyms: (do Coq users here share the 
same concerns?)
> 
> Lemma ident [binders] : type.
> Remark ident [binders] : type.
> Fact ident [binders] : type.
> Corollary ident [binders] : type.
> Proposition ident [binders] : type.
> 
> These commands are synonyms of Theorem ident [binders] : 
type.
> 
> Il giorno 03 gen 2019, alle ore 12:23, Makarius  ha 
scritto:
> 
> On 03/01/2019 11:23, Chun Tian (binghe) wrote:
> 
> Hi Michael,
> 
> thanks for fixing the bugs. (now I see why I can’t find its definition…)
> 
> Going in this direction, have you considered adding also “Lemma” and 
“Corollary”? Internally they're equivalent with “Theorem”, but they could 
literally help writers (and readers) identifying different levels of theorems, 
like those in math books.
> 
> This reminds me of Isabelle/Isar. Some decades ago I introduced these
> variants of 'theorem' and it became a running gag of confusion and
> unclear corner cases, because aliases were not really identical, but
> distinguished internally by some tools.
> 
> Recently, we even introduced 'proposition' as another variant, but it is
> unclear if it is more prominent than 'theorem' or less prominent than
> 'lemma'. Thus it depends on local conventions of particular
> formalization projects how to treat it, e.g. in document presentation.
> 
> If I had another chance today, I would probably eliminate all funny
> aliases of Isar commands.
> 
> 
> Makarius
> 
> 
> 
>

Re: [Hol-info] assignment

Your problem statement doesn’t make sense.  Why do you say “*the* ch in the 
pop”? Surely a pop may contain multiple ch values.

As I said before, it seems as if you should try to write your program in SML 
(or Haskell, or OCaml) first.  Then you might think about formalising it in 
HOL.  If you want to adjust all the values in a list, look at the map function 
(called MAP in HOL).

Michael

From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 8 January 2019 at 12:01
To: hol-info 
Subject: [Hol-info] assignment

The following data types are defined in HOL4.

   val _ = Datatype `

 coordinate = <|

x_axis: real;

y_axis: real;

z_axis: real

 |> `;

   val _ = Datatype `

   chromosome = <|

   r: num;

   b: num;

   distance: real;

   rx: coordinate;

   path: coordinate list;

   bx: coordinate

   |> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
 val get_def = Define `
 get pop = !ch  if (Certain condition) then (ch with <| distance := 
ch.distance + max_distance pop |>)
   else (ch with <| distance := ch.distance |>)`;


Given a pop(:chromosome list), I want to achieve a goal : If if-condition 
is met, the distance value of the ch in the pop is assigned to other values, 
otherwise the distance value of ch is unchanged. How to solve this problem?
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL's new measure theory (in progress)

2019-01-06 Thread Michael.Norrish

I am happy to let those most affected by or interested in the PR to discuss the 
best way forward, here, or on the hol-developers mailing list, or privately.  

My main concern would be to minimise unnecessary backwards incompatibilities. 
As someone who introduces the most incompatibilities from release to release, 
it is clear that I don't view this as an absolute requirement, so I'm happy to 
trust the interested parties to come to an appropriate agreement about the 
right way forward.

Michael

On 5/1/19, 09:02, "Chun Tian (binghe)"  wrote:

Thanks.

I think it’s better to let HOL maintainers to decide if we should keep the 
old version (14,700 lines) in “examples”, e.g. “examples/old-probability”. I 
personally don’t like this idea, because the old version is always accessible 
from previous HOL releases.  And there’re still many redundant 
probability-related scripts to be cleaned up from the example folder.

Comparing with the proof scripts I get from HVG’s web site, beside a lot of 
additions, I actually didn’t change any definition, and almost didn’t change 
any theorem name. I believe it should be quite easy to load HVG’s other proof 
scripts on top of my current work.

So far I haven’t touched or merged anything in the following scripts:

- normal_rv_hvgScript.sml
- PIE_EXTREALScript.sml
- lebesgue_measure_hvgScript.sml
- integration_hvgScript.sml
- derivative_hvgScript.sml

my future plan is to merge the first 3 (or 2) scripts and abandon last two, 
as the last two must be the so-called “Gauge integral” for constructing 
Lesbegue measure.  (Now with the new carathéodory theorem and the recent ported 
“real_topologyScript.sml” in HOL4, we can easily construct Lesbegue measure)  
If their original authors (you and Qasim, e.g.) could help, that will be great! 
  We should finally work out a usable and feature-rich probability theory for 
HOL4, and let it become the standard theory library for other applications of 
future HOL4 users.

In particular, If you have new theorems that can be added into my current 
version of “measureTheory”, I suggest you sending PRs to me for now. All your 
work will finally go into HOL official for sure!

Regards,

Chun Tian

> Il giorno 04 gen 2019, alle ore 22:08, Waqar Ahmad 
<12phdwah...@seecs.edu.pk> ha scritto:
> 
> Hi Chun,
> 
> Great work!!! I briefly went through the proof script and looks good to 
me. However, there are few things that need be discussed before this PR that 
are as follows:
> 
> 1) The current version of the measure theory, which is still part of 
HOL-sources, is formalized by taking a real-valued 'measure': ('a -> bool) -> 
real ... whereas, you're working on the version having extreal-valued 
'measure': ('a -> bool) -> extreal ... Do you have any plan to keep the 
previous version?
> 
> 2) My suggestion is to place the real-valued 'measure' theory somewhere 
in HOL/examples and continue further development on extreal-valued 'measure' 
theory.
> 
> 3) I've also further extended the Qasim's measure theory by porting more 
necessary defs/thms from Isabelle. I'd like to make them part of future measure 
theory PRs.. Let me know if you have any suggestions regarding it...
> 
> 
> Feel free to share your thoughts...
> 
> 
> On Fri, Jan 4, 2019 at 11:01 AM Chun Tian (binghe) 
 wrote:
> Hi all,
> 
> after 4 months’ hard work (mostly using my spare time), among other 
things, finally I have (re)proved Carathéodory's extension theorem [6] under 
the new [0, +Inf] measure theory (from HVG [5]). This is the most general 
version based on semi-ring, also with uniqueness arguments:
> 
>[CARATHEODORY_SEMIRING]  Theorem
> 
>   ⊢ ∀m0.
> semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
> ∃m.
> measure_space m ∧
> (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 
s)) ∧
> ((m_space m,measurable_sets m) =
>  sigma (m_space m0) (measurable_sets m0)) ∧
> (sigma_finite m0 ⇒
>  ∀m'.
>  measure_space m' ∧ (m_space m' = m_space m) ∧
>  (measurable_sets m' = measurable_sets m) ∧
>  (∀s.
>   s ∈ measurable_sets m0 ⇒
>   (measure m' s = measure m0 s)) ⇒
>  ∀s.
>  s ∈ measurable_sets m' ⇒
>  (measure m' s = measure m s))
> 
> The original CARATHEODORY (back to Joe Hurd [1] and A. R. Coble [2]) now 
becomes an easy corollary (as any algebra is also semiring):
> 
>[CARATHEODORY]  Theorem
> 
>   ⊢ ∀m0.
> algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
>

Re: [Hol-info] Relations which build upon each other

2019-01-04 Thread Michael.Norrish

Two relations are not likely to give you what you want in this scenario.

For example, if the first system has a rule for conjunction introduction:

  Thm1 p /\ Thm1 q ==> Thm1 (p AND q)

then this rule requires Thm1 hypotheses.  If you add

  Thm1 p ==> Thm2 p

you don’t get to use Thm2 hypotheses to prove conjunctions using the first rule.

If you’re committed to this notion of systems of rules that can be extended in 
the way you want, I think there’s probably a bit of work required I’m afraid, 
and it may not really win you much.  I agree though that having to repeat rules 
for things like conjunction introduction feels annoying.

Michael

From: Alexander Cox 
Date: Friday, 4 January 2019 at 09:11
To: hol-info 
Subject: [Hol-info] Relations which build upon each other


Hello,

I’m doing a project on proof theory, and I’m trying to define the proof rules 
with Hol_reln. I am defining multiple proof systems which build upon each 
other, i.e. intuitionistic logic then classical logic. It seems natural to have 
something like:

var (Sys1_rules, …,…) = Hol_reln `…`;
var (Sys2_rules,…,…) = Hol_reln `!x. Sys1 x ==> Sys2 x /\ …`

But when I go to prove something which needs to use Sys2 rules then Sys1 rules, 
I don’t know how to get it to work, since the Sys1 rules don’t know mention 
Sys2 (nor should they). For example:

`Sys2 x` by metis_tac[Sys2_rules]
`Sys2 y` by metis_tac[Sys1_rules,Sys2_rules] (* Sys1 has no rules for Sys2, so 
this fails! *)

The obvious solution is to just keep them independent and have all the rules in 
each of them, but I thought I might be missing some elegant way of achieving 
this. Please let me know if there is such a trick.

Thank you,
Alex
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] New grammar of defining theorems?

2019-01-02 Thread Michael.Norrish

Dear Chun,

This is indeed a new feature of the quotation filter.  Its purpose is to keep 
names consistent, and to reduce the amount of boilerplate typing that 
script-writers have to generate.

It's as yet undocumented, but I hope to get to that soon.

Michael

On 2/1/19, 06:20, "Chun Tian (binghe)"  wrote:

Hi,

(Happy New Year) I found the following code in 
src/patricia/sptreeScript.sml (added in commit 
2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)

Theorem list_to_num_set_append
  `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) 
(list_to_num_set l2)`
 (Induct \\ rw[list_to_num_set_def]
  \\ rw[Once insert_union]
  \\ rw[Once insert_union,SimpRHS]
  \\ rw[union_assoc]);

Where is the definition of the keyword “Theorem”? Is this a new grammar of 
defining theroems, aiming at preventing inconsistent theorem names in exported 
theories?

Regards,

Chun




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

Re: [Hol-info] Element assignment in structures

2018-12-19 Thread Michael.Norrish

As written (and with a definition provided for max_distance), your script works 
fine.  Your error message must be for some other problem.

From your description, it sounds as if you want to use MAP to alter all ch 
values in a pop (which is a chromosome list).

As it seems very computational, I’d recommend trying to write your algorithm in 
SML (or Haskell, or OCaml), and then translating it to HOL.

Michael

From: 幻＠未来 <849678...@qq.com>
Date: Thursday, 20 December 2018 at 12:38
To: hol-info 
Subject: [Hol-info] Element assignment in structures

The following data types are defined in HOL4.

   val _ = Datatype `

 coordinate = <|

x_axis: real;

y_axis: real;

z_axis: real

 |> `;

   val _ = Datatype `

   chromosome = <|

   r: num;

   b: num;

   distance: real;

   rx: coordinate;

   path: coordinate list;

   bx: coordinate

   |> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
 val get_def = Define `
 get pop ch =  if MEM ch pop then (ch with <| distance := 
ch.distance + max_distance pop |>)
   else (ch with <| distance := ch.distance |>)`;
 val get1_def = Define `
 get1 pop  = !ch.  if MEM ch pop then (ch.distance = ch.distance + 
max_distance pop)
   else ch.distance = ch.distance`;
 The definition of get_def is successful, but the definition of get1_def is 
unsuccessful. Defining get1_def will report an error:
Exception raised at Preterm.type-analysis:
roughly between line 878, character 19 and line 879, character 58:
Type inference failure: unable to infer a type for the application of

   ($! :(α -> bool) -> bool) :(α -> bool) -> bool

   on line 878, characters 14-17

   to

  λ(ch :chromosome).
 if MEM ch (pop :chromosome list) then
ch with distance := ch.distance + max_distance pop
  else ch with distance := ch.distance

   roughly between line 878, character 19 and line 879, character 58

 which has type

 :chromosome -> chromosome

  unification failure message: Attempt to unify different type operators: 
min$bool and scratch$chromosome

What I want to do is to give a pop(:chromosome list), for any 
ch(:chromosome) in the pop , if some conditions are met, then the distance 
value in ch is modified. How to solve this problem?
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Element assignment in structures

2018-12-17 Thread Michael.Norrish

HOL is not an imperative language, so you can’t “assign” fields of a record.  
However, you can write things like

My_record with <| b := 3; rx := x’; distance := 10.6 |>

to denote a chromosome value that is the same as My_record except that fields 
b, rx and distance have different values.

Michael

From: 幻＠未来 <849678...@qq.com>
Date: Tuesday, 18 December 2018 at 13:57
To: hol-info 
Subject: [Hol-info] Element assignment in structures

 Hello!
 I defined the following data structure in HOL4.
   Datatype `
chromosome = <|
r: num;
b: num;
   distance: real;
   rx: coordinate;
   path: coordinate list;
   bx: coordinate
   |>`;
  So, how do you assign values and modify values to elements in a structure?
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Research Scientist job at Data61

2018-11-18 Thread Michael.Norrish

Data61 Seeking Research Scientist
=

We are looking for a full-time research scientist in formal verification to
join us, the Trustworthy Systems group, at Data61, CSIRO. Our highly
international team is located on the UNSW campus, close to the beautiful
beaches of sunny Sydney, Australia, one of the world's most liveable cities.

Our vision is a world in which computer users can choose all three: correct,
secure, and fast. We believe that most current approaches to building systems
are fundamentally flawed. We aim to demonstrate a better way. Our approach is
rooted in foundational, formal verification using theorem provers (e.g.,
Isabelle, HOL4), and high-performance system design. If you find this vision
appealing, and have ideas about how to pursue it, we want to hear from you.

Our team brings together a unique combination of expertise in systems,
security, formal verification, and programming languages. We are the creators
of seL4, the world's first operating system microkernel with a
machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance
and foundational binary-level correctness and security proofs. We are also
involved in CakeML, the most realistic verified compiler for a functional
programming language, and a promising approach to scaling full verification
up to applications code.

We are building on these successes in various directions, including
concurrency (formal reasoning and implementation), timing (real-time
guarantees and timing channels), and whole-system verification using
component systems (e.g., CAmKES) and code+proof co-generation.

We publish in top conferences, and are involved in multiple international
research collaborations. You will have the opportunity to teach at UNSW
should you wish to take it. We have a flexible, friendly, and intellectually
stimulating work environment.

We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.

The salary range for this position (plus superannuation) is
- Research Scientist: 97k-105k
- Senior Research Scientist: 111k-130k
depending on experience and qualifications.

Apply online here:
https://jobs.csiro.au/job/Sydney%2C-NSW-Research-ScientistSenior-Research-Scientist-in-Formal-Verification/518430100/

Your application should include a cover letter, CV, short research statement,
and contact information for two references.

This round of applications closes on 15 January 2019.

For any questions on this position, please contact
june.andron...@data61.csiro.au

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

[Hol-info] Proof Engineer jobs in Sydney

2018-11-18 Thread Michael.Norrish

Data61 Seeking Proof Engineers

==



We are are hiring again!



If only there were a place where I could prove theorems for money,

change the world, and have fun while doing it...



Sounds too good to exist?



In the Trustworthy Systems team at Data61 that's what we do for a

living. We are the creators of seL4, the world's first fully formally

verified operating system kernel with extreme performance and strong

security & correctness proofs. Our highly international team is located

on the UNSW campus, close to the beautiful beaches of sunny Sydney,

Australia, one of the world's most liveable cities.



We are looking for multiple motivated proof engineers who want to join

our team in Sydney, move things forward, and have global impact. You

would



  - work on industrial-scale formal proofs in Isabelle/HOL

  - develop formally verified infrastructure for building secure systems

on top of seL4

  - contribute to improved proof automation and reasoning techniques

  - apply formal proof to real-world systems and tools



To apply for this position, you should possess a significant subset of

the following skills.



  - functional programming in a language like Haskell, ML, or OCaml

  - first-order or higher-order formal logic

  - basic experience in C

  - ability and desire to quickly learn new techniques

  - undergraduate degree in Computer Science, Mathematics, or similar

  - ability and desire to work in a larger team



We are hiring at two levels, so if you are more qualified or

experienced than the above would suggest, you can come in as a senior

proof engineer.



If you additionally have experience



  - in software verification with an interactive theorem prover such as

Isabelle/HOL, HOL4, or Coq, and/or

  - with operating systems and microkernels



you should definitely apply!



If you have the right skills and background, we can provide training on

the job. Continual learning is a central component of everything we do.

You will work with a unique world-leading combination of OS and formal

methods experts, students at undergraduate and PhD level, engineers,

and researchers from 5 continents, speaking over 15 languages.

Trustworthy Systems is a fun, creative, and welcoming workplace with

flexible hours & work arrangements.



We value diversity in all forms and welcome applications from people of

all ages, including people with disabilities, and those who identify as

LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information.



Salary ranges, in AUD (plus superannuation):

- Junior Proof Engineer: 73k-93k

- Senior Proof Engineer: 97k-105k

depending on experience and qualifications.



Apply online at the following link for the Proof Engineer positions:

 - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/

 - https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/



Your application should include a cover letter, CV, undergraduate

transcript (if applicable), and contact information for two references.



This round of applications closes on 17 December 2018.



For any questions on these positions, please contact

rafal.kolan...@data61.csiro.au



The seL4 code and proof are open source. Check them out at https://seL4.systems



More information about Data61's Trustworthy Systems team at

https://ts.data61.csiro.au



There are additional proof engineering positions available on the

Cogent project. Cogent is a language we designed to ease the

verification of systems components around seL4. For expressions of

interest, see contact details on

https://ts.data61.csiro.au/projects/TS/cogent.pml



Looking to do a PhD?

Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships!

See https://ts.data61.csiro.au/students/research.pml for details.



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

Re: [Hol-info] excessive number of MLTEMP files

2018-11-13 Thread Michael.Norrish

Thanks for the bug report!  I’m about to push a commit that should fix this 
issue and keep /tmp clear.

Best wishes,
Michael

From: Gergely Buday 
Date: Wednesday, 14 November 2018 at 12:34
To: "hol-info@lists.sourceforge.net" 
Subject: [Hol-info] excessive number of MLTEMP files

Hi there,

coming from the Poly/ML list.

Running a CakeML bootstrapping process I got an error

 no space left on device

Actually, the disk was not full but consumed all possible inodes:

$ sudo df -i /
[sudo] password for gbuday:
Filesystem Inodes  IUsed IFree IUse% Mounted on
/dev/sda1  512064 512064 0  100% /

That was because of 361391 MLTEMP files in /tmp.

James Clarke said on the Poly/ML list that

> MLTEMP is the pattern used by Poly/ML for its temporary files when you 
> call

> OS.FileSys.tmpName: unit -> string. However, Poly/ML itself is not calling it 
> itself, nor is CakeML; it looks like HOL

> makes a lot of calls, so I would guess that Holmake is at fault (if that's 
> the step where you run out of space).

Can I tweak Holmake not to create that much temporary files or to periodically 
delete unnecessary ones?

Or, might it be that CakeML bootstrapping does require that much temporary 
files?

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

Re: [Hol-info] assumption matching in SPLIT_LT

2018-09-21 Thread Michael.Norrish

match_mp_tac is indeed causing an error because it is not applicable in the 
other subgoals.

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Friday, 21 September 2018 at 08:39
To: "konrad.sl...@gmail.com" 
Cc: hol-info 
Subject: Re: [Hol-info] assumption matching in SPLIT_LT

Hi,

Thanks for the reply. I think the match_mp_tac is causing the error since if I 
only pop the assumption the tactic works on first subgoal.

rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))

> val it =

   SG3

A1 ==> B1

   SG2

A1 ==> B1

   (A1 ==> B1) ==> B1

3 subgoals
   : proof

On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind 
mailto:konrad.sl...@gmail.com>> wrote:
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the 
first one is the pop_assum match_mp_tac succeeding. So the proof is failing 
before it gets to the THEN_LT.

Konrad.

On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info 
mailto:hol-info@lists.sourceforge.net>> wrote:
Hi,

I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm 
facing error with assumption matching. For instance, I've a proof goal of this 
form:

`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`

rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS 
(rw[]))

I'm getting following matching error...

Exception raised at Tactic.MATCH_MP_TAC:
No match
Exception-
   HOL_ERR
 {message = "No match", origin_function = "MATCH_MP_TAC",
  origin_structure = "Tactic"} raised

It works otherwise for handling them individually...
--
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/
___
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/
___
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

2018-09-21 Thread Michael.Norrish

As Thomas said, you are probably encountering this use of temporary files for 
the first time.  In particular, I suppose you may not have tried to cut and 
paste large regions of your script file in the past.  You could confirm that 
this is the problem by seeing if smaller regions of text do transfer to the HOL 
session successfully.

You might also edit the hol-mode file to change the constant on line 803 from 
500 to something larger.  It’s possible the need for this limit has entirely 
disappeared, but SML sessions within emacs-comint buffers have in the past 
failed to consume large inputs all at once.

Michael

From: Yassmeen Derhalli 
Date: Friday, 21 September 2018 at 08:11
To: Thomas Tuerk 
Cc: "hol-info@lists.sourceforge.net" 
Subject: Re: [Hol-info] Exception raised while using HOL in hol-mode

Hi,

thank you for your reply.

I am using an oracle virtual machine on my laptop running 
ubuntu-16.04.4-desktop-i386. I have been using this machine for about three 
months now, and I have not had any problem until yesterday.

Best Regards,

Yassmeen

On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk 
mailto:tho...@tuerk-brechen.de>> wrote:

Hi,

I believe this is due to how hol-mode copies input from emacs buffers to HOL. 
Look at HOL-DIR/tools/hol-mode.el line 802 ff. 
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800).
 If a chunk of text you want to send exceeds a certain size, it is written to a 
temp-file instead and "use tempfile" is send to HOL. I fear this is going wrong 
for some reason. hol-mode tries to write the chunk of text to the file 
"/tmp/hol2207zVM" and then sends "use "/tmp/hol2207zVM" to HOL. However, for 
some reason HOL cannot find this file. This results in the error message you 
posted.

How to fix it is a good question. I have seen this error before when working 
remotely with HOL. When using HOL via ssh or in some virtual environment like a 
docker container, I had the problem before that the communication with HOL 
worked just fine, but HOL and emacs saw different "/tmp" directories (e.g. the 
ones on the local and remote machine). Are you using anything like this? What 
environment are you running HOL in?

Best

Thomas





On 20.09.2018 17:40, Yassmeen Derhalli wrote:
Hi,

Sorry for sending this email again, but it seems that there was a problem with 
the first email


I am using HOL4, yesterday I started receiving this error message


Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"}

I am using HOL4 in the hol-mode, but when I use HOL directly using the shell, 
my script runs fine, this only happens in the hol-mode, any clue why this could 
happen and how can I fix it?

thanks






___

hol-info mailing 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] The "limit" of a ``:'num->'a set`` function?

2018-09-13 Thread Michael.Norrish

You don't just want something like

   BIGUNION (IMAGE f univ(:num))

?

Michael

On 14/9/18, 05:02, "Chun Tian (binghe)"  wrote:

Hi,

I want to express the existence of a function (f :’num -> ‘a set) such 
that, whenever the number n goes to “infinite”, ``f n`` equals to a given set 
``X :’a set``.

This looks like something in limTheory, but I have nothing to do with real 
numbers here.

Does anyone know which definition in HOL4’s existing libraries should I 
look for?

Regards,

Chun Tian





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

Re: [Hol-info] QuoteFilter with precise positions

2018-09-05 Thread Michael.Norrish

On 5/9/18, 23:14, "Makarius"  wrote:

On 28/08/18 03:00, michael.norr...@data61.csiro.au wrote:
>> 
>> - there is evidently a bug in the position information when the leading 
delimiter is a Unicode quote mark (the number of bytes gets counted rather than 
the number of "characters");

> With Unicode text it is inherently difficult to say how "characters" are
> counted, and thus to say what is right or wrong. Whatever you do is
> likely to be wrong in some sense.

> For internal counting, I would prefer the raw byte address, as we have
> it already in our fine SML strings that are undiluted by Unicode. It
> allows to access large text chunks quickly without recoding back and 
forth.

We have committed to UTF8 everywhere internally and expect to consume/produce 
that to/from files and streams, meaning that we don't need to do any recoding 
per se. This does mean that we are utterly incompatible with environments that 
are not UTF8, and have to occasionally take care not to break strings badly 
(String.substring can not be blindly applied to byte sequences that are 
"secretly" in UTF8 for example). 

> For external purposes, e.g. error messages with characters positions, it
> is hard to tell. It depends on the "consumers" that you have in mind: a
> Java front-end is likely to expect 16-bit Char addresses. Unix tools are
> likely to expect UTF-8 characters in the sense of codepoints. Nothing of
> this is smallest textual unit, if you allow official Unicode in its full
> complexity (but nobody has implemented that correctly anyway).

As I'm willing to ignore combining characters etc, my desired behaviour (not 
yet realised as above bug demonstrates) is to indeed take the "Unix" attitude 
of reporting codepoint offsets.

Michael

--
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] Partial Order for Set Supremum

2018-09-02 Thread Michael.Norrish

It looks to me as if the assumption

  !x y. P x /\ P y ==> x <= y

Is false for all sets with cardinality greater than 1.  (If <= is over the 
reals, and P encodes a set with more than one element, then one or other will 
be strictly less than the other.  Then, it’s easy to specialise the above with 
x and y to be those two elements and have the assumption reduce to F.)

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 1 September 2018 at 09:31
To: hol-info 
Subject: [Hol-info] Partial Order for Set Supremum

Hi,

Lately, I proved the equivalence of two supremum functions as:

|- !P.
  (!x y. P x /\ P y ==> x <= y) /\ P <> {} ==>
  (BIGSUP $<= P P = SOME (sup P)): thm

where BIGSUP is defined in [1] and "sup" can be found in HOL realTheory.

I'm not sure why the premise (!x y. P x /\ P y ==> x <= y) is required mainly 
due to the fact that the binary relation $<= implicitly maintains the partial 
order in a set. This can be easily proved for any set:

rest_WeakOrder_le;
val it = |- !P. rest_WeakOrder P $<=: thm

Is there any way to discharge the first premise or can be inferred from the 
lemma "rest_WeakOrder_le"?

[1] 
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/examples/separationLogic/src/latticeScript.sml)

latticeTheory.BIGSUP_def;
val it = |- !f D M. BIGSUP f D M = OPTION_SELECT (\s. IS_SUPREMUM f D M s):
   thm





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

Re: [Hol-info] Reference cells in HOL4

2018-08-30 Thread Michael.Norrish

I'd be happy to see (1) made as a pull request.  (Doing it this way gets the 
Travis CI to automatically check it (at least to some extent).)

I agree that (2) is a useful distinction to make. 

Michael



On 30/8/18, 23:27, "Fabian Immler"  wrote:

Dear HOL4 Developers,

In a recent thread on this list, Makarius mentioned experiments to load 
HOL4 in the Isabelle Prover IDE. I participate in such experiments to 
load HOL4 with Isabelle/HOL as kernel.

Anyhow, some of the main obstructions concern references (type 'a ref in 
SML).

1) In a couple of places, the HOL4 code uses ref matching (i.e., ref is 
used as a pseudo constructor that dereferences the cell).
Would you mind converting those to explicit dereference operations? E.g. 
according to (or pulling) changeset [1]?

Such a change would make it easier to abstract over the concrete 
implementation of reference cells.


2) It seems like type 'a ref is used with (at least) two different 
intended meanings: one, to track global state variables and two, for 
private program variables.

It seems like Isabelle/ML's module for thread-local data (that you 
recently incorporated [2]) could be used for the first (global) meaning, 
and 'a ref could be retained for private variables.

Would you support distinguishing those different usages in one way or 
another?

Best regards,
Fabian

[1] https://github.com/immler/HOL/commit/b3ae0ef
[2] 

https://github.com/HOL-Theorem-Prover/HOL/blob/1e8573d/src/portableML/poly/fromIsabelle/thread_data.ML


--
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] Failure with REWRITE_TAC and UNDISCH on conjunctions

2018-08-28 Thread Michael.Norrish

Make the assumption the left-hand-side of an implication (moving it out of the 
assumptions), rewrite with the identity that says that

  ((P /\ Q) ==> R) <=> (P ==> (Q ==> R))

and then move all the implications’ left-hand-sides back into the assumptions.

In HOL4 you could use something like

  th |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> UNDISCH_ALL

The use of the _ALL functions makes this a bit fragile, but it will work in 
your case.

You might also find that the discharged theorem works directly as a conditional 
rewrite (I don’t know what the HOL Light tools is for this).

My HOL4-informed advice would be to avoid working with theorems that have 
assumptions like this: the machinery copes better with theorems that are just 
implications.  (Of course, goals can have assumptions and the machinery copes 
very well with those, but that is a different matter.)

Michael

From: Dylan Melville 
Date: Tuesday, 28 August 2018 at 22:48
To: "Norrish, Michael (Data61, Acton)" , 
"hol-info@lists.sourceforge.net" 
Subject: Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

That's what I figured. How can I separate the assumptions of 
second_b13_complete?

On Mon, Aug 27, 2018, 10:32 PM 
mailto:michael.norr...@data61.csiro.au>> wrote:
The assumption of the rewrite theorem is not present in the assumptions of the 
goal and so you get an invalid tactic.

Strictly speaking this is not REWRITE_TAC failing but e.   Indeed, you should 
find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine.

Michael

From: Dylan Melville mailto:dylanmelvi...@gmail.com>>
Date: Tuesday, 28 August 2018 at 11:45
To: "hol-info@lists.sourceforge.net" 
mailto:hol-info@lists.sourceforge.net>>
Subject: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

VERSION: HOL Light QE (augmentation of HOL Light, very similar)

Hello all. Today I’ve been having 2 issues with HOL. The first is that although 
the documentation for REWRITE_TAC says that the tactic has no failure 
conditions, when I use the following command:

# e (REWRITE_TAC[second_b13_complete]);;

Where second_b13_complete is:

# second_b13_complete;;
val it : thm =
  isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\
  ~isFreeIn (QuoVar "n" (TyBase "num")) f
  |- (\n. (\P. P n) (eval (f) to (num->bool))) =
 (\P n. P n) (eval (f) to (num->bool))

When used with the following goal already declared:

# p();;
val it : goalstack = 1 subgoal (1 total)

  0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`]
  1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`]
  2 [`isPeano f`]

`(eval (f) to (num->bool)) 0 /\
 (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool)))
 ==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))`

Results in the following error:

# e (REWRITE_TAC[first_b13_complete]);;
Exception: Failure "VALID: Invalid tactic”.

Which is confusing, since not only is the tactic supposed to have no failure 
conditions, but the bolded sections of the theorem and the goal are matched 
properly, and the two conjuncted antecedents of the theorem are assumptions 0 
and 1 of the goal. So, is the reason that the tactic application fails that 
antecedents of the theorem are conjuncted? If so, is there a command I’m 
missing that can transform the theorem to the proper form?

Thanks in advance.

Dylan Melville | McMaster University, Math and Computer Science
--
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] Lazy list: Stream in coinduction

Don’t use abbreviations before starting your proof: it’s muddling your 
quantifications.
Instead, use
   !s.  (?s0. s = StreamD s0) /\ P s ==> streams A s
as your goal and follow with
   ho_match_mp_tac streams_coind >> dsimp[]
You will then end up with

   ∀s0.
   P (StreamD s0) ⇒
   ∃a s0'. (StreamD s0 = a:::StreamD s0') ∧ a ∈ A ∧ P (StreamD s0')
as your goal.
Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 28 August 2018 at 13:53
To: hol-info 
Subject: [Hol-info] Lazy list: Stream in coinduction

Hi,

I see that the coinduction scheme obtained from coinductively definition 
predicate, in some cases, may require lazy list must not be LNIL. For instance,
using the LUNFOLD, I've defined the stream function mainly to rule out the LNIL 
case as:

|- StreamD xs = LUNFOLD (\n. SOME (THE (LTL n),THE (LHD n))) xs: thm

However, when I use it to for proving some useful properties over streams, 
which is defined coinductively as:

|- !A a s. a IN A /\ streams A s ==> streams A (a:::s): thm

and the resulting coinductive scheme produced is:

|- !A streams'.
  (!a0. streams' a0 ==> ?a s. (a0 = a:::s) /\ a IN A /\ streams' s) ==>
  !a0. streams' a0 ==> streams A a0: thm

Suppose, I've a property of form:

`P (StreamD s) ==> streams A (StreamD s)`

By abbreviating the 'xs = StreamD s', I applied the coinduction scheme and ends 
up:

?a xs'. (xs = a:::xs') /\ a IN A /\ Abbrev (xs' = xs) /\ P xs'
   
 0.  Abbrev (xs = StreamD s)
 1.  P xs

The first conjunction can be easily made true by using `LHD xs` and `LTL xs`. 
This also require that the lazy list 'xs' should not be LNIL, which can also be 
easily inferred (from premise 0). However, this makes Abbrev (LTL xs =  xs) 
false..

Is there any way that I can use the coinduction scheme directly such that I can 
have

   ∃a xs'. (StreamD xs = a:::xs') ∧ a ∈ A ∧ P xs'
   
 0.  P xs








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

Re: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

The assumption of the rewrite theorem is not present in the assumptions of the 
goal and so you get an invalid tactic.

Strictly speaking this is not REWRITE_TAC failing but e.   Indeed, you should 
find that REWRITE_TAC [second_b13_complete] applied to the goal works just fine.

Michael

From: Dylan Melville 
Date: Tuesday, 28 August 2018 at 11:45
To: "hol-info@lists.sourceforge.net" 
Subject: [Hol-info] Failure with REWRITE_TAC and UNDISCH on conjunctions

VERSION: HOL Light QE (augmentation of HOL Light, very similar)

Hello all. Today I’ve been having 2 issues with HOL. The first is that although 
the documentation for REWRITE_TAC says that the tactic has no failure 
conditions, when I use the following command:

# e (REWRITE_TAC[second_b13_complete]);;

Where second_b13_complete is:

# second_b13_complete;;
val it : thm =
  isExprType f (TyBiCons "fun" (TyBase "num") (TyBase "bool")) /\
  ~isFreeIn (QuoVar "n" (TyBase "num")) f
  |- (\n. (\P. P n) (eval (f) to (num->bool))) =
 (\P n. P n) (eval (f) to (num->bool))

When used with the following goal already declared:

# p();;
val it : goalstack = 1 subgoal (1 total)

  0 [`isExprType f (TyBiCons "fun" (TyVar "num") (TyBase "bool"))`]
  1 [`~isFreeIn (QuoVar "n" (TyBase "num")) f`]
  2 [`isPeano f`]

`(eval (f) to (num->bool)) 0 /\
 (\P. P = (\x. T)) (\n. (\P. P n ==> P (SUC n)) (eval (f) to (num->bool)))
 ==> (\P. P = (\x. T)) (\n. (\P. P n) (eval (f) to (num->bool)))`

Results in the following error:

# e (REWRITE_TAC[first_b13_complete]);;
Exception: Failure "VALID: Invalid tactic”.

Which is confusing, since not only is the tactic supposed to have no failure 
conditions, but the bolded sections of the theorem and the goal are matched 
properly, and the two conjuncted antecedents of the theorem are assumptions 0 
and 1 of the goal. So, is the reason that the tactic application fails that 
antecedents of the theorem are conjuncted? If so, is there a command I’m 
missing that can transform the theorem to the proper form?

Thanks in advance.

Dylan Melville | McMaster University, Math and Computer Science
--
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] QuoteFilter with precise positions

Two minor followups:

- there is evidently a bug in the position information when the leading 
delimiter is a Unicode quote mark (the number of bytes gets counted rather than 
the number of "characters");
- the unquote filter is built by the process of "configuring" the system before 
building; actually building the whole system (with the "build" executable) is 
not necessary if all you want to do is to play around with the unquote filter. 

Michael

On 28/8/18, 09:33, "Norrish, Michael (Data61, Acton)" 
 wrote:

The quotation filter doesn't really do any tokenization other than to spot 
occurrences of the magic term and quotation delimiters: 

  ` .. ` (a quotation)
  ‘ .. ’ (also a quotation, but with non-identical delimiters)
  ``:ty``  (an application of the type parser to a quotation)
  “:ty”(  ditto )
  ``term`` (an application of the term parser to a quotation)
  “term”   (  ditto )

The quotations produced by the filter get "pre-loaded" with line number 
information.  With HOL built you can see it all in action by running the 
unquote program (built in HOL/bin) as a standard Unix filter.  If file contains

 
foo bar
`foo bar`
“term p ∨ q”;

then the output of 

unquote < file

will be 

foo bar
[QUOTE " (*#loc 2 2*)foo bar"]
(Parse.Term [QUOTE " (*#loc 3 4*)term p \226\136\168 q"]);

You can see that it also converts the UTF8 character into something that is 
a valid string. 

Tokenization builds off the location information presented in the #loc 
comments.

Michael

On 28/8/18, 07:41, "Makarius"  wrote:

Dear experts on antiquotations HOL4,

I've looked through tools/Holmake/QuoteFilter, but could not read the
input format -- I am used to functional parser combinators instead of
lex + yacc.

Is there a specification of the input syntax in the documentation? But
it is also changing occasionally, so it might be better to re-use the
existing implementation.

Ultimately I want to turn HOL4 ML source into tokens with precise source
positions, e.g. byte addresses of the original string.

The idea is to continue some experiments with HOL4 inside the Isabelle
Prover IDE, see also https://sketis.net/2015/hol4-workshop-at-cade-25


Makarius


--
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] QuoteFilter with precise positions

The quotation filter doesn't really do any tokenization other than to spot 
occurrences of the magic term and quotation delimiters: 

  ` .. ` (a quotation)
  ‘ .. ’ (also a quotation, but with non-identical delimiters)
  ``:ty``  (an application of the type parser to a quotation)
  “:ty”(  ditto )
  ``term`` (an application of the term parser to a quotation)
  “term”   (  ditto )

The quotations produced by the filter get "pre-loaded" with line number 
information.  With HOL built you can see it all in action by running the 
unquote program (built in HOL/bin) as a standard Unix filter.  If file contains

 
foo bar
`foo bar`
“term p ∨ q”;

then the output of 

unquote < file

will be 

foo bar
[QUOTE " (*#loc 2 2*)foo bar"]
(Parse.Term [QUOTE " (*#loc 3 4*)term p \226\136\168 q"]);

You can see that it also converts the UTF8 character into something that is a 
valid string. 

Tokenization builds off the location information presented in the #loc comments.

Michael

On 28/8/18, 07:41, "Makarius"  wrote:

Dear experts on antiquotations HOL4,

I've looked through tools/Holmake/QuoteFilter, but could not read the
input format -- I am used to functional parser combinators instead of
lex + yacc.

Is there a specification of the input syntax in the documentation? But
it is also changing occasionally, so it might be better to re-use the
existing implementation.

Ultimately I want to turn HOL4 ML source into tokens with precise source
positions, e.g. byte addresses of the original string.

The idea is to continue some experiments with HOL4 inside the Isabelle
Prover IDE, see also https://sketis.net/2015/hol4-workshop-at-cade-25


Makarius


--
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] Assumptions of goal usage

2018-08-20 Thread Michael.Norrish

Yes.  Use tactics like drule, dxrule and others in this family.   See

  
https://hol-theorem-prover.org/kananaskis-12-helpdocs/help/Docfiles/HTML/Tactic.drule.html

Alternatively, write in a declarative style:

   `e` by metis_tac[th] >>
   `f` by metis_tac[] >>

Michael

From: Dylan Melville 
Date: Tuesday, 21 August 2018 at 06:57
To: "hol-info@lists.sourceforge.net" 
Subject: Re: [Hol-info] Assumptions of goal usage

As a more concise question: can you use assumptions of the hypothesis to 
eliminate the assumptions of a theorem?

On Mon, Aug 20, 2018, 4:51 PM Dylan Melville 
mailto:dylanmelvi...@gmail.com>> wrote:
Let's say I have a goal,

a /\ b /\ c ==> d

and 2 theorems

a /\ b ==> e

e ==> f

All I need to do to solve the goal is rewrite using a theorem that states `f`, 
however I need to first prove e, which is only probable because the goal 
assumes `a`.

The basis of my question, is whether or not I can use an assumption of the goal 
outside of a tactical. My proof would be a lot more readable if I could use `a` 
and `b` to "prove" `e` outside of a tactical application like ASSUM_LIST and 
similar tactics require.
--
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 Assumptions

2018-08-16 Thread Michael.Norrish

Mario is right if you are happy to write the whole assumption out (as he 
describes), or if you have your hands on the relevant term some other way.

If you also want the benefit of parsing a string into a term in the context of 
the current goal, you might also want to try 

  QTY_TAC bool (mythtactic o ASSUME) `assumption`

where mythtactic is a continuation/thm_tactic such as mp_tac, strip_assume_tac, 
drule. 

By using this version, you can write the assumption between single quotations, 
and hopefully not need to write quite so many type annotations.

If you want to remove the assumption and work on it with mythtactic, then use 

  Q.UNDISCH_THEN `assumption` mythtactic

There's probably an argument for defining the first form above, perhaps as 
Q.ASSUME_THEN, so that you could write

  Q.ASSUME_THEN `assumption` mythtactic

Michael

On 17/8/18, 05:20, "Mario Xerxes Castelán Castro"  
wrote:

In HOL4 you can use the “ASSUME” primitive inference rule, passing the
same term as it appears in the hypotheses (up to α-conversion). Make
sure that the types of the constants are the same, for otherwise this
will fail (it will be either detected and an exception is raised or a
theorem is produced where the assumption was not eliminated).

On 16/08/18 11:07, Dylan Melville wrote:
> Is there anyway to reference a specific assumption of the current goal as 
a theorem?
> 
--
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] PhD opportunities at the ANU

2018-08-08 Thread Michael.Norrish

++

The Logic and Computation Group at the Research School of Computer
Science, The Australian National University has a number of PhD
scholarship available for bright, enthusiastic doctoral students in
the following subjects:

- Logic and Linguistics (Ekaterina Lebedeva)
- Logic in Computer Science (Ranald Clouston, Rajeev Gore, Dirk Pattinson, 
Alwen Tiu)
- Non-Classical Logics (Ranald Clouston, Rajeev Gore, John Slaney, Dirk 
Pattinson)
- Proof Theory (Rajeev Gore, Dirk Pattinson, Alwen Tiu)
- Automated Reasoning (Rajeev Gore)
- Probabilistic Reasoning (Peter Baumgartner)
- Computer Aided Verification (Sergiy Bogomolov, Michael Norrish, Dirk 
Pattinson)
- Interactive Theorem Proving (Michael Norrish, Dirk Pattinson)
- Computer Security Foundations (Alwen Tiu)
- Concurrency Theory (Alwen Tiu)
- Electronic Voting and Social Choice Theory (Rajeev Gore, Dirk Pattinson)
- Semantics Of Programming Languages (Ranald Clouston, Dirk Pattinson)
- Type Theory (Ranald Clouston)

Potential applicants are encouraged to consult the group’s web pages
at https://cecs.anu.edu.au/research/theory/logic/ and make direct
contact with potential supervisors.

Students will be based at the Research School of Computer Science
within the Australian National University. The studentship is a
tax-free allowance of A$ 27,082 (2018 rate) per year, tenable for a
maximum of 3.5 years.

Applications are to be submitted electronically at
http://applyonline.anu.edu.au/ before the closing date, August 31,
2018. Further information about graduate research within Computer
Science at ANU, please see

 https://cs.anu.edu.au/study/graduate-research .

The scholarships are open to individuals of any nationality. We are
based in Canberra, Australia, the top-ranking region of the 2014 OECD
quality of life survey
(http://www.canberra.com.au/canberra-the-worlds-most-liveable-city/).

The ANU actively seeks to promote diversity in the workplace.

++

--
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] Partial Function on lazy list

2018-08-08 Thread Michael.Norrish

The function is already ready for use with any P; the final until_thm looks like

val until_thm =
   ⊢ (until P [||] = [||]) ∧
 (until P (h:::t) = if P h then [|h|] else h:::until P t): thm

meaning that one can write things like

  until (\x. x MOD 3 = 0) ll

for example.  This seems like a suitably polymorphic function.

To tweak it to put your example element Q into the list instead of the actual 
elements, change the core definition to also refer to Q. You will then need to 
generalise Q as well as P, and to then skolemize twice.

Incidentally, Q is a bad name for an element; it looks too much like a name for 
a predicate.  You should use a name like ‘e’ instead.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Thursday, 9 August 2018 at 06:08
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] Partial Function on lazy list

Hi,

Great!. This really helps alot...:) However, I may be interested in defining it 
for [\forall P]  so that I don't need to instantiate every time with a specific 
instance of P.  I tried this by myself but every time I lost in connecting my 
definition in llist form to its corresponding option theory form...:( Also, 
what change should be made if I change my definition a little

val recur_llist_fn1_def = Define
`recur_llist_fn1 P Q w =
 if (w = [||]) then [||]
  else if P (THE (LHD w)) then
  THE (LHD w) ::: (recur_llist_fn1 P Q (THE (LTL w)))
   else Q:::(recur_llist_fn1 P Q (THE (LTL w)))`;

Any suggestions or thoughts?




On Mon, Aug 6, 2018 at 8:52 PM 
mailto:michael.norr...@data61.csiro.au>> wrote:
You need to define a helper function that has as its state not only the llist 
that is being consumed but also a Boolean indicating whether or not to stop 
(because a P-satisfying element has been seen).

- -
val until0_def =
new_specification ("until0_def", ["until0"],
  ISPEC ``λbll. if FST bll then NONE
else if SND bll = [||] then NONE
else if P (THE (LHD (SND bll))) then
  SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND bll)))``
llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV SKOLEM_THM));

val until0_T =
until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []

val until0_FCONS =
  until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss()) []
 |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
 |> SIMP_RULE bool_ss [Once COND_RATOR]
 |> SIMP_RULE (srw_ss()) [until0_T]

val until0_FNIL =
  until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []

val until_def = Define‘until P ll = until0 P (F, ll)’

val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
   [until0_FNIL, until0_FCONS])
- -

Michael



From: Waqar Ahmad via hol-info 
mailto:hol-info@lists.sourceforge.net>>
Reply-To: Waqar Ahmad 
<12phdwah...@seecs.edu.pk>
Date: Tuesday, 7 August 2018 at 03:26
To: hol-info 
mailto:hol-info@lists.sourceforge.net>>
Subject: [Hol-info] Partial Function on lazy list

Hi all,

Is there any easy way to define the following partial function on lazy list

val recur_llist_fn_def = Define
`recur_llist_fn P w =
 if P (THE (LHD w)) then [|THE (LHD w)|]
 else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;

Otherwise, I can also include the LNIL case as

val recur_llist_fn_def = Define
`recur_llist_fn P w = if (w = [||]) then [||] else
 if P (THE (LHD w)) then [|THE (LHD w)|]
 else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;

but I'm having issue to write its corresponding axiomatic form for

llist_Axiom_1:

!f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a

Particularly for  P (THE (LHD w)) what will be SOME (?)

Any suggestion or thoughts?

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

Re: [Hol-info] Partial Function on lazy list

2018-08-06 Thread Michael.Norrish

You need to define a helper function that has as its state not only the llist 
that is being consumed but also a Boolean indicating whether or not to stop 
(because a P-satisfying element has been seen).

- - 
val until0_def =
new_specification ("until0_def", ["until0"],
  ISPEC ``λbll. if FST bll then NONE
else if SND bll = [||] then NONE
else if P (THE (LHD (SND bll))) then
  SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND bll)))``
llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV SKOLEM_THM));

val until0_T =
until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []

val until0_FCONS =
  until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss()) []
 |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
 |> SIMP_RULE bool_ss [Once COND_RATOR]
 |> SIMP_RULE (srw_ss()) [until0_T]

val until0_FNIL =
  until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []

val until_def = Define‘until P ll = until0 P (F, ll)’

val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
   [until0_FNIL, until0_FCONS])
- - 

Michael 



From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 7 August 2018 at 03:26
To: hol-info 
Subject: [Hol-info] Partial Function on lazy list

Hi all, 

Is there any easy way to define the following partial function on lazy list

val recur_llist_fn_def = Define
`recur_llist_fn P w =
 if P (THE (LHD w)) then [|THE (LHD w)|]
 else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;

Otherwise, I can also include the LNIL case as

val recur_llist_fn_def = Define
`recur_llist_fn P w = if (w = [||]) then [||] else
 if P (THE (LHD w)) then [|THE (LHD w)|]
 else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;

but I'm having issue to write its corresponding axiomatic form for 

llist_Axiom_1:

!f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a

Particularly for  P (THE (LHD w)) what will be SOME (?)

Any suggestion or thoughts? 

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

Re: [Hol-info] Undefined references building “description.pdf”

2018-07-29 Thread Michael.Norrish

Thanks for the bug report.

The error is due to this:

! pdfTeX error (font expansion): auto expansion is only possible with scalable
fonts.
\AtBegShi@Output ...ipout \box \AtBeginShipoutBox
\fi \fi

I will try to look into what is going on at this point in the file to see if
there is something obviously wrong in our LaTeX sources. This error doesn't
manifest on my setup, but that's not necessarily an excuse :)

Re: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12

2018-07-03 Thread Michael.Norrish

This looks like a regression.

Can you turn this into an issue on github please?

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 3 July 2018 at 01:41
To: hol-info 
Subject: [Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12

Hi all,

I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12

Consider a proof goal

``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)``

e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV));

(* In HOL-k10, the tactic results a desired behavior*)

?!m. ((m = n) \/ m < n) /\ (~(m < n) \/ (f m = x)) /\ (m < n \/ (a = x))

(* In HOL-k12, the tactic results *)

?!m. ((m = n) \/ m < n) /\ (if m < n then $= (f m) else $= a) x

Am I missing something?


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

[Hol-info] Kananaskis-12 release of HOL4

2018-06-19 Thread Michael.Norrish

Release notes for HOL4, Kananaskis-12
=

(Released: 20 June 2018)

We are pleased to announce the Kananaskis-12 release of HOL 4.

We would like to dedicate this release to the memory of Mike Gordon
(1948–2017), HOL’s first developer and the leader of the research group
to which many of us were attached at various stages of our careers.

The official download tarball for this release is available from 
[Sourceforge](https://sourceforge.net/projects/hol/files/hol/kananaskis-12/hol-kananaskis-12.tar.gz/download)
 and 
[Github](https://github.com/HOL-Theorem-Prover/HOL/releases/download/kananaskis-12/hol-kananaskis-12.tar.gz),
 with `shasum` equal to 8d4754f11411c15501a23c218c0fe5561607de6c.

New features:
-

-   `Holmake` under Poly/ML (*i.e.*, for the moment only Unix-like
systems (including OSX/MacOS, and Windows with Cygwin or the
Linux subsystem)) now runs build scripts concurrently when targets
do not depend on each other. The degree of parallelisation depends
on the `-j` flag, and is set to 4 by default. Output from the build
processes is logged into a `.hollogs` sub-directory rather than
interleaved randomly to standard out.

-   Theory files generated from script files now load faster. The
machinery enabling this generates `xTheory.dat` files alongside
`xTheory.sig` and `xTheory.sml` files. Thanks to Thibault Gauthier
for the work implementing this.

-   We now support monadic syntax with a `do`-notation inspired by
Haskell’s. For example, the `mapM` function might be defined:

   Define‘(mapM f [] = return []) ∧
  (mapM f (x::xs) =
 do
   y <- f x;
   ys <- mapM f xs;
   return (y::ys);
 od)’;

The HOL type system cannot support this definition in its full
polymorphic generality. In particular, the above definition will
actually be made with respect to a specific monad instance (list,
option, state, reader, *etc*). There are API entry-points for
declaring and enabling monads in the `monadsyntax` module. For more
details see the *DESCRIPTION* manual.

-   Users can define their own colours for printing types, and free and
bound variables when printing to ANSI terminals by using the
`PPBackEnd.ansi_terminal` backend. (The default behaviour on what is
called the `vt100_terminal` is to have free variables blue, bound
variables green, type variables purple and type operators
“blue-green”.) Thanks to Adam Nelson for this feature. Configuring
colours under `emacs` is done within `emacs` by configuring faces
such as `hol-bound-variable`.

-   We now support the infix `$` notation for function application from
Haskell. For example

   f $ g x $ h y

is a low-parenthesis way of writing `f (g x (h y))`. The
dollar-operator is a low-precedence (tighter than infix `,` but
looser than other standard operators), right-associative infix. This
is a “parse-only technology”; the pretty-printer will always use the
“traditional” syntax with parentheses as necessary and what might be
viewed as an invisible infix application operator.

Bugs fixed:
---

-   Pretty-printing of record type declarations to TeX now works even if
there are multiple types with the same name (necessarily from
different theory segments) in the overall theory.

-   Pretty-printing has changed to better mesh with Poly/ML’s native
printing, meaning that HOL values embedded in other values (*e.g.*,
lists, records) should print better.

New theories:
-

-   We have promoted the theories of cardinality results for various
flavours of infinite sets, and of ordinal numbers to `src` from
`examples`. There is a minor backwards-incompatibility: references
to `examples/set-theory/hol_sets` (in Holmakefile `INCLUDES`
specifications for example) should simply be deleted. Any theory can
build on these theories (`cardinalTheory`, `ordinalTheory`) simply
by `open`-ing them in the relevant script file.

New tools:
--

-   For every algebraic type, the `TypeBase` now automatically proves
what we term “case-equality” rewrite theorems that have LHSes of the
form

  ((case x of con1_pattern => e1 | con2_pattern => e2 ...) = v)

For example, the case-equality theorem for the `α option` type is

  (option_CASE opt nc sc = v) ⇔
 (opt = NONE) ∧ (nc = v) ∨
 ∃x. (opt = SOME x) ∧ (sc x = v)

where `option_CASE opt nc sc` is the general form of the term that
underlies a case expression over an option value `opt`.

These theorems can be powerful aids in simplifications (imagine for
example that `v` is `T` and `nc` is `F`), so we have made it easy to
include them in arguments to `simp`, `fs`, `rw` *etc*. The `CaseEq`

Re: [Hol-info] big records

2018-06-06 Thread Michael.Norrish

If you understand what the package is doing (and I admit that this is not 
easy), then the behaviour of the simplifier on big records is in turn fairly 
understandable.

The advantage of the package is not suffering a quadratic blow-up in elapsed 
time and theorem sizes (in turn leading to quadratic theory sizes and similar 
time in loading said theories) when defining the record type. The simplifier’s 
normalisation of record expressions is also an implementation of bubble sort, 
so there are conceivably simplification scenarios which might exhibit quadratic 
time costs.

All that said, I think that there’s probably a strong case for simply forcing 
users to suffer (perhaps with warning messages), and encouraging them to define 
nested records themselves to group related fields of their super-large records. 
 They would thus be manually doing what the big record package is doing not 
quite invisibly.

Pull requests gratefully accepted.

Michael

From: Ramana Kumar 
Date: Wednesday, 6 June 2018 at 19:18
To: hol-info 
Subject: [Hol-info] big records

Dear HOL users,

Does anyone know how to use the big record package? I always find I want to 
turn it off (by increasing the big record size to above the max number of 
fields in my types) because many things don't work on big records (in 
particular the simplifier and EVAL) whereas they do work on "small" records.

Would it be OK to disable the big record package by default (e.g., set the size 
limit to "infinity" by default)? Or would it be easy to make the above tooling 
work for big records too? What are the advantages of big records anyway?

Cheers,
Ramana
--
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] On equivalence of two definitions of PERMUTES

2018-05-28 Thread Michael.Norrish

The two definitions are not equivalent.  The BIJ overload permits functions to 
be designated permutations that the definition does not. BIJ can be used to 
identify bijections between different types so it can't/shouldn't require 
anything much of functions outside their domain.  I think one's choice of 
definition will depend on the sort of theorems one wants to prove.  In 
particular, the definition approach only lets one function serve as a 
particular permutation. The BIJ-overload approach will let many functions be 
the "same" permutation.

Michael

On 28/5/18, 19:01, "Chun Tian"  wrote:

Hi,

(I’m trying to convert the current pending PR into acceptable code changes)

in pred_setTheory, I saw there’s a definition of PERMUTES (permutation 
functions over a set) as overloading of BIJ (bijections):

val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``);
val _ = set_fixity "PERMUTES" (Infix(NONASSOC, 450)); (* same as relation *)

val SUM_IMAGE_PERMUTES = store_thm(
  "SUM_IMAGE_PERMUTES",
  ``!s. FINITE s ==> !g. g PERMUTES s ==> !f. SIGMA (f o g) s = SIGMA f s``,
  …);

this definition seems clear: a function is a permutation over a set if it’s 
a bijection from the set to itself.  But let’s recall HOL is a logic of total 
functions, and what about the value of this permutation function over values 
NOT in the set? Does above definition automatically indicate ``f(x) = x`` for 
all elements not in the set?

On the other side, I saw the following (possible) alternative definition: 
(in that pending PR)

PERMUTES p s = (!x. ~(x IN s) ==> (p(x) = x)) /\ (!y. ?!x. p x = y)

it explicitly states that, for all values not in the set s, a permutation 
function acts like identity function; and it must be a total bijection (c.f. 
BIJ_ALT in pred_setTheory).

Are these two definitions really equivalent?

Regards,

Chun





--
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] Reverse Function on LazyLists

2018-05-23 Thread Michael.Norrish

As reverse on llist only really works when the argument is finite, the easiest 
definition would be

  Lrev ll = fromList (REVERSE (toList ll))

You could lift this to infinite lists by having

  ~LFINITE ll ==> (Lrev ll = infinite-list-of something)

Or similar.  As it happens, I believe such a definition then satisfies your 
desired characterisation.

One f you could instantiate the axiom with to get this effect would be

  f ll = if LFINITE ll then if ll = [||] then NONE else SOME (fromList (FRONT 
(toList ll)), LAST (toList ll))
  else SOME (ll, ARB)

Your characterisation should follow from a bisimulation argument.

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 23 May 2018 at 15:21
To: hol-info 
Subject: [Hol-info] Reverse Function on LazyLists

Hi,

Lately, I've been trying to define the "reverse" function on lazy lists but I'm 
facing some issues. I understand that, unlike lists, in order to define 
recursive function over lazy lists every time I need to justify the definition 
of (co-)recursive functions (reverse in my case) that map into the llist type 
using

llist_Axiom;
val it =
   |- !f.
 ?g.
   (!x. LHD (g x) = OPTION_MAP SND (f x)) /\
   !x. LTL (g x) = OPTION_MAP (g o FST) (f x):
   thm

So I'm trying to prove the following reverse function definition over llist type

`?reverse.
 ( reverse ([||]) = LNIL) /\
 (!x xs.  reverse (LCONS x xs) = LAPPEND ( reverse xs) [|x|])`

but could not find the appropriate instance of "f" in llist_Axiom to prove both 
the base and the inductive cases...

Any suggestion or comments?

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

Re: [Hol-info] HOL 4 Kananaskis 11 Installation Problem

2018-05-22 Thread Michael.Norrish

Subscript is the standard exception raised if you attempt to do things like 

  List.nth([1,2,3], 3)

or 

  String.sub("foo bar", 9)

I guess that Holmake is trying to do one of the above sorts of things. 

What happens if you move the Holmakefile in tools/set_mtime out of the way and 
call 

  Holmake --poly_not_hol --no_sigobj --qof

in that directory?

Michael
 

On 23/5/18, 07:53, "Chun Tian"  wrote:

I’m not 100% sure, but the keyword “Subscript” seems related to X11 
bindings. I guess you must have enabled X11 when building Poly/ML. If so, you 
can try to rebuild Poly/ML without X11 and try to build latest HOL again. Hope 
this helps,

—Chun

> Il giorno 22 mag 2018, alle ore 22:51, Ashish Darbari 
 ha scritto:
> 
> Hi Chun
> 
> You may have a point, not sure about Poly ML woes...I was able to move a 
bit further by cloning the latest HOL distro.
> 
> I get the configuration done now but as soon as I start the build I get a 
Subscript error.
> 
> [adarbari@localhost HOL]$ bin/build
> *** Using kernel spec --stdknl from earlier build command;
> use one of --expk, --stdknl, --otknl to override
> Cleaning out /home/adarbari/HOL/sigobj
> /home/adarbari/HOL/sigobj cleaned
> Building directory tools/set_mtime [22 May, 22:24:34]
> Holmake failed with exception: Subscript
> Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with 
code 1)
> [adarbari@localhost HOL]$
> 
> Detailed log:
> 
> [adarbari@localhost HOL]$  poly < tools-poly/smart-configure.sml
> Poly/ML 5.7.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/adarbari/HOL
> DOT_PATH:   NONE
> MLTON:  NONE
> 
> 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.
> Removing old quotation filter from bin/
> Making mllex
> Making mlyacc
> 
> Number of states = 95
> Number of distinct rows = 47
> Approx. memory size of trans. table = 6063 bytes
> Making Holmake
> 
> Number of states = 1020
> Number of distinct rows = 847
> Approx. memory size of trans. table = 1734656 bytes
> Making unquote.
> Making holdeptool
> Making build
> Making heapname
> Making buildheap
> Making genscriptdep
> Making hol-mode.el (for Emacs/XEmacs)
> Making tools/vim/*
> Generating bin/hol.
> 
> Finished configuration!
> [adarbari@localhost HOL]$ bin/build
> *** Using kernel spec --stdknl from earlier build command;
> use one of --expk, --stdknl, --otknl to override
> Cleaning out /home/adarbari/HOL/sigobj
> /home/adarbari/HOL/sigobj cleaned
> Building directory tools/set_mtime [22 May, 22:24:34]
> Holmake failed with exception: Subscript
> Build failed in directory /home/adarbari/HOL/tools/set_mtime (exited with 
code 1)
> 
> 
> 
> --
> 
> Dr Ashish Darbari, FBCS, FIETE, DPhil (Oxon)
> Founder & CEO
> +44 207 096 0465
> ashish.darb...@axiomise.com
> Axiomise Ltd. Company No: 11016128
> 71-75 Shelton Street
> WC2H 9JQ
> London, UK
> 
> 
> On 22 May 2018 at 21:07, Chun Tian (binghe)  wrote:
> Hi,
> 
> I think you should use Poly/ML 5.6 to build Kananaskis 11. (and Poly/ML
> 5.6 or5.7 to build latest HOL on GitHub)
> 
> Regards,
> 
> Chun
> 
> Ashish Darbari wrote:
> > I'm running into this problem on Cent OS 7. No issues reported with
> > Poly ML installation (installation from sources).
> >
> > When running either smart-configure or tweaking by hand the
> > configure.sml file I get Static Errors.
> >
> > Any idea how to fix this?
> >
> >
> > Ashish
> >
> > [adarbari@localhost hol-kananaskis-11]$ poly
> >  > Poly/ML 5.7.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/adarbari/hol-kananaskis-11
> > 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

Re: [Hol-info] Comparing two Linear Temporal Logic (LTL) formalizations in HOL4

2018-05-20 Thread Michael.Norrish

The paper describing the work in examples/logic/ltl will appear at ITP this 
year.  Because there's a slight CakeML angle to it, it's available from 
cakeml.org at https://cakeml.org/itp18.pdf.

You are right that this work could be described as a deep embedding. 

Deep embeddings usually have the advantage that you can describe algorithms on 
the syntax, and not just have to think about the semantic values. For example, 
you can describe the NNF transformation when you have a deep embedding, but the 
best option for something similar with a shallow embedding is a statement of 
some equivalences between different semantic formulations of the same thing. 

It's also obviously useful to have a type corresponding to the syntax if you 
are going to define computable functions to traverse over it and transform it 
into automata (as is done in our work).

Michael

On 19/5/18, 00:42, "Chun Tian"  wrote:

Hi,

I saw how the new LTL formalization (in `examples/logic/ltl`) by Simon 
Jantsch suddenly appeared in the past months and because more and more complete 
also with help of HOL maintainers. But there’s already an older LTL 
formalization (in `src/temporal`) since long time ago, done by Klaus Schneider 
et al. [1]

My first question: is there a paper (in PDF, published or unpublished) 
documenting the work in `examples/logic/ltl` so that I can learn beside looking 
at raw HOL scripts?

Second question: regarding the difference between two versions of LTL 
formalizations, can I say the work in `examples/logic/ltl` is a *deep* 
embedding? (because it has to define the LTL syntax by a datatype:

val _ = Datatype`
  ltl_frml
  = VAR 'a
  | N_VAR 'a
  | DISJ ltl_frml ltl_frml
  | CONJ ltl_frml ltl_frml
  | X ltl_frml
  | U ltl_frml ltl_frml
  | R ltl_frml ltl_frml`;
)

while the work in `src/temporal` is *shallow* embedding? (because it 
embeds LTL term into HOL as ``:num -> bool`` without using any datatype)

and if so, what’s the pros and cons for choosing one of them as a 
working basis (for proving further results)?

Third question: is there a way to connect the two versions of LTL, so that 
LTL theorems proved from one side can be (somehow) automatically translated 
into theorems on the other side?

Regards,

Chun

[1] Schneider, K., Hoffmann, D.W.: A HOL Conversion for Translating Linear 
Time Temporal Logic to ω-Automata. In: Bassiliades, N., Gottlob, G., Sadri, F., 
Paschke, A., and Roman, D. (eds.) LNCS 9202 - Rule Technologies: Foundations, 
Tools, and Applications. pp. 255–272. Springer Berlin Heidelberg, Berlin, 
Heidelberg (1999).







--
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] Extension of Co-algebraic Datatype

2018-05-15 Thread Michael.Norrish

There is no documentation I’m afraid, except that the interface and behaviour 
is basically exactly the same as for IndDefLib, which is described in the 
DESCRIPTION manual.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 16 May 2018 at 06:11
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Great!. This is exactly what I want. Thanks for helping me out...:) I located 
the file  "CoIndDefLib" in the HOL folder "src/IndDef".. Is there any 
documentation available regarding this file?

On Sun, May 13, 2018 at 6:04 AM, 
> wrote:
If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 12 May 2018 at 05:45

To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀L. Stream L = LFILTER (λn. T) L:

type_of ``stream``;

 ``:α llist -> α llist``:

Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈ A; s ∈ streams A]] ⟹ a ## s ∈ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀A. streams A = IMAGE (λa. Stream a) {llist_abs (λn. SOME x) | x ∈ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈ streams A ⇒ (? a s. a = a ##s ⇒ a ∈ A ⇒ s ∈  streams A ⇒ P) 
⇒ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?

On Mon, May 7, 2018 at 8:49 PM, 
> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a 
constructor of type

(α -> bool) -> α llist

On Sun, May 6, 2018 at 8:39 PM, 
> wrote:
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-13 Thread Michael.Norrish

If you want the coinductively defined streams predicate over lllist, you can 
write

>  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> s)`;

<>

<>

val it =

   (⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),

⊢ ∀A streams'.

  (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒

  ∀a0. streams' a0 ⇒ streams A a0,

⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):

I think the last theorem of the triple is the cases theorem you want.

Note that if you are going to define Stream with

  Stream L = LFILTER (\n. T) L

You might as well write the equivalent

  Stream L = L

Best wishes,
Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 12 May 2018 at 05:45
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks!. I understand that the working of LNIL and LCONS constructors since I'm 
exploring "llistTheory" for quite some time. To be very clear, I'm in the 
process of porting "stream theory" form Isabelle 
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which 
is formalized as coinductive "stream":

codatatype (sset: 'a) stream =
  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
  map: smap
  rel: stream_all2

 I can see that its datatype is very similar to lazy list (llistTheory) 
datatype so rather defining a new type I defined a function that returns the 
same 'a llist-typed (lazy) list as given to its input:

∀L. Stream L = LFILTER (λn. T) L:

type_of ``stream``;

 ``:α llist -> α llist``:

Later in Isabelle "stream theory", a coinductive set "streams" is defined based 
on "stream" datatype as:

coinductive_set
  streams :: "'a set ⇒  'a stream set"
  for A :: "'a set"
where
  Stream[intro!, simp, no_atp]: "[[a ∈ A; s ∈ streams A]] ⟹ a ## s ∈ 
streams A"
end

Using llistTheory functions, I'm able to define a similar function as:

∀A. streams A = IMAGE (λa. Stream a) {llist_abs (λn. SOME x) | x ∈ A}:

type_of ``streams``;

 ``:('a -> bool) -> 'a llist -> bool``:

However, by using shallow embedding approach, I'm not able to use some 
essential properties that are accompanied when a new coinductive datatype is 
defined. For instance, if a streams datatype is define, I may have this 
property of form:

streams.cases (Isabelle):

a ∈ streams A ⇒ (? a s. a = a ##s ⇒ a ∈ A ⇒ s ∈  streams A ⇒ P) 
⇒ P

I'm having the issues of defining these types in HOL4. Is there any way that I 
can replicate the same in HOL4?

On Mon, May 7, 2018 at 8:49 PM, 
> wrote:
You can probably define a function of that type, but you can’t define a 
*constructor* of that type for llist.   (Contrast what I’d consider to be 
llist’s standard constructors, LNIL and LCONS. They have types α llist, and α 
-> α llist -> α llist respectively.)

You said you wanted a stream type, does this mean you want a constructor for 
stream of type

  (α -> bool) -> α stream

?

Such a constructor is not recursive, so I can just write

Datatype`stream = SetConstructor (α -> bool)`

The SetConstructor term then has the desired type.

So I’m afraid I still don’t understand your question.

Michael

From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Monday, 7 May 2018 at 11:38
To: "Norrish, Michael (Data61, Acton)" 
>
Cc: hol-info 
>
Subject: Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a 
constructor of type

(α -> bool) -> α llist

On Sun, May 6, 2018 at 8:39 PM, 
> wrote:
I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In particular, write down the type of the “general” destructor

  myType -> F(myType)

For lazy lists, this is

  α llist -> (α # α llist) option

For the co-algebraic numbers it’s

  num -> num option

For arbitrarily (but finite)-branching trees, it’s

  Tree -> Tree list

(If you change list to llist you get possibly infinitely branching trees.)

In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s 
“predecessor”; in the trees it’s “children”.  Because the types are 
co-algebraic each might be iterable an infinite number of times.  (The 
corresponding destructors in the algebraic types are always well-founded.)

What are the co-algebras for your desired types?  I don’t think I’ve understood 
what you want, but it superficially appears as if you want dependent types, 
where you combine the type with some term-level predicate. That sort of

Re: [Hol-info] Extension of Co-algebraic Datatype

2018-05-06 Thread Michael.Norrish

I think you may be able to make your needs more precise by explicitly 
considering what your co-algebra would be.

In particular, write down the type of the “general” destructor

  myType -> F(myType)

For lazy lists, this is

  α llist -> (α # α llist) option

For the co-algebraic numbers it’s

  num -> num option

For arbitrarily (but finite)-branching trees, it’s

  Tree -> Tree list

(If you change list to llist you get possibly infinitely branching trees.)

In the lazy lists, this destructor might be called “HDTL”; in the numbers, it’s 
“predecessor”; in the trees it’s “children”.  Because the types are 
co-algebraic each might be iterable an infinite number of times.  (The 
corresponding destructors in the algebraic types are always well-founded.)

What are the co-algebras for your desired types?  I don’t think I’ve understood 
what you want, but it superficially appears as if you want dependent types, 
where you combine the type with some term-level predicate. That sort of thing 
is impossible to capture within a HOL type.

Finally, I’m afraid that there is no general tool for defining co-algebraic 
types in HOL4 at the moment.

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info 
Cc: Waqar Ahmad 
Subject: [Hol-info] Extension of Co-algebraic Datatype

Hi,

Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which is 
developed based on the co-algebraic datatype. I understand that the datatype 'a 
llist  is derived as a subset of  the option type :num -> 'a option.  Now, I 
want to define a new datatype based on datatype 'a llist. For instance,

P of  'a llist

such that P: 'a llist -> 'a stream, where 'a stream is essentially the similar 
datatype as 'a llist  but having different properties. In shallow embedding, I 
can define it by using filter function of llistTheory as:


val Stream = Define `Stream L =  LFILTER (\n:'a. T) L`;

One way of defining the co-inductive datatype stream is to follow the same 
procedure as described in "llistTheory", which is quite cumbersome. Is there 
any alternate way similar to that of package "Hol_datatype"?

Secondly, Is it possible to define a co-inductive datatype that takes a set 
type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A similar 
function, in shallow embedding, I can think of is:

val streams_def = Define
`streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;

where the function streams is of type (:num -> 'a option) ->bool -> 'a llist-> 
bool

In some cases, the function streams doesn't suffice for modeling the correct 
behavior of streams related properties..

Any suggestion or thoughts would be highly helpful...






--
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/
[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
--
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] Poly/ML debugging facility does not work in HOL4

2018-04-29 Thread Michael.Norrish

It looks as if it came from 

  polyml/basis/FinalPolyML.sml

Michael

On 29/4/18, 20:23, "Chun Tian"  wrote:

Thanks for the detailed explanation. Just one more question: do you know 
which code file in Poly/ML sources corresponds to tools-poly/holrepl.ML?

—Chun

> Il giorno 29 apr 2018, alle ore 11:00, michael.norr...@data61.csiro.au ha 
scritto:
> 
> As I said earlier, the breakage is certainly caused by the way in which 
the REPL executable now includes a custom lexer (for handling the various 
backquote ```` syntaxes), and is not the standard Poly REPL. This is 
exactly the change that was implemented in the heaps-reworked branch. Having to 
run a separate process just to achieve that lexing has caused many difficulties 
in the past, and I am definitely not inclined to go back to it.
> 
> It's possible that the Poly/ML debugging facility can be re-implemented 
in the new REPL; you may be able to get useful advice about how this might be 
done on the Poly/ML mailing list.  Such tweaking would almost certainly have to 
be done against the code in tools-poly/holrepl.ML, which is basically a 
slightly adjusted copy of code from the Poly/ML sources.
> 
> Michael
> 
> On 29/4/18, 02:56, "Chun Tian"  wrote:
> 
>Hi Michael,
> 
>I… took some time trying to find out the revision which breaks the 
debugging facility. After many rounds of binary searching, I found that, until 
the following revision
> 
>   e5fc0f365922cfd11ec32c4531983d20892777a6 (Improving naming of 
bit-vector signed division constants…) on Sep 11, 2017
> 
>the debugging facility still works, then after the next revision it’s 
broken:
> 
>   69125acadde5cf629e4b9d5604bc33b226c57b5d (Merge branch 
'heaps-reworked’) on Sep 13, 2017
> 
>many revisions after e5fc0f36 is not buildable under Poly/ML 5.7 
(until c52815a4 “Comment out optional(?) code that doesn't work/exist under 
poly5.7…”) so I used Poly/ML 5.6 to confirm above broken revisions.
> 
>I’ll try to dig into your branch 'heaps-reworked’ to further find out 
the exact changes related to the breaks of debugging facility.
> 
>Could you please make some efforts to fix this issue? I think HOL 
should be considered as a normal Poly/ML with theorem proving built in, and in 
theory HOL executions can be used for developing any SML-based applications, 
and the the debugging facility is very important for large complex applications.
> 
>Regards,
> 
>Chun
> 
>> Il giorno 26 apr 2018, alle ore 01:22, michael.norr...@data61.csiro.au 
ha scritto:
>> 
>> The REPL (allows great interactive unit-testing) and annotation with 
print statements.
>> 
>> Michael
>> 
>> On 25/4/18, 03:36, "Mario Xerxes Castelán Castro" 
 wrote:
>> 
>>   What do you use for debugging, or instead of debugging?
>> 
>>   On 19/04/18 23: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.
>>   --
>>   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



--
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] Poly/ML debugging facility does not work in HOL4

2018-04-29 Thread Michael.Norrish

As I said earlier, the breakage is certainly caused by the way in which the 
REPL executable now includes a custom lexer (for handling the various backquote 
```` syntaxes), and is not the standard Poly REPL. This is exactly the 
change that was implemented in the heaps-reworked branch. Having to run a 
separate process just to achieve that lexing has caused many difficulties in 
the past, and I am definitely not inclined to go back to it. 

It's possible that the Poly/ML debugging facility can be re-implemented in the 
new REPL; you may be able to get useful advice about how this might be done on 
the Poly/ML mailing list.  Such tweaking would almost certainly have to be done 
against the code in tools-poly/holrepl.ML, which is basically a slightly 
adjusted copy of code from the Poly/ML sources.

Michael

On 29/4/18, 02:56, "Chun Tian"  wrote:

Hi Michael,

I… took some time trying to find out the revision which breaks the 
debugging facility. After many rounds of binary searching, I found that, until 
the following revision

e5fc0f365922cfd11ec32c4531983d20892777a6 (Improving naming of 
bit-vector signed division constants…) on Sep 11, 2017

the debugging facility still works, then after the next revision it’s 
broken:

69125acadde5cf629e4b9d5604bc33b226c57b5d (Merge branch 
'heaps-reworked’) on Sep 13, 2017

many revisions after e5fc0f36 is not buildable under Poly/ML 5.7 (until 
c52815a4 “Comment out optional(?) code that doesn't work/exist under poly5.7…”) 
so I used Poly/ML 5.6 to confirm above broken revisions.

I’ll try to dig into your branch 'heaps-reworked’ to further find out the 
exact changes related to the breaks of debugging facility.

Could you please make some efforts to fix this issue? I think HOL should be 
considered as a normal Poly/ML with theorem proving built in, and in theory HOL 
executions can be used for developing any SML-based applications, and the the 
debugging facility is very important for large complex applications.

Regards,

Chun

> Il giorno 26 apr 2018, alle ore 01:22, michael.norr...@data61.csiro.au ha 
scritto:
> 
> The REPL (allows great interactive unit-testing) and annotation with 
print statements.
> 
> Michael
> 
> On 25/4/18, 03:36, "Mario Xerxes Castelán Castro" 
 wrote:
> 
>What do you use for debugging, or instead of debugging?
> 
>On 19/04/18 23: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.
>--
>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] Poly/ML debugging facility does not work in HOL4

2018-04-25 Thread Michael.Norrish

The REPL (allows great interactive unit-testing) and annotation with print 
statements.

Michael

On 25/4/18, 03:36, "Mario Xerxes Castelán Castro"  
wrote:

What do you use for debugging, or instead of debugging?

On 19/04/18 23: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.
-- 
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

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

2018-04-19 Thread Michael.Norrish

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

Re: [Hol-info] About the experimental kernel

2018-04-11 Thread Michael.Norrish

Term.lazy_beta_conv, which is in turn called by Thm.Beta and Thm.Specialize.

Michael

On 12/4/18, 09:50, "Jeremy Dawson"  wrote:



On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote:
>   for explicit lazy beta
> conversions (with an internal explicit substitution calculus)

I assume this refers to Clos, mk_clos etc in src/0/Term.sml

My questions is: is this actually used?  I can't see where anything in 
the source code creates a Clos where there isn't already one existing.

This would be odd, so I guess I've overlooked it somewhere - but where?

Jeremy


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

2018-04-07 Thread Michael.Norrish

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 
Date: Friday, 6 April 2018 at 21:27
To: Ramana Kumar , HOL-info list 

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

Attached is a port of tamarack.ml, which seems to just be 
definitions. I guess the proofs might be harder to port, but I haven't looked...
They could be added to HOL/examples in the HOL4 distribution -- if I find time 
to port them later (must leave it for now though..)

On 5 April 2018 at 14:02, Lawrence Paulson 
> wrote:
It would be nice to give them a permanent home, perhaps as part of the HOL4 
distribution. Also I may create a small memorial page for Mike and could 
include it there.

I found mountains of old stuff in Mike's file space, though sadly, much of it 
is protected.

Larry

On 5 Apr 2018, at 13:41, Ramana Kumar 
> wrote:

It doesn't look too bad to me - happy to port them if you like.

--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] PhD Scholarships at the Australian National University

2018-03-28 Thread Michael.Norrish

The Logic and Computation Group at the Research School of Computer
Science, The Australian National University has a number of PhD
scholarship available for bright, enthusiastic doctoral students in
the following fields:

- Logic and Linguistics (Ekaterina Lebedeva)
- Logic in Computer Science (Rajeev Gore, Dirk Pattinson, Alwen Tiu)
- Non-Classical Logics (Rajeev Gore, John Slaney, Dirk Pattinson)
- Proof Theory (Rajeev Gore, Dirk Pattinson, Alwen Tiu)
- Automated Reasoning (Peter Baumgartner, Rajeev Gore)
- Computer Aided Verification (Sergiy Bogomolov, Michael Norrish, Dirk 
Pattinson)
- Interactive Theorem Proving (Michael Norrish, Dirk Pattinson)
- Verification of Computational Complexity (Abdallah Saffidine)
- Computer Security Foundations (Alwen Tiu)
- Electronic Voting and Social Choice Theory (Rajeev Gore, Dirk Pattinson)

Potential applicants are encouraged to consult the group’s web pages
at https://cecs.anu.edu.au/research/theory/logic/ and make direct
contact with potential supervisors.

Students will be based at the Research School of Computer Science
within the Australian National University. The studentship is a
tax-free allowance of A$ 27,082 (2018 rate) per year, tenable for a
maximum of 3.5 years.

Applications are to be submitted electronically at
http://applyonline.anu.edu.au/ before the closing date, April 20,
2018. Further information about graduate research within Computer
Science at ANU, please see

https://cs.anu.edu.au/study/graduate-research .

The scholarships are open to individuals of any nationality. We are
based in Canberra, Australia, the top-ranking region of the 2014 OECD
quality of life survey
(http://www.canberra.com.au/canberra-the-worlds-most-liveable-city/).

The ANU actively seeks to promote diversity in the workplace.

++ 

--
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] Unexpected failure to considerate equality of lambda terms in Metis and MESON

2018-03-28 Thread Michael.Norrish

I'm afraid there is no solution to this problem whereby automatic tools will 
make lots of progress. First order reasoners such as PROVE_TAC and METIS_TAC 
try to do a little in this area (converting lambda-expressions to terms 
involving combinators for example), but this only goes so far, and also makes 
it hard to see what one should additionally provide to prime the provers.  In 
your case, the underlying goal might end up being

  f (<=) = f (\x. B ((<) x) SUC)
 = f (S (B B (<)) (K SUC))

Where B is actually combin$o.  Given this, the supposedly relevant theorem 
relating < and <= isn't going to apply.  You could try giving METIS FUN_EQ_THM 
as an argument I suppose.

Michael

On 27/3/18, 04:56, "Mario Xerxes Castelán Castro"  
wrote:

Hello.

Metis can prove «(λx m. x ≤ m) = (λx m. x < SUC m)» using
arithmeticTheory.LESS_EQ_IFF_LESS_SUC, but if the left hand side and
right hand instead appear as the operands of a combination then it no
longer works. The same behavior applies to “PROVE_TAC”.

> TAC_PROOF (([], “(λx m. x ≤ m) = (λx m. x < SUC m)”), METIS_TAC
[arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
metis: r[+0+5]+0+0+1+0+0+1#
val it = ⊢ (λx m. x ≤ m) = (λx m. x < SUC m): thm

> TAC_PROOF (([], “f (λx m. x ≤ m) = f (λx m. x < SUC m)”), METIS_TAC
[arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
<>
metis: r[+0+7]+0+0+0+0+0+0+0!
Exception-
   HOL_ERR
 {message = "no solution found", origin_function = "FOL_FIND",
  origin_structure = "folTools"} raised

> TAC_PROOF (([], “f (λx m. x ≤ m) = f (λx m. x < SUC m)”),
metisTools.HO_METIS_TAC [arithmeticTheory.LESS_EQ_IFF_LESS_SUC]);
<>
metis: r[+0+7]+0+0+0+0+0+0+0!
Exception-
   HOL_ERR
 {message = "no solution found", origin_function = "FOL_FIND",
  origin_structure = "folTools"} raised

This is a reduced test case to show the problem. Obviously I could use
the simplifier here, but in general Metis and MESON seem to be unable to
use equality of lambda terms to complete a proof and thus they fail for
some otherwise simple use cases that occur in practice. What should I do
about this?

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

[Hol-info] Data61 seeking proof engineers

2018-03-17 Thread Michael.Norrish

Data61 Seeking Proof Engineers
==

If only there were a place where I could prove theorems for money, change the
world, and have fun while doing it...

Sounds too good to exist?

In the Trustworthy Systems team at Data61 that's what we do for a living. We
are the creators of seL4, the world's first fully formally verified operating
system kernel with extreme performance and strong security & correctness
proofs. Our highly international team is located on the UNSW campus, close to
the beautiful beaches of sunny Sydney, Australia, one of the world's most
liveable cities.

We are looking for 3 motivated proof engineers who want to join our team in 
Sydney,
move things forward, and have global impact. We are expanding our team,
because seL4 is going places. There are active projects around the world in

  - Automotive - because cars have been hacked enough
  - Aviation - for more security and safety for autonomous vehicles
  - Defence - protecting confidential information
  - Connected consumer devices - with security built in from the start
  - Spaceflight - because awesome

To make these projects successful, we need to scale formal verification.
You would

  - work on industrial-scale formal proofs in Isabelle/HOL
  - develop formally verified infrastructure for building secure systems
on top of seL4
  - contribute to improved proof automation and better reasoning techniques
  - apply formal proof to real-world systems and tools

To apply for this position, you should possess a significant subset of the
following skills.

  - functional programming in a language like Haskell, ML, or OCaml
  - first-order or higher-order formal logic
  - basic experience in C
  - ability and desire to quickly learn new techniques
  - undergraduate degree in Computer Science, Mathematics, or similar
  - ability and desire to work in a larger team

We are hiring at two levels, so if you are more qualified or experienced than
the above would suggest, you can come in as a senior proof engineer.

If you additionally have experience

  - in software verification with an interactive theorem prover such as
Isabelle/HOL, HOL4, or Coq, and/or
  - with operating systems and microkernels

you should definitely apply!

If you have the right skills and background, we can provide training on the
job. Continual learning is a central component of everything we do. You will
work with a unique world-leading combination of OS and formal methods
experts, students at undergraduate and PhD level, engineers, and researchers
from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun,
creative, and welcoming workplace with flexible hours & work arrangements.

We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.

Salary ranges for this position, in AUD (plus superannuation):
- Junior: 80-91K
- Senior: 95-103K
depending on experience and qualifications.

Apply online at the following links:
- https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/464792900/
- https://jobs.csiro.au/job/Sydney%2C-NSW-Senior-Proof-Engineer/464792300/

Your application should include a cover letter, CV, undergraduate transcript
(if applicable), and contact information for two references.

This round of applications closes 15 April 2018.

The seL4 code and proof are open source. Check them out at https://seL4.systems

More information about Data61's Trustworthy Systems team at
https://ts.data61.csiro.au

Still studying? We also have internship opportunities!
https://ts.data61.csiro.au/students/


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

2018-03-12 Thread Michael.Norrish

Indeed.  There is no need to distinguish axioms and axiom schemata (as Thomas 
said, oracles are not the latter). This is because of the INST and INST_TYPE 
rules of inference.  In a system with schemata, instantiation (or matching) is 
the way you check whether or not you have an oracle, and you have a special 
category of schema variable. The variables in HOL’s axioms are normal 
variables, and can be instantiated both in axioms and derived theorems.

Michael

From: Thomas Tuerk 
Date: Tuesday, 13 March 2018 at 08:51
To: "hol-info@lists.sourceforge.net" 
Subject: Re: [Hol-info] HOL Help for Axiom.


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] [ExternalEmail] Re: Using polyscripter with user-written theories

2018-02-19 Thread Michael.Norrish

Just to confirm that polyscripter as of 0146fefd73f now does pay attention to 
INCLUDES and PRE_INCLUDES lines in Holmakefiles.

Michael

On 19/2/18, 11:51, "michael.norr...@data61.csiro.au" 
 wrote:

Thanks for the question Heiko.

I think Thomas’s answer is the best that can be done at the moment, but now 
that I’m aware of the problem, I will adjust polyscripter to pay attention to 
`INCLUDES =` lines in a Holmakefile, and perhaps also `-I` command-line options 
passed to polyscripter.

With a little work, it might not even be necessary to manually `load` the 
theories first: there’s no strong reason that I can see why the input lines 
can’t be parsed for module references in the same way that the Emacs mode does. 
(Indeed, if using Poly/ML this might even be possible in the interactive system 
more generally.)

Michael

On 16/2/18, 18:05, "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

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

2018-02-18 Thread Michael.Norrish

Thanks for the question Heiko.

I think Thomas’s answer is the best that can be done at the moment, but now 
that I’m aware of the problem, I will adjust polyscripter to pay attention to 
`INCLUDES =` lines in a Holmakefile, and perhaps also `-I` command-line options 
passed to polyscripter.

With a little work, it might not even be necessary to manually `load` the 
theories first: there’s no strong reason that I can see why the input lines 
can’t be parsed for module references in the same way that the Emacs mode does. 
(Indeed, if using Poly/ML this might even be possible in the interactive system 
more generally.)

Michael

On 16/2/18, 18:05, "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

2018-02-04 Thread Michael.Norrish

In fact,

  bin/build cleanForReloc

will purge a directory tree of the files in rebuild-excludes.txt, so it might 
be easier to copy a tree and then “clean” it.

This workflow should be documented before the next release.

Best wishes,
Michael

From: Ramana Kumar 
Date: Monday, 5 February 2018 at 04:28
To: Mario Xerxes Castelán Castro 
Cc: hol-info 
Subject: Re: [Hol-info] Dependency on absolute paths remaining the same

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
If there are additional developments outside of HOL that you want to build 
using the newly located HOL, you may also need to use Holmake's --relocbuild 
argument when rebuilding them initially (and also see --nolmbc).

On 4 February 2018 at 17:16, Mario Xerxes Castelán Castro 
> wrote:
Hello.

Is it possible to use HOL4 in such a way that it continues working
despite moving the directory to a different absolute path? The option
“--relocbuild” of “bin/build” seems to be related. Is it documented
anywhere? (I did not find anything in the manual)

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] Inquiry: Introducing new types as predicates

2018-01-22 Thread Michael.Norrish

HOL’s core principle of type definition *is* based on predicates, inasmuch as a 
new type is constructed by appealing to a non-empty predicate over an existing 
type to represent the new type.

But I guess this doesn’t quite give you the “style” you want.

Are you aware of the predicate sub-typing offered by PVS?

Michael


From: Cris Perdue 
Date: Tuesday, 23 January 2018 at 11:36
To: hol-info 
Subject: [Hol-info] Inquiry: Introducing new types as predicates

Are any of you readers of this list aware of investigations or implementations 
of logics that, like the HOL family of provers, are based on the simple theory 
of types, but which support introduction of new types through new predicates 
rather than new type constants? Presumably numbers then could be individuals, 
like other individuals, with some being integers, some real, and so on.

Any references to results of existing efforts to explore the potential and/or 
issues raised by such arrangements would be much appreciated.

A significant part of my own interest in this approach is related to usability 
by non-specialists, and in that sense style might be more an issue than 
ultimate expressive power. Ideally such a system would also support a 
relatively flexible and rich system of "types", without the need to bring in 
the conceptual complexity of dependent types, and their accompanying notations.

Best regards and thanks in advance,
Cris





--
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] Share list of terms with later theories

2018-01-16 Thread Michael.Norrish

If people wanting to store these “uninteresting” theorems are happy to wrap and 
unwrap the OMITs, this would be one approach.  

I had been thinking of adding a 

  save_private_thm(name, privatedbname, thm)

entrypoint to Theory.sml.  You’d want multiple possible “private dbs”, so there 
would be an entry-point along the lines of

  get_private_db : string -> (string,thm) Binarymap.dict

Every time a theory was loaded, this private_db would change, so in many 
applications it might not be appropriate to store the result of 

  get_private_db “cakeml/translator”

but to instead write

  val th = Binarymap.peek(get_private_db “cakeml/translator”, “theorem-name”)

Michael 

On 16/1/18, 18:35, "Magnus Myreen"  wrote:

Hi all,

How about defining:

  OMIT x = x

in markerScript.sml and making it print as ... and adjust HOL so that
a theorem with a top-level OMIT does not show up in DB searches.

Cheers,
Magnus


On 12 January 2018 at 00:00,   wrote:
> I was thinking along these lines, yeah.  Such theorems could also be 
stopped from appearing in the Theory.sig file.
>
> Michael
>
> On 12/1/18, 07:31, "Konrad Slind"  wrote:
>
> Theorems that need to persist between sessions are most easily stored 
by name
> in theories. Maybe some kind of PolyML database magic could also be
> used, I don't
> know. As far as DB searches, it wouldn't be hard to implement a
> refined DB search
> mechanism that first discarded all theorems that met some kind of
> naming convention
> (e.g., those starting with an underscore or something like that) and
> then did the usual
> search (which can be on name fragment or pattern).
>
> Konrad.
>
>
> On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen  
wrote:
> > Ah, I didn't realise this existed. Thanks for the pointers!
> >
> > How does storing of theorems work in this setting? One can't 
construct
> > a theorem from a string in a decode function.
> >
> > I guess the string could refer to a theorem name that's stored in 
the
> > theory, but this is a bit inconvenient because some of the theorems 
in
> > the translator's state are currently not stored in the theory (other
> > than in the automatically produced theorem that is an encoding of 
the
> > entire state). I guess an encode function could invent an unused 
name
> > and store the theorem while it's producing the encoding. This can 
lead
> > to some strange things turning up in DB searches (as is the case 
with
> > the current approach).
> >
> > Cheers,
> > Magnus
> >
> >
> > On 11 January 2018 at 11:24,   
wrote:
> >> That level of generality is already possible, and has always been 
a desideratum for the design.  (The grammar update information stored is about 
that complicated for example; consider the types that occur in a call to 
add_rule.)
> >>
> >> The painful part is that you have to write functions to encode and 
decode the types into and out of strings (because these strings are written 
into the theory files).  There are functions for doing basic SML types in 
src/parse/Coding, and the handling of terms is handled by writing functions 
that take functions for doing this as parameters.  See the bottom of 
src/parse/term_grammar for the encoding and decoding, and 
src/parse/GrammarDeltas for the way this is put together for the grammar 
example.
> >>
> >> You can see the fundamental building blocks at the LoadableThyData 
structure in src/postkernel/Theory.
> >>
> >> Certainly, providing a method for going through a generic 
s-expression type might be easiest for users to understand, so perhaps I can 
build that as well as term lists.
> >>
> >> Michael
> >>
> >> On 11/1/18, 11:08, "Magnus Myreen"  wrote:
> >>
> >> Hi Michael,
> >>
> >> I see that you are considering to add a TermSetData feature. 
Could you
> >> please add something more general? I'd appreciate a feature 
that can
> >> store the CakeML translator's state in theories. Currently, 
the CakeML
> >> translator stores its state in a single theorem so that the 
other
> >> theories can load the state and continue from previous states.
> >>
> >> As far as I can tell, the ThmSetData machinery (and probably 
the
> >> TermSetData equivalent) won't help with the translator. The 
reason is
> >> that the translator's state is a collection of lists of list 
of tuples
> >>

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

2018-01-11 Thread Michael.Norrish

I was thinking along these lines, yeah.  Such theorems could also be stopped 
from appearing in the Theory.sig file. 

Michael

On 12/1/18, 07:31, "Konrad Slind"  wrote:

Theorems that need to persist between sessions are most easily stored by 
name
in theories. Maybe some kind of PolyML database magic could also be
used, I don't
know. As far as DB searches, it wouldn't be hard to implement a
refined DB search
mechanism that first discarded all theorems that met some kind of
naming convention
(e.g., those starting with an underscore or something like that) and
then did the usual
search (which can be on name fragment or pattern).

Konrad.


On Wed, Jan 10, 2018 at 7:09 PM, Magnus Myreen  wrote:
> Ah, I didn't realise this existed. Thanks for the pointers!
>
> How does storing of theorems work in this setting? One can't construct
> a theorem from a string in a decode function.
>
> I guess the string could refer to a theorem name that's stored in the
> theory, but this is a bit inconvenient because some of the theorems in
> the translator's state are currently not stored in the theory (other
> than in the automatically produced theorem that is an encoding of the
> entire state). I guess an encode function could invent an unused name
> and store the theorem while it's producing the encoding. This can lead
> to some strange things turning up in DB searches (as is the case with
> the current approach).
>
> Cheers,
> Magnus
>
>
> On 11 January 2018 at 11:24,   wrote:
>> That level of generality is already possible, and has always been a 
desideratum for the design.  (The grammar update information stored is about 
that complicated for example; consider the types that occur in a call to 
add_rule.)
>>
>> The painful part is that you have to write functions to encode and 
decode the types into and out of strings (because these strings are written 
into the theory files).  There are functions for doing basic SML types in 
src/parse/Coding, and the handling of terms is handled by writing functions 
that take functions for doing this as parameters.  See the bottom of 
src/parse/term_grammar for the encoding and decoding, and 
src/parse/GrammarDeltas for the way this is put together for the grammar 
example.
>>
>> You can see the fundamental building blocks at the LoadableThyData 
structure in src/postkernel/Theory.
>>
>> Certainly, providing a method for going through a generic s-expression 
type might be easiest for users to understand, so perhaps I can build that as 
well as term lists.
>>
>> Michael
>>
>> On 11/1/18, 11:08, "Magnus Myreen"  wrote:
>>
>> Hi Michael,
>>
>> I see that you are considering to add a TermSetData feature. Could 
you
>> please add something more general? I'd appreciate a feature that can
>> store the CakeML translator's state in theories. Currently, the 
CakeML
>> translator stores its state in a single theorem so that the other
>> theories can load the state and continue from previous states.
>>
>> As far as I can tell, the ThmSetData machinery (and probably the
>> TermSetData equivalent) won't help with the translator. The reason is
>> that the translator's state is a collection of lists of list of 
tuples
>> of combinations of strings, type, terms and theorems.
>>
>> The current approach encodes all of these structures into a single
>> unreadable theorem. This works but it seems a bit ad hoc and causes
>> huge unreadable theorems to pop up in various DB searches.
>>
>> Suggestion: could we have a way to store a s-expression-like data 
into
>> theories? If the s-expressions would allow strings, types, terms,
>> theorems and, of course, pairs/lists of s-expressions, then I think
>> the translator's state could very naturally be stored in theories.
>>
>> Cheers,
>> Magnus
>>
>> > There is generic machinery for adding values of various forms to 
theories so
>> > that future theories and ML code can see them.  The smoothest 
instantiation
>> > is in ThmSetData (in src/1) which allows storage of sets of 
theorems in a
>> > “2D matrix” indexed by theory-name and set-name.  For example, the 
automatic
>> > rewrites behind the “simp” attribute are implemented this way.
>> >
>> > The storage of grammar updates is handled with the same technology.
>> >
>> > A hacky way to store terms would be to use theorems with 
conclusions of the
>> > form
>> >
>> >K T (myterm)
>> >
>> > and to then use ThmSetData.
>> >
>> > A better

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

2018-01-10 Thread Michael.Norrish

That level of generality is already possible, and has always been a desideratum 
for the design.  (The grammar update information stored is about that 
complicated for example; consider the types that occur in a call to add_rule.)

The painful part is that you have to write functions to encode and decode the 
types into and out of strings (because these strings are written into the 
theory files).  There are functions for doing basic SML types in 
src/parse/Coding, and the handling of terms is handled by writing functions 
that take functions for doing this as parameters.  See the bottom of 
src/parse/term_grammar for the encoding and decoding, and 
src/parse/GrammarDeltas for the way this is put together for the grammar 
example.

You can see the fundamental building blocks at the LoadableThyData structure in 
src/postkernel/Theory.

Certainly, providing a method for going through a generic s-expression type 
might be easiest for users to understand, so perhaps I can build that as well 
as term lists.

Michael

On 11/1/18, 11:08, "Magnus Myreen"  wrote:

Hi Michael,

I see that you are considering to add a TermSetData feature. Could you
please add something more general? I'd appreciate a feature that can
store the CakeML translator's state in theories. Currently, the CakeML
translator stores its state in a single theorem so that the other
theories can load the state and continue from previous states.

As far as I can tell, the ThmSetData machinery (and probably the
TermSetData equivalent) won't help with the translator. The reason is
that the translator's state is a collection of lists of list of tuples
of combinations of strings, type, terms and theorems.

The current approach encodes all of these structures into a single
unreadable theorem. This works but it seems a bit ad hoc and causes
huge unreadable theorems to pop up in various DB searches.

Suggestion: could we have a way to store a s-expression-like data into
theories? If the s-expressions would allow strings, types, terms,
theorems and, of course, pairs/lists of s-expressions, then I think
the translator's state could very naturally be stored in theories.

Cheers,
Magnus

> There is generic machinery for adding values of various forms to theories 
so
> that future theories and ML code can see them.  The smoothest 
instantiation
> is in ThmSetData (in src/1) which allows storage of sets of theorems in a
> “2D matrix” indexed by theory-name and set-name.  For example, the 
automatic
> rewrites behind the “simp” attribute are implemented this way.
>
> The storage of grammar updates is handled with the same technology.
>
> A hacky way to store terms would be to use theorems with conclusions of 
the
> form
>
>K T (myterm)
>
> and to then use ThmSetData.
>
> A better way, which, now that I’ve been prodded, I may implement soon, 
would
> be to write a TermSetData.
>
> I hope this helps. I’m happy to discuss the details of this relatively
> undocumented feature further if you want more help.
>
> Best wishes,
> Michael
>
> On 11/1/18, 01:51, "Heiko Becker"  wrote:
>
> Hello everyone,
>
> suppose I have a custom tactic that depends on a list of terms and I
> want to keep adding elements to the list throughout my development.
> I tried to achieve this using a :term list ref on the ML level. 
However,
> it is the case that if I add some term in theory A and inspect the 
list
> in theory B, where A is in the theory graph before B, all elements 
added
> in A are not in the list anymore.
>
> Can someone give me a hint on why this is the case or tell me a better
> way to "share" a list of terms from a theory with theories depending 
on
> it?
>
> Cheers,
>
> Heiko
>
>
> 
--
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> 
--
> 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

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

2018-01-10 Thread Michael.Norrish

There is generic machinery for adding values of various forms to theories so 
that future theories and ML code can see them.  The smoothest instantiation is 
in ThmSetData (in src/1) which allows storage of sets of theorems in a “2D 
matrix” indexed by theory-name and set-name.  For example, the automatic 
rewrites behind the “simp” attribute are implemented this way. 

The storage of grammar updates is handled with the same technology. 

A hacky way to store terms would be to use theorems with conclusions of the 
form 
  
   K T (myterm)

and to then use ThmSetData.

A better way, which, now that I’ve been prodded, I may implement soon, would be 
to write a TermSetData.

I hope this helps. I’m happy to discuss the details of this relatively 
undocumented feature further if you want more help.

Best wishes,
Michael

On 11/1/18, 01:51, "Heiko Becker"  wrote:

Hello everyone,

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

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

Cheers,

Heiko


--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


--
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 build only hol.bare?

2017-12-23 Thread Michael.Norrish

The way to do this sort of thing is to specify the sequence of directories you 
want built with the 

  --seq=fname

command line option.  Sequence files can #include other files.  See the 
documentation in the top-level file

  tools/build-sequence

If you are hacking HOL frequently, please read the manual at Manual/Developers, 
and if there’s stuff not there, please suggest possible fixes (or make pull 
requests to fix it of course).

I hope this helps,
Michael

On 22/12/17, 05:01, "Mario Castelán Castro"  wrote:

Hello.

When modifying HOL4 itself, sometimes building “hol.bare” suffices to
test the effects of the change.

A complete build from scratch with -j 2 (I have 2 hardware threads)
takes around 1,600 s in my computer. Changing “early” files (like those
in “src/1”) causes nearly everything to be re-built, so the time is
around the same. Is it possible to build *only* “hol.bare”?. This would
make testing the effect of my changes much more convenient.

I tried with “bin/build bin/hol.bare” but it fails with “Multi-dir build
not implemented yet”.

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] The origin of the HOL4 logo

2017-12-20 Thread Michael.Norrish

I’m pretty sure I derived the small logo GIF file from the eps file in the HOL 
repo using some image manipulation process, and perhaps some bitmap tweaking. 

The photo may be the one linked to earlier at the URL under cl.cam.ac.uk/~mjcg.

Michael

On 19/12/17, 13:13, "Mario Castelán Castro"  wrote:

Thanks.

This comment appears to refer to the old logo featured in the manual
 (because it was
in the manual back when it featured that logo) instead of the current
one (which is very similar).

Do you have a link to the aforementioned photo of the snow-watching
lantern in Avra Cohn's garden?

On 17/12/17 16:19, michael.norr...@data61.csiro.au wrote:
> Our manuals’ acknowledgements text includes:
> 
>   The cover design is by Arnold Smith, who used a photograph of a `snow 
watching lantern' taken by 
>   Avra Cohn (in whose garden the original object resides).  John Van 
Tassel composed the \LaTeX\ 
>   picture of the lantern.
> 
> This would have been done in the late 80s (and I am taking the 
acknowledgement text on trust).
> 
> Michael

-- 
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] The origin of the HOL4 logo

2017-12-17 Thread Michael.Norrish

Our manuals’ acknowledgements text includes:

  The cover design is by Arnold Smith, who used a photograph of a `snow 
watching lantern' taken by 
  Avra Cohn (in whose garden the original object resides).  John Van Tassel 
composed the \LaTeX\ 
  picture of the lantern.

This would have been done in the late 80s (and I am taking the acknowledgement 
text on trust).

Michael

On 15/12/17, 07:39, "Mario Castelán Castro"  wrote:

On 14/12/17 12:00, Konrad Slind wrote:
> Maybe you are thinking of the snow-watching latern?
> 
> https://www.cl.cam.ac.uk/archive/mjcg/lantern.html

Maybe. I am not sure, but I think not.

This lantern is very similar to the older logo of HOL.

I think that I recall seeing a photo that is almost identical to the
current logo found in the HOL4 documentation (and it was different from
the snow-watching lantern in this page) but my memory may be failing.

Do you know where the current logo comes from?

Regards and 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] Representation of functions with explicit domain

2017-12-05 Thread Michael.Norrish

I’m afraid it depends.

There are at least three different options.

The obvious one is to use an option type in the range. This makes everything 
very explicit, but can be quite ugly.

Another approach is to just use the normal function space, knowing that you 
will have the intended domain provided “at some distance”.  For example, define 
a monoid type:

  <| carrier : α set; opn : α -> α -> α; id: α |>

The third approach would more explicitly tie the domain into the type 
representing the function value so that you might write

  type_abbrev (“fn”, ``:(α -> β) # (α set)``)

If manipulating such values, you’d end up wanting to define what it means to 
apply these, to compose them etc. I don’t know of any serious attempts to 
follow this sort of approach through.

Michael

On 6/12/17, 08:59, "Mario Castelán Castro"  wrote:

Hello.

Is there some established standard as to how to represent a function 
with a domain that may be smaller than the type? More specifically, I 
need a representation of arbitrary products (i.e.: The “tuples” are 
functions from an arbitrary set to the elements of the tuple) to 
formalize theorems about product spaces in topology.

If there does not exists a suitable existing formalization, I have no 
problem writing it myself, but it would be good to re-use existing work 
to avoid wasted time and to have better integration with other (possibly 
future) HOL theories that use functions with explicit domain and 
products of an arbitrary “indexed collection” of sets.

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] Proof about sorting

2017-12-03 Thread Michael.Norrish

I’m pretty confident that your property is a consequence of being SORTED; see 
SORTED_EQ in sortingTheory for example.

You would then need to establish that your function does indeed create lists 
that are SORTED.

Your property0 is also too specific, you shouldn’t require pop = mySort pop.

Michael

From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 14:38
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol4_QA 
Subject: Re: Re: [Hol-info] Proof about sorting


Hi Michael,

I have been seen these documents before, but there is no theorem same to which 
I wanted. Also, I try to use QSORT to prove the property1 which same as 
property0, as follows:

!xs. EVERY (\y. HD (QSORT (\x. $<= x) xs) <= y) xs
Induct >-
   RW_TAC list_ss [] >>
RW_TAC list_ss [listTheory.EVERY_DEF,QSORT_DEF] >| [
   FULL_SIMP_TAC list_ss [PARTITION_DEF] >>
   Cases_on `xs` >| [
  FULL_SIMP_TAC list_ss [PART_DEF,listTheory.EVERY_DEF] >>
  `l1 = []` by RW_TAC std_ss [] >>
  `l2 = []` by RW_TAC std_ss [] >>
  FULL_SIMP_TAC list_ss [QSORT_DEF],
  ……

(*Here,I think I need to prove any elements in l1 are smaller than h firstly, 
then to prove HD [x++y++z] = HD [x], so I can prove this subgoal. 
Unfortunately, I am failed*)

In addition, I think the definition about sorting(i.e. mergesortN_curried_def, 
QSORT_curried_DEF, QSORT3_curried_DEF etc.) in mergesortTheory and 
sortingTheory is different from mine. Even if I proved property1, I still can't 
prove property0.

Regards,

Liu


-Original Messages-
From:michael.norr...@data61.csiro.au
Sent Time:2017-12-04 11:03:39 (Monday)
To: 2015200...@mail.buct.edu.cn, hol-info@lists.sourceforge.net
Cc:
Subject: Re: [Hol-info] Proof about sorting
There are proofs that quick-sort and merge-sort are correct in the distribution 
already.  Perhaps looking at these examples in src/sort will give you some 
clues.

Michael

From: Liu Gengyang 
<2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 13:02
To: hol4_QA 
>
Subject: [Hol-info] Proof about sorting

Hi,

Recently I am meeting a problem, it has been confusing me a few days, seeking 
for help.

I defined a sorting predicate mySort:

val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
   then (x::h::t)
   else (h::(insert x t)))`;

val mySort_def = Define `
  (mySort [] = []) /\
  (mySort (h::t) = (insert h (mySort t)))`;

EVAL ``mySort [2;4;1;5;3;2]``
> val it = |- mySort [2; 4; 1; 5; 3; 2] = [1; 2; 2; 3; 4; 5] : thm

Now I want to prove the property0: for any pop: list, if it is sorted by 
mySort, the first element in pop will less than or equal to other elements in 
pop.

I try to represent property0 in HOL4, but I meet a question, that is ``mySort 
pop`` isn't a bool term, so I use two ways to solve it:

1, !pop. (pop = mySort pop) ==> EVERY(\x. (HD pop) <= x) pop

2, !pop. EVERY (\x. HD (mySort pop) <= x) (mySort pop)

However, I can't prove both of them. When I used the Induct tactic to `pop` or 
`mySort pop`, the goal will be more and more complex, and the property0 can't 
reflect in the proving process, it seems unsolvable. Does the representation of 
1 and 2 is wrong, or the definition of mySort is wrong too？How can I prove the 
property0?

By the way, I prove 3 property about mySort and insert during I prove 1 and 2.

val INSNOTNULL_POP = prove(``!h pop.insert h pop <> []``,
RW_TAC std_ss [] >>
Cases_on `pop` >-
  RW_TAC list_ss [insert_def] >>
RW_TAC list_ss [insert_def]);
val SORTNOTNULL_POP = prove(``!pop. pop <> [] ==> mySort pop <> [] /\ (mySort 
pop= insert (HD pop) (mySort (TL pop)))``,
RW_TAC list_ss [] >| [
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP],
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def]
]);
val SORTNULL_POP = prove(``!pop. (pop = []) <=>(mySort pop = [])``,
GEN_TAC >>
EQ_TAC >-
  RW_TAC list_ss [mySort_def] >>
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def] >>
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def,insert_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP]);

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

Re: [Hol-info] Proof about sorting

2017-12-03 Thread Michael.Norrish

There are proofs that quick-sort and merge-sort are correct in the distribution 
already.  Perhaps looking at these examples in src/sort will give you some 
clues.

Michael

From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Monday, 4 December 2017 at 13:02
To: hol4_QA 
Subject: [Hol-info] Proof about sorting

Hi,

Recently I am meeting a problem, it has been confusing me a few days, seeking 
for help.

I defined a sorting predicate mySort:

val insert_def = Define `
(insert x [] = [x]) /\
(insert x (h::t) = if x <= h
   then (x::h::t)
   else (h::(insert x t)))`;

val mySort_def = Define `
  (mySort [] = []) /\
  (mySort (h::t) = (insert h (mySort t)))`;

EVAL ``mySort [2;4;1;5;3;2]``
> val it = |- mySort [2; 4; 1; 5; 3; 2] = [1; 2; 2; 3; 4; 5] : thm

Now I want to prove the property0: for any pop: list, if it is sorted by 
mySort, the first element in pop will less than or equal to other elements in 
pop.

I try to represent property0 in HOL4, but I meet a question, that is ``mySort 
pop`` isn't a bool term, so I use two ways to solve it:

1, !pop. (pop = mySort pop) ==> EVERY(\x. (HD pop) <= x) pop

2, !pop. EVERY (\x. HD (mySort pop) <= x) (mySort pop)

However, I can't prove both of them. When I used the Induct tactic to `pop` or 
`mySort pop`, the goal will be more and more complex, and the property0 can't 
reflect in the proving process, it seems unsolvable. Does the representation of 
1 and 2 is wrong, or the definition of mySort is wrong too？How can I prove the 
property0?

By the way, I prove 3 property about mySort and insert during I prove 1 and 2.

val INSNOTNULL_POP = prove(``!h pop.insert h pop <> []``,
RW_TAC std_ss [] >>
Cases_on `pop` >-
  RW_TAC list_ss [insert_def] >>
RW_TAC list_ss [insert_def]);
val SORTNOTNULL_POP = prove(``!pop. pop <> [] ==> mySort pop <> [] /\ (mySort 
pop= insert (HD pop) (mySort (TL pop)))``,
RW_TAC list_ss [] >| [
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP],
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def]
]);
val SORTNULL_POP = prove(``!pop. (pop = []) <=>(mySort pop = [])``,
GEN_TAC >>
EQ_TAC >-
  RW_TAC list_ss [mySort_def] >>
Induct_on `pop` >-
  RW_TAC list_ss [] >>
RW_TAC list_ss [mySort_def] >>
Cases_on `pop` >-
  RW_TAC list_ss [mySort_def,insert_def] >>
RW_TAC list_ss [mySort_def,INSNOTNULL_POP]);

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

[Hol-info] FW: A problem of derivation

2017-11-08 Thread Michael.Norrish



From: "Norrish, Michael (Data61, Acton)" 
Date: Thursday, 9 November 2017 at 14:15
To: Liu Gengyang <2015200...@mail.buct.edu.cn>
Subject: Re: [Hol-info] A problem of derivation

Use the theorem SQRT_POW_2.  E.g.:

Q.prove(
  `!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`,
  simp[transcTheory.SQRT_POW_2, realTheory.REAL_LE_POW2, 
realTheory.REAL_LE_ADD]);

Michael

From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Thursday, 9 November 2017 at 14:07
To: hol4_QA 
Subject: [Hol-info] A problem of derivation

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

Re: [Hol-info] Can the simplifier from simpLib normalize symmetric relations?

2017-10-30 Thread Michael.Norrish

In these situations, the simplifier detects the potential loop and only 
rewrites if the resulting term is smaller than the original in some 
well-founded order.

Michael

On 31/10/17, 04:30, "Mario Castelán Castro"  wrote:

On 29/10/17 16:18, michael.norr...@data61.csiro.au wrote:
> Passing the theorem EQ_SYM_EQ will normalise this sort of thing:

Thanks.

Before your answer thought that would loop but it does not.

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

Re: [Hol-info] build failed with latest HOL

2017-10-29 Thread Michael.Norrish

That’s a Poly/ML bug.  Please use the 5.7 release available at

  https://github.com/polyml/polyml/archive/v5.7.tar.gz

Michael

From: Waqar Ahmad via hol-info 
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 28 October 2017 at 18:13
To: hol-info 
Subject: [Hol-info] build failed with latest HOL

Hi all,
I'm installing the latest HOL (Github version) in Ubuntu. The installation of 
the polyml v5.7.1 went successfully. However, the building of HOL failed with 
following error message:

waqar@waqar-VirtualBox:~/Downloads/HOL/HOL$ bin/build
*** Using kernel option -stdknl from earlier build command;
use -expk, -otknl, or -stdknl to override
*** Using -j 2 from earlier build command; use -j to override
Cleaning out /home/waqar/Downloads/HOL/HOL/sigobj
/home/waqar/Downloads/HOL/HOL/sigobj cleaned
*** Build log exists; new logging will concatenate onto this file
Building directory tools/mlyacc/mlyacclib [28 اكتوبر, 11:36:46]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML/poly [28 اكتوبر, 11:36:49]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML [28 اكتوبر, 11:37:03]
FunctionalRecordUpdate.sml   OK
GetOpt.sig   OK
GetOpt.sml   OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/portableML/monads [28 اكتوبر, 11:37:32]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/prekernel [28 اكتوبر, 11:37:41]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/0 [28 اكتوبر, 11:38:01]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/postkernel [28 اكتوبر, 11:38:11]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/parse [28 اكتوبر, 11:38:21]
base_lexer.sml   OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/opentheory [28 اكتوبر, 11:39:29]
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/bool [28 اكتوبر, 11:39:33]
boolTheory   OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/1 [28 اكتوبر, 11:39:49]
DiskFiles.lex.smlOK
DiskFiles.grm-sig.sml DiskFiles.grm.sml  OK
DiskFiles.grm-sig.sml DiskFiles.grm.sml  OK
ConseqConvTheory OK
Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj
Building directory src/proofman [28 اكتوبر, 11:41:00]
/home/waqar/Downloads/HOL/HOL/bin/hol.state0FAILED!
 error in quse /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec.sml : Fail 
"Exception- InternalError: codeToPRegRev raised while compiling"
 error in load /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec : Fail "Exception- 
InternalError: codeToPRegRev raised while compiling"
 error in load boolLib : Fail "Exception- InternalError: codeToPRegRev raised 
while compiling"
 Exception- InternalError: codeToPRegRev raised while compiling

Build failed in directory /home/waqar/Downloads/HOL/HOL/src/proofman (exited 
with code 1)

 I wonder whether this error is due to polyml or HOL.. Can anybody help me in 
fixing this issue?

--
Waqar Ahmed, Ph.D.
System Analysis and Verification  (SAVe) Lab
School of Electrical Engineering and Computer Science (SEECS)
National University of Science and Technology (NUST), H-12, Islamabad, Pakistan
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/

[http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
--
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 define term-like multi-recursive structures?

2017-10-29 Thread Michael.Norrish

You would have to define every function in terms of “fix” and then come up with 
a clause for the new constant using “Fix” as well (or prove a new “axiom” for 
the type).  You would also need to prove new induction and cases theorems.  But 
yes, this “cheap approach” might be doable.

Michael

On 28/10/17, 02:39, "Chun Tian"  wrote:


> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian  
ha scritto:
> 
> Thanks for your comments.
> 
> If I quotient [1] the original CCS datatype into another one, I could 
expect to have the a “fix” constructor with a finite map, right?
> 
> On the the other side, what if I directly define another similar 
constant, say “Fix” in this form:
> 
> |- Fix fm X = fix (alist_to_fmap ls) X

Sorry, it should be:

|- Fix fm X = fix (fmap_to_alist fm) X

> 
> And in all theorems I only use “Fix”. Is this possible (as a cheap 
solution) for resolving the “structural congruences” issue?
> 
> Regards,
> 
> Chun Tian
> 
> [1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic. 
preparation; draft available at http://www cis …. (1969).



--
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] Can the simplifier from simpLib normalize symmetric relations?

2017-10-29 Thread Michael.Norrish

Passing the theorem EQ_SYM_EQ will normalise this sort of thing:

> EQ_SYM_EQ;
val it =
   |- ∀x y. x = y ⇔ y = x:
   thm
> SIMP_CONV (srw_ss()) [EQ_SYM_EQ] “a = b ∧ x = z ⇔ b = a ∧ x = z”;
<>
val it =
   |- (a = b ∧ x = z ⇔ b = a ∧ x = z) ⇔ T:
   thm

Michael

On 29/10/17, 02:58, "Mario Castelán Castro"  wrote:

Sometimes I have a goal of the form “P = Q” where P and Q are terms that
are the same except for the order of the arguments of a symmetric
relation, e.g. (in this case equality): “a = b ∧ x = z ⇔ b = a ∧ x = z”.

Can these sub-terms be normalized by SIMP_TAC analogous to how it can
normalize associative and commutative functions?.

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

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-26 Thread Michael.Norrish

Using alists rather than finite-maps will have the issue that

  fix [(X, a + Y); (Y, b + X)] X

will be seen as different to

fix [(Y, b + X); (X, a + Y)] X

when you might prefer them to be syntactically identical, but there are so many 
“structural congruences” in this syntax that having to deal with one more 
perhaps won’t be such a big deal.

And of course, you could try quotienting it up to all those identities….

Michael

From: "Chun Tian (binghe)" 
Date: Thursday, 26 October 2017 at 21:00
To: "Norrish, Michael (Data61, Acton)" 
Cc: hol-info 
Subject: Re: [Hol-info] How to define term-like multi-recursive structures?

Hi again,

I'm surprised that, ``('a, 'b) alist`` (or ``('a # 'b) list``) is supported by 
datatype package. So I'm going to have the following datatype in the future:

val _ = Datatype `CCS = nil
 | var 'a
 | prefix ('b Action) CCS
 | sum CCS CCS
 | par CCS CCS
 | restr (('b Label) set) CCS
 | relab CCS ('b Relabeling)
 | fix (('a # CCS) list) 'a `;

I wanted to use finite_map (learnt from Konrad Slind) but datatype package 
doesn't support it, however alist is a prefect replacement.

Thus I would say my question can be closed, if there's no other suggestions.

Regards,

Chun Tian

On Thu, Oct 26, 2017 at 10:56 AM, Chun Tian (binghe) 
> wrote:
Let me describe the problem again: (actually I have a candidate solution)

The central idea in the CCS grammar designed by Robin Milner is to use 
inductively defined finite structures to represent potential infinite 
structures. If I have the following equation of CCS:

X = a + X

The only solution would be an infinite sum of a:

X = a + a + a + ...

But we don't really need the infinite sum as part of CCS grammar, we can write 
this form instead:

rec X (a + var X)

So the "equation with single variable" itself can be treated as a CCS process.  
 But if I have multi-variable equations:

X = a + Y
Y = b + X

the solution should be:

X = a + b + a + b + ...
Y = b + a + b + a + ...

to represent the equation itself as a CCS process, I should at least put the 
following "fix" constructor into the datatype:

fix ('a list) (CCS list) 'a

so that I can write a term

``fix [X; Y] [a + var Y; b + var X] X``

which means "the value of X in the equation group in which X and Y are unknown 
variables".  But if I write only partially:

``fix [X; Y] [a + var Y; b + var X]``

above term should have the type ``:'a -> ('a, 'b) CCS``, which works like a 
choice function, given any variable it returns the corresponding value of that 
variable.

In my initial question, I wanted to put only ``fix ('a list) (CCS list)`` into 
the CCS datatype, and that was wrong because the type of ``fix ('a list) (CCS 
list)`` is not CCS, but (CCS list).

Can you see a better way to have a similar datatype?

Regards,

Chun Tian

On Thu, Oct 26, 2017 at 1:20 AM, 
> wrote:
I’m not sure why you say that you can’t add “fix” to the datatype declaration.

A line like

   | fix (CCS list)

would be accepted by Datatype.  Then the type of the constructor “fix” would be

  fix : ('a,'b) CCS list -> ('a,'b) CCS

In short, I don't understand why you write "the type of ``fix …`` is *not* CCS 
at all".

If your underlying constructors don't allow for "infinite" CCS terms (or their 
encoding), then it's hard to know how you would ever define the sorts of CCS 
constants that have infinite behaviours in time.  Perhaps one approach would be 
to define the syntax as a co-datatype, allowing the syntax itself to be 
infinite.  This'd be a bit weird though…

Michael

From: "Chun Tian (binghe)" >
Date: Thursday, 26 October 2017 at 00:05
To: hol-info 
>
Subject: [Hol-info] How to define term-like multi-recursive structures?

Hi,

sorry for keeping asking questions.  In my current CCS datatype, there's a 
recursive constructor:

val _ = Datatype `CCS = nil
 | var 'a
...
 | rec 'a CCS `;

A term ``rec X (f (var X))`` is like the solution of an equation X = f(X), or 
the fixed-point of f(), and its behavior is then defined by a set of rules.  
What the Datatype package gives me, is to make sure "rec" and "var" are kind of 
*primitive* constants, such that they're part of the one_one and distinctness 
theorems of the CCS. (if I simply define a constant outside of the datatype, I 
don't have such benefits at all, and many theorems will not be proved)

Now  (as a long-term plan) I want to implement the ultimate, original form of 
Milner's CCS [1], in which there's a "fix" (fixed-point) constructor.  It's 
like a multi-variable version of above "rec" costructor, something like:

fix X p1 Y p2 Z p3 ...

If you think above term as a

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-25 Thread Michael.Norrish

I’m not sure why you say that you can’t add “fix” to the datatype declaration.

A line like

   | fix (CCS list)

would be accepted by Datatype.  Then the type of the constructor “fix” would be

  fix : ('a,'b) CCS list -> ('a,'b) CCS

In short, I don't understand why you write "the type of ``fix …`` is *not* CCS 
at all".

If your underlying constructors don't allow for "infinite" CCS terms (or their 
encoding), then it's hard to know how you would ever define the sorts of CCS 
constants that have infinite behaviours in time.  Perhaps one approach would be 
to define the syntax as a co-datatype, allowing the syntax itself to be 
infinite.  This'd be a bit weird though…

Michael 

From: "Chun Tian (binghe)" 
Date: Thursday, 26 October 2017 at 00:05
To: hol-info 
Subject: [Hol-info] How to define term-like multi-recursive structures?

Hi, 

sorry for keeping asking questions.  In my current CCS datatype, there's a 
recursive constructor:

val _ = Datatype `CCS = nil
     | var 'a
...
     | rec 'a CCS `;

A term ``rec X (f (var X))`` is like the solution of an equation X = f(X), or 
the fixed-point of f(), and its behavior is then defined by a set of rules.  
What the Datatype package gives me, is to make sure "rec" and "var" are kind of 
*primitive* constants, such that they're part of the one_one and distinctness 
theorems of the CCS. (if I simply define a constant outside of the datatype, I 
don't have such benefits at all, and many theorems will not be proved)

Now  (as a long-term plan) I want to implement the ultimate, original form of 
Milner's CCS [1], in which there's a "fix" (fixed-point) constructor.  It's 
like a multi-variable version of above "rec" costructor, something like:

fix X p1 Y p2 Z p3 ...

If you think above term as a multi-variable equation groups, then each part in 
its solution will be defined as a valid CCS term.  Such a "solution" (as a 
container of CCS terms) may be represented as a finite_map ``:('a |-> ('a, 'b) 
CCS)`` or simply a list ``:('a, 'b) CCS list``.

Obviously I can't put this "fix" directly into the definition of above CCS 
datatype (let's assume HOL4 can do support nesting recursive datatype), because 
the type of ``fix ...`` is *not* CCS at all.   But what is it if I want such a 
constant? some kind of specification?

Regards,

Chun Tian

-- 
Chun Tian (binghe)
University of Bologna (Italy)

[1] Milner, R.: Operational and Algebraic Semantics of Concurrent Processes. 
1–41 (2017).



--
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] LRTC (Reflexive Transitive Closure with a List)

I’m afraid I can’t now remember if someone has already pointed this out, but I 
think you probably should use the theory of “paths” for this sort of thing.

See the description in the DESCRIPTION manual, and the theory itself in src/path

Michael

From: "Chun Tian (binghe)" 
Date: Thursday, 5 October 2017 at 23:35
To: hol-info 
Subject: [Hol-info] LRTC (Reflexive Transitive Closure with a List)

Hi,

In listTheory there's a concept called "LRC":

(* --
LRC
  Where NRC has the number of steps in a transitive path,
  LRC has a list of the elements in the path (excluding the rightmost)
   -- *)

val LRC_def = Define`
  (LRC R [] x y = (x = y)) /\
  (LRC R (h::t) x y =
   (x = h) /\ ?z. R x z /\ LRC R t z y)`;

But I think a more useful similar concept should be a Reflexive Transitive 
Closure which is able to remember all the transition labels in a relation R (of 
type 'a -> 'b -> 'a -> bool), that is:

val LRTC_DEF = new_definition ("LRTC_DEF",
  ``LRTC (R :'a -> 'b -> 'a -> bool) a l b =
  !P. (!x. P x [] x) /\
  (!x h y t z. R x h y /\ P y t z ==> P x (h :: t) z) ==> P a l b``);

For example, if we have a relation R and things like P --a--> Q, Q --b--> R,  
the resulting closure (LRTC R) can be used to describe P --[a;b]--> R.

Following a similar path with RTC in relationTheory, I can prove the following 
basic theorems:

   [LRTC0_NO_TRANS]  Theorem

  |- ∀R x y. LRTC R x [] y ⇔ (x = y)

   [LRTC_CASES1]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   if NULL l then x = y else ∃u. R x (HD l) u ∧ LRTC R u (TL l) y

   [LRTC_CASES2]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   if NULL l then x = y
   else ∃u. LRTC R x (FRONT l) u ∧ R u (LAST l) y

   [LRTC_CASES_LRTC_TWICE]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   ∃u l1 l2. LRTC R x l1 u ∧ LRTC R u l2 y ∧ (l = l1 ⧺ l2)

   [LRTC_INDUCT]  Theorem

  |- ∀R P.
   (∀x. P x [] x) ∧
   (∀x h y t z. R x h y ∧ P y t z ⇒ P x (h::t) z) ⇒
   ∀x l y. LRTC R x l y ⇒ P x l y

   [LRTC_LRTC]  Theorem

  |- ∀R x m y. LRTC R x m y ⇒ ∀n z. LRTC R y n z ⇒ LRTC R x (m ⧺ n) z

   [LRTC_REFL]  Theorem

  |- ∀R. LRTC R x [] x

   [LRTC_RULES]  Theorem

  |- ∀R.
   (∀x. LRTC R x [] x) ∧
   ∀x h y t z. R x h y ∧ LRTC R y t z ⇒ LRTC R x (h::t) z

   [LRTC_SINGLE]  Theorem

  |- ∀R x t y. R x t y ⇒ LRTC R x [t] y

   [LRTC_STRONG_INDUCT]  Theorem

  |- ∀R P.
   (∀x. P x [] x) ∧
   (∀x h y t z. R x h y ∧ LRTC R y t z ∧ P y t z ⇒ P x (h::t) z) ⇒
   ∀x l y. LRTC R x l y ⇒ P x l y

   [LRTC_TRANS]  Theorem

  |- ∀R x m y n z. LRTC R x m y ∧ LRTC R y n z ⇒ LRTC R x (m ⧺ n) z

Is this something general enough for putting into, say, rich_listTheory? (or 
has anyone already done a similar development?)

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

Re: [Hol-info] res_quanLib and res_quanTools are exact duplicates

Agreed: let’s keep Lib and ditch Tools.

Thanks,
Michael

On 21/10/17, 03:12, "Mario Castelán Castro"  wrote:

res_quanLib and res_quanTools are exact duplicates. Is there some reason
to have both of these structures instead of just one? If not, then which
one should be keep? The most followed convention (according to the HTML
manual “HOLindex.html”) would dictate that “res_quanLib” is the
preferred name (as in “boolLib”, not “boolTools”).

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

Re: [Hol-info] Small question about sqrt

Square root is unspecified on numbers < 0, so you don’t know that there is not 
a negative number whose square root is 0.

Michael

From: Liu Gengyang <2015200...@mail.buct.edu.cn>
Date: Saturday, 21 October 2017 at 00:05
To: hol4_QA 
Subject: [Hol-info] Small question about sqrt

Hi,

I want to prove the goal: !x. (sqrt x = 0) ==> (x = 0) as below,

RW_TAC realLib.real_ss [] >>
`sqrt 0 = 0` by RW_TAC realLib.real_ss [transcTheory.SQRT_0]

The result is:
x = 0

  0.  sqrt x = 0
  1.  sqrt 0 = 0

I think it is obvious, but I can'n prove it by rewrite or simplify tactic.

However, if the goal is: !x. x>=0 /\ (sqrt x = 0) ==> (x = 0), I can prove it 
as below:

RW_TAC std_ss [] >>
`sqrt x pow 2 = 0 pow 2` by RW_TAC std_ss [] >>
`0 <= x` by RW_TAC std_ss [realTheory.real_ge] >-
RW_TAC std_ss [GSYM realTheory.real_ge] >>
FULL_SIMP_TAC realLib.real_ss [transcTheory.SQRT_POW_2]

So, what the problem about the first goal?

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

Re: [Hol-info] Spurious parent theories