Re: [Hol-info] HOL4-Emacs Problem

[Norrish, Michael (Data61, Acton)]

Your version of emacs is too old.  (The code certainly works on emacs 26.3.)  

Can you report what you get when you do a
  
  M-x emacs-version

so I can try to adjust the elisp code to cope with older versions?

Alternatively, try

 sudo apt install emacs26

Best wishes,
Michael

On 17/3/21, 09:17, "Elif Deniz"  wrote:

Dear all,

I have a problem while using emacs after installation HOL4 as following:

"Symbol's function definition is void: if let*"

When I want to run HOL4 (polyml5.7.1 or polyml5.8.1, kananaskis-13 or  
kananaskis-14) on Ubuntu 16 or Ubuntu 18  which is already all  
correctly installed. But, when I run HOL4 in emacs, I got above  
notification.

Could anyone help me please how can I fix this problem?

Thanks in advance!

Sincerest appreciation,
Elif



___
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] Abstract algebra in HOL4 and Isabelle/HOL – Re: Abstract algebra in HOL4 – Re: Release notes for HOL4, Kananaskis-14

[Norrish, Michael (Data61, Acton)]

`);
mult:'a -> 'a -> 'a
   |>`;
*)
val _ = type_abbrev ("group", Type `:'a monoid`);

(* Define Group by Monoid *)
val Group_def = Define`
  Group (g:'a group) <=>
Monoid g /\ (G* = G)
`;

https://bitbucket.org/jhlchan/hol/src/master/algebra/group/group.hol (February 
5, 2021)


Quote from monoid.hol:

(* - *)
(* Monoid Documentation  *)
(* - *)
(* Data type:
   The generic symbol for monoid data is g.
   g.carrier = Carrier set of monoid, overloaded as G.
   g.op  = Binary operation of monoid, overloaded as *.
   g.id<http://g.id>  = Identity element of monoid, overloaded as #e.

   Overloading:
   *  = g.op
   #e = g.id<http://g.id>
   ** = g.exp
   G  = g.carrier
   GITSET g s b   = ITSET g.op s b
*)
(* Definitions and Theorems (# are exported):

   Definitions:
   Monoid_def|- !g. Monoid g <=>
(!x y. x IN G /\ y IN G ==> x * y IN G) /\
(!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * 
y) * z = x * (y * z))) /\
#e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * 
#e = x))
[...]

(* - *)
(* Monoid Definition.*)
(* - *)

(* Monoid and Group share the same type *)

