How classical is std4?

Stream: std4

[Bernhard Reinke]

What kind of axioms are normally assumed in the lemmas of std4? For example, it seems that the current proof of Nat.min_succ_succ depends on [propext, Classical.choice, Quot.sound]. I find it a bit surprising that Classical.choice and quotient types are used for such a lemma. I believe it is because of the split tactic in the proof. There is a simple proof only depending on propext.

Is there a design goal of reducing classical assumptions in std4? I would guess some CS applications would be happy to avoid using Classical.choice

[Henrik Böving]

I don't think CS applications care about use of axioms in proofs. Proofs are irrelevant at runtime and get erased so having a constructive proof doesn't give you anything. What you could do on the other hand is have a decision procedure (that is actually computable) and try to verify it (the verification itself can again include arbitrary axioms though)

The only reason that I can think of that you would care about axiom usage in proofs in Lean is if you don't trust the axioms let it be because they are actually dangerous like the ones that pull in the compiler as trusted code or because you dislike say choice or LEM.

[Mario Carneiro]

Yes, std4 tries to avoid classical logic when it can be accomplished without significant difficulty. Unfortunately, as you note the split tactic introduces classical axioms and yet is absolutely essential for reasoning about match expressions and not easily reimplemented outside of core, so let's just say that getting classical logic out of basic proofs is blocked on fixing this issue in core

[François G. Dorais]

Just to clarify how core uses the axiom in split...

The split tactic is used to breakdown a match and if statements into cases. On the second and later cases, the assumption is not just that this case matches but also that earlier cases do not match. This is where excluded middle comes in: it's much cheaper to simply invoke Classical.em than to search for a decidabiliy instance. This is generally harmless even if the decidability instances are actually not there. I principle though, that does mean that split could be used to prove that certain functions are total even though it is not constructively provable that they are.

[Ruben Van de Velde]

I guess if someone cared deeply they could propose a slower isplit tactic

[Mario Carneiro]

I think there is no actual need for EM (decidable or otherwise) to be used here, the conditions being cased on are already decided by virtue of being separate constructors

[Mario Carneiro]

alternatively stated, I question your claim that split can be used to prove things that require EM to prove. I think it is possible to generate exactly the same subgoals as split without ever using EM

[Jun Yoshida]

splitting if is implemented by Lean.Meta.SplitIf.splitIfAt defined in Lean.Meta.Tactic.SplitIf in the core. It looks just ignoring Decidable instance which should comes with ite or dite. I wonder what is the advantage of the use of EM.

[Mario Carneiro]

yeah, last time I looked into this that's where I ended up, we need to pass the decidability instance out of that function and use it to split the goal instead of searching for one

[François G. Dorais]

Yes, I believe that's true: in the match case, .noConfusion should work and the if case has an attached Decidable instance.

[François G. Dorais]

Actually, it's by_cases that uses EM indiscriminately: https://github.com/leanprover/lean4/blob/75a92843200e009ffcb4ab0617cf11a4b4ba9efb/src/Lean/Meta/Tactic/Cases.lean#L308-L316

[Eric Wieser]

I think that's deliberate, but there's no need for split to use by_cases

[François G. Dorais]

Exactly: findIfToSplit? could record the condition and the decidability instance. Then splitIfAt? could use that info to avoid using byCases.

[Jun Yoshida]

As I am maintaining a private research project where I am doing some constructive math (related to computational topology), it would be so great if split tactic becomes Classical-free.

[François G. Dorais]

@Jun Yoshida My current solution is to override by_cases with a constructive version (this is already in Std) and manually use {d}if_{pos|neg}. I don't expect core to change this soon. Maybe after the long awaited decidable refactor happens?

[Eric Wieser]

You can always just replace by_cases h : P with cases' Decidable.em P with h h if you really want decidability, right?

[François G. Dorais]

That's already in Std: https://github.com/leanprover/std4/blob/dbffa8cb31b0c51b151453c4ff8f00ede2a84ed8/Std/Tactic/ByCases.lean#L16

[Jun Yoshida]

@François G. Dorais The problem is not that I cannot split but that some basic theorems in the core and std unnecessarily depend on Classical.choice because of it as mentioned by @Bernhard Reinke in the first post. As a result, I have to re-prove them by myself, which causes some problems including #lean4 > Inter-project name collision. If split were Classical-free, most of them would be solved at once. But reading #lean4 > Compartmentalization of axioms in Lean 4, I am pessimistic about the refactor, either.

[François G. Dorais]

That's partly why I had my own Std equivalent for a long time. I'm currently rolling it into Std, hopefully fixing some of these issues.

[Scott Morrison]

We're not at a point presently where changes like this are likely to be accepted in core. I appreciate this is unfortunate for people doing constructive maths, but in the medium term it's not a priority, and will have to be supported by separate libraries that redo foundations lemmas and tactics as required.

[François G. Dorais]

Although I don't expect anything to happen, I submitted a PR to fix this: https://github.com/leanprover/lean4/pull/2412

