mathlib & constructivity

Stream: new members

[Scott Olson]

is there a standard library structure for isomorphisms, like this type in Idris? https://github.com/idris-lang/Idris-dev/blob/bae730a7ffaeae09a835a35bac132c141f3b50b3/libs/base/Control/Isomorphism.idr#L10-L16

i'm not sure what name to search for

[Simon Hudon]

In mathlib, you may want data.equiv.basic

[Simon Hudon]

https://github.com/leanprover/mathlib/blob/master/data/equiv/basic.lean

[Scott Olson]

thanks, that looks like what i want

that brings me to another question, though... should i be using mathlib, in general? is it basically just expected that most people will be using it?

[Simon Hudon]

Most people use mathlib because it's the largest repository of definitions and theorems in Lean and it keeps growing. Most importantly it has a lot of useful stuff

[Mario Carneiro]

That is certainly the intent... it is like the standard library of most programming languages

[Scott Olson]

is mathlib generally constructive or classical? or at least, does it clearly delimit which things depend on classical axioms? curious if i'll have to "wary" and check with #print axioms

[Simon Hudon]

You'll have to be wary. An effort is made to label classical theorems but people still use them pretty loosely

[Mario Carneiro]

mathlib is mostly classical. In particular, we only worry about constructivity in so far as it avoids the noncomputable marking. In any props or theorems we use AC freely

[Mario Carneiro]

There really isn't any point in being "wary" with #print axioms, because all you will achieve by doing that is get yourself in a tizzy about the many unnecessary uses of AC. Suffice it to say it is used in many difficult to avoid places in the foundation, some of which are in lean core and so are not even accessible to mathlib

[Scott Olson]

is there a discussion somewhere on the pros and cons of being classical for something like mathlib or just Props in general?

[Scott Olson]

the mathlib docs i've found so far just don't mention it

[Mario Carneiro]

We've had the discussion off and on for a while. Lean 2 made a concerted effort to be both constructive and classical

[Mario Carneiro]

At the beginning I held out hope that we could avoid AC when unnecessary, but at this point it's clear this isn't going to happen

[Simon Hudon]

I wonder if that's part of why mathlib was able to move quickly too

[Scott Olson]

i don't have much understanding of the implications of using such axioms in a system like Lean. i understand noncomputable prevents even bytecode, but any axioms at all prevent the term from evaluating to a normal form, and i'm curious if that can cause problems in practice

[Mario Carneiro]

We don't evaluate proofs at all in practice

[Mario Carneiro]

it doesn't matter if they are classical or not because they aren't programs

[Scott Olson]

that was my thinking for Prop, but i haven't been able to find much documentation talking about this point

[Mario Carneiro]

The only mechanism we have for evaluating proofs is #reduce and it falls over on all but the most trivial examples

[Mario Carneiro]

I guess there isn't much docs on this

[Mario Carneiro]

The VM evaluates anything that is not a Prop and is not noncomputable

[Simon Hudon]

When computation is involved, you really need to look at defs that are in Type 0 and over. Then an effort is often made to be efficient

[Scott Olson]

that makes sense, thanks for all the responses

[Simon Hudon]

:+1:

[Scott Olson]

i realized while talking to a friend just now that an interesting argument in favor of using fewer axioms is that it makes the proof potentially more "portable" to different formalisms, but that's somewhat aspirational and lacking it doesn't block anything in mathlib in the meantime

[Mario Carneiro]

Unfortunately, the axioms that really prevent portability of lean proofs aren't turn-off-able

[Mario Carneiro]

Most systems have some equivalent of the axiom of choice, but few have inductive types and a hierarchy of universes

[Kevin Buzzard]

i realized while talking to a friend just now that an interesting argument in favor of using fewer axioms is that it makes the proof potentially more "portable" to different formalisms, but that's somewhat aspirational and lacking it doesn't block anything in mathlib in the meantime

I'm a pure mathematician (as are several other people here) and one of the things that attracted me to Lean is precisely the attitude that "we will do maths like regular pure mathematicians do" (i.e. assume things like the axiom of choice, which in my circles is regarded as "just another axiom, with no particular reason to fuss about it".)

[Sean Leather]