(* Set up monoid type as a record
   A Monoid has:
   . a carrier set (set = function 'a -> bool, since MEM is a boolean function)
   . a binary operation (2-nary function) called multiplication
   . an identity element for the binary operation
*)
val _ = Hol_datatype`
  monoid = <| carrier: 'a -> bool;
   op: 'a -> 'a -> 'a;
   id: 'a
|>`;
[...]

(* Using symbols m for monoid and g for group
   will give excessive overloading for Monoid and Group,
   so the generic symbol for both is taken as g. *)
(* set overloading  *)
val _ = overload_on ("*", ``g.op``);
val _ = overload_on ("#e", ``g.id<http://g.id>``);
val _ = overload_on ("G", ``g.carrier``);

(* Monoid Definition:
   A Monoid is a set with elements of type 'a monoid, such that
   . Closure: x * y is in the carrier set
   . Associativity: (x * y) * z = x * (y * z))
   . Existence of identity: #e is in the carrier set
   . Property of identity: #e * x = x * #e = x
*)
(* Define Monoid by predicate *)
val Monoid_def = Define`
  Monoid (g:'a monoid) <=>
(!x y. x IN G /\ y IN G ==> x * y IN G) /\
(!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * y) * z = x * (y * z))) /\
#e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * #e = x))
`;

https://bitbucket.org/jhlchan/hol/src/master/algebra/monoid/monoid.hol 
(February 5, 2021)


Quote from bossLib.Hol_datatype.html:

Hol_datatype : hol_type quotation -> unit

STRUCTURE
bossLib

SYNOPSIS
Define a concrete datatype (deprecated syntax).

DESCRIPTION
The Hol_datatype function provides exactly the same definitional power as the 
Datatype function (which see), with a slightly different input syntax, given 
below:
   spec::= [  ; ]* 

   binding ::=  = [  | ]* 
|   = <| [  :  ; ]*  :  |>

   clause  ::= 
|   of [ => ]* 

https://hol-theorem-prover.org/kananaskis-14-helpdocs/help/Docfiles/HTML/bossLib.Hol_datatype.html
 (February 5, 2021)


Quote from bossLib.Datatype.html:

Datatype : hol_type quotation -> unit

STRUCTURE
bossLib

SYNOPSIS
Define a concrete datatype.

DESCRIPTION
Many formalizations require the definition of new types. For example, ML-style 
datatypes are commonly used to model the abstract syntax of programming 
languages and the state-space of elaborate transition systems. In HOL, such 
datatypes (at least, those that are inductive, or, alternatively, have a model 
in an initial algebra) may be specified using the invocation Datatype ``, 
where  should conform to the following grammar:
   spec::= [  ; ]* 

   binding ::=  = [  | ]* 
|   = <| [  :  ; ]*  :  |>

   clause  ::=  *

   tyspec  ::= (  )
    |  

where  is a single token denoting a type. For example, num, bool 
and 'a.

https://hol-theorem-prover.org/kananaskis-14-helpdocs/help/Docfiles/HTML/bossLib.Datatype.html
 (February 5, 2021)



Am 03.02.2021 um 23:29 schrieb Norrish, Michael (Data61, Acton) 
mailto:michael.norr...@data61.csiro.au>>:

Hing Lun Chan’s thesis (linked to in the notes below) provides pretty good 
documentation of the approach taken, as do the various papers arising from the 
work.

The short version of the story is that the “obvious” ap

Re: [Hol-info] Abstract algebra in HOL4 – Re: Release notes for HOL4, Kananaskis-14

[Norrish, Michael (Data61, Acton)]

Hing Lun Chan’s thesis (linked to in the notes below) provides pretty good 
documentation of the approach taken, as do the various papers arising from the 
work.

The short version of the story is that the “obvious” approach of working with a 
polymorphic type-variable to represent the type of group elements doesn’t make 
the task of proving the required results too arduous.

Michael



On 4 Feb 2021, at 01:13, Ken Kubota 
mailto:m...@kenkubota.de>> wrote:

Is there any documentation on how abstract algebra is implemented in HOL4?
Usually the HOL type system is considered too weak.

Freek Wiedijk: “The HOL type system is too poor. As we already argued in the 
previous section, it is too weak to properly do abstract algebra.”
John Harrison, Josef Urban, and Freek Wiedijk: “Another limitation of the 
simple HOL type system is that there is no explicit quantifier over polymorphic 
type variables, which can make many standard results [...] awkward to express 
[...]. [...] For example, in one of the most impressive formalization efforts 
to date [Gonthier et al., 2013] the entire group theory framework is developed 
in terms of subsets of a single universe group, apparently to avoid the 
complications from groups with general and possibly heterogeneous types.”
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00074.html

Kind regards,

Ken Kubota



Ken Kubota
https://doi.org/10./100



Am 03.02.2021 um 03:47 schrieb Norrish, Michael (Data61, Acton) 
mailto:michael.norr...@data61.csiro.au>>:

Release notes for HOL4, Kananaskis-14

(Released: 3 February 2021)

We are pleased to announce the Kananaskis-14 release of HOL4.

New examples:

  *   algebra: an abstract algebra library for HOL4. The algebraic types are 
generic, so the library is useful in general. The algebraic structures consist 
of monoidTheory for monoids with identity, groupTheory for groups, ringTheory 
for commutative rings, fieldTheory for fields, polynomialTheory for polynomials 
with coefficients from rings or fields, linearTheory for vector spaces, 
including linear independence, and finitefieldTheory for finite fields, 
including existence and uniqueness.


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

[Hol-info] Release notes for HOL4, Kananaskis-14

[Norrish, Michael (Data61, Acton)]

Release notes for HOL4, Kananaskis-14

(Released: 3 February 2021)

We are pleased to announce the Kananaskis-14 release of HOL4.

Contents

  *   New 
features
  *   Bugs 
fixed
  *   New 
theories
  *   New 
tools
  *   New 
Examples
  *   
Incompatibilities

New features:

  *   The special Type syntax for making type abbreviations can now map to 
temp_type_abbrev (or temp_type_abbrev_pp) by adding the local attribute to the 
name of the abbreviation.

For example

   Type foo[local] = “:num -> bool # num”

or

   Type foo[local,pp] = “:num -> bool # num”

Thanks to Magnus Myreen for the feature suggestion.

  *   We have added a special syntactic form Overload to replace various 
flavours of overload_on calls. The core syntax is exemplified by

   Overload foo = “myterm”

Attributes can be added after the name. Possible attributes are local (for 
overloads that won’t be exported) and inferior to cause a call 
inferior_overload_on (which makes the overload the pretty-printer’s last 
choice).

Thanks to Magnus Myreen for the feature suggestion.

  *   The Holmake tool will now build multiple targets across multiple 
directories in parallel. Previously, directories were attacked one at a time, 
and parallelisation only happened within those directories. Now everything is 
done at once. The existing -r option takes on a new meaning as part of this 
change: it now causes Holmake to build all targets in all directories 
accessible through INCLUDESdirectives. Without -r, Holmake will build just 
those dependencies necessary for the current set of targets (likely 
files/theories in the current directory).

  *   It is now possible to write let-expressions more smoothly inside monadic 
do-od blocks. Rather than have to write something like

   do
 x <- M1;
 let y = E
 in
   do
 z <- M2 x y;
 return (f z);
   od
   od

one can replace the let-bindings with uses of the <<- arrow:

   do
 x <- M1;
 y <<- E;
 z <- M2 x y;
 return (f z)
   od

(The <<- line above is semantically identical to writing y <- return E, but is 
nonetheless syntactic sugar for a let-expression.)

The pretty-printer reverses this transformation.

Thanks to Hrutvik Kanabar for the implementation of this feature.

  *   There is (yet) another high-level simplification entry-point: gs 
(standing for “global simplification”). Like the others in this family this has 
type

   thm list -> tactic

and interprets theorems as rewrites as with the others. This tactic simplifies 
all of a goal by repeatedly simplifying goal assumptions in turn (assuming all 
other assumptions as it goes) until no change happens, and then finishes by 
simplifying the goal conclusion, assuming all of the (transformed) assumptions 
as it does so.

There are three variants on this base (with the same type): gns, gvs and gnvs. 
The presence of the vindicates a tactic that eliminates variables (as is done 
by rw and some others), and the presence of the n causes assumptions to not be 
stripped as they are added back into the goal. Stripping (turned on by default) 
is the effect behind strip_assume_tac (and strip_tac) when these tactics add to 
the assumptions. It causes, for example, case-splits when disjunctions are 
added.

We believe that gs will often be a better choice than the existing fs and rfs 
tactics.

  *   Automatic simplification of multiplicative terms over the real numbers is 
more aggressive and capable. Multiplicative terms are normalised, with 
coefficients being gathered, and variables sorted and grouped (e.g., z * 2 * x 
* 3 turns into 6 * (x * z)). In addition, common factors are eliminated on 
either side of relation symbols (<, ≤, and =), and occurrences of inv (⁻¹) and 
division are rearranged as much as possible (e.g., z * x pow 2 * 4 = x⁻¹ * 6 
turns into x = 0 ∨ 2 * (x pow 3 * z) = 3). To turn off normalisation over 
relations within a file, use

   val _ = diminish_srw_ss [“RMULRELNORM_ss”]

To additionally stop normalisation, use

   val _ = diminish_srw_ss [“RMULCANON_ss”]

These behaviours can also be turned off in a more fine-grained way by using 
Excl invocations.

  *   The Induct_on tactic is now more generous in the goals it will work on 
when inducting on an inductively defined relation. For example, if one’s goal 
was

   ∀s t. FINITE (s ∪ t) ∧ s ⊆ t ⇒ some-concl

and the aim was to do an induction using the principle associated with 
finite-ness’s inductive characterisation, one had to manually turn the goal 
into something like

   ∀s0. FINITE s0 ==> ∀s t. s0 = s ∪ t ∧ s ⊆ t ⇒ some-concl

before applying Induct_on ‘FINITE’.

Now, Induct_on does the necessary transformations first itself.

  *   The Inductive and CoInductive syntaxes now support labelling of specific 
rules. The supported syntax involves names in square brackets in column 0, as 
per the following:

   Inductive dbeta:
   [~redex:]
 (∀s t. dbeta (dAPP (dABS s) t) (nsub t 0 s)) ∧
   [~appL:]
 (∀s t u. dbeta s 

Re: [Hol-info] HOL4 Datatype recursion on the right hand side of a function arrow

[Norrish, Michael (Data61, Acton)]

I'm afraid your picture of the current state-of-play is entirely accurate. 

I can add the following:

- the tree type that lurks behind Harrison's datatype package already has 
countably infinite branching "for free". (IOW, that's where you have num on the 
left of the arrow.) In HOL4, our port of this code has this defined in 
src/datataype/ind_typeScript.sml. If you wanted infinite branching on a larger 
type (the reals say), this would be a bit fiddlier to set up, but the approach 
in John's paper would be slick. The problem would remain of needing to handle 
the function space functor in the SML code.  Fundamentally, the datatype 
package's assumption is that all nested recursion happens through existing 
algebraic types. That assumption would have to be changed so that the 
recursions are assumed to happen through the equivalent of the LICS paper's 
bounded natural functors. 

- the inftree type is a distraction really; it can be used to help in a manual 
construction of a new type but it depends on lists, so isn't really a good 
basis for a foundational datatype package. 

- there is no ongoing development of anything on this front at the moment 
because there aren't enough hours in the day

Michael

On 4/12/20, 01:48, "Pablo Buiras"  wrote:

Hello everyone,


I was wondering about the status of data type recursion on the right 
hand side of a function arrow in HOL4. For the sake of clarity, this 
would be to add support for a data type such as the following:


test = A (num -> test) | B


As far as I know this is currently not supported by the datatype 
package, and I am aware this issue has been raised a few times before 
[1,2] and is also an issue in the HOL4 GitHub repo [3].


As of 2015, it seems the most direct way of adding this feature was to 
implement the approach found in a LICS 2012 paper [4]. I was not able to 
find any new developments since 2015. Is this still a viable plan or has 
the situation changed in any way? Does anyone know if there are any 
ongoing efforts to implement this?


Previously I found a paper by Harrison [5] in which he claims that it 
would be easy to extend his package to infinitely-branching trees, 
though I think this was never implemented. I found that there is a 
definition of potentially infinitely-branching trees in the HOL4 
repository, under src/datatype/inftree, but it seems this is not used in 
the rest of the package.


I know we could just use an alternative representation and/or manually 
construct the type we need, but this would be quite a hassle in the 
particular application we have in mind, as the development itself is 
exported from another tool.


I’d be grateful for any other pointers you can provide.


Thanks,

Pablo


References

[1] https://sourceforge.net/p/hol/mailman/message/24442904/

[2] 
https://sourceforge.net/p/hol/mailman/hol-developers/thread/B678E335-C741-4F09-8803-187E00BCFD92%40nicta.com.au/#msg34282410

[3] https://github.com/HOL-Theorem-Prover/HOL/issues/266

[4] https://ieeexplore.ieee.org/document/6280479

[5] 
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.115.1474=rep1=pdf



___
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] Visualizing subgoals in a proof script

[Norrish, Michael (Data61, Acton)]

The short answer is "no". 

I'm afraid that working from a script file to do this would require a (more or 
less general purpose) SML parser as our tactics are just functions, and they 
are composed together with other SML functions into one overarching SML value. 
A gross approximation that did parenthesis-aware lexing of the >>/THEN/\\ 
operators might achieve pretty good results in practice however.

