[isabelle] Issues of Isabelle

[José Manuel Rodriguez Caballero]

to develop better proof assistant and possible rewrite
everything. Instead of basing everything on top of Isabelle in its current
form (0 / 0 = 0).

The beautiful formula 0 / 0 = 0 makes sense to a mathematician, although
this was not the original motivation. I interprete it as the identification
between 0 and infinity. Indeed, let G be the multiplicative group of
non-zero real numbers. This is a Lie group with two connected components:
the positive real numbers and the negative ones. Let H be the union of G
with the zero. In H we take the topology from G and we define the set of
fundamental neighbourhoods of zero to be the set of real numbers either
larger than n or smaller than 1/n.

Consider the function f(x) = 1/x if x is non-zero and f(0) = k. This
function transform H into itself. It is easy to prove that f(x) is
continuous in H if and only if k = 0. Notice that f(0) = 0 can be rewritten
as 0/0 = 0 using a slight abuse of notation.

Jose M.

[José Manuel Rodriguez Caballero]

typographical correction (I forgot to multiply by 0 at the right)

0*f(0) = 0 can be rewritten as 0/0 = 0 using a slight abuse of notation.

Jose M.



2018-08-15 5:28 GMT-04:00 José Manuel Rodriguez Caballero <

Post by José Manuel Rodriguez Caballero

to develop better proof assistant and possible rewrite
everything. Instead of basing everything on top of Isabelle in its current
form (0 / 0 = 0).

The beautiful formula 0 / 0 = 0 makes sense to a mathematician, although
this was not the original motivation. I interprete it as the identification
between 0 and infinity. Indeed, let G be the multiplicative group of
the positive real numbers and the negative ones. Let H be the union of G
with the zero. In H we take the topology from G and we define the set of
fundamental neighbourhoods of zero to be the set of real numbers either
larger than n or smaller than 1/n.
Consider the function f(x) = 1/x if x is non-zero and f(0) = k. This
function transform H into itself. It is easy to prove that f(x) is
continuous in H if and only if k = 0. Notice that f(0) = 0 can be rewritten
as 0/0 = 0 using a slight abuse of notation.
Jose M.

[José Manuel Rodriguez Caballero]

another typographical correction
in place of
the set of real numbers either larger than n or smaller than 1/n.

read

set of real numbers which in absolute value are either larger than n or
smaller than 1/n.


2018-08-15 5:33 GMT-04:00 José Manuel Rodriguez Caballero <

Post by José Manuel Rodriguez Caballero
typographical correction (I forgot to multiply by 0 at the right)
0*f(0) = 0 can be rewritten as 0/0 = 0 using a slight abuse of notation.
Jose M.
2018-08-15 5:28 GMT-04:00 José Manuel Rodriguez Caballero <

Post by José Manuel Rodriguez Caballero

to develop better proof assistant and possible rewrite
everything. Instead of basing everything on top of Isabelle in its current
form (0 / 0 = 0).

The beautiful formula 0 / 0 = 0 makes sense to a mathematician, although
this was not the original motivation. I interprete it as the identification
between 0 and infinity. Indeed, let G be the multiplicative group of
the positive real numbers and the negative ones. Let H be the union of G
with the zero. In H we take the topology from G and we define the set of
fundamental neighbourhoods of zero to be the set of real numbers either
larger than n or smaller than 1/n.
Consider the function f(x) = 1/x if x is non-zero and f(0) = k. This
function transform H into itself. It is easy to prove that f(x) is
continuous in H if and only if k = 0. Notice that f(0) = 0 can be rewritten
as 0/0 = 0 using a slight abuse of notation.
Jose M.

[Lawrence Paulson]

Hello. I want to share my personal experience with Isabelle. I will list
its issues and give some ideas, which can be implemented in Isabelle and
other proof assistants. This letter is attempt to help you, I don't want to
blame you.

Dear Askar, thanks for your thoughtful message. It's always valuable to have feedback from new users.

1. The question of partial functions has been around for a long time, and the following 20 year old survey is still worth reading: Treating Partiality in a Logic of Total Functions <http://wwwbroy.in.tum.de/publ/papers/MS97.pdf> (Müller and Slind, 1996). I won't repeat the arguments here. I would merely mention that other approaches have been tried in other systems. PVS <http://pvs.csl.sri.com/> can support partial functions (by generating validity conditions), as did IMPS <https://link.springer.com/article/10.1007/BF00881906> (using a calculus of definedness). As I understand it, type theory-based systems such as Coq <https://coq.inria.fr/> also handle partial functions (using the implicit argument approach you outline, along with irrelevance of proofs). The penalty for using more complicated approaches is that proofs become longer and more difficult.