I'm a pure mathematician (as are several other people here) and one of the things that attracted me to Lean is precisely the attitude that "we will do maths like regular pure mathematicians do" (i.e. assume things like the axiom of choice, which in my circles is regarded as "just another axiom, with no particular reason to fuss about it".)

On the other hand, some of the things that attracted me to Lean included the ability to do constructive mathematics, the nice syntax, a fast theorem prover, and a comprehensive library. :slight_smile:

[Scott Olson]

i figured some of what i said might have given away my friend's and my bias towards constructive type theories :P

i can see why Lean attracted pure mathematicians who might have otherwise used Coq or similar, though. the experience out of the box with Lean in VSCode is the best i've seen from any theorem prover

[Mario Carneiro]

I am also attracted to constructive mathematics generally, but the pure mathematicians have worn me down. :) I realize now that lean is not remotely geared towards limiting its axiom strength, and if you want a system for playing with axioms you should look elsewhere. "Having few axioms" only means having few interesting subsystems, and none of the available subsystems are recognizable to traditional mathematicians except possibly intuitionistic type theory

[Simon Hudon]

@Sean Leather how inconvenient is it for you that mathlib makes such liberal use of classical axioms?

[Mario Carneiro]

Instead, it seems much more likely that lean will be able to support doing logic at the meta level, which is something that few systems can currently do well. This approach is much more flexible, of course, with regards to its axioms and with the permissible methods of proof

[Sean Leather]

I haven't had any issues so far. I'm not even sure where I would run into any.

[Scott Olson]

i figure i'll just adjust my expectations of what exactly i will play with in lean, but it will still be suitable for a lot of the stuff i want to experiment with

[Sean Leather]

The only thing is this output:

#print axioms

quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
classical.choice : Π {α : Sort u}, nonempty α → α
propext : ∀ {a b : Prop}, (a ↔ b) → a = b

[Simon Hudon]

Is your requirement that functions be computable or actually to avoid the axioms?

[Sean Leather]

Computable, I suppose. I don't do anything actively to avoid axioms, but I don't think I use anything that does use the axiom of choice.

[Scott Olson]

#print axioms <name> will list the axioms used (transitively) for the given thing

[Scott Olson]

but as we discussed, this shouldn't be a problem in the bodies of proofs that will never need to be evaluated or examined by other proofs

[Sean Leather]

#print axioms <name> will list the axioms used (transitively) for the given thing

When I create an empty file, #print axioms shows what I wrote above. :smile:

[Scott Olson]

yeah, #print axioms just prints the axioms that are currently in scope

[Mario Carneiro]

Can anyone come up with a reasonable (not completely contrived) example of a computable function that uses AC/LEM in its definition?

[Mario Carneiro]

I will amend "not completely contrived" to not eliminable, in the sense that there isn't a way to write the same function without the axiom, or at least it's not easy to do so

[Kevin Buzzard]

on nat?

[Mario Carneiro]

sure, I doubt it makes a difference but nat -> nat is a fine target

[Kevin Buzzard]

I'm sure you're right but I'm such a noob at this sort of thing. A year ago I wouldn't even have been able to formalise the question rigorously.

[Mario Carneiro]

To give a hint on why it's even possible: nat.find will calculate the smallest value satisfying a predicate, given only a proof that there is such a value (in Prop). This proof can rely on any axioms, and the function will still be computable

[Kevin Buzzard]

What about f(n)=1 if Fermat's Last Theorem is true and 0 otherwise? It's completely contrived but I'm trying to get the hang of the question. All known proofs of FLT use AC.

[Mario Carneiro]

That won't work because f is just the constant function 1, it doesn't need any axioms for its definition

[Mario Carneiro]

But I think you are on the right track. Can you think of any forall exists theorem on nat that relies on AC?

[Simon Hudon]

I don't know how to formalize that statement but it seems like a computable function like you described cannot be constructed

[Mario Carneiro]

Here is an example that relies on the input being in a nonoptimal form: if the input is a function f : nat -> nat which is not the constant zero function, then you can computably find a nonzero nat in the range of f

[Simon Hudon]

That's true. I stand corrected

[Kevin Buzzard]

What about f(n)=1 if Fermat's Last Theorem is true and 0 otherwise? It's completely contrived but I'm trying to get the hang of the question. All known proofs of FLT use AC.

