Re: [Hol-info] Inquiry: Introducing new types as predicates

[Mario Castelán Castro]

On 22/01/18 18:35, Cris Perdue wrote:
> 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.

Hello.

I really do not understand what you are looking form.

If you want something like “subtypes”, you can use restricted
quantification (theory "res_quan"). E.g. You can define a term “ODD:(num
-> bool)” and then quantify as in “∀x::ODD. P x”.

However, many tactics in HOL4 are blind to restricted quantification.
Fixing this it is just a matter of making a change in the source code or
writing a wrapper. In my repository of HOL4 developments
 have a wrapper for
“MESON_TAC” and a tactic that is like “MATCH_MP_TAC” but extended in
that it adds support for restricted quantification and other things.

Alternatively, you can embed a type system with coercing/casting
functions. E.g. You have a function “COERCE_ODD (:num -> :num)” which
returns the same number of it is odd, and an arbitrary odd number
otherwise. Then to quantify over odd numbers, you write “∀x. P
(COERCE_ODD x)” instead of (with the above approach) “∀x::ODD x”.

As far as I know: Simple type theory has no means to introduce new
types; that is a conservative extension found in some proof assistants
like HOL4. The types in Church's formulation [1] are the individuals
(type “ind” in HOL4), propositions (roughly type “bool” in HOL4; but
Church allows the possibility of intensional propositional functions),
and the scheme: if “'a” and “'b” are types, then “'a -> 'b” is a type.

I would like to share some of my observations regarding type theories
compared to set theories:

If you want, roughly speaking, that all objects are treated the same (as
“individuals”), set theory already does that. I am aware that a common
complain against set theory is the existence of “junk theorems” like “0
∈ 1” (E.g.: this holds if 0 and 1 are ordinals with the usual
Mirimanov-von Neumann construction, or reals with the Dedekind
construction). But this is unfounded. In a proof assistant based on set
theory with atoms (a.k.a. “urelements”) one could in principle add (akin
to type definitions in HOL4) new sets of atoms disjoint from the set of
all previously-defined atoms; then objects that are conceptually not
sets (numbers, etc.) could be introduced as atoms and there would not be
“junk theorems”; this is like a typical type theory, but instead of
having bad-typed formulas, you would have theorems of non-elementhood
like “∀S. 1 ∉ S”.

Another complaint against well-founded (Zermelo-style) set theories is
that in general, the set of all {groups, topological spaces, categories,
etc} is not itself a set. The set theory New Foundations, which is not
well-founded, has a set of all sets, but the price it pays is that in
general separation does not hold (i.e.: There exists a set S and formula
P in which x is free, for which {x | x ∈ S ∧ P} is _not_ a set). I hear
that it has problems with constructions like “the set of all categories”
but I have not investigated into that. By contrast, I am not aware of
any type theory which has a equivalent of an universal set. Usually
either there are terms without a type, or “kinds” that are not types,
which is the antithesis of an universal set/type.

Polymorphism gives _the illusion_ that one has the set of all sets _and_
at the same time the separation axiom; but it is just an illusion, for
if that was really the case the system would contain a contradiction
(i.e.: Russell paradox). For example, in HOL4 you have the seemingly
universal type {x | T}; and for any P, if “{x | P x}” is well-typed then
it is a “set”). “UNIV ∈ UNIV” is provable; yet the occurrences of “UNIV”
have different types; trying to derive “∃S. S ∈ S” fails because it is
not even a WFF.

Polymorphism is usually found in type theories, and it is usually hidden
by the printer so it is not very conspicuous, thus enhancing the
illusion of a very expressive theory. But this is just the current
trend. One can polymorphism in set theory too. In a vague sense, New
Foundations can be seen as having polymorphism “built-in”. It can be
added to ZFC if one restricts the scope of quantifiers to sets. If you
add classes (as in NBG) and pretty-printing on top, it can too give the
illusion of having universal comprehension. Now, I _imagine_ that by a
suitable limitation of quantification one could have a set of atoms
“True” and “False” in a ZFC+atoms and then have propositions as ordinary
functions. However I have not explored this possibility.

In my opinion, sophisticated type theories (specifically, those with
types that can depend on terms, like the Calculus of Constructs) merely
make more complex what can 

Re: [Hol-info] How to build only hol.bare?

[Mario Castelán Castro]

Understood. Thanks.

On 23/12/17 03:36, michael.norr...@data61.csiro.au wrote:
> 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

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

[Hol-info] How to build only hol.bare?

[Mario Castelán Castro]

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

Re: [Hol-info] Can not build documentation because building polyscripter fails

[Mario Castelán Castro]

I found the place where “-lgmp” was missing (see attached diff). This is
a workaround. A better solution would be to allow the user to override
the linker flags with a declaration in “poly-includes.ML”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
diff --git a/tools-poly/configure.sml b/tools-poly/configure.sml
index cb9f7b873..3b6b83b72 100644
--- a/tools-poly/configure.sml
+++ b/tools-poly/configure.sml
@@ -215,7 +215,7 @@ in
  case pkgconfig_info of
  SOME list => list
| _ => ["-L" ^ polymllibdir, "-lpolymain", "-lpolyml", "-lpthread",
-   "-lm", "-ldl", "-lstdc++", "-lgcc_s", "-lgcc"]
+   "-lgmp", "-lm", "-ldl", "-lstdc++", "-lgcc_s", "-lgcc"]
else []
 end;
 
--
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] Can not build documentation because building polyscripter fails

[Mario Castelán Castro]

In a recent development version (commit 38d36b51a) doing “make” in the
directory “Manual” fails. I traced the error to a failure to build
polyscripter. Here is what appears in Manual/Tools/.hollogs/polyscripter:

“““

-
   HOL-4 [Kananaskis 11 (stdknl, built Tue Dec 19 11:34:27 2017)]

   For introductory HOL help, type: help "hol";
   To exit type -D