It's a good bet that anybody using Isabelle or HOL is willing to live with a calculus of total functions only. As that survey article describes, we can formalise what we want to express well enough, without being forced to repeatedly prove that subexpressions are defined. You mention your wish to make assumptions explicit (e.g., that an FOL term is well-defined), even when those assumptions aren't needed to prove the given property. But one could equally say that the formalism itself is telling us which assumptions are needed and which are not. Your theory only regards an FOL term as well-defined if each function application has the required number of arguments, and yet the set of variables in a raw term is perfectly meaningful regardless of that.

Division is another excellent example. It's easy to imagine that postulating x/0 = 0 introduces inconsistency, but instead it reveals which identities are sensitive to division by zero and which are not. We discover that x/x=1 still requires the assumption that x is nonzero, while (u+v)/x = u/x + v/x does not. Most of us are happy to have as few assumptions as possible, as this makes proofs easier.

2. We'd certainly like to have a proof method that works for all simple cases, but it isn't easy. In theory, auto should do it, but as you note, it doesn't (and auto is unlikely to change very much). Work on better automation has been ongoing for decades now. Sledgehammer is one attempt at a magic bullet, but it's also defeated in some surprisingly easy cases. But a lot of new work is promising, e.g. Zhan's auto2 <https://arxiv.org/abs/1707.04757> and some recent work by Nagashima, e.g. PSL <https://arxiv.org/abs/1606.02941>.

Mathematicians who use Isabelle today are pioneers, which means that some things will be painful, but on the other hand, they will be the first to make new discoveries.

Larry Paulson

[Lars Hupel]

You said that "x / x = 1" requires assumption "x ~= 0", but "(u+v)/x = u/x
+ v/x" does not. And you present this as feature. This is not a feature,
this is absolutely strange behavior. What will "working mathematician" say
about this? Let both theorems require "x ~= 0". This makes slightly harder
to use this theorems, but this will make whole system more sound.

As Larry has already said, this has literally nothing to do with
soundness. See also <https://www.hillelwayne.com/post/divide-by-zero/>
for a survey on this.

So, when this "next generation of proof assistants" will emerge?! How long
should I wait for them?! Why not to create them right now?!!!

Nobody prevents you from working on a next-generation proof assistant.
In fact, I think many people would be very excited about a proof of concept.

Cheers
Lars

[Peter Lammich]

On Do, 2018-08-23 at 18:35 +0300, Askar Safin via Cl-isabelle-users

Post by Lars Hupel
As Larry has already said, this has literally nothing to do with
soundness. See also < https://www.hillelwayne.com/post/divide-by-ze
ro/ >
for a survey on this.

I will repeat: main drawback of Isabelle's totality is need to
manually
keep track of assumptions, i. e. see my first letter, where I had to
write
all assumptions in comments without any help from Isabelle. This was
main
reason I gave up on developing this proof script more.
And the second drawback is that what I write doesn't correspond to
what I
mean. When I write "(x + y) / z = x / z + y / z" I mean "only if z ~=
0",
but Isabelle doesn't require such assumption. So, I have to manually
make
sure that such assumption is always present in the context and thus
what I
write is actually correspond to what I mean.

Another option would be to encode partiality explicitly, on top of HOL,
e.g., by lifting everything into an option monad. Then, you could use
Isabelle's standard reasoning tools to reason about definedness. I
doubt that definedness is trivial enough to do it fully automatic,
e.g., what is about "1/f(x)", with a very complicated f, that has a
very complicated proof that !x. f(x) ~= 0.

However, current Isabelle lacks automation or syntax support for such
an embedding, but maybe this might be a more feasible short-term
solution than writing a new proof assistant from scratch.

So, current approach lacks some degree of automation.
And finally, I will say again that division is partial in actual
mathematics. Actual proofs assume partial division, and proof
assistants
must do the same to be close to real math. I will repeat that phrase
"Let's
assume that b ~= 0 and a / b = 4" is OK for mathematical text, but
"Let's
assume that a / b = 4 and b ~= 0" is not, and thus the same should
apply to
proof assistants. 