So by "computable" you mean "externally provable to be equal to a certain given fixed computable function", rather than "provable in Lean with/without AC to be equal to a certain given fixed computable function"

[Kevin Buzzard]

What about f(n)=1 if RH is true and 0 otherwise? Don't I need LEM to define this?

[Kevin Buzzard]

I'm still struggling to move away from the "contrived" part, as you can see ;-)

[Mario Carneiro]

If you pick something which is definitely not decidable, or not known to be decidable like RH, then the function won't be computable either. By "computable" I mean "passes lean's noncomputable check"; you can't write def f := if RH then 1 else 0 because RH is not decidable

[Scott Olson]

yeah, that would specifically require the classical instance for decidable that uses LEM internally, which is noncomputable, which forces f to be noncomputable

[Kevin Buzzard]

Here is something much less contrived but I am much less clear about whether it fits into the scope of this question. Let's say a pure mathematician proves that for every g>=2 there is a computable upper bound $B(g)$ for the number of rational points on a smooth projective curve of genus g over the rationals, and their proof uses a bunch of algebraic geometry and AC / LEM everywhere. I suspect I could find arithmetic geometers who were prepared to conjecture that this mathematical statement was true. If this result got proved, and it turned out that a deep theorem implied that $B(g)=10000*g$, this would not be an example, right? :-/

[Mario Carneiro]

You can write def f := if FLT then 1 else 0 only if you have already provided a computable proof of decidable FLT, which will involve a proof of FLT. This falls afoul of the second restriction because then you could just replace the definition of f with 1

[Mario Carneiro]

You are right, this is an interesting situation. If we know a bound on the function then we can skip the clever maths and just use the bound

[Mario Carneiro]

Somehow it has to be an existence theorem with no bound

[Edward Ayers]

How about f(n) is 1 if the nth turing machine halts and 0 otherwise? If I'm not mistaken the proof that f is total requires LEM.

[Mario Carneiro]

I have been thinking about examples like that, but again it needs to be computable

[Edward Ayers]

But that might be because I've never seen a constructive proof of halting problem

[Mario Carneiro]

To define that function you have to know whether the nth turing machine halts

[Edward Ayers]

Ah in that case I think that it's impossible.

[Edward Ayers]

As in you can always rewrite the function to not use AC

[Mario Carneiro]

Here's another way to put it: Find computable predicates p(n), q(m,n) such that if p(n) is true then there exists an m such that q(m,n), but there is no computable upper bound on the least satisfying instance

[Scott Olson]

so with nat.find we could find the least nat satisfying some predicate while only proving this search will actually terminate with, for example, a proof by contradiction (the kind that requires classical double negation elimination)?

[Edward Ayers]

I can just run the q machine on each value of m = 0,1,2,... in turn. Since there exists an m where q(m,n) works, that program will halt. Right?

[Mario Carneiro]

yes, that's the idea

[Edward Ayers]

So it's impossible (to find such computable predicates)

[Mario Carneiro]

that's the computable function

[Mario Carneiro]

hm, you may be right. The very constraint that makes it lean-computable will also produce a computable upper bound, namely this function

[Mario Carneiro]

but I think maybe "computable upper bound" isn't what I want either; it needs to be an upper bound that you can't prove using lean without AC

[Mario Carneiro]

you can't use this function as a proof because it requires a proof that it will halt to run

[Mario Carneiro]

If we use something weaker than DTT, it should be possible to use some Ackermann-like function here

[Edward Ayers]

Ok I think I see what you mean now. You want a pair p(n), q(m,n) where the existence of a satisfying mis proved using AC or LEM.

[Mario Carneiro]

exactly

[Johan Commelin]

Can you prove that such a function exists using AC?

[Mario Carneiro]

You can use whatever methods you like to prove the existence of such p and q, but they have to be computable functions

[Johan Commelin]