For purposes such as this, and others, I'm generally interested in the idea of 
defining a much simpler tactic language (a "DSL" I suppose) that would be 
easier to parse and analyse.

Best wishes,
Michael
 

On 2/8/20, 05:36, "Mario Xerxes Castelán Castro «Ksenia»" 
 wrote:

Hello. In HOL4 is there a way to generate something like the entries in
Metamath proof explorer for the subgoals generated within a proof and
the tactics used to solve them? Example:



___
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] Using @ for multiple selections in HOL Light

[Norrish, Michael (Data61, Acton)]

Maybe use the choice function to select a pair. I.e., write

@(m,c). .

?

Michael

On 19 Feb 2020, at 09:30, "jpe...@student.bham.ac.uk" 
 wrote:


Hi

This is a question about using the select operator @ to return multiple values 
which depend on each other in HOL Light.

For example when working with polynomial_function defined as 
polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i)​  it 
might be useful to be able to use the @ operator to return the upper bound m 
and the coefficient function c, however as the choice of m depends on c and 
visa versa you cannot use 2 separate select statements. (e.g. if m > degree(p) 
then c(n) must be 0 for degree(p)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] grammar for HOL Light terms

[Norrish, Michael (Data61, Acton)]

Every term in HOL can be summarised by the BNF

  term ::= var | const | term @ term | \v. term