This imposes an execution order! But don't you also want to have 
"a&b = b&a", and substitution? then both terms must have the same
meaning.

Of course, in the option monad, you could explicitly define a 
short-circuit version of "&", which, however, would not be commutative.

--
  Peter

p.s.
  My interest in this stuff stems from the fact that explicitly partial
terms are much nicer parametric than underspecified total ones, e.g.,
the term 
"case l of [] => None | x#_ => Some x" is parametric (the element type
of the list can be replaced, without invalidating any theorems),
whereas "hd l" is not (the "undefined" values on two types need not be
related in any way!)

==
Askar Safin
http://vk.com/safinaskar

[Lawrence Paulson]

Dear Askar,

The problem is that different mathematicians have quite different ideas of what a proof assistant should do. Some people want mathematics to be typed while other people firmly reject type systems. Some would like to see actual texts formalised, including syntactic elements such as parentheses. Some would like to be notified when the statement of a theorem includes assumptions not needed for the proof. You have the opposite wish: you'd like some definitions to be conditional on certain well-formedness assumptions, even when they aren't strictly necessary. It's not a common wish, but note that once you leave the world of definitions, you can include additional assumptions in theorems and they will be checked when you use the theorems.

An interesting observation about division is that when we put x/0 = 0, we do not change the meaning of definition where it is defined but merely extend its domain. Contrast this with the way division is implemented in computer hardware and in most computer languages: in OCaml I can type

# -4 mod 3;;
val it : int = -1

and this violates an elementary property of division: that the remainder lies between 0 and the divisor. In other words, division on a computer (any computer) regularly delivers the wrong answer. Somehow people cope with this. Similarly people are able to cope with the formalisms of today's proof assistants, none of which are a perfect match to mathematical reasoning.

It may be that in the future, somebody will come up with a natural and practical formalisation of partial functions. Probably people are getting research funding for this sort of work. But I have funding for a different research programme.

Larry

Post by Lars Hupel
As Larry has already said, this has literally nothing to do with
soundness. See also < https://www.hillelwayne.com/post/divide-by-zero/ >
for a survey on this.

I will repeat: main drawback of Isabelle's totality is need to manually
keep track of assumptions, i. e. see my first letter, where I had to write
all assumptions in comments without any help from Isabelle. This was main
reason I gave up on developing this proof script more.
And the second drawback is that what I write doesn't correspond to what I
mean. When I write "(x + y) / z = x / z + y / z" I mean "only if z ~= 0",
but Isabelle doesn't require such assumption. So, I have to manually make
sure that such assumption is always present in the context and thus what I
write is actually correspond to what I mean.
So, current approach lacks some degree of automation.
And finally, I will say again that division is partial in actual
mathematics. Actual proofs assume partial division, and proof assistants
must do the same to be close to real math. I will repeat that phrase "Let's
assume that b ~= 0 and a / b = 4" is OK for mathematical text, but "Let's
assume that a / b = 4 and b ~= 0" is not, and thus the same should apply to
proof assistants. It should be possible to directly convert any mathematical
text to proof script.
==
Askar Safin
http://vk.com/safinaskar

[Chun Tian (binghe)]

Hi,

I want to point out a similar problem in Isabelle’s Extended_Real theory, in which the sum operator as a total function permits that ∞ + (-∞) = (∞::ereal), the case in which textbooks said it should be avoided (i.e. no definition):

function plus_ereal where
"ereal r + ereal p = ereal (r + p)"
| "∞ + a = (∞::ereal)"
| "a + ∞ = (∞::ereal)"
| "ereal r + -∞ = - ∞"
| "-∞ + ereal p = -(∞::ereal)"
| "-∞ + -∞ = -(∞::ereal)"

HOL4’s extrealTheory [1] currently has the same problem, but its original authors have fixed the definition, and soon it [2] will be submit to HOL4 official.

What I observed is, having a total function here, many related theorems have simpler proofs and less assumptions, because otherwise lemmas like "a + b = b + a” is not true any more, if we don’t put extra assumptions that a and b are not mixing of ∞ and (-∞). I found that, theorem prover doesn’t forbid its user to write down a term which has no definition, just with that term it is not possible to manipulate it with any theorem.

Is above definition of “plus_ereal” *wrong*? I think so, but I don’t think everyone agrees with me.

—Chun

[1] https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/probability/extrealScript.sml <https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/probability/extrealScript.sml>
[2] https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml <https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml>

