Compartmentalization of axioms in Lean 4

Stream: lean4

[Jason Rute]

On the PA SE I asked How usable is Lean for constructive mathematics?. @François G. Dorais pointed out that as long as one doesn't use the Classical namespace then one won't get LEM or AC? This isn't actually true in Lean 3 (e.g. in the order library there is lt_or_eq_of_le), and it is even less true in Lean 3 community (by_cases tactic is always available). Will there be a clear separation of classical reasoning in Lean 4? (I'm not saying their should be, I'm just curious.) Also, what about the other axioms, quot.sound and propext? Will it be easy to avoid them in Lean 4?

[Jason Rute]

To be clear, I'm referring to base Lean 4, not Mathlib 4, which I assume will remain unashamedly classical.

[Leonardo de Moura]

@Jason Rute
The bare-bones system can be used for constructive mathematics. That being said, a lot of the proof automation we are building is using axioms such as propext. For example, simp uses it all over the place. Similarly, the builtin by_cases in Lean 4 uses em and doesn't even bother checking whether the proposition is decidable. Moreover, any theorem in core Lean that uses these theorems will depend on these axioms. So, the short answer is "no, we are not trying to compartmentalize axioms".
In previous versions of Lean, we spent a lot of time trying to avoid these axioms and providing special constructions for special cases, but I think it was not worth it.
Are you interested in constructive mathematics, or just curious?

[Jason Rute]

I personally am more curious than anything else at this point. I think others might be more interested, but they can speak for themselves. I totally understand the need to make tradeoffs, and I was just looking for some clarity on what these tradeoffs currently are. Thanks!

[Leonardo de Moura]

We didn't take this decision lightly. It would be great if we had infinite resources, and we could support the minority that cares about constructive mathematics. In my point of view, the vast majority of the CS community don't care about constructivism, same for the math community. Sometimes, I see mathematicians assuming that most CS people care about constructivism, this is not true at all. Most don't even know constructivism exists. Moreover, verifying software is already super hard, I don't think it is worth making it even harder by trying to produce a constructive proof. Imagine someone verified a TLS protocol implementation is correct, would you really care whether the proof is constructive or not?
Note that the power of Lean comes from its community and Mathlib. Mathlib is already much bigger than the Lean implementation, in a few years, it will be many orders of magnitude bigger. I think it will not be feasible to refactor the whole thing to make it friendly for constructive users. I don't like to send users away, but if a user is interested in constructive mathematics, we should explicitly say they should consider using a different system (e.g., Agda or Coq).

[Tomas Skrivan]

I'm interested in synthesizing programs in Lean. I'm experimenting in using tactic mode to rewrite specification to computable programs. So far, I have never run into a problem with non-computability.

What would a better support for constructivism in Lean actually mean? What kind stuff would that allow that is currently not possible?

The only thing I'm aware of is the problem with stuff like recursor 'Even.casesOn' can only eliminate into Prop but then I can just define Even n to by in Type instead of Prop and problem solved. Maybe the problem is with Eq as you can't change that to be in Type.

[Leonardo de Moura]

I'm interested in synthesizing programs in Lean. I'm experimenting in using tactic mode to rewrite specification to computable programs. So far, I have never run into a problem with non-computability.

This is not a problem. Tactics that use classical principles produce terms of type Prop which are erased anyway during code generation.

What would a better support for constructivism in Lean actually mean?

In previous versions of Lean, we spent time writing proof automation that would avoid using axioms such as propext and Quot.sound. For example, the proof for function extensionality in Lean depends on the Quot.sound axiom, and we use funext to go inside quantifiers in simp and conv.

TPIL has a chapter about these axioms https://leanprover.github.io/theorem_proving_in_lean4/axioms_and_computation.html

[Kevin Buzzard]

I am probably someone who conflates computer scientists with constructivists -- I should be more careful. I suspect that the computer scientists I've met in the last few years are not a representative sample.

[James Gallicchio]

This also can be addressed gradually down the road, no? There's nothing stopping future users of Lean with too much time on their hands from slowly pushing LEM out of parts of mathlib.

[Mario Carneiro]

