Confusing axioms in trivial theorem

Stream: lean4

[Ioannis Konstantoulas]

I would like to use the following assertion in my work (bare lean 4, no libraries):

theorem mwe {l : Nat} {ls : List Nat} : (l :: ls)[0] = l := rfl

Unfortunately, the assertion depends on a bizarre list of axioms:

theorem mwe {l : Nat} {ls : List Nat} : (l :: ls)[0] = l := rfl
#print axioms mwe

'mwe' depends on axioms: [Classical.choice, Quot.sound, propext]

The rfl is not the problem, any proof I give of this depends on Classical.choice and Quot.sound. Why is this, and is there a way to work with lists that avoids these axioms?

[Yaël Dillies]

Guess: Those axioms come from the l[0] notation.

[Patrick Massot]

I don't see anything bizarre in that list of axioms.

[Kevin Buzzard]

I don't know the answer to your question but I do know that Lean doesn't really make an attempt to support non-classical arguments and this won't be the first time you'll run into this sort of thing. There are various tactics which use classical axioms too (probably when they don't need to but it just makes things easier). In his recent type theory podcast Leo argues that constructivism is hard to support and he has not seen an impactful project which is blocked by this design decision to be classical.

[Kyle Miller]

Interesting, if you import Mathlib.Data.Nat.Basic then it only depends on propext. I think Yaël is right that it's the l[0] notation.

[Kyle Miller]

Reading the proof term, I think it's that simp is being run with arith := true to discharge the 0 < List.length (l :: ls) goal (and I'm inferring that it uses Classical.choice), but if you import enough mathlib then simp can handle the goal without making use of that option.

[Mario Carneiro]

yes, the basic theorems used in the simp_arith decision procedure have an unnecessary use of choice due to... split

[Matthew Ballard]

Indeed, using Nat.zero_lt_succ _ explicitly eliminates the axioms.

[Kyle Miller]

Here's the syntax:

theorem mwe {l : Nat} {ls : List Nat} :
    have h : 0 < List.length (l :: ls) := Nat.zero_lt_succ _
    (l :: ls)[0]'h = l := rfl

(If you have it, use haveI to prevent a let_fun in the term)

This works too:

theorem mwe {l : Nat} {ls : List Nat} :
    (l :: ls)[0]'(Nat.zero_lt_succ _) = l := rfl

[Ioannis Konstantoulas]

Kevin Buzzard said:

In his recent type theory podcast Leo argues that constructivism is hard to support and he has not seen an impactful project which is blocked by this design decision to be classical.

Of course, such a project will never be attempted if the stumbling block is l[0], so this is a self-fulfilling prophecy.

More importantly, I believe it is worth pursuing proofs with the weakest hypotheses that are "reasonable", both for the elegance/insight this can provide as well as the extensibility of the result. For example, someone may want to try weakening choice in a theorem to dependent or countable choice. What is reasonable is debatable, but to me it seems reasonable for list access to not depend on the axiom of choice.

[Kyle Miller]

Lean is extensible enough that you can modify what tactics are used to handle indexing goals; see the get_elem_tactic tactic in core Lean

[Kyle Miller]

Ioannis Konstantoulas said:

Of course, such a project will never be attempted if the stumbling block is l[0], so this is a self-fulfilling prophecy.

I take it you're meaning that l[0] seems very basic. But, it hides the fact that it's actually running a tactic to prove the index is within bounds for you. A less-fancy pre-Lean-4 version of this is docs#List.head, where you have to give a nonemptiness proof yourself.

[Mario Carneiro]

you can just use l[0]'_ if you want to provide the proof explicitly

[Kyle Miller]