Ok, I should have put more emphasis on you in my last post (-;

[Johan Commelin]

I have no clue at all about all this computability stuff.

[Mario Carneiro]

I don't have a solution to this puzzle

[Mario Carneiro]

but I believe it is possible

[Edward Ayers]

I am still not satisfied that the question is well posed. If I found a p and q with that property. I could take the AC proof, throw it away and replace it with a machine that just tries all m. Eventually it would find the m (which I know but Lean doesn't) and Lean would use that. But then I guess my new program would have to run in unsafe mode.

[Mario Carneiro]

For a fixed n you can do that, but I don't think you can do that for all n

[Mario Carneiro]

i.e. if p(5) is true and it turns out that q(100,5) is the satisfying instance, then you can use an upper bound of 100 in the construction

[Johan Commelin]

Mario, do you want a proof that can only prove the upper bound under the assumption of LEM/AC?

[Mario Carneiro]

right

[Johan Commelin]

Or is it enough that we know no such proof.

[Mario Carneiro]

Even that would be nice

[Mario Carneiro]

I'm worried that since no axioms lean has the same consistency strength as lean + AC, it will not be able to prove any new turing machines halt

[Johan Commelin]

So, there are only finitely many abelian varieties of dimension g over rat with good reduction outside {favourite finite list of primes}.

[Johan Commelin]

I don't think we know any upper bounds on this. The proof is a celebrated theorem of Faltings and uses classical maths all over the place.

[Johan Commelin]

If your favourite finite list of primes is not empty, then this function is extremely hard to compute.

[Johan Commelin]

(Otherwise it is if g = 0 then 1 else 0.)

[Johan Commelin]

Does this mean that f g = card (abelian varieties of dim g with good reduction outside blah) is not computable?

[Johan Commelin]

Hmmm.... I'm too much of a newbie when it comes to such questions.

[Mario Carneiro]

hm, this theorem has AEA quantifier complexity, which is a bit hard to use

[Johan Commelin]

AEA?

[Johan Commelin]

\forall \exists \forall?

[Mario Carneiro]

"for all g, there exists an n such that all variety things don't have good reduction above n"

[Johan Commelin]

No, I don't think that's what it says.

[Mario Carneiro]

I assume there is a way to enumerate abelian varieties?

[Mario Carneiro]

and the theorem says this enumeration runs dry after a certain point

[Johan Commelin]

For all P : finset primes and for all g there exists n such that card { abvar of dim g and good reduction outside P } is less than n.

[Johan Commelin]

Well, an abelian variety is defined by a finite number of polynomials

[Mario Carneiro]

right, so we enumerate all such things

[Mario Carneiro]

and only a finite number of them will have good reduction

[Johan Commelin]

Right (the polys are over Q), so we could do that.

[Mario Carneiro]

so there is an upper bound on the last one with good reduction

[Mario Carneiro]

thus AEA

[Johan Commelin]

Right, but testing the good reduction has to happen at all primes outside P

[Johan Commelin]

So you can't enumerate that.

[Mario Carneiro]

oh, I see

[Johan Commelin]

But I guess you can compute some discriminant in terms of the polynomials

[Mario Carneiro]

the property of having good reduction depends on all p?

[Johan Commelin]

and then bad reduction at p implies that p divides the discriminant.

[Johan Commelin]

This works for elliptic curves (the case g = 1)

[Mario Carneiro]

then it is AEAE

[Johan Commelin]

Lol

[Mario Carneiro]

for all g/P, there exists n, such that for all abvars above n, there is a p such that the var has bad reduction at p

[Johan Commelin]

No, it isn't about abvars above n, I think.

[Johan Commelin]

At least I can't parse that.

[Johan Commelin]

Ooh, wait, you enumerated them

[Mario Carneiro]

that is to exclude the finite number of things with good reduction

[Johan Commelin]

Hmmm.... but we still need a decision procedure to determine if a bunch of polynomials defines an AV

[Mario Carneiro]

that's surely decidable

[Johan Commelin]

Ok, if you say so... I have no idea how to do that...

[Mario Carneiro]

I have no idea what an AV is, so there

[Mario Carneiro]

but it surely can't be more than AE complexity

[Johan Commelin]

It means that there exists a group structure on the solution set defined by the polynomials, and the solution set must be compact (in the algebro-geometric sense of compact)

[Johan Commelin]

Both seem hard to check at first sight.

[Edward Ayers]

For a fixed n you can do that, but I don't think you can do that for all n

Is this argument on the right lines?
If p and q are computable and we know that for all n, if p(n) then there exists a m such that q(m,n). Then there exists a computable function n -> m using AC. So I can find the code which runs that function, and put that in Lean. So n doesn't have to be fixed.

[Mario Carneiro]

but the code that runs that function uses AC

[Mario Carneiro]

oh you mean the code of a computable function

[Edward Ayers]

Right but I can find the code outside Lean and just put the code in

[Mario Carneiro]

but then you need to know it codes a (total) computable function

[Mario Carneiro]

and the proof of that uses AC

[Mario Carneiro]

lean won't just let you run whatever function you like

[Edward Ayers]

I can run the n->m in unsafe mode because it's not part of the proof. I just need to get the m

[Mario Carneiro]

the idea with this reduction is to build a computable function in no axioms lean, right? You can't run in unsafe mode since then you don't have a well defined term

[Mario Carneiro]

i.e. the m that you pick depends on n, so there is no closed term you can give for the function without unsafe lean stepping in to provide the m

[Jared Corduan]

how about this:
let A(n) be some computable predicate that requires either AC or LEM to show that either {n | A(n)} or {n | ~A(n)}is infinite. (in other words, A witnesses the nonconstructive nature of the infinite pigeon hole principle).

then let q1(m, n) be the statement that there is an n < x < m such that A(x) holds. and similarly define q2(m, n) with ~A(x). both of these are computable since A is computable. since either {n | A(n)} or {n | ~A(n)}is infinite, then for at least one of q1 or q2we can show the existence of such an m for any given n. but we need AC or LEM for the existence of the ms.

[Kenny Lau]

is there a tl;dr for this thread?

[Patrick Massot]

Do you really want me to write it?

[Kenny Lau]

well this thread is way too long, a tl;dr would be good, I don't see why not

[Patrick Massot]

Ok, let me try: constructivity questions are pointless.

[Kenny Lau]

I don't think that's a very faithful summary, nor is it contributing to the discussion at hand

[Patrick Massot]

I'm sorry, but you explicitly asked for it!

[Patrick Massot]

Anyway, I should work instead of trolling

[Mario Carneiro]

I don't think that works, although it's so close I can taste it. What is the computable function that we are defining?

[Mario Carneiro]

(Kenny, the gist is I posed a puzzle here and people are trying to solve it.)

[Jared Corduan]

well, it's one of two functions. either 1) it is f(n) is the least m>nsuch that A(n) or 2) it is f(n) is the least m>nsuch that ~A(n).

[Jared Corduan]

but I punted on giving you an actual A...

[Mario Carneiro]

But we can't define either of those functions unless we have a proof (possibly using AC) that A(n) is infinite (resp. co-infinite)

[Jared Corduan]

you can prove the infinite pigeon hole with AC and LEM, so all I'm missing is a good A, right?

[Mario Carneiro]

right, but if we assume A is something about which we can prove very little, then we can't prove A(n) is infinite, so 1) can't be defined, and we can't prove ~A(n) is infinite either, so 2) can't be defined

[Chris Hughes]

What's the constructive proof that there exists a natural such that a^n=1 in a finite group?

[Mario Carneiro]

If it is finite, then there is an upper bound on the cardinality, enumerate them all and test for equality

[Mario Carneiro]

(you need decidable equality)

[Jared Corduan]

ok, I might have misunderstood the problem! I thought we wanted an f that needed AC and/or LEM in order to be defined, though it was built from these computable predicates.

[Mario Carneiro]

That is what we want, but it also needs to be a term that represents a lean-computable function

[Mario Carneiro]

It is okay if the proof of existence of the term is nonconstructive, like you tried, but the term itself must contain a proof that it halts since lean expects as much

[Jared Corduan]

ah ok, I'll have to think about that some more!

[Reid Barton]

Could we do something like this? Inside Lean, build a language for programs in STLC or another system which Lean can prove is strongly normalizing, but incorporating the type $\hat \mathbb{N}$ = nondecreasing functions nat -> bool. Then the input to our function is a code for a function f from $\hat \mathbb{N}$ to bool together with a proof that f inf = tt (where inf $\in \hat \mathbb{N}$ is the constant function ff); we can enumerate such programs because the system is strongly terminating. In Lean+LEM, we can prove that every such function satisfies f n = tt for some finite n, and we ask that our function return the smallest such n.

[Reid Barton]

Actually we don't even need the type $\hat \mathbb{N}$, we can just use the whole type nat -> bool, but with the same idea.

[Reid Barton]

If f (const ff) = tt, then there must be some finite n such that f (\lam x, x > n) = tt.

[Reid Barton]

Then we seek g f = the least n for which the above holds, provided that f (const ff) = tt, otherwise 37

[Reid Barton]

(Compare http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/)

[Reid Barton]

Maybe this is actually still computable without LEM though

[Reid Barton]

Yeah, I doubt this can be made to work. If you can constructively define a normalizer for your language, then you can presumably modify it to keep track of the invocations of the argument, and return the largest number on which it is invoked, then search up to there. If you can't constructively define a normalizer for your language, then you should just use a normalizer for your language as the function we're looking for.

[Mario Carneiro]

Note that one way to "cheat" here is to have as input a nondecidable proposition, which you then use in the construction. I did something similar with my example of a function that takes as input a function that is not constant zero and returns a value in the range

[Mario Carneiro]

Here again we seem to be stuck: if we use STLC or something provably normalizing, then we won't need LEM to prove the compactness property, and if we use DTT functions then even AC won't help since compactness isn't provable (though true)

[Reid Barton]

Yes. We would need a language whose power is just right so that the proof of normalization requires LEM, which I have no idea how to go about (or whether it is even plausible that such a language could exist).

[Reid Barton]

Can we prove that Lean-with-N-universes is normalizing inside Lean-with-N+1-universes? What do we know about the relative consistency of AC?

[Reid Barton]

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

[Mario Carneiro]

I believe that Con(CIC+AC) = Con(CIC) for the same reasons as Con(ZF) = Con(ZFC)

[Reid Barton]

I wonder whether we can just describe a meta-level procedure for taking a function defined in Lean+AC and producing an equal one defined in Lean (using one more universe) explicitly

[Mario Carneiro]

I believe that lean-with-n-universes is normalizing in n+1 universes

[Mario Carneiro]

I have to prove that lean is normalizing first though :)

[Mario Carneiro]

any term of type nat -> nat may contain universe variables but is parametric in them, so you get the same result no matter what they are set to

[Kenny Lau]

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

I heard FLT uses universes

[Kenny Lau]

Fermat's Last Theorem

[Reid Barton]

by writing an evaluator for Lean+AC-in-N-universes in Lean-in-N+1-universes, and then at the meta level looking to see how many universes are actually used, picking N to be bigger than that and writing down a term in the model that corresponds to the given function

[Mario Carneiro]

It may be that even without any universe variables you still need type 3 or something in the term

[Mario Carneiro]

(re: kenny)

[Kenny Lau]

but is it just because nobody has cleaned up the proof yet?

[Kenny Lau]

do we really need type 3?

[Reid Barton]

Kenny is taking over for Patrick on trolling duty

[Kenny Lau]

i'm serious

[Mario Carneiro]

We know that ZFC is equiconsistent with ZF, but I think that may include a double negation translation

[Mario Carneiro]

(if you use IZF in place of ZF)

[Reid Barton]

I believe that Con(CIC+AC) = Con(CIC) for the same reasons as Con(ZF) = Con(ZFC)

This is unclear to me because, in the case of ZF, we start from classical logic, at least in the version I know. But that's not to say that LEM is required for the relative consistency, only that I don't know whether it is.

[Mario Carneiro]

I also know that classical prop calc is equiconsistent with intuitionistic

[Reid Barton]

@Kenny Lau https://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof (See the first few answers.)

[Reid Barton]

Mario, right, that seems plausible then.

[Kevin Buzzard]

What's the constructive proof that there exists a natural such that a^n=1 in a finite group?

Let n be the order of the group ;-)

[Kevin Buzzard]

Any term of type nat -> nat is equal (in a meta sense) to one defined without using universe variables right?

I heard FLT uses universes

Kenny that is fake news, but the rumour seems hard to kill. Some people might argue that "the proof is written using universes" (because at some point Wiles says the word "representable functor" and at some other point uses etale cohomology) but they can easily be expunged using standard tricks.