This is already done to some extent. For example ring int used to need LEM and doesn't on more recent versions. But the tooling for preventing regressions is lacking at the moment, because most contributors don't pay attention to LEM usage (and we don't want them to have to either)

[Kevin Buzzard]

Call me a skeptic but I suspect that it will be impossible to remove much LEM. The issue is not just that lots of maths in mathlib simply doesn't work without LEM and in many of the cases where it can be done it's already done that way anyway; the issue is that without LEM one definition can become two or three independent definitions and changing a definition which is super convenient for defeqs to one which is constructively stronger but more inconvenient to use is not going to be a PR which will look appealing ("a definition is changed to something which is classically the same and now we have to add 100 new lines of code")

[Kevin Buzzard]

We had this with valuations once. One of the axioms for a valuation on a ring is v(a+b)<=max (v(a),v(b)) and when Kenny wrote the code he wrote the constructive version "v(a+b)<=v(a) or v(a+b)<=v(b)" because he didn't want to take a max on an arbitrary linear order because max is defined via a case split. It drove us nuts trying to use this though so we just changed it to the max version and any attempt to change it back would involve just making a bunch of code worse

[François G. Dorais]

@Kevin Buzzard I don't think anyone is really concerned about removing LEM from theorems. Classical theories are just that: classical theories. It's a take it or leave it thing. Some people are interested in intuitionistic and constructive theories, all of these people are aware that they can't use classical theories willy nilly. The issue which is of concern is whether _tactics_ can introduce LEM surreptitiously. by_cases does that, so people who care about avoiding LEM should be aware that they need to avoid this tactic. It's the only place where mkEM is used in Lean 4, so I would assume it's the only one so far.

[Kevin Buzzard]

In lean 3 there was even a tactic which billed itself as intuitionistic but would occasionally accidentally use classical axioms. It was either called itauto or ifinish. It caused so much confusion at some point that I think we might have removed it.

[Kevin Buzzard]

Avoiding certain tactics sounds like a slippery slope to me. In mathlib I should think we would reserve the right to rewrite tactics so that they magically became nonconstructive but were somehow better (eg faster) as a consequence.

[François G. Dorais]

@Kevin Buzzard Mathlib should stay classical. I think everybody here is fine with that. Maybe some people think mathlib should be everything for everybody but that doesn't make sense. Most things for most folks is more than enough a goal for one library!

[James Gallicchio]

For the select few that do care about this (mainly PL researchers) does it seem feasible to have some sort of lint rule that ensures all definitions in a file don't rely on classical? I haven't looked into how much support the compiler has for tracking axiom usage...

[Tomas Skrivan]

You can use #print axioms Classical.em to print out axioms for a symbol. I don't know if there is a linter for checking axioms, but should be possible to implement.

[Leonardo de Moura]

James Gallicchio said:

For the select few that do care about this (mainly PL researchers) does it seem feasible to have some sort of lint rule that ensures all definitions in a file don't rely on classical?

I haven't looked into how much support the compiler has for tracking axiom usage.

Note that almost everything that was proved using simp depends on propext. Example:

#print axioms List.length_append

[Mario Carneiro]

The underlying simp algorithm doesn't really need this though, and we might want to relax it to support relations other than Eq and HEq, in which case most of those propext applications will go away

[Mario Carneiro]

(that is, I think there are good reasons to pursue extending simp to support congruence through other relations which has nothing to do with axiom use, but will incidentally fix this propext behavior)

[Leonardo de Moura]

@Mario Carneiro
Yes, we know. This is exactly the approach we used in Lean 3 ;)
However, it imposes additional bookkeeping in simp, extra effort from users (they have to keep proving congruence lemmas for such as and_congr, or_congr), etc. We did all that in Lean 3, and it was barely useful. I don't recall seeing people simplifying terms using different relations in Mathlib. If I remember correctly, Mathlib contains [congr] rules for the list permutation relation, but I think I was the one that added them for fun and testing simp, and they can be avoided.

Moreover, we use funext to go inside binders, and funext depends on Quot.sound. One could use Setoids to avoid the Quot.sound dependency, but I don't think it is worth the trouble.

[Mario Carneiro]

My general impression was that the support for relations other than equality in simp and rw was incomplete or deficient in some way, and so it may not have gotten much use in mathlib for that reason (although that impression might have been mistaken). It's true that with quotient types and propext we don't really have a huge need to care about relations other than eq, although especially for non-symmetric relations we had to hack something together in its place (mono)

[Leonardo de Moura]

