RFC: avoid Classical.em to split ifs

[fgdorais]

fixes #2414

This is a low priority item but here is a patch for your consideration.

[digama0]

Could you add a test (using #print axioms on a split proof)?

[fgdorais]

Could you add a test (using #print axioms on a split proof)?

I added a simple test and I tried to follow the guidelines for new tests but it looks like I didn't do it right the first time...

[leodemoura]

https://github.com/leanprover/lean4/blob/master/doc/contributions.md

[fgdorais]

https://github.com/leanprover/lean4/blob/master/doc/contributions.md

Thank you for the reminder Leo. Apologies for not following guidelines. The RFC now exists at #2414

[kim-em]

Could we also have some tests that exercise the nested ifs situation?

[fgdorais]

Could we also have some tests that exercise the nested ifs situation?

Done.

[Kha]

I'm closing this for the reasons described by Scott before this PR was opened: https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/How.20classical.20is.20std4.3F/near/383780177. Apologies for not being clear about this during the follow-up interactions.

[fgdorais]

No need to apologize. I never had any expectation for this PR to get merged. I did enjoy getting it done though, that was fun!

[digama0]

This is actually quite upsetting to me. This is not a poorly written PR, it is a small change with tests which satisfies the contribution requirements and the RFC for it has not been rejected. 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), which TBH I am considering doing in std. Just because it's a low priority doesn't mean it should just be closed, that's what you do to things that are unwanted not low priority.

[leodemoura]

Hi Mario,

Firstly, I'd like to sincerely apologize for any upset caused by the decision to close the PR. Your dedication to the Lean theorem prover project is evident, and we value all contributions made by our collaborators.

We recently updated our external contribution guidelines to streamline the process. However, as with any evolving system, there will inevitably be moments of misalignment or miscommunication. We're working on ironing out the kinks, and your feedback plays a crucial role in this.

I'd like to clarify that the PR was closed primarily because the RFC process was still in progress. Our intention is to have PRs opened only after the RFC process is complete and contributors have received the necessary approval. This ensures that all contributions align with the project's direction and requirements. I recognize that this might not have been clearly communicated, and we will take steps to make this clearer in our guidelines.

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.

I genuinely hope we can move past this bump and continue collaborating productively. Your input, experience, and dedication are invaluable to the project

Best,
Leo

[digama0]

Firstly, I'd like to sincerely apologize for any upset caused by the decision to close the PR. Your dedication to the Lean theorem prover project is evident, and we value all contributions made by our collaborators.

I appreciate that. I'm not personally hurt or walking away or anything like that, but I will keep trying to push for a more transparent and open process for lean 4 contributions for myself and others.

The new external contribution guidelines are good! I only hope that this is reflected better in the PR process as well, and I'm willing to give this one the benefit of the doubt seeing as the guidelines were modified while it was in flight.

I'd like to clarify that the PR was closed primarily because the RFC process was still in progress. Our intention is to have PRs opened only after the RFC process is complete and contributors have received the necessary approval. This ensures that all contributions align with the project's direction and requirements. I recognize that this might not have been clearly communicated, and we will take steps to make this clearer in our guidelines.

I think this is not a good idea. For one thing, the PR may in fact be the first thing written and then the contributor is just sitting on some code that could help clarify the proposal, and additionally seeing the code can help inform why the RFC author thinks the issue is fixable and at least one proposal for how to go about doing so.

How about using draft PRs for this purpose? I don't think it necessarily has to be a "real" PR, but it is useful to be able to have code as an addendum to the proposal even before it is completed. I believe Scott has done this with a few recent issues and it doesn't seem to have caused major strife.

In any case, you should clarify the contribution guidelines to explain what contributors should do with their PRs after they have been transformed into RFCs (if indeed the work proceeded in that order).

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.

Indeed, this is why I really don't like to duplicate or replace tactics if I can possibly help it. Lean 4 has some great monkey-patching capabilities, but we can't (yet) replace plain function calls in existing upstream code. If the replacement tactic is "strictly better" than the original, then for users it can sometimes just work, but there are still issues sometimes when parts of the system refer directly to a syntax declaration or call functions directly in core instead of using the frontend tactics, leading to a spotty experience. I said I was considering it, but I have made no actions to actually do so yet (and possibly ever - the issues described here don't really change no matter what upstream tactic change is under consideration, other than the quantity of potentially copied code). A simpler possibility is to offer a split' tactic so that people opt in to it, we have a few examples of this in mathlib, but it's still imperfect. The only really perfect solution is to fix the issue at its source.

It sounds like the PR was closed because the RFC is not yet complete, which means that it's not actually dead yet, it was just a procedural issue and can be revived after the RFC is completed. If so, then this is good news, and I will await the resolution of the RFC.

[leodemoura]

It sounds like the PR was closed because the RFC is not yet complete, which means that it's not actually dead yet, it was just a procedural issue and can be revived after the RFC is completed. If so, then this is good news, and I will await the resolution of the RFC.

Correct. The PR can be reopened after the RFC process is completed.

[fgdorais]

It should be documented somewhere that there is a pathway out of closure since this is not typical usage. I'm also not sure this is a good idea since it opens the possibility of "closing wars" and other mayhem. From my prior experience on MathOverflow, these are extremely time consuming and mostly pointless (@semorrison can confirm this). I would steer away from using closure in this way.

[eric-wieser]

Just to note, this is consistent with the Lean 3 behavior:

import tactic.split_ifs

theorem ittt2 (c : Prop) :
  (fun [decidable c], by exactI if c then 0 else 0) = (fun _, 0) :=
begin
  split_ifs,
  sorry,
  sorry
end

#print axioms ittt2

(suggesting the choice that was made to fallback to classical rather than failing is the correct one)