From: Ken Kubota <mail@kenkubota.de>

Where can I find this paper?

How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?

https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/#type_abstraction

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html

https://sympa.inria.fr/sympa/arc/coq-club/2020-02/msg00138.html (see section: B. Kevin Buzzard on Isabelle/HOL)

Ken Kubota

https://doi.org/10.4444/100

From: Manuel Eberl <eberlm@in.tum.de>

Where can I find this paper?

See here: https://doi.org/10.1007/s10817-019-09537-9How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?

I don't know why people keep claiming you need dependent types/type

abstraction/whatever to do abstract algebra.

We've had abstract algebra in Isabelle for well over 10 years (the

HOL-Algebra library, which is distinct from the new experimental

approach presented in the above paper, which is more like a proof of

concept). There was even a paper about the existence of the algebraic

closure of fields at ITP 2020, which is a very advanced result. (I don't

think any other system has that result yet, although Lean is well on its

way and Coq has it at least for countable fields).

We don't have schemes, but that is not, as Kevin suggests, because

Isabelle/HOL is too weak to define schemes – indeed I did it for him a

while ago in response to that very article just to demonstrate that it

can be done and it's not difficult (although whether it is pleasant to

work with them is another matter; I cannot say because I have not

tried). The main reason why we don't have schemes is quite simply

because there are not /that/ many mathematicians in the Isabelle

community and none of the ones who are seemed to care about schemes

enough to formalise them. I barely know what schemes are, and I would

imagine it is the same for most of the Isabelle community, so why should

I formalise something that I know virtually nothing about? In order to

formalise something, it is good to have a good informal understanding of

it first. If I had some concrete goal and schemes were the way to get

there, I would look into it, but otherwise, I'd rather stick to doing

things that are closer to my field of expertise.

That said, it is of course entirely possible that there is some

mathematics that is too tedious to do in Isabelle/HOL due to a lack of

dependent types; some people, like Sébastien Gouëzel, have said

something to that effect. But saying that abstract algebra in general is

not possible without them is certainly a huge overstatement.

The way abstract algebra is done in Isabelle is simply to have some big

enough type and the carrier of your group is then only a subset of that

type and not the entire type. HOL-Algebra additionally also packages the

group operations up into a record and uses locales to bundle all the

group axioms together. It's a bit painful and perhaps not as natural as

it is in Coq and Lean, but it undoubtedly works.

HOL-Analysis has similar "relativised" notions of topologies. Normally,

the topology of a type always spans the entire type and is fixed for

that type using type classes, but one can also have topologies as values

and then say that a set is open w.r.t. a particular topology.

The main disadvantage of this is that you have two parallel

developments: the typeclass-based ones and the relativised ones. That is

certainly a drawback, but people (cf. Mikhail Chekhov) seem to be

working on making this smoother.

Cheers,

Manuel

From: Lawrence Paulson <lp15@cam.ac.uk>

This is nothing. Too often I hear claims that dependent types are *necessary* to do formal mathematics. I have seen “proof assistant” defined as “software implementing the propositions-as-types principle". And there is a widespread idea that the “LCF architecture” is an instance of propositions-as-types. Not very long ago, I had to explain at great length how LCF's use of an abstract type eliminated the need to store proofs (to a person exceptionally familiar with functional programming). Such preconceptions seem to be widespread even among some experienced professionals.

Larry

From: Ken Kubota <mail@kenkubota.de>

It is not legitimate to mix up the question of dependent types (or type abstraction) with other, obviously wrong approaches.

And I find it difficult to call Mike Gordon's suggestion as well as the clear statements by John Harrison, Freek Wiedijk, and others on the limitations of the HOL type system "nothing".

Often some features can be emulated by auxiliary techniques, as this has already been the case with the traditional HOL system.

But then the mathematical expression is less natural, and usually not all formal statements can be expressed.

If there is an obvious dependency, clearly it is desirable to express this symbolically in formal logic.

Ken Kubota

https://doi.org/10.4444/100

From: Ken Kubota <mail@kenkubota.de>

Am 23.07.2020 um 14:44 schrieb Manuel Eberl <eberlm@in.tum.de>:

Where can I find this paper?

See here: https://doi.org/10.1007/s10817-019-09537-9

Thank you very much.

I will try to have a look at it soon.

How are the type dependencies in expressing group theory covered, as type abstraction, as suggested by Mike Gordon, still isn’t implemented in HOL?

I don't know why people keep claiming you need dependent types/type

abstraction/whatever to do abstract algebra.The way abstract algebra is done in Isabelle is simply to have some big