Post by Lawrence Paulson
Dear Askar,
The problem is that different mathematicians have quite different ideas of what a proof assistant should do. Some people want mathematics to be typed while other people firmly reject type systems. Some would like to see actual texts formalised, including syntactic elements such as parentheses. Some would like to be notified when the statement of a theorem includes assumptions not needed for the proof. You have the opposite wish: you'd like some definitions to be conditional on certain well-formedness assumptions, even when they aren't strictly necessary. It's not a common wish, but note that once you leave the world of definitions, you can include additional assumptions in theorems and they will be checked when you use the theorems.
An interesting observation about division is that when we put x/0 = 0, we do not change the meaning of definition where it is defined but merely extend its domain. Contrast this with the way division is implemented in computer hardware and in most computer languages: in OCaml I can type
# -4 mod 3;;
val it : int = -1
and this violates an elementary property of division: that the remainder lies between 0 and the divisor. In other words, division on a computer (any computer) regularly delivers the wrong answer. Somehow people cope with this. Similarly people are able to cope with the formalisms of today's proof assistants, none of which are a perfect match to mathematical reasoning.
It may be that in the future, somebody will come up with a natural and practical formalisation of partial functions. Probably people are getting research funding for this sort of work. But I have funding for a different research programme.
Larry

Post by Lars Hupel
As Larry has already said, this has literally nothing to do with
soundness. See also < https://www.hillelwayne.com/post/divide-by-zero/ >
for a survey on this.

I will repeat: main drawback of Isabelle's totality is need to manually
keep track of assumptions, i. e. see my first letter, where I had to write
all assumptions in comments without any help from Isabelle. This was main
reason I gave up on developing this proof script more.
And the second drawback is that what I write doesn't correspond to what I
mean. When I write "(x + y) / z = x / z + y / z" I mean "only if z ~= 0",
but Isabelle doesn't require such assumption. So, I have to manually make
sure that such assumption is always present in the context and thus what I
write is actually correspond to what I mean.
So, current approach lacks some degree of automation.
And finally, I will say again that division is partial in actual
mathematics. Actual proofs assume partial division, and proof assistants
must do the same to be close to real math. I will repeat that phrase "Let's
assume that b ~= 0 and a / b = 4" is OK for mathematical text, but "Let's
assume that a / b = 4 and b ~= 0" is not, and thus the same should apply to
proof assistants. It should be possible to directly convert any mathematical
text to proof script.
==
Askar Safin
http://vk.com/safinaskar

[Makarius]

lemma l1: assumes "x ~= 0" shows "(u+v)/x = u/x + v/x" sorry
notepad begin
assume a1: "c ~= 0"
... (* Some steps *)
have "(a+b)/c = a/c + b/c" using l1 and a1 by auto

Just a side remark on proper naming of facts in Isabelle/Isar: if you
need meaningless names, you can just use *, **, *** or decimal numerals
1, 2, 3, ...

There is no need to have a prefix like "l" for "lemma" or "a" for
assumption above. In fact, it is bad style to decorate fact names
according to there provenience, especially in Isar proofs, where facts
often change there origin between 'assume', 'obtain', 'case', 'have',
'show', 'note' etc.

have "(a+b)/c = a/c + b/c" using l1 and a1 by auto

More stylistic notes: Isar goals can have before and after it. Before
you have important things from the local proof context, after it
relevant global things from the library. According to this rule of of
thumb, the above becomes:

from a1 have "(a+b)/c = a/c + b/c" using l1 by auto

This discipline works more smoothly, if you always expand the old
(obsolete) command abbreviations "hence" == "then have" and "thus" ==
"then show" -- on average they make proof texts longer, and harder to write.


Makarius

[Dr A. Koutsoukou-Argyraki]

Dear Askar,

When I write proof scripts, it is nearly impossible to figure which
proof
method (auto, blast etc) I should use and why. Usually I first try
"auto",
then "blast", then, say, "fastforce", then "metis" etc. This is very
annoying.

just a small practical tip (in case you don't use this already)
it saves plenty of time to use the keyword : "try0 "
which tries several methods and tells you if one of them works,
so the users don't need to try them all one by one themselves.

Also the keyword "try" does the above plus moreover runs sledgehammer
and looks for counterexamples with quickcheck and nitpick,
so you don't need to try all the proof methods separately one by one
yourself.

Best wishes,
Angeliki