I am curious about this claimed deficiency. In Lean 3, simp is rewriting with <-> all the time. So, the support should work.
Regarding rw, let's not include it on this thread. It is a different piece of automation used to apply Eq.rec.

[Leonardo de Moura]

James Gallicchio said:

For the select few that do care about this (mainly PL researchers) does it seem feasible to have some sort of lint rule that ensures all definitions in a file don't rely on classical?

I haven't looked into how much support the compiler has for tracking axiom usage.

Yes, I have seen PL researchers (working on type theory) claiming to be constructivists and saying axioms like propext and Quot.sound are a "sin". Most of them seem to be leaning towards cubical systems. Even if we compartmentalize axioms in Lean, I think Lean will not be an attractive system for them. I think this is fine, and they can use a system such as Cubical Agda.

[Kyle Miller]

Leonardo de Moura said:

I am curious about this claimed deficiency. In Lean 3, simp is rewriting with <-> all the time. So, the support should work.

Something we're not sure how to do in mathlib is use simp to rewrite relations such as docs#int.modeq. There have been a few discussions about it, and the best ideas we've had seem to involve writing custom tactics. (As far as my own understanding goes, the only simp feature I know about that applies to general relations is lift_eq, to prove reflexive relations by trying to prove an equality instead.)

[Leonardo de Moura]

@Kyle Miller The Lean 3 simplifier is parametrized by a relation. Example: https://github.com/leanprover/lean/blob/master/src/library/tactic/simplify.cpp#L220

[Kyle Miller]

@Leonardo de Moura This is surely showing my ignorance about congruence lemmas, but when I saw the following error I assumed it wasn't designed to work this way. (I specialized it to mod-5 just to be sure it didn't have to do with additional arguments for relations.)

import data.int.modeq

def mod5 (x y : ℤ) : Prop := x ≡ y [ZMOD 5]

infix ` ≡₅ `:50 := mod5

@[refl] theorem mod5.refl (a : ℤ) : a ≡₅ a := @rfl _ _

@[symm] theorem mod5.symm {a b : ℤ} : a ≡₅ b → b ≡₅ a := eq.symm

@[trans] theorem mod5.trans {a b c : ℤ} : a ≡₅ b → b ≡₅ c → a ≡₅ c := eq.trans

@[congr]
theorem mod5.add (a b c d : ℤ) (h₁ : a ≡₅ b) (h₂ : c ≡₅ d) : a + c ≡₅ b + d := int.modeq.add h₁ h₂
/-
invalid congruence lemma, 'mod5.add' the left-hand-side of the congruence resulting type must be
of the form (has_add.add x_1 ... x_n), where each x_i is a distinct variable or a sort
-/

(I'm looking through the logic simp_lemmas.cpp to try to understand how this works better.)

[Leonardo de Moura]

@Kyle Miller See this https://github.com/leanprover-community/mathlib/blob/master/src/data/list/perm.lean#L189-L190

[Kyle Miller]

That gave me a hint for what's going on, but I still don't completely understand the problem. This is a workaround:

def zadd (a b : ℤ) : ℤ := a + b

@[congr]
theorem mod5.add (a b c d : ℤ) (h₁ : a ≡₅ b) (h₂ : c ≡₅ d) : zadd a c ≡₅ zadd b d := int.modeq.add h₁ h₂

[Kyle Miller]

@Leonardo de Moura Based on my understanding of the source code, my guess is that int.has_add is not allowed in the LHS since it's not a variable.

theorem mod5.add : ∀ (a b c d : int),
  mod5 a b → mod5 c d → mod5 (@has_add.add int int.has_add a c) (@has_add.add int int.has_add b d)

It can't be a variable, though, since this theorem depends on a specific additive structure.

[Kyle Miller]

Is it safe to extend the list of allowed non-variable objects to include instances (or maybe if it's an argument that's identical on the LHS and RHS)? https://github.com/leanprover-community/lean/blob/master/src/library/tactic/simp_lemmas.cpp#L997

[Leonardo de Moura]

@Kyle Miller I am sorry, but I don't have cycles to invest in the old Lean 3 code. If supporting relations such as ≡₅ would make a big difference to users, I am happy to help with it after the Mathlib porting has been completed.

[Kyle Miller]

@Leonardo de Moura That's fine -- I'll probably look into it since rewriting for ZMOD has been an issue a number of us have faced for teaching.

[Kevin Buzzard]

The fix I used with ZMOD in my class was to quotient out and then just rewrite equality

[Reid Barton]

How about just avoiding unnecessary use of AC/LEM in the core library? In the internal language of a topos (with sufficient universes) all the other rules and axioms of Lean are valid. This would make it possible to use the core Lean system for various sorts of synthetic reasoning involving anticlassical postulates (e.g., synthetic differential geometry).

I agree that mathlib should remain classical for the reasons Kevin mentioned (classical notions do not map in a one-to-one fashion to constructive notions). But at least at the moment, it looks like it would be quite easy to eliminate uses of AC from the core library. The only uses I saw are that LEM is used to decide (in)equalities on Nat and maybe Int, arising from by_cases. The simplest thing to do would be to add by_cases_dec (using Decidable.em) and use it where appropriate.

I guess the main question is: going forward, as the core library (potentially?) expands, is it reasonable to assume that PRs removing unnecessary uses of AC would be accepted?

[Kevin Buzzard]

Mathlib should definitely remain classical if it wishes to remain relevant to Fields Medalists :-) What goes on in core is of course none of my business, they can do what they like in there as long as I can still use it to do classical maths.