where @ is function application (and if you use concrete syntax, you don’t 
write the @), and \v. term represents a lambda-abstraction.   If you want to 
programmatically generate terms, using this view is probably best, particularly 
if you use the standard API calls that help with common cases.

There is a surface syntax that users write, but it’s extensible (users can 
define new infixes, new binders and perhaps new mix-fixes and the like). That 
makes it impossible/hard to generate a grammar for everything that the 
pretty-printer might generate.  On the other hand, the parser will almost 
certainly let you input using the core syntax in such a way that you don’t need 
to worry about the pretty versions.  Thus, you can write

   !x. p x ==> q x

Or

  (!) (\x. (==>) (p x) (q x))

where I’ve had to put parentheses around the ! and the ==> to stop the parser 
from getting confused by the fact that they are also infixes/binders.  There 
are also other issues to do with distinguishing variables from constants, and 
from getting the types of these things to be what you want.

Michael

From: "Miranda, Brando" 
Date: Saturday, 9 November 2019 at 02:50
To: hol-info 
Subject: [Hol-info] grammar for HOL Light terms

Hi,

This is my first message to the HOL list so hope its not out of the rules for 
the list (couldn’t find the rules).

I wanted to find the formal grammar for generating terms (formulas) in HOL 
(Light). I was wondering were I could find such a specification?


Thanks!

Brando



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

Re: [Hol-info] Simplify/normalize propositional logic terms?

[Norrish, Michael (Data61, Acton)]

Of course, it’s possible to be surprised by the behaviour of the simplifier, 
and simplification wrt conjuncts is a bit “out of the ordinary” perhaps, but in 
principle it is no riskier than rewriting wrt assumptions or terms that appear 
to the left of an implication.  E.g., if

  P /\ Q ==> R

induces looping in R because of the P and Q, then the same thing may happen in 
P /\ Q /\ R.

Michael

From: Thomas Sewell 
Date: Tuesday, 1 October 2019 at 18:43
To: hol-info 
Subject: Re: [Hol-info] Simplify/normalize propositional logic terms?

Try this:

SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] `` (q \/ p /\ x) /\ p /\ ~q  ``;

That CONJ_ss just adds a congruence rule that uses each side of a conjunction 
to simplify the other.

I found it by investigating bossLib.csimp, which you might also want to know 
about.

Once upon a time in Isabelle I had a problem with such congruences, since they 
might locally add rewrites which might be looping or inefficient. Is there a 
similar risk in HOL4?

Cheers,
Thomas.

On 2019-09-30 23:49, Konrad Slind wrote:
A couple of places to look in HOLindex: refuteLib and normalForms structure.


On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) 
mailto:binghe.l...@gmail.com>> wrote:
Hi,

it can be proven (by DECIDE_TAC) that,

|- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x

but is there any conversion function available in HOL4 such that from LHS of 
above equation I can directly get the RHS - something like a canonical form?

--Chun



___
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] A possible bug in ext_suminf (extrealTheory)?

[Norrish, Michael (Data61, Acton)]

Fair enough.  It seems clear that this is not a huge problem (using a function 
such as this outside of its intended domain is a bad idea), but on the other 
hand, it also seems clear that needlessly having it return the wrong value is a 
bug. 

Having said all that, getting suminf (\x. -1) to return -1 doesn't seem much of 
a win: the sum of an infinite sequence of -1s is hardly -1.

I think it would be better style to use new_specification so as to avoid giving 
a specific value when the argument is not always positive.

Michael


On 20/9/19, 09:51, "Chun Tian (binghe)"  wrote:

In fact, even for arbitrary functions with both positive and negative 
values, if the partial sum ever reached +/-Inf, further adding finite values on 
the other side cannot “pull” the result back to “normal”. For instance, suppose 
at some moment the partial sum is +inf, adding any normal reals will not change 
it, it’s then not allowed to add -Inf on it, because under the textbook 
definition of `+`, PosInf + NegInf is unspecified.  Thus, in some sense the 
suminf of possible limiting values has a very different behavior with the real 
version.

Chun

Inviato da iPad

> Il giorno 20 set 2019, alle ore 01:33, Chun Tian (binghe) 
 ha scritto:
> 
> Hi,
> 
> The extreal version of `suminf` is only “correct” and equivalent with the 
real version when the involved function is positive - the partial sum is 
mono-increasing. Its relatively simple definition serves the current need (in 
measure and probability theories). Fully mimicking the real version requires a 
(full) porting of seqTheory (and limTheory, netsTheory, eventually 
metricTheory) to extreals, which is an almost impossible task in my opinion.
> 
> Besides, I think it’s also not needed to do so, because if the sum limit 
never reaches +Inf, one can just reduce the work back to the ‘suminf’ of reals. 
On the hand, If the partial sum ever reached +Inf, assuming it’s monotonic, 
then the limit value must be also +Inf, it’s reduced to a finite sum.
> 
> Chun
> 
>> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61, Acton) 
 ha scritto:
>> 
>> The definition of suminf over the reals (in seqTheory) is completely 
different; is it clear that the extreal version can't mimic the original?
>> 
>> Michael
>> 
>> On 18/9/19, 06:18, "Chun Tian (binghe)"  wrote:
>> 
>>   Hi,
>> 
>>   I occasionally found that HOL's current definition of ext_suminf 
(extrealTheory) has a bug:
>> 
>>  [ext_suminf_def]  Definition  
>> ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))
>> 
>>   The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1) 
+  To make the resulting summation "meaningful", all lemmas about 
ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how 
it's used in all applications.  For instance, one lemma says, if f is positive, 
so is `suminf f`:
>> 
>>  [ext_suminf_pos]  Theorem
>> ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
>> 
>>   However, I found that the above lemma can be proved even without 
knowing anything of `f`, see the following proofs:
>> 
>>   Theorem ext_suminf_pos_bug :
>>   !f. 0 <= ext_suminf f
>>   Proof
>>   RW_TAC std_ss [ext_suminf_def]
>>>> MATCH_MP_TAC le_sup_imp'
>>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
>>>> Q.EXISTS_TAC `0` >> BETA_TAC
>>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
>>   QED
>> 
>>   where [le_sup_imp'] is a version of [le_sup_imp] before applying 
IN_APP:
>> 
>>  [le_sup_imp']  Theorem
>> 
>> ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
>> 
>>   For the reason, ext_suminf is actually calculating the sup of the 
following values:
>> 
>>   0
>>   f(0)
>>   f(0) + f(1)
>>   f(0) + f(1) + f(2)
>>   ...
>> 
>>   The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`, 
then SUM_IMAGE f {} = 0.
>> 
>>   Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3 
  But since the sup of a set containing 0 is at least 0, the `suminf f` in 
this case will be 0 (instead of the correct value -1).  This is why `0 <= 
suminf f` holds for whatever f.
>> 
>>   I believe Isabelle's suminf (in Extended_Real.thy) has the same 
problem (but I can't find its definition, correct me if I'm wrong here), i.e. 
the following theorem holds even without the "assumes":
>> 
&

Re: [Hol-info] A possible bug in ext_suminf (extrealTheory)?

[Norrish, Michael (Data61, Acton)]

The definition of suminf over the reals (in seqTheory) is completely different; 
is it clear that the extreal version can't mimic the original?

Michael

On 18/9/19, 06:18, "Chun Tian (binghe)"  wrote:

Hi,

I occasionally found that HOL's current definition of ext_suminf 
(extrealTheory) has a bug:

   [ext_suminf_def]  Definition  
  ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))

The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1) + 
 To make the resulting summation "meaningful", all lemmas about ext_suminf 
assume that (!n. 0 <= f n) (f is positive). This also indeed how it's used in 
all applications.  For instance, one lemma says, if f is positive, so is 
`suminf f`:

   [ext_suminf_pos]  Theorem
  ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

However, I found that the above lemma can be proved even without knowing 
anything of `f`, see the following proofs:

Theorem ext_suminf_pos_bug :
!f. 0 <= ext_suminf f
Proof
RW_TAC std_ss [ext_suminf_def]
 >> MATCH_MP_TAC le_sup_imp'
 >> REWRITE_TAC [IN_IMAGE, IN_UNIV]
 >> Q.EXISTS_TAC `0` >> BETA_TAC
 >> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
QED

where [le_sup_imp'] is a version of [le_sup_imp] before applying IN_APP:

   [le_sup_imp']  Theorem
  
  ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p

For the reason, ext_suminf is actually calculating the sup of the following 
values:

0
f(0)
f(0) + f(1)
f(0) + f(1) + f(2)
...

The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`, then 
SUM_IMAGE f {} = 0.

Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3  
 But since the sup of a set containing 0 is at least 0, the `suminf f` in this 
case will be 0 (instead of the correct value -1).  This is why `0 <= suminf f` 
holds for whatever f.

I believe Isabelle's suminf (in Extended_Real.thy) has the same problem 
(but I can't find its definition, correct me if I'm wrong here), i.e. the 
following theorem holds even without the "assumes":

lemma suminf_0_le:
  fixes f :: "nat ⇒ ereal"
  assumes "⋀n. 0 ≤ f n"
  shows "0 ≤ (∑n. f n)"
  using suminf_upper[of f 0, OF assms]
  by simp

The solution is quite obvious. I'm going to fix HOL's definition of 
ext_suminf with the following one:

val ext_suminf_def = Define
   `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;

That is, using `SUC n` intead of `n` to eliminate the fake base case (0). I 
believe this change only causes minor incompatibilities.

Any comment?

Regards,

Chun Tian




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

Re: [Hol-info] 0 / 0 = 0 ???

[Norrish, Michael (Data61, Acton)]

My comment is about how this is done in HOL, where the existing axiomatization 
is sufficient to give the behaviour as I have explained it.

Michael

From: Saburou Saitoh 
Date: Saturday, 10 August 2019 at 10:28
To: "Norrish, Michael (Data61, Acton)" 
Cc: "Chun Tian (binghe)" , hol-info 

Subject: Re: [Hol-info] 0 / 0 = 0 ???


Dear  Michael

For  x/0, the essential problem is on its definition.
I think the division by zero is trivial and clear all.
However, we will need a new axiom.
So, I would like to ask for your kind help for the axiom problem; Foundation of 
Mathematics.

Please look the draft:


viXra:1908.0100<http://vixra.org/abs/1908.0100> submitted on 2019-08-06 
20:03:01,

Fundamental of Mathematics; Division by Zero Calculus and a New Axiom


With best regards,
Sincerely yours,

Saburou Saitoh
2019.8.10.9:25



2019年8月10日(土) 9:07 Norrish, Michael (Data61, Acton) 
mailto:michael.norr...@data61.csiro.au>>:
It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use 
that term to define other things in turn.   For example, I can define foo = x/0 
+ 1 and then quite successfully prove that x/0 < foo.

I would avoid the use of the word undefined in this context; rather x/0 has an 
unspecified value.  All functions are total so all applications of functions to 
all possible arguments have values.

Michael

> On 9 Aug 2019, at 21:46, Chun Tian (binghe) 
> mailto:binghe.l...@gmail.com>> wrote:
>
> A follow-up of this old topic:
>
> Finally I found the following definitions of `extreal_inv` and `extreal_div` 
> based on new_specification():
>
> local
>  val lemma = Q.prove (
> `?i. (i NegInf = Normal 0) /\
>  (i PosInf = Normal 0) /\
>  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
>   (* proof *)
>  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
>else if x = Normal 0 then ARB
>else Normal (inv (real x))` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- extreal_inv NegInf = Normal 0 /\
>extreal_inv PosInf = Normal 0 /\
>!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
>   *)
>  val extreal_inv_def = new_specification
>("extreal_inv_def", ["extreal_inv"], lemma);
> end;
>
> local
>  val lemma = Q.prove (
> `?d. (!r. d (Normal r) PosInf = Normal 0) /\
>  (!r. d (Normal r) NegInf = Normal 0) /\
>  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
> (Normal r`,
>   (* proof *)
>  Q.EXISTS_TAC `\x y.
>if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
>else if y = Normal 0 then ARB
>else extreal_mul x (extreal_inv y)` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
>(!r. extreal_div (Normal r) NegInf = Normal 0) /\
>!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
>   *)
>  val extreal_div_def = new_specification
>("extreal_div_def", ["extreal_div"], lemma);
> end;
>
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
> undefined.
>
> --Chun
>
> Il 20/02/19 06:48, 
> michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au> ha 
> scritto:
>> Your right hand side is no better than ARB really.  You say that your aim is 
>> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
>> literal extreal, then I will define
>>
>>  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>>
>> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
>> surely pni is too.
>>
>> (Recall that ARB's definition is `ARB = @x. T`.)
>>
>> Michael
>>
>>
>> On 20/2/19, 09:31, "Chun Tian (binghe)" 
>> mailto:binghe.l...@gmail.com>> wrote:
>>
>>Some further updates:
>>
>>With my last definition of `extreal_div`, I still have:
>>
>> |- !x. x / 0 = ARB
>>
>>and
>>
>> |- 0 / 0 = ARB
>>
>>trivially holds (by definition). This is still not satisfied to me.
>>
>>Now I tried the following new definition which looks more reasonable:
>>
>>val extreal_div_def = Define
>>   `extreal_div x y = if y = Normal 0 then
>>  (@x. (x = PosInf) \/ (x = NegInf))
>>  else extreal_mul x (extreal_inv y)`;
>>
>>literally, it says anything (well, let's ignore zero) divides zero is
>>equal to either +Inf or -In

[Hol-info] Kananaskis-13 release

[Norrish, Michael (Data61, Acton)]

Dear all,

We are pleased to announce the Kananaskis-13 release of HOL 4.  Tarballs and 
PDFs are available from 
[Sourceforge](https://sourceforge.net/projects/hol/files/hol/kananaskis-13/) 
and [github]( 
https://github.com/HOL-Theorem-Prover/HOL/releases/tag/kananaskis-13). 

Contents


-   [New features](#new-features)
-   [Bugs fixed](#bugs-fixed)
-   [New theories](#new-theories)
-   [New tools](#new-tools)
-   [New Examples](#new-examples)
-   [Incompatibilities](#incompatibilities)

New features:
-

*   We have implemented new syntaxes for `store_thm` and `save_thm`, which 
better satisfy the recommendation that `name1` and `name2` below should be the 
same:

   val name1 = store_thm("name2", tm, tac);

Now we can remove the “code smell” by writing

   Theorem name: term-syntax
   Proof tac
   QED

which might look like

   Theorem name:
 ∀x. P x ⇒ Q x
   Proof
 rpt strip_tac >> ...
   QED

This latter form must have the `Proof` and `QED` keywords in column 0 in 
order for the lexing machinery to detect the end of the term and tactic 
respectively.
Both forms map to applications of `Q.store_thm` underneath, with an ML 
binding also made to the appropriate name.
Both forms allow for theorem attributes to be associated with the name, so 
that one can write

   Theorem ADD0[simp]: ∀x. x + 0 = x
   Proof tactic
   QED

Finally, to replace

   val nm = save_thm(“nm”, thm_expr);

one can now write

   Theorem nm = thm_expr

These names can also be given attributes in the same way.

There is also a new `local` attribute available for use with `store_thm`, 
`save_thm` and the `Theorem` syntax above.
This attribute causes a theorem to not be exported when `export_theory` is 
called, making it local-only.
Use of `Theorem`-`local` is thus an alternative to using `prove` or 
`Q.prove`.
In addition, the `Theorem`-`local` combination can be abbreviated with 
`Triviality`; one can write `Triviality foo[...]` instead of `Theorem 
foo[local,...]`.

-   Relatedly, there is a similar syntax for making definitions.
The idiom is to write

   Definition name[attrs]:
 def
   End

Or

   Definition name[attrs]:
 def
   Termination
 tactic
   End

The latter form maps to a call to `tDefine`; the former to `xDefine`.
In both cases, the `name` is taken to be the name of the theorem stored to 
disk (it does *not* have a suffix such as `_def` appended to it), and is also 
the name of the local SML binding.
The attributes given by `attrs` can be any standard attribute (such as 
`simp`), and/or drawn from `Definition`-specific options:

-   the attribute `schematic` alllows the definition to be schematic;
-   the attribute `nocompute` stops the definition from being added to the 
global compset used by `EVAL`
-   the attribute `induction=iname` makes the induction theorem that is 
automatically derived for definitions with interesting termination be called 
`iname`.
If this is omitted, the name chosen will be derived from the `name` of 
the definition: if `name` ends with `_def` or `_DEF`, the induction name will 
replace this suffix with `_ind` or `_IND` respectively; otherwise the induction 
name will simply be `name` with `_ind` appended.

Whether or not the `induction=` attribute is used, the induction theorem is 
also made available as an SML binding under the appropriate name.
This means that one does not need to follow one’s definition with a call to 
something like `DB.fetch` or `theorem` just to make the induction theorem 
available at the SML level.

-   Similarly, there are analogous `Inductive` and `CoInductive` syntaxes for 
defining inductive and coinductive relations (using `Hol_reln` and `Hol_coreln` 
underneath).
The syntax is

   Inductive stem:
  quoted term material
   End

or

   CoInductive stem:
  quoted term material
   End

where, as above, the `Inductive`, `CoInductive` and `End` keywords must be 
in the leftmost column of the script file.
The `stem` part of the syntax drives the selection of the various theorem 
names (*e.g.*, `stem_rules`, `stem_ind`, `stem_cases` and `stem_strongind` for 
inductive definitions) for both the SML environment and the exported theory.
The actual names of new constants in the quoted term material do not affect 
these bindings.

-   Finally, there are new syntaxes for `Datatype` and type-abbreviation.
Users can replace ``val _ = Datatype`...` `` with

   Datatype: ...
   End

and `val _ = type_abbrev("name", ty)` with

   Type name = ty

if the abbreviation should introduce pretty-printing (which would be done 
with `type_abbrev_pp`), the syntax is

   

Re: [Hol-info] 0 / 0 = 0 ???

[Norrish, Michael (Data61, Acton)]

It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use 
that term to define other things in turn.   For example, I can define foo = x/0 
+ 1 and then quite successfully prove that x/0 < foo.

I would avoid the use of the word undefined in this context; rather x/0 has an 
unspecified value.  All functions are total so all applications of functions to 
all possible arguments have values.   

Michael

> On 9 Aug 2019, at 21:46, Chun Tian (binghe)  wrote:
> 
> A follow-up of this old topic:
> 
> Finally I found the following definitions of `extreal_inv` and `extreal_div` 
> based on new_specification():
> 
> local
>  val lemma = Q.prove (
> `?i. (i NegInf = Normal 0) /\
>  (i PosInf = Normal 0) /\
>  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
>   (* proof *)
>  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
>else if x = Normal 0 then ARB
>else Normal (inv (real x))` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- extreal_inv NegInf = Normal 0 /\
>extreal_inv PosInf = Normal 0 /\
>!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
>   *)
>  val extreal_inv_def = new_specification
>("extreal_inv_def", ["extreal_inv"], lemma);
> end;
> 
> local
>  val lemma = Q.prove (
> `?d. (!r. d (Normal r) PosInf = Normal 0) /\
>  (!r. d (Normal r) NegInf = Normal 0) /\
>  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
> (Normal r`,
>   (* proof *)
>  Q.EXISTS_TAC `\x y.
>if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
>else if y = Normal 0 then ARB
>else extreal_mul x (extreal_inv y)` \\
>  RW_TAC std_ss [extreal_not_infty, real_normal]);
> in
>  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
>(!r. extreal_div (Normal r) NegInf = Normal 0) /\
>!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
>   *)
>  val extreal_div_def = new_specification
>("extreal_div_def", ["extreal_div"], lemma);
> end;
> 
> In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
> undefined.
> 
> --Chun
> 
> Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
>> Your right hand side is no better than ARB really.  You say that your aim is 
>> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
>> literal extreal, then I will define
>> 
>>  val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
>> 
>> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
>> surely pni is too.
>> 
>> (Recall that ARB's definition is `ARB = @x. T`.)
>> 
>> Michael
>> 
>> 
>> On 20/2/19, 09:31, "Chun Tian (binghe)"  wrote:
>> 
>>Some further updates:
>> 
>>With my last definition of `extreal_div`, I still have:
>> 
>> |- !x. x / 0 = ARB
>> 
>>and
>> 
>> |- 0 / 0 = ARB
>> 
>>trivially holds (by definition). This is still not satisfied to me.
>> 
>>Now I tried the following new definition which looks more reasonable:
>> 
>>val extreal_div_def = Define
>>   `extreal_div x y = if y = Normal 0 then
>>  (@x. (x = PosInf) \/ (x = NegInf))
>>  else extreal_mul x (extreal_inv y)`;
>> 
>>literally, it says anything (well, let's ignore zero) divides zero is
>>equal to either +Inf or -Inf.  But actually the choice of +Inf/-Inf is
>>irrelevant, as the sole purpose is to prevent any theorem like ``|- x /
>>0 = y`` being proved, in which y is a literal extreal. For example, if I
>>try to prove ``!x. x / 0 = ARB``:
>> 
>>(* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't
>>be proved, e.g.
>>val test_div = prove (
>>   `!x. extreal_div x (Normal 0) = ARB`,
>>RW_TAC std_ss [extreal_div_def]
 Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))`
>>> - RW_TAC std_ss []
 MATCH_MP_TAC SELECT_ELIM_THM
 RW_TAC std_ss [] (* 3 gubgoals *)
>>   NegInf = ARB
>> 
>>   PosInf = ARB
>> 
>>   ∃x. (x = PosInf) ∨ (x = NegInf));
>> *)
>> 
>>at the end I got 3 subgoals like above. I *believe*, no matter what
>>value I put instead of ARB, at least one of the subgoals must be false.
>>Thus the theorem should be unprovable. (am I right?)
>> 
>>Can I adopt this new definition of `extreal_div` in the future? Any
>>objection or suggestion?
>> 
>>--Chun
>> 
>>Il 15/02/19 23:37, Chun Tian (binghe) ha scritto:
>>> I'm going to use the following definition for `extreal_div`:
>>> 
>>> (* old definition of `extreal_div`, which allows `0 / 0 = 0`
>>> val extreal_div_def = Define
>>>   `extreal_div x y = extreal_mul x (extreal_inv y)`;
>>> 
>>>   new definition of `extreal_div`, excluding the case `0 / 0`: *)
>>> val extreal_div_def = Define
>>>   `extreal_div x y = if (y = Normal 0) then ARB
>>>  else extreal_mul x 

[Hol-info] post-doc opportunity at UNSW Sydney

[Norrish, Michael (Data61, Acton)]

UNSW Sydney Seeking a Postdoc in Programming Languages and Verification

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

Sounds too good to exist?

In the Trustworthy Systems team at UNSW and 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 offering a two-year postdoctoral researcher position that would allow 
you to join
us in Sydney, move things forward, and have a global impact.

Cogent is a language we designed that co-generates code and proofs in order to 
ease
the verification of systems components around seL4. Potential topics include 
designing
and implementing new domain-specific programming languages extending Cogent, 
writing
formal specifications and proofs in Isabelle/HOL, developing formally verified
infrastructure for building secure systems on top of seL4, contributing to 
improved
proof automation and reasoning techniques, and applying formal proof to 
real-world
systems and tools.

To apply you should have (or be about to obtain) a PhD degree in Computer 
Science,
Mathematics, or similar.

You should also 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
- ability and desire to work in a larger team

If you additionally have experience

- in software verification with an interactive theorem prover such as
Isabelle/HOL, HOL4, Coq, or Agda, and/or
- with programming languages and verified or certifying compilers

you should definitely apply!


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.


For applying, use the following link:
http://external-careers.jobs.unsw.edu.au/cw/en/job/497074/postdoctoral-fellow-computer-programming
 


-Salary range depending on experience and qualifications: 
$95,449 - $102,091 (AUD) + 17% superannuation (retirement funds)
- 2-year fixed term contract
- the start date is negotiable
- flexible hours and work arrangements

This round of applications closes on the 13th of July 2019, 11:50pm AEST.


For any questions on this position, please contact Christine Rizkallah 
mailto:c.rizkal...@unsw.edu.au>>

The seL4 code and proof, and the Cogent project, are open source.
Check them out at https://seL4.systems  and 
https://ts.data61.csiro.au/projects/TS/cogent.pml 



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