enough type and the carrier of your group is then only a subset of that

type and not the entire type. HOL-Algebra additionally also packages the

group operations up into a record and uses locales to bundle all the

group axioms together. It's a bit painful and perhaps not as natural as

it is in Coq and Lean, but it undoubtedly works.HOL-Analysis has similar "relativised" notions of topologies. Normally,

the topology of a type always spans the entire type and is fixed for

that type using type classes, but one can also have topologies as values

and then say that a set is open w.r.t. a particular topology.The main disadvantage of this is that you have two parallel

developments: the typeclass-based ones and the relativised ones. That is

certainly a drawback, but people (cf. Mikhail Chekhov) seem to be

working on making this smoother.

Let me ask directly. Is it possible to:

- Prove a property in an abstract way for all groups (e.g., the uniqueness of the identity element),
- and then, given a certain group, transfer (instantiate) this theorem for that particular group without having to carry out the proof again?

If so, please provide a link.

Your description above doesn't look like a natural representation at all.

a) Circumlocations are necessary ("have some big enough type and the carrier of your group is then only a subset of that type").

b) Duplication of structures ("two parallel developments: the typeclass-based ones and the relativised ones").

c) Auxiliary structures like type classes are needed.

d) Extra work is required to unify the parallel developments ("working on making this smoother").

I'm not too familiar with Isabelle's type classes.

But I vaguely remember that in the past they lead to an inconsistency (antinomy: negative self-reference) in Isabelle/HOL, and the way this was fixed was by manually tracking the dependencies, if I'm not mistaken.

However, this clearly contradicts the very idea of type theory, in which the formal language (the syntax: types) prevents the formulation of antinomies from the very beginning.

One may accept the fix as an auxiliary solution, but not more.

So altogether the impression is, that simply because the formal language (the type system) used here is too poor, a lot of problems and extra work are created.

There is no sense in defending an impoverished type system, in which trivial ideas such as the link (the dependency) between the type and the term level cannot be expressed naturally.

In particular, since it can easily be expressed using the lambda variable binder, as suggested by Mike Gordon.

Ken Kubota

https://doi.org/10.4444/100 <https://doi.org/10.4444/100>

From: Manuel Eberl <eberlm@in.tum.de>

On 23/07/2020 23:24, Ken Kubota wrote:

Let me ask directly. Is it possible to:

1. Prove a property in an abstract way for all groups (e.g., the

uniqueness of the identity element),

Of course:

lemma (in monoid) one_unique:

assumes "u ∈ carrier G"

and "⋀x. x ∈ carrier G ⟹ u ⊗ x = x"

shows "u = 𝟭"

What you cannot do (due to lack of type-level quantification) is write

down a statement like "there exists a group G such that …" without

fixing the type of G. But I've never seen that cause problems in practice.

- and then, given a certain group, transfer (instantiate) this theorem

for that particular group without having to carry out the proof again?

If so, please provide a link.

All you have to prove is that the structure you're looking at is indeed

a monoid and then you get that theorem. For instance, HOL-Number_Theory

defines

definition residue_ring :: "int ⇒ int ring"

where

"residue_ring m =

⦇carrier = {0..m - 1},

mult = λx y. (x * y) mod m,

one = 1,

zero = 0,

add = λx y. (x + y) mod m⦈"

and then proves that this is a commutative ring for "m > 1". That gives

you for free that the additive and multiplicative subgroup are abelian

groups (and therefore monoids) and you can use the above fact. You can

also talk about subgroups of these groups and apply the result to them.

Your description above doesn't look like a natural representation at all.

a) Circumlocations are necessary ("have some big enough type and the

carrier of your group is then only a subset of that type").

b) Duplication of structures ("two parallel developments: the

typeclass-based ones and the relativised ones").

c) Auxiliary structures like type classes are needed.