[Reid Barton]

I mean, Voevodsky was a Fields medalist and he created the HoTT/UF library--are we only counting living ones?
I agree with your general point, but I think you could find a better way to express it.

[Reid Barton]

The classical interest in this particular set of axioms comes from externalization--a constructive theorem about abelian groups is also a classical theorem about sheaves of abelian groups on the etale site of a scheme or whatever.

[Kevin Buzzard]

You're right Reid, my post is not at all well expressed. Sorry. Probably a much more sensible thing to say would be "remain relevant to people like me"!

Here's a maths question coming from this though. Say I have a constructive proof in mathlib about mathlib's abelian groups. Can one now write some kind of tactic which spits out the corresponding theorem about mathlib's sheaves of abelian groups?

[Mario Carneiro]

I think that this is painting an unnecessarily adversarial picture of intuitionizing lean / mathlib. It's perfectly possible to remove unneeded axioms from (proof irrelevant!) theorems without having the slightest impact on classical math or mathematicians

[Mario Carneiro]

And regarding Reid's question, it's not my decision but I would certainly say "absolutely, yes" to PRs removing unnecessary uses of AC (indeed I've filed a couple of these to lean 3 core myself), provided they do not make the classical mathematics situation more cumbersome (including breaking useful defeqs). For other things like intuitionistic concepts fractured from classically equivalent things, they should just be new theories and classical mathematicians should feel free to ignore them

[Mario Carneiro]

I think everyone is aware that classical mathematics is an important use case of mathlib and no one has ever suggested that it would be okay to make sacrifices in this use case for the sake of intuitionizing. But it's not like it's a zero sum game

[Reid Barton]

Kevin Buzzard said:

Here's a maths question coming from this though. Say I have a constructive proof in mathlib about mathlib's abelian groups. Can one now write some kind of tactic which spits out the corresponding theorem about mathlib's sheaves of abelian groups?

In principle yes (assuming mathlib's definition of a group hasn't diverged from the constructively correct one). In practice, it would probably take a lot of design and engineering work to make it useful.

[Leonardo de Moura]

I guess the main question is: going forward, as the core library (potentially?) expands, is it reasonable to assume that PRs removing unnecessary uses of AC would be accepted?

@Reid Barton Thanks for raising this issue. Is the use case you described a hypothetical one? "Hypothetical" here means "perhaps one day someone will benefit from this modification". I agree with you that it is currently easier to eliminate unnecessary uses of AC/LEM than removing uses of propext and Quot.sound. I feel it is only worth doing this kind of change if we have real applications right now that will benefit from it. I spent a lot of time in the past adding code for special cases that have never been used in practice, and I am trying to avoid this kind of waste. Even if the PRs are simple, they still need to be reviewed, and future automation will also have to make sure AC/LEM is only used when needed to make sure we provide a coherent system to users.

[Mario Carneiro]

I like to think of this something like rust's target tiers, which make it a bit easier to formalize what level of support is provided:

• Tier 1: guaranteed to work, has official support
• Tier 2: guaranteed to build, but no automatic testing so bugs might happen
• Tier 3: The codebase nominally supports it, but support is primarily handled by interested external users

I would classify intuitionistic logic support in lean as tier 3: devs won't actively try to remove support but they also won't try to keep things working (i.e. automated regression testing for AC use), and of course support is not on any roadmap. I think the big question is whether unsolicited PRs that adjust support for tier 3 things are rejected, given that there is not really any testing to ensure that the changes work; I would be inclined to be generous with such PRs as long as they don't impact any of the tier 1 goals.

[Mario Carneiro]

I find classifying support into levels like this makes it easier as a dev to be at peace with not working on certain things that seem good on their face but might not fit with current priorities.

[Leonardo de Moura]

@Mario Carneiro I think the tier system is a great suggestion. However, right now I don't see "intuitionistic logic support" as tier 3. It was in the past, but it has now a "not supported" status. I think intuitionistic logic is beautiful, but we have finite resources. We have to focus on the applications we have right now, and none of them rely on intuitionistic logic. I asked Reid in my previous comment whether the use case he described is hypothetical or not. If there is an application that would benefit from this kind of change, let's invest time, otherwise, let's postpone it. PRs are not free, we need to review them, and make sure we can maintain the code later. We are currently overwhelmed by the tier 1 to-do list.

[Mario Carneiro]

Tier 3 is a pretty low bar, I'm surprised you object to that. In rust that basically equates to hobbyist systems that no one even knows how to find examples of

[Mario Carneiro]

you can be sure no one is spending any cycles on supporting them

[Mario Carneiro]

that is, tier 3 is explicitly defined to get around the "I don't have time to support that" objection because it does not demand any actual dev time commitment

[Mario Carneiro]

but maybe things are different if the pool of reviewers is too small so that taking PRs is already too much work

[Leonardo de Moura]

@Mario Carneiro We still have to review the PR and make sure it does not break tier 1 features, or get in the way of features we do want to implement in the future.

[Mario Carneiro]

True. I don't really want to push for this right now, but I thought I would suggest it as a mental framework (and a warning that I might one day attempt to make one of those intuitionistic PRs - probably not any time in the near to mid term though)

[Leonardo de Moura]

@Mario Carneiro If you have extra time to invest in extra PRs, please invest in the ones that will help the Mathlib port. They will have a much bigger impact. After we manage to put things in a stable state and Mathlib is ported to Lean 4, we will have the flexibility to handle lower priority PRs such as "intuitionistic logic support" PRs.

[Mario Carneiro]

Yep yep, those are way higher on my todo list. An intuitionization PR would probably come up in conjunction with a project to formalize something without AC for some reason, and that's not even on my radar ATM but it is something I have worked on in the past so I can't discount it completely. (Right now my number 1 priority is finishing my thesis so PRs of any kind have taken a back seat.)

[Brandon Brown]

This is probably a naive question as I have no background in logic but is there a way to embed constructive/intuitionistic logic into the classical logic of Lean? I read something about constructive logic being equivalent to an infinitely valued logic, so i wonder if that could be embedded somehow. I have no preference for constructive logic per se but I am interested in smooth infinitesimal analysis/synthetic differential geometry, which denies double negation/LEM.

[Mac]

@Brandon Brown Lean's kernel is actually constructive/intuitionistic. Classical logic is only achieved through additional axioms. The caveat, though, is that many of the tactics in the Lean core make liberal uses of classical axioms even when not strictly necessary. Thus, proper intuitionistic support in Lean would be achieved through the refinement of such tactics to aim for intuitionistic solutions rather than classical ones.

[Mac]

Some good examples of tactics and definitions which are unnecessarily classical would be split (which uses choice when often not necessary) and many simp lemmas (e.g., for Bool) which use equal = and propext when the biconditional <-> would be sufficient.

[Brandon Brown]

Right, I suppose it would be nice if the tactics didn't use LEM by default, but I also understand that the vast majority of Lean code is going to be classical so from an efficiency perspective it makes sense, that's why I was wondering if if it is possible to embed a constructive logic inside a classical universe so you don't have to rewrite tactics, so the onus would be on the constructivists to put in more upfront work.

[Alex Keizer]

On a related note: it would be nice to have some way to say you don't want to use a certain axiom, which would raise an error when using a tactic/theorem that depends on this forbidden axiom. Besides the intuitionism discussion, this can also help track down unexpected dependencies on sorryAx.