[Jun Yoshida]

I appreciate the great PR. I sincerely wish it would be merged eventually.

[François G. Dorais]

Nope, it's closed now. I gave it a shot... :shrug:

[François G. Dorais]

This issue might fix itself when the decidable refactor happens: https://github.com/leanprover/lean4/pull/2038 After that, ite/dite will basically be matches on Bool. That's probably a better solution than patching the current code.

[Mario Carneiro]

I doubt it, you still want to be able to write things like if h : x = y then ... and that requires dite to take a Prop (so that it can present that prop as the type of h) and yet match on it in a Bool-like way, which would have to be supplied by a typeclass, and hence would be indistinguishable from Decidable p

[Mario Carneiro]

the only alternative design I can see that would allow matching on Bool would be to interpret it as if decide (x = y) then ... where if takes a Bool argument and decide is an auto-inserted coercion. But then you have the issue that if you bind a variable to it you get h : decide (x = y) = true and this will make the mathlib crowd very unhappy

[François G. Dorais]

The alternative is what I was thinking and you're right that it's not as simple as that. The other ingredient is for match to seamlessly support type views.

[François G. Dorais]

I guess the latter would already be enough but it's a wild dream at this point.

[Mario Carneiro]

note that bif exists, if you want to write the Bool matching version today

[Mario Carneiro]

it doesn't have a dependent version though

[James Gallicchio]

Mario Carneiro said:

you get h : decide (x = y) = true and this will make the mathlib crowd very unhappy

is that related to what the IsTrue proposal was trying to improve? or do you just mean that people would not like having to simp at h to get h : x = y?

[Mario Carneiro]

the latter

[Mario Carneiro]

simp at h wouldn't necessarily even do the right thing

[Mario Carneiro]

plus that makes the dependent simplification case way more complicated (when reasoning about this dite application itself, now there are some new Eq.rec's in the term which will make it harder to avoid getting stuck)

[François G. Dorais]

Would it make sense for Std to have a split_ifs tactic as a temporary workaround? It's an investment but it would't be too hard to implement. However, it wouldn't fix everything. It would be separate from split and would do only a subset of the work. Other tactics, from core or elsewhere, might still use split instead of split_ifs (for convenience or other reasons).

[Eric Wieser]

Echoing Mario Carneiro's comment on the issue:

Moreover, making this change outside of core borders on completely infeasible, as one would have to duplicate the entirety of split and simp (which calls split)

[Eric Wieser]

So simp is still not going to do what you want

[Mario Carneiro]

and I'm pretty sure a fair number of the "accidental classical" uses in std are due to split via simp

[Eric Wieser]

Can we do a hack with implemented_by to swap out the implementation of splitIfAt? in Std and downstream?

[François G. Dorais]

Would that actually work???

[Eric Wieser]

Or does that not help because simp has already been compiled?

[Eric Wieser]

That type of thing worked with vm_override in Lean 3

[Mario Carneiro]

it doesn't work, for either compiled or interpreted code

[Mario Carneiro]

implemented_by is consulted by the compiler when it is compiling, once it has compiled a definition that's it

[Mario Carneiro]

The only way you can get behavior that is modified by downstream stuff is if you e.g. look up into a map in an initialize or environment extension that is extended later

[Mario Carneiro]

tactic evaluation is like this, so you can define another elab_rules for split and get the tactic to do something different even if others call it

[Eric Wieser]

So no more monkey-patching implementation details then...

[Mario Carneiro]

but only if they do so via macro expansion or evalTactic `(tactic| split), not if they call the splitIfAt? function directly

[Jun Yoshida]

Can I use @François G. Dorais's PR branch as a toolchain? Also, is it possible to force Std4 to use it in my local project?

[Scott Morrison]

At present, there aren't releases for every PR. Instead you need to push a tag to your own repo. There are some instructions at the very bottom of https://leanprover.github.io/lean4/doc/dev/index.html.

[Scott Morrison]

@Jun Yoshida, I pushed one for you. In ~90 minutes semorrison/lean4:release-2023-08-17-split-ifs should work in your lean-toolchain file.

[Jun Yoshida]

@Scott Morrison Thank you very much!

[Jun Yoshida]

Oh, elan says error: binary package was not provided for 'linux' I'll try following the manual you pointed out. Thanks anyway.

[Scott Morrison]

@Jun Yoshida, it won't be ready until you see more green ticks here: https://github.com/semorrison/lean4/actions/runs/5874467371

[Jun Yoshida]

@Scott Morrison I am sorry. I stupidly misunderstood your message. Now, I have got the toolchain successfully.

[Jun Yoshida]

It works perfectly fine. I got the following with semorrison/lean4:release-2023-08-17-split-ifs on lean-toolchain file:

import Std.Data.Nat.Lemmas

-- `Nat.le_min` in Std uses `split` tactic
#print axioms Nat.le_min -- 'Nat.le_min' depends on axioms: [propext]

I deeply thank @François G. Dorais and @Scott Morrison.