-
[extending loadPath with Holmakefile INCLUDES variable]
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`add_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int)':
arb.cpp:(.text+0x181): undefined reference to `__gmpn_add_n'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`sub_unsigned_long(TaskData*, SaveVecEntry*, SaveVecEntry*, int)':
arb.cpp:(.text+0x2d8): undefined reference to `__gmpn_sub_n'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`quotRem(TaskData*, SaveVecEntry*, SaveVecEntry*, SaveVecEntry*&,
SaveVecEntry*&)':
arb.cpp:(.text+0xbf1): undefined reference to `__gmpn_tdiv_qr'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`gcd_arbitrary(TaskData*, SaveVecEntry*, SaveVecEntry*)':
arb.cpp:(.text+0xf2c): undefined reference to `__gmpn_gcd_1'
arb.cpp:(.text+0x102e): undefined reference to `__gmpn_rshift'
arb.cpp:(.text+0x10d3): undefined reference to `__gmpn_rshift'
arb.cpp:(.text+0x1153): undefined reference to `__gmpn_gcd'
arb.cpp:(.text+0x1175): undefined reference to `__gmpn_lshift'
/home/mario/local/stow/polyml/lib/libpolyml.a(arb.o): In function
`mult_longc(TaskData*, SaveVecEntry*, SaveVecEntry*)':
arb.cpp:(.text+0x1964): undefined reference to `__gmpn_mul'
collect2: error: ld returned 1 exit status
”””

I am using Debian 9 with Poly/ML 5.7.1 built from source and installed
using GNU Stow. The error message appears to indicate that libGMP is not
being found. However, compiling HOL (“bin/build -j 2”) works without
such problems. libGMP has been installed using the package manager; the
shared objects and static library are under
“/usr/lib/x86_64-linux-gnu/”, which is the standard location for Debian.

It appears that “ld” is called somewhere (I can not figure where) and it
is missing the command line option “-lgmp”.

What can I do to make it work?

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 can I instantiate the variable which constrained by the existential quantifier in the parentheses？

[Mario Castelán Castro]

Hello.

You can not choose the value of «l» because it is in the antecedent. You
must prove it for any value of “l”, as seen in the following equivalence:

> SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM]
  “(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”;
<>
val it =
   ⊢ (∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2) ⇔
 ∀l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2) ⇒ (m1 ⧺ m2 = l1 ⧺ l2):
   thm


You can discharge the antecedent and strip the existential quantifier
leaving a fresh free variable. Use “disch_then strip_assume_tac” or more
simply, “rpt strip_tac”.

Maybe this is what you want:

prove(
  “(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”,
  disch_then strip_assume_tac >>
  rpt BasicProvers.var_eq_tac >>
  MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC);

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

-- 
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 can I instantiate the variable which constrained by the existential quantifier in the parentheses？

[Mario Castelán Castro]

Hello.

You can not choose the value of «l» because it is in the antecedent. You
must prove it for any value of “l”, as seen in the following equivalence:

  > SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM]
“(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”;
  <>
  val it =
 ⊢ (∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2) ⇔
   ∀l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2) ⇒ (m1 ⧺ m2 = l1 ⧺ l2):
 thm


You can discharge the antecedent and strip the existential quantifier
leaving a fresh free variable. Use “disch_then strip_assume_tac” or more
simply, “rpt strip_tac”.

Maybe this is what you want:

prove(
  “(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”,
  disch_then strip_assume_tac >>
  rpt BasicProvers.var_eq_tac >>
  MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC);

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

-- 
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 can I instantiate the variable which constrained by the existential quantifier in the parentheses？

[Mario Castelán Castro]

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

Hello.

You can not choose the value of «l» because it is in the antecedent. You
must prove it for any value of “l”, as seen in the following equivalence:

> SIMP_CONV pure_ss [GSYM LEFT_FORALL_IMP_THM]
  “(?l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ==> (m1 ++ m2 = l1 ++ l2)”;
<>
val it =
   ⊢ (∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2) ⇔
 ∀l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2) ⇒ (m1 ⧺ m2 = l1 ⧺ l2):
   thm


You can discharge the antecedent and strip the existential quantifier
leaving a fresh free variable. Use “disch_then strip_assume_tac” or more
simply, “rpt strip_tac”.

Maybe this is what you want:

prove(
  “(∃l. (l1 = m1 ⧺ l) ∧ (m2 = l ⧺ l2)) ⇒ (m1 ⧺ m2 = l1 ⧺ l2)”,
  disch_then strip_assume_tac >>
  rpt BasicProvers.var_eq_tac >>
  MATCH_ACCEPT_TAC listTheory.APPEND_ASSOC);

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

[Mario Castelán Castro]

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

Re: [Hol-info] The origin of the HOL4 logo

[Mario Castelán Castro]

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

[Hol-info] The origin of the HOL4 logo

[Mario Castelán Castro]

Hello.

I recall having read that the HOL4 logo (as found in TUTORIAL, MANUAL,
DESCRIPTION, LOGIC) is based on a photo of a lamp found in Canada.
Despite searching my browser history and using a search engine I failed
to find the message again.

To somebody who knows what photo I am referring to or otherwise knows
the origin of the HOL4 logo, could you please link me to further
information about the origin of the logo, including the photo that it is
based from?

This is just for curiosity.

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

[Mario Castelán Castro]

On 12/12/17 12:08, John Harrison wrote:
> Hi Mario,
> 
> | 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.
> 
> Unless you actually need to encode domain and codomain in the function
> (rather than treating them as other related parameters in your theorem)
> a reasonable "cheap" alternative is to use ordinary functions that map
> to some canonical value (say ARB = @x. F) outside the domain. This at
> least gives a set of functions of the right size so you can do things
> like talk about its cardinality and about the existence of a unique
> function in the usual way. And it is at the same time a normal kind of
> HOL function and can be applied as usual etc. [...]
Thanks for your reply John.

In your experience, what is the advantage of this approach over
introducing a dedicated type for “partial” functions? Currently my
approach is to introduce a new type “('a,'b) pfun”, where the constant
“APPLY:('a,'b) pfun -> 'a -> 'b” is used for function application
(“APPLY Fn x” is displayed and can be entered as “Fn‘x”). One can
recover an ordinary HOL function with partial application. i.e.: “APPLY
Fun”. The constant “apply” is “undefined” outside the domain (the
definition is an implication of the form “x ∈ dom Fn ⇒ Fn‘x = [...]”)
but it could be modified to change it to “ARB”.

Regards.

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

[Mario Castelán Castro]

I have written this 
 
HOL4 theory that introduces a new type for partial (with respect to the 
universe of the type) functions. The script file is tiny and trivial, 
but at least it can save the time to type it to somebody else; it can be 
reused as it is under a free license (GNU GPL 3 or later).


Regards.

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

[Mario Castelán Castro]

Thanks you very much.

On 05/12/17 16:17, michael.norr...@data61.csiro.au wrote:

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


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

[Mario Castelán Castro]

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

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

[Mario Castelán Castro]

On 30/10/17 16:16, michael.norr...@data61.csiro.au wrote:
> 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.

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Can the simplifier from simpLib normalize symmetric relations?

[Mario Castelán Castro]

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



signature.asc
Description: OpenPGP digital signature
--
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 building time and using HOL4 development version

[Mario Castelán Castro]

On 25/10/17 17:31, michael.norr...@data61.csiro.au wrote:
> It may well be that the dependency graph forces theories to be built 
> sequentially, in which case –j2 won’t win you anything. 

Right.

> And then, even when concurrent execution is possible, we are still at the 
> mercy of the OS’s scheduler.

Yes, but that is only an issue in practice when there is contention for
CPU time (i.e.: other CPU-intensive processes are running).


Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 building time and using HOL4 development version

[Mario Castelán Castro]

On 25/10/17 17:16, michael.norr...@data61.csiro.au wrote:
> The –j number dictates how many processes Holmake will fork/exec at once to 
> run theory scripts.  On a 1 core machine (without hyperthreading), you will 
> only get time-sliced concurrency between the scripts. As scripts do minimal 
> I/O (reading the script and writing theory files at the end), you may not get 
> much advantage from scripts able to run while others are blocked.
> 
> With –j1, Holmake doesn’t monitor the child process asynchronously, but uses 
> “system” to run scripts one after the other.

Sorry. I made a typing error in my previous message I meant to write:

   I used “bin/build -j 2” and it still used only *1* core
   most of the time. My CPU is *2* core.”.

So it mostly wastes the opportunity to use both cores.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 building time and using HOL4 development version

[Mario Castelán Castro]

On 25/10/17 16:23, Chun Tian wrote:
>> How do I know if I have to re-run “smart-configure.sml”? Also, is there
>> some way I can run build jobs in parallel?
> 
> When that happens, the “bin/build” command will tell you to re-run 
> smart-configure;To build in parallel, you can use “bin/build -j 4” (or -j 
> 8).

Thanks you.

I used “bin/build -j 2” and it still used only 1 core most of the time.
My CPU is 1 core.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 building time and using HOL4 development version

[Mario Castelán Castro]

On 25/10/17 14:29, Chun Tian wrote:
> HOL doesn’t rebuild everything when you re-run “bin/build”: it only rebuilds 
> changed theories and all dependencies. Sometimes you need to re-run “poly < 
> tools/smart-configure.sml” and rebuild everything, other times you need to 
> clean everything “bin/build cleanAll” to fix the building process.

How do I know if I have to re-run “smart-configure.sml”? Also, is there
some way I can run build jobs in parallel?

In my experience when making changes, it rebuilt nearly everything and
took approximately the same time as compilation from scratch. Probably
that was because I modified the theory “res_quan” which has many
descendants.

> Anyway, I think by large chances you only need 10 minutes to keep your build 
> up-to-date.   But if I have a poly process with everything loaded, I can 
> normally use it even when HOL is rebuilding.

Running HOL while coiling seems prone to errors. Very probably there are
race conditions between the compilation process and interactive loading
of HOL files (e.g.: a file can be read while it was being written to).

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] About building time and using HOL4 development version

[Mario Castelán Castro]

Hello.

If my understanding is correct, when using the development version of
HOL4 one has to recompile every time one updates the local copy (i.e.:
“git pull” or “git fetch; git checkout origin/master”). In my computer,
running bin/build takes around 20 min. If a theory with many descendants
is changed, then it takes approximately the same time.

If I use the development version, does that mean that I have to wait 20
minutes for compilation after updating my local copy before I can use
it? Is that how it is supposed to be or is there some command line
switch, or something related that I am missing, to shorten compilation
time when updating?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Mario Castelán Castro]

On 22/10/17 18:43, michael.norr...@data61.csiro.au wrote:
> Agreed: let’s keep Lib and ditch Tools.

Acknowledged. :)

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Mario Castelán Castro]

On 22/10/17 17:54, michael.norr...@data61.csiro.au wrote:
> We don’t track logical dependencies. Rather, we record what theories have 
> been loaded. […]
> 
> Both the command-line --holstate= and Holmakefile HOLHEAP= methods seem fine 
> to me. […]

Thanks for the answer.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Mario Castelán Castro]

On 22/10/17 13:04, Konrad Slind wrote:
> Some of these are support for other proof infrastructure, but the main
> theories give you booleans, products, sums, options, numbers, lists,
> and sets. This is a useful basis on which to begin most formalizations.

Thanks. I thought “export_theory” computed the actual dependencies, as
opposed to using all loaded theories indiscriminately.

> […] Then you will have to explicitly load in all the needed tools and 
> theories.
> For use of Holmake, I am pretty sure there is an option to support
> hol.bare, but I am not sure what it is.

There is the “--holstate” command line option of Holmake and the special
variable HOLHEAP in a Holmakefile which can be used to employ the bare
heap. But I do not know what is the preferred method.

Regards.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Spurious parent theories

[Mario Castelán Castro]

Hello.

When I process the following file with Holmake from a recent Git build I
get indexedLists and patternMatches as parents; with Kananaskis-11 I get
quantHeuristics and rich_list as parents. Why? There is no apparent
dependency on anything but the bool theory.

“open HolKernel Parse boolLib boolTheory;
val _ = new_theory "test";
save_thm("T", TRUTH);
val _ = export_theory ();”

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] res_quanLib and res_quanTools are exact duplicates

[Mario Castelán Castro]

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



signature.asc
Description: OpenPGP digital signature
--
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 express the elements in a list are all identical?

[Mario Castelán Castro]

On 20/10/17 01:48, Chun Tian wrote:
> Thanks, I’m going to use: ALL_IDENTICAL t = ?x. !y. MEM y t ==> y = x

You are welcome.

Yes, that definition looks good to me. ☺

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 express the elements in a list are all identical?

[Mario Castelán Castro]

On 19/10/17 15:57, Mario Castelán Castro wrote:
> “∃x. set l ⊆ x”.

I meant “∃x. set l ⊆ {x}”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 express the elements in a list are all identical?

[Mario Castelán Castro]

If you want to allow the empty list then:

“∀x y. MEM x l ∧ MEM y l ⇒ x = y”

or:

“∃x. set l ⊆ x”.

or:

“∃x. MEM y l ⇒ y = x”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 express the elements in a list are all identical?

[Mario Castelán Castro]

On 19/10/17 14:08, Chun Tian wrote:
> I need to express the fact that the elements in a list are all identical, 
> what’s the suggest way?  Currently I have this: (inspired by ALL_DISTINCT)

What about this:?

“∃x. set l = {x}”

also:

“∃!x. MEM x l”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] line wrap length in hol-mode

[Mario Castelán Castro]

On 16/10/17 17:15, michael.norr...@data61.csiro.au wrote:
> You need to adjust Globals.linewidth (an int ref).
Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 14:55, Chun Tian wrote:
> I’m using HOL built from latest Git “master” branch; you’re using HOL 
> Kananaskis-11 release.

Understood.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] line wrap length in hol-mode

[Mario Castelán Castro]

Hello. How can I change the column at which the pretty printer will wrap
expressions using hol-mode in GNU Emacs? I want it to use the full width
of the Emacs “window” (the cell that displays a buffer, not the whole
window).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 09:35, Chun Tian (binghe) wrote:
> I'm fine with constant overloading. But I think the "term_name" used in
> add_rule() doesn't know constant overloading at all. After realaxTheory is
> loaded, the previous rule defined in relationTheory has absolutely no
> effects, even I'm using "inv" for relations.

I do not know what is your situation. In my case (HOL4 Kananaskis-11),
there is no custom parser rule for relation$inv:

“mario@svetlana [0] [/home/mario]
$ hol

-
   HOL-4 [Kananaskis 11 (stdknl, built Sun Aug 06 16:33:32 2017)]

   For introductory HOL help, type: help "hol";
   To exit type -D
-
> ancestry "-";
val it =
   ["ConseqConv", "quantHeuristics", "ind_type", "operator", "while",
"pair",
"num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
"one", "marker", "combin", "min", "bool", "sat", "sum", "option",
"basicSize", "numpair", "pred_set", "list", "rich_list"]: string list
> “inv R”;
<>
val it = ``inv R``: term”

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

If you want to completely remove the mapping of “inv” to the constant
from “realax”, then do “remove_ovl_mapping "inv" {Name = "inv", Thy =
"realax"};”. This constant can then still be accessed with “realax$inv”.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Mario Castelán Castro]

On 16/10/17 08:23, Chun Tian (binghe) wrote:
> Is this something can be fixed? (I don't know how) i.e. preserving the
> pp_setting of  "inv" for relations and correctly define TeX notations for
> both of them.

“inv” has 2 possible resolutions after loading realTheory:

> overload_info_for "inv";
inv parses to:
  realax$inv
  (relation$inv :(α -> α -> bool) -> α -> α -> bool)
inv might be printed from:
  (relation$inv :(α -> α -> bool) -> α -> α -> bool)
  realax$inv
val it = (): unit

Typically the correct one will be chosen by the parser because of type
constraints. If you want to force one of them, you can write
“relation$inv” or “realax$inv”. If you want to make the one from
“relation” the default, then do “overload_on("inv",“relation$inv”):”. I
do not know how to manipulate the TeX mapping.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



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

Re: [Hol-info] What is the purpose of labels?

[Mario Castelán Castro]

Thanks for your answer Michael.

On 15/10/17 06:27, michael.norr...@data61.csiro.au wrote:
> This is a feature that hasn’t really been pursued.  There is some code 
> supporting their use (akin to the way Abbr`v` is supported in calls to the 
> simplifier), but it is incomplete and thus unused, and pretty well 
> undocumented. 
> 
> But yes, the idea is to be able to label assumptions to make it easier to 
> refer to them in later stages of a proof.  In practice, most people use the 
> ability to match assumptions with patterns, and/or the ability to select them 
> by whether or not they do or don’t raise exceptions when manipulated by rules 
> of inference.  (For example, first_x_assum (qspec_then [`x`, `y`] mp_tac) 
> will only work on assumptions that are universally quantified with two 
> variables, and if x and y appear in the goal (which is likely), those 
> universal variables will have to also be of the right type.)

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



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

Re: [Hol-info] What is the purpose of labels?

[Mario Castelán Castro]

I accidentally posted this as a reply to an unrelated message. Apologies.

On 14/10/17 10:53, Mario Castelán Castro wrote:
> Hello.
> 
> What is the purpose of labels? The ones from the theory “marker”: “$:-”.
> 
> I see that there are some functions in src/marker/markerLib.sml that
> suggest these are used to designate labels on assumptions. Is this
> documented somewhere?
> 
> Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] What is the purpose of labels?

[Mario Castelán Castro]

Hello.

What is the purpose of labels? The ones from the theory “marker”: “$:-”.

I see that there are some functions in src/marker/markerLib.sml that
suggest these are used to designate labels on assumptions. Is this
documented somewhere?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Difficulties in formalizing an informal proof with cardinals (or ordinals)

[Mario Castelán Castro]

On 12/10/17 13:34, Chun Tian wrote:
> My structure can contain (‘a ordinals) as part of it, and I have a function, 
> given any ordinal N, for all n < N, f(n) is a different value of my structure 
> (which contains ordinal too). Its cardinality must be very huge, and that’s 
> the only thing I know.

Hello.

Sorry, I do not know about that formalization of ordinals in HOL4. I
will take a look at the papers you mentioned sometime.

It occurs to me that a possible approach is to shift the burden of
proving cardinality conditions to the “user”. That is, to prepend your
theorems with the hypothesis that there exists a suitable universe
containing sets of the cardinalities you need.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Difficulties in formalizing an informal proof with cardinals (or ordinals)

[Mario Castelán Castro]

Hello.

Note: I know nothing about process algebra. I had to perform a web
search to know what the term means.

Do you really need to consider set of arbitrary cardinalities? Aren't
your structures always below some cardinality? Would it suffice for your
formalization to speak of _representations_ of ordinals below, say, ε0?
Those can be represented as finite formulas in ordinal arithmetic, so
the set of all such representations can fit within a single monomorphic
HOL4 type.

> If I've learnt correctly, in standard set theory, all cardinals are ordinals, 
> but the reverse is not true, because not every ordinals “has the same number 
> (as itself) of smaller ordinals”.

As far as I know, that “all cardinals are ordinals” is just an effect of
the “standard” definition of ordinal numbers and cardinal numbers in ZFC
(card A is the least ordinal X such that X === A [End, p. 197]) but it
is not a property intrinsic to the informal concept of cardinal numbers.
I think of this as a technical definition analogous to the Kuratowski
definition of ordered pairs. One can also define card A as the _class_
“{X | X === A}” in a theory that admits classes (like von
Neumann-Gödel-Bernays, and HOL4's “pred_set”), then this property no
longer holds (w.r.t. the standard way of defining ordinals, which is
also due to von Neumann).

> “Let c be the smallest infinite cardinal, such that NODES(p) and NODES(q) has 
> less than c nodes.

If NODES(p) and NODES(q) are of type “bool -> 'a” (or you have one
equinumerous term with such a type), then you can define the cardinality
of p and q as “{X | ∃f. BIJ f (NODES p) X}” but I do not know how this
applies to your case.

[End] Herbert B. Enderton “Elements of set theory” (1977).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Definitions of partial functions (incl. predicates)

[Mario Castelán Castro]

Hello Ramana.

On 05/10/17 19:18, Ramana Kumar wrote:
> My intuition says that working with total functions (and especially
> predicates) will be easier.
> Why? I don't know exactly, but here are some possible reasons:
> you can just use plain rewriting rather than conditional rewriting,
> and you don't need to state so many assumptions explicitly on your
> theorems.

Thanks for your comments. I do not think that those caveats will give
problems. At most, one needs to introduce the side condition as a lemma
before calling “simp” (or similar), so that it can apply use the
conditional rewrite.

> I also want to make a point against the supposed elegance of partial
> definitions. My understanding is that it seems more elegant to not
> specify a function on inputs that are supposed to be "invalid" for
> that function, […]

At least I see it, the justification for partial definitions is a
pragmatic one: To avoid some misleading results. For example, consider
the hypothetical situation where one has proved a seemingly
contradictory about the function; and at close inspection, one realizes
that the function is being applied outside the intended domain, hence
that one was able to prove the unexpected result in the first place.

Regards.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Experience and opinions on proof assistants with “rich” type systems

[Mario Castelán Castro]

Hello Jeremy.

Thanks for your reply.

On 05/10/17 13:25, Jeremy Dawson wrote:
> Hi Mario,
> 
> I don't mind the question, but the answer may not be much use because
> it's a comparison between the 2005 version of Isabelle which I use and
> HOL4.
> 
> In terms of the type systems they are identical.
> 
> Isabelle has schematic variables and type classes, both of which can
> make proof easier.  Otherwise, I don't find major differences.
> 
> Turning to modern day Isabelle - other factors may be:
> 
>   - the extent of unnecessarily incompatible changes between one version
> of Isabelle and the next (which is in fact why I'm still using the 2005
> version, when I'm not using HOL)
> 
>   - the difficulty of using ML to program complex proof tactics -
> mandatory for a small proportion of my work (I've had various and highly
> conflicting reports of whether this is possible or reasonably easy in
> current Isabelle)
> 
>   - documentation, and willingness of developers to help with questions
> (and for me, location at GMT+10 means I can often get an immediate answer)
> 
> In HOL4 the source code is effectively available for users to look at
> (in Isabelle they can look at it, but it - or a lot of it - is highly
> obfuscated).
> 
> Cheers,
> 
> Jeremy

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Definitions of partial functions (incl. predicates)

[Mario Castelán Castro]

Hello.

What is the preferred way to define functions only for some values? For
example, as in arithmetic$DIV in HOL?:

  ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)

Here nothing is asserted for the value of DIV for n = 0, thus it is
“undefined” in some sense. I know that this can be done with
“new_specification” but proving _trivial_ existence theorems seems like
something that should be automatized.

I am writing a formalization of elementary topology[1]. I have to define
the concept of the interior, closure, etc. Currently I use total
definitions. I am thinking that it may be more elegant to use a partial
definition like the above.

For example, currently I have the definition:

interior To X r ⇔
  is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
  ∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To

I want to change this to:

is_topo To ∧ X ⊆ space To ⇒
  interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}

Is there some expected difficulty with this under-specification?

Thanks.

[1]  (work in progress).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Experience and opinions on proof assistants with “rich” type systems

[Mario Castelán Castro]

On 05/10/17 11:53, Jeremy Dawson wrote:
> Hi Mario,
> 
> Slightly off-topic, I had experience with the type system of HOL-Omega
> (system F, if I recall the terminology right, not dependent types, so my
> experience may not be very relevant)
> 
> My dominant recollection is the difficulty of getting the system to do
> the right type inference, and getting terms to typecheck.  I was forever
> working out where I needed to put in type annotations.  Quite
> frustrating after my experience with regular HOL, and Isabelle.
> 
> It led me to conclude that the systems offering automatic inference of a
> principal type really occupy a "sweet spot", ie the best compromise
> between ease of use and expressive power.

Hello Jeremy. Thanks for your answer! If you do not mind an off-topic
question, what differences in terms of usability and ease of formalizing
pure mathematics did you experience find between Isabelle and HOL4 (or
HOL Light if that is the one you use)?.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Experience and opinions on proof assistants with “rich” type systems

[Mario Castelán Castro]

On 04/10/17 20:09, Ramana Kumar wrote:
> Perhaps it would make more sense to ask people who are using rich type
> systems what their motivations are :)
> (On this list it's probably mostly people who are satisfied with simple
> type theory.)

Yes, you are right. I wrote to this list because I am interesting in the
opinion of informed “outsiders”, not only “insiders”, so to speak.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Is it possible to make Holmake print timing information?

[Mario Castelán Castro]

On 29/09/17 03:20, Ramana Kumar wrote:
> One possible variation on your must_prove might be the following:
> qmatch_rename_tac {term quotation} >- {tactic}

Good idea. Thanks you.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Is it possible to make Holmake print timing information?

[Mario Castelán Castro]

On 27/09/17 05:29, Chun Tian (binghe) wrote:
> Honestly speaking, I like those abbreviated “power” tactics, such that
"fs"
> for FULL_SIMP_TAC, "rfs" for REV_FULL_SIMP_TAC, etc., but using all
tactics
> in smaller cases (e.g. strip_tac/STRIP_TAC) doesn't make much sense to me,
> because it makes me harder to distinguish between the "inner" and "outer"
> languages in HOL proof scripts...

Yes. I use an explicit chain of “GEN_TAC”, “DISCH_TAC”, “EQ_TAC” and/or
“CONJ_TAC” when the first step (which is most of the time) is to strip
the original goal. After that, I declare what the resulting goal is with
a trivial tactic I wrote: “must_prove:(term quotation -> tactic ->
tactic)”. “must_prove” checks that the goal is alpha-equivalent to the
quotation and then applies the user-provided tactic (it must completely
solve the goal). Of course, taking a tactic as an argument is just for
syntactic convenience, as the same could be done with “THEN1”/“>-”.

I was going to put here the code of “must_prove”, but I just realized
how ugly my implementation is. Instead I am going to rewrite it.

P.S.: I wrote this message yesterday (UTC—05) but source forge rejected
my message.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



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

Re: [Hol-info] Question on rewriting with assumptions

[Mario Castelán Castro]

On 27/09/17 00:56, Ramana Kumar wrote:
> I just wanted to point out, in case you didn't know, that many tactics have
> lowercase synonyms so you don't have to write them out in all capital
> letters. For example pop_assum and rewrite_tac.

Right; thanks. I do not mind using uppercase identifiers. When
both are available, I use the uppercase one because it seems to be the
de-facto standard (e.g.: there is “gen_tac” but no “disch_tac”, although
one can define it with “val”), but I would also be comfortable using the
other one.

> There are also some cheatsheets around online for commonly used tactics,
> e.g., http://sange.fi/~magnus/cheatsheet.txt and
> https://gist.github.com/xrchz/71048e26e42f7f195d1726a855a4d2ff. Maybe these
> should be linked from the main website (and probably merged)...

Thanks you. These are nice.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan




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

Re: [Hol-info] Question on rewriting with assumptions

[Mario Castelán Castro]

Hello Chun Tian.

On 25/09/17 17:12, Chun Tian (binghe) wrote:
> To prevent "explicit" lambda expressions in this case, what I've learnt
> from Joe Hurd is the following simple helper ML function:
> 
> fun wrap a = [a];
> 
> then your "POP_ASSUM (fn thm => REWRITE_TAC [thm])" becomes "POP_ASSUM
> (REWRITE_TAC o wrap)".

Thanks you. This does nicely what I wanted.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Question on rewriting with assumptions

[Mario Castelán Castro]

Hello.

Suppose that in a tactic-based proof I have just proved with “by” a
lemma of the form “P = Q”, where “P” can be matched against a proper
subterm of the goal. I want to use this lemma to rewrite the respective
subterm of the goal. What is the preferred approach to do this?

The obvious approach is “POP_ASSUM (fn thm => REWRITE_TAC [thm])” (or
another rewriter in place of “REWRITE_TAC”). But I feel that embedding a
lambda expression in a proof is an inelegant approach.

I am aware that “ASM_REWRITE_TAC” or “FULL_SIMP_TAC” can be used in some
of these cases, but sometimes there are assumptions that would lead to
an undesired rewriting.

Is there something like “SUBST1_TAC” that does matching?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Experience and opinions on proof assistants with “rich” type systems

[Mario Castelán Castro]

Hello.

I want ask for your experience and opinion of proof assistants with
“rich” type systems (allowing types dependent on terms and “proofs as
terms, propositions as types”) like Agda and Coq. Specifically, how
practical are these systems for pure mathematics, compared to HOL4 and
HOL Light? Is there a significant advantage of these systems for pure
mathematics compared to higher order logic?

Systems with types dependent on terms promise many expressibility
built-it into the logic. My impression is that this is unnecessary and
generates more problems than what it solves. When one tries to make the
logic as rich as possible instead of as simple as possible, containing
everything that could be desired built-in, the result is an enormously
complex logic (with the implications that the logical kernel, if any,
will be more difficult to verify either by ordinary code review or
formally). In the case of Coq, it is my understanding that the logical
foundation even changes regularly with new releases.

Yet a system that has everything that could be wanted from it is an
unachievable goal. Users or interested parties eventually find something
missing so a process of endless revision of the foundations begins.

This does not seem to happen with foundations based on set theory. ZFC
(possibly augmented with proper classes and large cardinals) seems to be
both sufficient for all mathematics and written in stone (in the sense
that we are not continuously revising the foundations continuously).

What is thus the motivation for the search for logical foundations and
systems based on “rich” type theory (beyond higher order logic)? Setting
aside philosophical interest in type theories (intuitionism), is there
some advantage to them as foundations or practical systems beyond the
built-in syntactic sugar? I am missing something?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 find existing developments in HOL4?

[Mario Castelán Castro]

> Why did you ignore Google web search (www.google.com) and Google scholar 
> search (scholar.google.com)?   DuckDuckGo is built-in supported by some open 
> source products, but I think it’s generally a garbage.

Google has a lot of private data about people. They can do, and do, many
bad things with this data. I can not stop Google surveillance, but I do
not want to make their task easier. Anyway, Startpage is an independent
proxy for Google Search therefore the results should be similar to what
Google Search would provide directly. In my experience DuckDuckGo has
served well enough. It is my main search engine.

Unfortunately, I still use Google Scholar because I have not found a
good general purpose alternative. I use PubMed when I need to search for
publications in medicine, but for mathematics/logic I do not know of any
good alternative. Suggestions would be very welcome.

> My experience: “HOL4” is a bad key word, because mostly what you may found is 
> a formalization done in old HOL versions. Instead, “formalization” + “higher 
> order logic” + domain keywords should be enough.

Thanks! This gives much better results for my aforementioned benchmark
test about prime numbers. ☺

There seems to be no signification formalization of elementary topology
in HOL4. I am aware that there is some topology in “/src/real” in the
HOl4 distribution, but it is very limited. Searching with DuckDuckGo,
Startpage and Google Scholar for “formalization "higher order logic"
topology” does not turn anything relevant. As my first development with
a proof assistant I am formalizing some theorems of elementary topology
in HOL4. I plan to develop and publish a theory which is suitable as the
foundation for further developments.

If you know of an existing formalization of elementary topology in HOL4
please let me know, so that I can avoid duplicating work.

Regards.

Note: It seems that you forgot to reply to the mailing list.

On 10/09/17 13:34, Chun Tian (binghe) wrote:
> Hi,
> 
> Why did you ignore Google web search (www.google.com) and Google scholar 
> search (scholar.google.com)?   DuckDuckGo is built-in supported by some open 
> source products, but I think it’s generally a garbage.
> 
> My experience: “HOL4” is a bad key word, because mostly what you may found is 
> a formalization done in old HOL versions. Instead, “formalization” + “higher 
> order logic” + domain keywords should be enough.
> 
> Regards,
> 
> Chun Tian
-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] [SOLVED] Theorems used by an invocation of simp, fs, rw or REWRITE_TAC.

[Mario Castelán Castro]

On 08/09/17 14:12, Mario Castelán Castro wrote:
> Is there some way to know what theorems or rewrite rules have been used
> by these simplifiers when acting over a goal in goal-based proof?

I found that this feature can be enabled setting the trace “simplifier”
to 1.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Theorems used by an invocation of simp, fs, rw or REWRITE_TAC.

[Mario Castelán Castro]

Hello.

Is there some way to know what theorems or rewrite rules have been used
by these simplifiers when acting over a goal in goal-based proof?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 restricted quantification and algebraic-like structures

[Mario Castelán Castro]

On 06/09/17 03:11, michael.norr...@data61.csiro.au wrote:
> This depends a little on what you mean by “find a type”.  In the initial 
> state of HOL, there are two types (bool and ind), and one operator -> 
> (function space).  The core axiomatization allows us to conclude that bool 
> has two elements, and that ind has at least aleph_0 many elements. Applying 
> the function operator generates a type that is strictly bigger than the 
> exponent/domain type. With these tools, it is clear that one cannot construct 
> a type with cardinality one. 
> 
> Yet, the predicate ?y. !x. x = y captures the idea of a type having just one 
> element. So, if I’m interpreting your question correctly, the answer is no. 

Yes, this answers my question. Thanks you.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] About restricted quantification and algebraic-like structures

[Mario Castelán Castro]

Hello.

This is a question concerning the formalization of “generic” structures,
like a group, ring, field, topological space, vector space, and so on.
That is, structures that satisfy some “axioms” and need not be unique up
to isomorphism.

In the theory “ring” as found in the HOL4 library the definition of
“is_ring r” requires that there is a type of elements of the ring “r”,
call it “α”, and that the ring sum, product and inverse are functions
“[α → ]α → α” that obey the ring axioms. It appears that if one wants to
use this theory, one must have such a type “α”.

Consider the case that I do not have such a type a-priory. Instead I
have a larger type “β” where the elements that satisfy the predicate
“P:β → bool” form a ring. Is there any way to apply the ring theory from
the HOL4 library to this “subset” of β?

If ringTheory used a predicate to represent ring elements “P:γ→bool”
instead of a type, then there would be no such problem. Obviously this
would require that the theorems of ring use the restricted quantifiers
(“∀::P…”, “∃::P…”, et cetera).

What is the reason that several theories in the HOL library use the
approach of “type as the elements of the ring/topology/etc.” instead of
“predicate as the sets of elements of the ring/topology/etc.”?

Additionally, when one has a predicate and functions defined over the
same type (as in my ring example above) that meet some algebraic axioms,
is it always possible (in HOL4) to define a *type*, for which *all*
elements meet the same algebraic axioms?

Thanks.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light?

[Mario Castelán Castro]

On 02/09/17 18:05, Chun Tian (binghe) wrote:
> My highly subjective opinions: as an end-user, I choose HOL4 over HOL light 
> because I think and/or found:
> 
> 1. Standard ML is a better language than OCaml (as a programming language);
> 2. Poly/ML is a better implementation than OCaml (as a language 
> implementation);
> 3. HOL4 has a richer and more systematic theory library.
> 
> The logic core of HOL family of theorem provers is already much simpler than 
> others (e.g. Coq). Although the logic core of HOL light sounds more 
> reasonable and slightly simpler, the fact that it’s implemented in OCaml and 
> it lacks of many useful theories which I depend on, has lead me to stick with 
> HOL4 and ignore HOL light. But I admit, as theorem provers they’re equally 
> powerful, given both infinite time, I can’t imagine any formalization project 
> which can only be done in one of the two software.

Thanks for your reply. I understand your point.

I had an impression which is in agreement with your commentary: I know
very little of SML and OCaml to make an overall comparison. But I know
that a point where SML easily beats OCaml is that SML has a clear and
formal specification and is a stable language with many implementations,
very much like C or Common Lisp. On the other hand, OCaml appears to
change frequently and it is implementation-centered like Python instead
of specification-centered.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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 Light – Re: What is the practical (end-user level) difference between HOL4 and HOL Light?

[Mario Castelán Castro]

On 01/09/17 15:12, Ken Kubota wrote:
> Hi Mario,
> 
> John has explained some of his motivation for HOL Light in an email
> available online at […]

Thanks you. These links provide useful insight.

> A HOL family tree with both HOL4 and HOL Light can be found at […] and at […].

Yes, I have read those papers. But they focus mostly on the foundational
and not the user-level differences.

> What makes HOL Light special (in my opinion), is that it tries to
> reduce the logic to a simpler logical core (hence, HOL "Light").
> In this respect, it is very similar to the philosophy of Metamath and Q0/R0.
> 
> For this reason, I chose HOL Light as point of reference in my draft
> describing R0, writing that "HOL Light […] has [only] 'ten primitive
> rules of inference' [Harrison, 2009, p. 61]" [Kubota, 2015, p. 14].

I see. It is good to know. But these differences are abstracted from the
user who writes proofs using high-level tactics. I doubt that even at
the level of applying inferences to the theorem data type through the
OCaml or ML interface, it would make much difference whether –for
example, “SUBST”– is primitive or derived.

From the level of writing high-level proof scripts, is there any
difference between the systems, apart from the choice of
metalanguage/programming language (SML and OCaml) and the differences in
the name of the identifiers of tactics?

> Recalling our previous private communication, I could send you
> the draft describing R0, if you are interested (for private use only,
> please do not quote). I hope to publish a full description by the
> end of the year.

I thank you for your kindness and confidence.

I am still studying the “well-known” formal systems of type theory. I
have read chapter 1 of HOL4's “The HOL system LOGIC [For HOL
Kananaskis-11]” and I am currently reading “Type Theory and Formal
Proof: An Introduction” by R. Nederpelt and H. Geuvers (2014).

Thus although I am interested, I shall turn down your kind offer because
–right now– my background knowledge in type theory is very limited, and
could neither make much use of the draft nor provide the feedback that
is expected when sharing pre-publication drafts. I am fine waiting until
your paper is ready as I have much to read of the same topic in the
meantime. ☺

-
Regards.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Sad news regarding Mike Gordon

[Mario Castelán Castro]

It is sad news to hear. :(

We can not cheat death, but we can do something good with our life until
its eventual end. Many people die without leaving anything good. While I
am no expert in the HOL system, I can attest that Mike Gordon is a
person who left a positive legacy.

The phase “Write something worth reading or do something worth writing“
is appropriate, as Mr. Gordon for example wrote several papers that will
outlive all of us.

My condolences.

-- 
Do not eat animals, respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Indentation of proof script in Emacs

[Mario Castelán Castro]

On 2017-08-21 02:31 +  wrote:
>> *Is there some solution that gives C-like automatic indentation*
>> (without having to hack SML mode)?
>
>Short answer: no.

Thanks for your honest answer.

>If I run my cursor down column 0 and hit TAB at each point, the string and
>quotation both move inwards to column 6, and the tactic lines move across
>to column 7, creating:

I see.

For manually indenting several lines at once, the “indent-rigidly” command
(M-x TAB) is more convenient. The amount of space that it adds when using
shift is given by “tab-width” (even when “indent-tabs-mode” is nil).

>and I have no idea why there is a difference in the handling of the
>tactic line.  Luckily, tactics will typically indent correctly after the
>first line has been put to the right level.  I think the relevant parts
>of my .emacs config are:

What do you think about replacing the SML mode indentation function with
“indent-relative-maybe” as I mentioned in my previous message?

(defun sml-mode-sane-indent ()
  (setq-local tab-width 4)
  (setq-local indent-line-function 'indent-relative-maybe))
(add-hook 'sml-mode-hook 'sml-mode-sane-indent)

Then auto-indentation after  works reasonably, so it needs not be
disabled with “(setq electric-indent-chars nil)”. Moreover, M-x
indent-region will do a good enough job for many cases if one line before
the region is intended to what one.

For example, consider this trivial example:

val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);

Then I go to the beginning of the second line and press TAB.

val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);

Then I mark the other 2 lines and press TAB again once:

val DIVIDES_0 = store_thm(
"DIVIDES_0",
“!x. x divides 0”,
metis_tac [divides_def, MULT_CLAUSES]);

Done.

>Pull requests from capable emacs hackers would be gratefully received.
>Unfortunately, I am not a particularly capable emacs hacker, and I don’t
>have a great deal of time to spend on it at the moment.

Unfortunately I am no Emacs expert either. I have been using it for years
but I have only recently started to try to learn to use it properly.

I am also still learning HOL4. I do not know if I will stay with it or move
to a different proof assistant, since I am new to proof assistants overall
and I have yet to try the alternatives. However, if I become a regular
user, I will probably try to write a “HOL4-script-mode”.

Regards and thanks.

-- 
Do not eat animals, respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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] Indentation of proof script in Emacs

[Mario Castelán Castro]

Hello.

Is there some way to make the behavior of auto-indentation in GNU Emacs
when writing for proof scripts more predictable? By default it uses SML
mode, which is shipped with Emacs. I can not find any documentation about
it other than the built-in help, which is not of much use.

I find that SML mode chooses indentation level in an unpredictable way, for
example, it intend the following code this way:

val DIVIDES_0 =
store_thm(
"DIVIDES_0",
``!x. x divides 0``,
  metis_tac [divides_def,MULT_CLAUSES]);

(note the extra 2 spaces before “metis_tac”)

If I put “store_thm” in a line of its own, I get an exaggerate amount of
indentation:

val DIVIDES_0 = store_thm
("DIVIDES_0",
 ``!x. x divides 0``,
   metis_tac [divides_def,MULT_CLAUSES]);

Disabling indentation completely (e.g.: M-x fundamental-mode) is not a
satisfactory solution. Is there some way to make Emacs perform sensible
indentation for HOL proof scripts?

Thanks in advance.


pgp4KJ7NyqMKU.pgp
Description: OpenPGP digital signature
--
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