d) Extra work is required to unify the parallel developments ("working

on making this smoother").

Yes, it's not great. But if you want to make a system work for practical

use, you always have to make some compromises and/or do a lot of

engineering. If I recall correctly, the Coq people have been investing a

lot of work into their type classes as well because they were found to

be insufficient for practical use. The Lean people recently overhauled

their system as well because (I think) it was too slow and unpredictable.

I'm not too familiar with Isabelle's type classes.

But I vaguely remember that in the past they lead to an inconsistency

(antinomy: negative self-reference) in Isabelle/HOL, and the way this

was fixed was by manually tracking the dependencies, if I'm not mistaken.

The problem wasn't type classes per se, but the low-level mechanism that

they use (overloaded constant definitions). These are now well

understood; I think there's even some kind of mechanised soundness proof

and more is on the way.

However, this clearly contradicts the very idea of type theory, in which

the formal language (the syntax: types) prevents the formulation of

antinomies from the very beginning.

One may accept the fix as an auxiliary solution, but not more.

You may oppose this on a philosophical and aesthetic level and that is

fine (I will hardly prescribe you your sense of aesthetics), but I for

one don't care much about such foundational issues as long as things are

sound. I just want a system that allows me to do stuff, and Isabelle/HOL

usually works great in practice.

So altogether the impression is, that simply because the formal language

(the type system) used here is too poor, a lot of problems and extra

work are created.

There is no sense in defending an impoverished type system, in which

trivial ideas such as the link (the dependency) between the type and the

term level cannot be expressed naturally.

In particular, since it can easily be expressed using the lambda

variable binder, as suggested by Mike Gordon.

I don't know anything about that lambda variable binder since I am not a

foundational guy; perhaps somebody else can comment on that. But I would

be surprised if it didn't make some things more difficult.

You criticise Isabelle/HOL as unnatural because you sometimes have to

express things in a certain way. But when I look at e.g. Coq

developments like the group theory behind Feit–Thompson, I was told they

restrict everything to finite groups represented them as lists. That

doesn't sound like a natural representation to me either. I'm sure they

/could/ have done it in a different, more natural way, but they chose

not to for some (probably technical) reason, and that's my point.

Systems like Coq and Lean also have the difference between Bool and Prop

and between definitional equality and other types of equality. I'm

pretty sure most mathematician find such distinctions very strange.

Isabelle/HOL also has two kinds of equality and a distinction between

bool and prop, but the logic allows hiding the difference completely in

practice.

(Just in case that your opinion is that Lean and Coq are also bad and

some other system X is the real solution: I am focusing on Lean and Coq

because they are the other two really big systems that have stronger

logics than Isabelle/HOL and it only makes sense to compare Isabelle/HOL

to systems of roughly comparable size.)

The way I see it, theorem proving is not a game of type-theoretic

one-upmanship. The objective is not to just pick the most powerful logic

imaginable and then you win. Expressiveness often comes with a price. I

think it is widely agreed upon that Isabelle has exceptionally good

automation and performance, and I'm sure that has a lot to do with the

LCF approach and the foundational choices (although I am hardly an

expert on this). Some Lean people, for instance, told me that their

simplifier is still very slow.

Another big advantage of Isabelle/HOL is that there is a huge library!

In my opinion, good libraries are far more important in practice than

powerful logical foundations. If you want to do some work requiring

analytic combinatorics (an example chosen because it is close to my

heart), the very expressive type systems of Coq and Lean and Agda will

not be particularly helpful, since none of them have any complex

analysis, let alone analytic combinatorics.

You're certainly right that we Isabelle/HOL people sometimes have to go

out of our way to do certain things (such as the duplication of

HOL-Computational_Algebra vs HOL-Algebra) and we are well aware of that.

Occasionally, you have to take a step back and figure out if the extra

work you have to do is still worth doing or whether you are working

against the system more than you are working with it. If that ever

happens, I might well consider switching to another, more suitable

system, but it hasn't happened so far.

If someone were to come along and make a system that offers the

advantages of Isabelle/HOL (structured proofs, good automation,

scalability) with the addition of dependent types, I would very

seriously consider switching as well (although the library issue remains).

Theorem provers are not artworks to be displayed on a wall in a gallery

for everyone to marvel at their beautiful and elegant design. They are

software intended for practical use by many people for a large variety

of different use cases, and they succeed or fail in practical applications.

Isabelle/HOL has worked well for a lots of practical use cases in

computer science and mathematics. If it will someday be the case that

other systems are clearly and unequivocally better, it will probably

just die.

But I think we're still far away from that.

Cheers,

Manuel

From: Lawrence Paulson <lp15@cam.ac.uk>

For sure. I have been noticing since the 1990s that with certain well-known systems you have to build a new library for each project. Precisely why isn’t clear; perhaps it is quite difficult to judge how heavy a use to make of dependent types. That the most popular Coq library (SSREFLECT) emphasises computable representations of mathematics seems remarkable, since it goes against the natural objective reasoning abstractly.

We have a similar situation ourselves with the Algebra library, where the use of records may have been a mistake. But at least we don’t feel compelled to throw it away and start fresh.

As I keep saying: the precise role of dependent types in the formalisation of mathematics is one of the key scientific questions of our field. It can only be answered empirically.

Larry

Last updated: Jan 25 2022 at 01:11 UTC