(@Mario Carneiro That's a few messages up)

[Mario Carneiro]

but I agree with the thrust of Ioannis Konstantoulas 's argument, there are a bunch of things I could do to grow the choice free part of lean but which is blocked on stupid stuff in core. It's not just that lean doesn't care about constructivity, it is becoming more aggressively anti-intuitionistic over time

[Mario Carneiro]

to the point where a really simple proof fix to avoid a use of choice will end up with a long discussion and no progress, followed by a complaint that it takes up too much time of the maintainers and where are the big impactful projects?

[Mario Carneiro]

they say a journey of a thousand miles begins with a single step but if you can't take a step then no journeys will be happening

[Patrick Massot]

I think the point is exactly that Leo doesn't want to travel a thousand miles in this direction. Hence he refuses to take the first step.

[Kevin Buzzard]

My impression from the podcast was that he currently can't see where the interesting place is 1000 miles in that direction. This certainly aligns with my experience as a mathematician, where I was taught as an undergraduate that Hilbert and Brouwer had a disagreement, Hilbert won, and that was the end of it. I have since come to realise that this is not the message being taught in computer science departments but in Leo's podcast he seems to be arguing that a lot of program verification can also be done classically as well, which I had not appreciated. Leo seems to be good at making hard decisions about what and what not to support, for example he dropped univalence when moving to lean 3 and now seems to be dropping constructivism when moving to lean 4. There are plenty of communities using the other provers who are interested in these more exotic (at least to me) logics but I guess you have to choose your battles and like it or not this seems to be what Leo has chosen.

[Eric Wieser]

I think the discussion at #2414 has gotten rather muddied from here on about the difference between noncomputable and "uses classical.choice", which certainly doesn't help the prospects for that RFC

[Eric Wieser]

Patrick Massot said:

I think the point is exactly that Leo doesn't want to travel a thousand miles in this direction. Hence he refuses to take the first step.

Mario's argument as I understand is that Leo it only has to travel at most 3 steps (the first of which has already been carefully planned), and then the other 1000 miles are Mario's problem

[Mario Carneiro]

To be clear, I won't be going 1000 miles either. I'll probably go 1 mile and help others gearing up for the long haul

[Eric Wieser]

One thing to consider is that constructivist users might be more likely to be converted by attempting the long haul and finding it too hard to be worth the effort, than they are by being told "no we refuse to allow constructivism on principle"

[Mario Carneiro]

I really like to be able to sell lean as the proof assistant that you can use to do anything as long as you put enough time and effort into it. The only thing between you and your goals is... you. That's a really great feeling to have, very freeing, and lean4 does a really great job of it. I see this constructivism business as being in the same category: if I see a pilgrim walking to mecca I might give some pointers but ultimately the trek is up to them. But standing in their way just because I'm not a muslim is not very nice

[Sky Wilshaw]

It's one of the reasons that Lean stood out to me when I was first learning it - the focus on constructivism felt refreshing after being exposed to classical mathematics for the rest of my life.

[Henrik Böving]

What focus on constructivism? Classical logic is already introduced almost at the very beginning: https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html?highlight=classical#classical-logic

[Mario Carneiro]

well, the very fact that "classical logic" is introduced by this name, at the end as a separate category, after introducing a fully working basis for intuitionistic logic, contributes to this impression

[Mario Carneiro]

In actual classical logic texts it's three axioms + modus ponens and you are off to the races

[Mario Carneiro]

One of them is vaguely responsible for LEM but if you get rid of it you end up with a really weak implicational calculus, not intuitionistic logic

[Mario Carneiro]

or for example /\ and \/ will be definitions like p /\ q := ~(p -> ~q), without even considering a standalone axiomatization for them - why would you? it's a waste of axioms when a definition will do fine

[Ioannis Konstantoulas]

For the record, I am not a constructivist, nor am I aiming for constructive proofs of various theorems. I do care for using the weakest hypotheses I can reasonably work with to prove stuff; I see this as providing a service to people who want to use and extend my results (which includes my future self).

And I believe that the simpler, more widely used, and more fundamental a result is (e.g. propositions in core), the more important it is to eliminate dependence on extraneous hypotheses, so that more people can use it, more easily and in more contexts.

[Mario Carneiro]

Incidentally, the project https://github.com/leanprover-community/iris-lean I've been working on is an implementation of a separation logic framework with a bunch of nice tactics for manipulating the logic, and the embedded logic is essentially intuitionistic, and this is important because it has actual models (in fact, proofs in the logic really are proofs about a class of models) which are anti-classical. This isn't topoi, but you see a lot of similar discussion there: inside some internal language you really have to be intuitionistic because the classical axioms just don't hold in all models under consideration.

[Sky Wilshaw]

Sky Wilshaw said:

the focus on constructivism

I meant in Lean's type theory, not mathlib.

[Yuyang Zhao]

I would also like to see Classical.choice avoided in the most basic tactics such as split.
simp is relatively insignificant.

[Kevin Buzzard]

The argument for better support for non-classical logic being presented here seems to be "then we can do more". But it was already explained very early on in this thread how to do all the things that Ioannis wants to do in lean already without any changes to core, so this argument is incorrect. They have to avoid certain idioms -- but this is normal in the prover world if people want to use exotic logics. Look at how Voevodsky used Coq to do univalent mathematics, for example.

[Kevin Buzzard]

In particular the design decision is "everything is so configurable that you can do whatever you like". Don't like core split? Then just don't use it.

[Damiano Testa]

EDIT: I had written something wrong!

[Kevin Buzzard]

I would urge anyone who thinks that it's just a case of "change core and all the problems go away" to read Leo's detailed responses at lean4#2414 and then think about things from his point of view. Leo says that if he changes core then it won't solve the problem, there will still be cases where split works in a way not desirable to people working in exotic logics and who will still be arguing for more changes. Leo doesn't want this on his plate, he feels that the users can solve this themselves and he wants to make it their problem not his. If you are the lead dev in a project then sometimes you have to make hard decisions and this is a very good example.

[Marc Huisinga]

Kevin Buzzard said:

I have since come to realise that this is not the message being taught in computer science departments

Since this keeps coming up: Constructivism wasn't mentioned in our computer science department. I believe most CS people don't know what constructivism is and that it's mostly folks who are adjacent to theorem provers and related topics like logic and formal methods who are aware of it.

[Marc Huisinga]

Though from the people I've talked to, the automated formal methods people at our university didn't really seem to know much about it, either.

[Kevin Buzzard]

My impression from listening to the podcast is that lean 3 taught Leo the very important lesson that you cannot please all of the people all of the time and I think Mario's post above is an attempt to argue that this change to split will have this effect. Leo's response is that it won't work and there will still be people who are not pleased. Changing split now will come back to bite him later when people want him to change it again, observing that he's changed it once already so it's not unreasonable to change it more.

[Yuyang Zhao]

Kevin Buzzard said:

In particular the design decision is "everything is so configurable that you can do whatever you like". Don't like core split? Then just don't use it.

This is what Mario did with by_cases in Std4. But if possible, we all don't like to duplicate or replace tactics.

Kevin Buzzard said:

I would urge anyone who thinks that it's just a case of "change core and all the problems go away" to read Leo's detailed responses at lean4#2414 and then think about things from his point of view. Leo says that if he changes core then it won't solve the problem, there will still be cases where split works in a way not desirable to people working in exotic logics and who will still be arguing for more changes. Leo doesn't want this on his plate, he feels that the users can solve this themselves and he wants to make it their problem not his. If you are the lead dev in a project then sometimes you have to make hard decisions and this is a very good example.

I believe the new tactic is still much better than the original for these people, at least this tactic works for them now. Also, it would not disrupt its normal function.

I don't strongly want that PR to be merged. It's understandable not to merge it. But I also don't think that's bad.

[Eric Wieser]

Kevin Buzzard said:

Leo says that if he changes core then it won't solve the problem, there will still be cases where split works in a way not desirable to people working in exotic logics and who will still be arguing for more changes.

The proposed change makes split behave the same way as split_ifs did in Lean 3, which I don't recall anyone ever complaining about.

he feels that the users can solve this themselves and he wants to make it their problem not his.

If Mario decides to "solve this themselves", this means throwing out the entire split and simp tactics and writing them again from scratch in Std4, which is obviously an even worse outcome!

[Kevin Buzzard]

Not for Leo!

[Kevin Buzzard]

If Mario wants to take on the mantle of person who pleases all of the people all of the time then I'm sure everyone will be fine with that, until Mario also realises that it's not possible.

[Kevin Buzzard]

Leo's argument is that rewriting split and simp does not solve the problem, it just means that people continue to complain but now have evidence that you'll buckle. This is exactly where Leo doesn't want to be.

[Eric Wieser]

Eric Wieser said:

which is obviously an even worse outcome!

Kevin Buzzard said:

Not for Leo!

this message from Leo to Mario suggests otherwise:

That said, I must express my disappointment regarding your consideration to duplicate simp and split in Std. I entrusted you with the responsibility of maintaining Std due to your expertise and dedication, and you have indeed done a commendable job. Duplicating such significant components can lead to fragmentation, causing confusion and inconsistencies for our users. Our shared goal is to ensure that Lean and Std offer a coherent and seamless experience. Let's work together to avoid such divergences.

[Kevin Buzzard]

Yes, I stand corrected. It looks like a more accurate summary of the situation is simply then that it is very difficult to please all of the people all of the time :-(

[Kevin Buzzard]

Perhaps the answer then is to develop a new repo where non-classical versions of these tactics are maintained. This provides a focus point where people interested in non-classical logics can develop the things they want to see in Lean (this is what Voevodsky did for example, he didn't ask for changes in Coq, he just used Coq in a new way with his univalence library, and it's what Gabriel did with univalence in Lean 3).

[Eric Wieser]

Perhaps the answer then is to develop a new repo where non-classical versions of these tactics are maintained.

Making a new repo with the entire tactics (and all their dependencies: other tactics built on top of them and lemmas proved with them) duplicated is a lot more work than someone deciding to maintain a fork of Lean4 with 9 lines added; but this is exactly the type of community-fragmenting behavior that Leo didn't want.

[Eric Wieser]

Which is to say; I think our current stance is effectively just to tell these users to go away and use some other system.

[Kevin Buzzard]

I think that "sometimes we have to tell some potential users to go and use some other system" is an unfortunate consequence of "you can't please all of the people all of the time", a fact which is very hard to get around despite Mario's optimism. Leo is not afraid to tell some people that he cannot afford to suppor them -- for example this is what he told all the univalent users at the 2/3 switch, and I know there was great disappointment from some people at that time. The goal of the project is not to please all of the people all of the time, it seems to be far more focussed now on enabling big impactful projects, which is a far more pragmatic goal for a system such as Lean. For example I have had far more positive feedback from Leo when discussing a possible formalisation of a proof of Fermat's Last Theorem.

[Pedro Sánchez Terraf]

This has been a very interesting debate.

Kevin Buzzard said:

This certainly aligns with my experience as a mathematician, where I was taught as an undergraduate that Hilbert and Brouwer had a disagreement, Hilbert won, and that was the end of it.

In my current practice, I agree with this (but beware! I'm a logician).

Going kinda orthogonally to Lean's foundations, for me it makes a difference whether we are talking about LEM or AC. I always assume LEM, but there is some significant math a few miles in the direction of LEM + ¬AC (plus countable choice, for instance). Namely, there are translations of sorts between statements in the lines of "¬AC + Every set of reals is Lebesgue measurable" and "AC + Every definable set is Lebesgue measurable" (an instance of "definable" is given by the projective sets). This is the content of Theorem 2 in this paper by Solovay.

[Yuyang Zhao]

For me, it's not about pleasing everyone. It's just providing a convenience that isn't hard to do and will not annoy other people. We do not support univalence because we do need something against it. It is far more difficult to support than this PR.