Review request for batteries#1431

Stream: batteries

[Wrenna Robson]

I have addressed one of the few remaining proof_wanteds in batteries, see batteries#1431. I hope this will be a fairly straightforward review.

My only comment is that I could see an argument for Mathlib's docs#Fin.find_min to be ported over to batteries (which I would have made use of here).

[Wrenna Robson]

Actually having said that I realise maybe I've just proved the equivalent of it for Fin.find?. Also... Fin.find and Fin.find? seem pretty much identical in function except the latter takes Bool-valued predicates and the former takes Decidable Prop-valued ones. These are not very different.

[François G. Dorais]

I think the plan was to eventually deprecate Mathlib's Fin.find for Batteries Fin.find? but that fell out of sight.

[Wrenna Robson]

Makes sense. I have an alternative plan I'm working on for that.

[Wrenna Robson]

@François G. Dorais hey: have responded to your easy review comments but there's one persistent one I want to respond to: namely this thing about the "<" condition being redundant.

It "obviously" is redundant. However... I found the proof of the iff that I began with a lot easier to just do straightforwardly by induction if it is included - it's a lot more natural. It's like trying to work with Nat.find while not using Nat.find_min.

It's obvious that if a witness exists, a minimal witness exists. However... just because something is obvious doesn't suffice. Where is the theorem that proves it? I couldn't find it (perhaps I missed it).

[Wrenna Robson]

From a certain perspective, this is the theorem that proves this.

[Wrenna Robson]

If you can provide me with the library theory that expresses the obvious thing, I'll be happy.

[Wrenna Robson]

It feels like a thing that should surely exist, I agree!

[Wrenna Robson]

Lacking the API I have written in #30037 for a new Fin.find, though, I'm not sure how one expresses "minimal solution".

[François G. Dorais]

Is there a reason you wouldn't use the strong form findSome?_eq_some_iff or find?_eq_some_iff when you also need minimality? My thought is that someone using find?_isSome_iff doesn't care about the value of find? so probably doesn't care about minimality either.

[Wrenna Robson]

Yeah it's a good point. I'm not even really sure when you'd use the isSome one!

[Wrenna Robson]

I think I've come down on the side of it being good to have both iffs (the one that looks weaker and the one that looks stronger). I'm not sure about naming though.

[François G. Dorais]

The name is incorrect.

[Wrenna Robson]

Indeed. Really I think it wants something after the iff? I'm happy to hear suggestions.

[François G. Dorais]

We can figure that out in the second review pass.

[Wrenna Robson]

Alright. I think it might nearly be ready for that but I will have a check.

[Wrenna Robson]

@François G. Dorais I would like to mimic the naming of Init.Data.List.Find with e.g. docs#List.find?_replicate_of_neg

[Wrenna Robson]

i.e. use pos and neg and have p j = true and ¬ p j = true.

[François G. Dorais]

Why not eq_true and ne_true?

[Wrenna Robson]

I like that more, but it is less the standard.

[Wrenna Robson]

Also: how would you feel about adding the following lemma into the Fin namespace in an appropriate place:

theorem fin_exists_iff_exists_min (p : Fin n → Prop) [DecidablePred p] :
    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by
  induction n with
  | zero =>
    exact ⟨fun ⟨i, _⟩ => i.elim0, fun ⟨i, _⟩ => i.elim0⟩
  | succ n ih =>
    simp only [Fin.exists_fin_succ, Fin.forall_fin_succ, not_lt_zero,
      false_implies, implies_true, and_true, succ_lt_succ_iff, succ_pos, forall_const]
    by_cases h0 : p 0
    · grind
    · rw [ih]
      grind

[Wrenna Robson]

François G. Dorais said:

Why not eq_true and ne_true?

Specifically to be fair it is less the standard when they are a hypothesis.

[François G. Dorais]

A bit of a bummer but since ne_true is not simp NF we really should use eq_false instead. I'm not a huge fan of this simp lemma but I don't think that will change.

[Wrenna Robson]

Mmm. I think the other issue is that it makes it a bit less straightforward to compare to a predicate, but maybe.

[François G. Dorais]

Agreed. But decide P = false simps to ¬P so it might not be too bad.

[François G. Dorais]

Another handy lemma:

theorem exists_minimal {P : Fin n → Prop} [DecidablePred P] (h : P i) :
    ∃ i, P i ∧ ∀ j < i, ¬P j := by
  match heq : Fin.find? fun i => decide (P i) with
  | none =>
    rw [← decide_eq_true_iff (p := P i)] at h
    absurd isSome_find?_of_eq_true (p := fun i => decide (P i)) h
    simp [heq]
  | some i =>
    exists i
    simp_all [find?_eq_some_iff]

[Wrenna Robson]

Oh yes that is even better. Though I think neither entirely help with the findSome? = some a ones, because basically there's this a parameter.

[Wrenna Robson]

My one does avoid the use of Fin.find? which I do prefer.

[François G. Dorais]

I never asked to change findSome?_eq_some_iff nor find?_eq_some_iff, these are fine. But isSome_findSome?_iff and isSome_find?_iff should not include the minimality condition since that makes them weaker than without it.

[Wrenna Robson]

Right

[Wrenna Robson]

I think there's an argument that either it doesn't change it or it makes it stronger. But arguably that is just covered by having the one direction of the minimality condition.

[François G. Dorais]

It makes the <- direction weaker since there is an unnecessary hypothesis.

[Wrenna Robson]

Right, and the -> stronger because an extra conclusion. So we just have the -> I guess. I am still not sure when you would actually use this iff, mind.

[François G. Dorais]

The <- direction is more useful (without minimality). Maybe it should be written the other way around?

[François G. Dorais]

But they already existed in the better form, so we should just restore the original.

[Wrenna Robson]

Yes.

[François G. Dorais]

Let's add this theorem somewhere in the file:

theorem exists_eq_true_iff_exists_minimal_eq_true {p : Fin n → Bool} :
    (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ j < i, p j = false := ...

The nontrivial direction is basically exists_minimal from above.

[Wrenna Robson]

Is this not my exists_fin_iff_exists_min, but for Bool preds

[Wrenna Robson]

I really don't think we should duplicate every result for decidable preds on boolean ones.

[Wrenna Robson]

theorem exists_eq_true_iff_exists_minimal_eq_true {p : Fin n → Bool} :
    (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ j < i, p j = false := by
  rw [exists_fin_iff_exists_min]
  simp only [Bool.not_eq_true]

[Wrenna Robson]

Similarly I think I simply disagree that we should correct to the simp-normal form p j = false.

[Wrenna Robson]

theorem exists_minimal {P : Fin n → Prop} [DecidablePred P] (h : P i) :
    ∃ i, P i ∧ ∀ j < i, ¬P j := by
  rw [← exists_fin_iff_exists_min]
  exact ⟨i, h⟩

[Wrenna Robson]

Your exists_minimal is just one direction of my theorem.

[François G. Dorais]

Right. Let's first do the pending changes and then come back to this since it's not clear exactly where to put these lemmas.

[Wrenna Robson]

OK, I've pushed my latest.

[Wrenna Robson]

Sorry for delay - had a life meeting thing

[Wrenna Robson]

Family planning.

[François G. Dorais]

No worries. I'm never in a rush when reviewing.

[Wrenna Robson]

Could we close the existing comments and start from this revision? I am struggling to keep track of what we've settled on. I've tried to action everything thus far, with the exception of this p i = false thing

[François G. Dorais]

I closed all the old comments and added some more, nothing controversial except for the = false thing.

[Wrenna Robson]

Grand. I think we should get a third opinion on that maybe? I don't disagree with your perspective but I worry about deviating too much from the existing style.

[François G. Dorais]

Fair enough.

We should keep track of deprecations:

import Batteries.Data.Fin.Lemmas
import Batteries.Tactic.Alias

namespace Fin

@[deprecated (since := "2025-09-28")]
alias exists_of_findSome?_eq_some := exists_eq_some_of_findSome?_eq_some

@[deprecated (since := "2025-09-28")]
alias findSome?_isSome_iff := isSome_findSome?_iff

@[deprecated (since := "2025-09-28")]
alias findSome?_isNone_iff := isNone_findSome?_iff

@[deprecated (since := "2025-09-28")]
alias find?_isSome_iff := isSome_find?_iff

@[deprecated (since := "2025-09-28")]
alias find?_isNone_iff := isNone_find?_iff

[Wrenna Robson]

Thanks. Good stuff.

[François G. Dorais]

This is quick:

theorem exists_eq_true_iff_exists_minimal_eq_true (p : Fin n → Bool) :
    (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ j < i, p j = false := by
  cases _ : find? p with grind [find?_eq_none_iff, find?_eq_some_iff]

theorem exists_iff_exists_minimal (p : Fin n → Prop) [DecidablePred p] :
    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by
  have := exists_eq_true_iff_exists_minimal_eq_true fun i => decide (p i)
  simp_all

[Wrenna Robson]

I don't disagree but it uses find? to do it. I'm not sure if that's desirable.

[Wrenna Robson]

I do wonder if some of these lemmas should be grind lemmas, in particular the two you have there.

[François G. Dorais]

How would you do it without using find?

[Wrenna Robson]

Well see my proof above that doesn't use it?

[Wrenna Robson]

Wrenna Robson said:

Also: how would you feel about adding the following lemma into the Fin namespace in an appropriate place:

theorem fin_exists_iff_exists_min (p : Fin n → Prop) [DecidablePred p] :
    (∃ i, p i) ↔ ∃ i, p i ∧ ∀ j < i, ¬ p j := by
  induction n with
  | zero =>
    exact ⟨fun ⟨i, _⟩ => i.elim0, fun ⟨i, _⟩ => i.elim0⟩
  | succ n ih =>
    simp only [Fin.exists_fin_succ, Fin.forall_fin_succ, not_lt_zero,
      false_implies, implies_true, and_true, succ_lt_succ_iff, succ_pos, forall_const]
    by_cases h0 : p 0
    · grind
    · rw [ih]
      grind

Here.

[Wrenna Robson]

Like I'm not sure if you missed this? But it is deliberately independent of find?

[François G. Dorais]

Using find? allows eliminating Classical.choice. Of course grind uses it always but this expanded proof avoids it:

theorem exists_eq_true_iff_exists_minimal_eq_true (p : Fin n → Bool) :
    (∃ i, p i = true) ↔ ∃ i, p i = true ∧ ∀ j < i, p j = false := by
  cases h : find? p with
  | none => simp_all
  | some i =>
    rw [find?_eq_some_iff] at h
    constructor
    · intro; exists i
    · intro; exists i; exact h.1

Batteries does not not care about constructivity. :grinning:

In the end, it just depends on where that theorem goes.

[Wrenna Robson]

I suppose. I find it more elegant not to use definitions that aren't necessary I think.

[Wrenna Robson]

I think if you're using a Fin n -> Bool it makes sense to be constructive.

[Wrenna Robson]

I'm not sure mine uses Classical.choice?

[François G. Dorais]

It does, but if you eliminate grind then it probably doesn't.

Since find? is almost literally the constructive argument for these theorems, it makes sense to use it for that.

I'm not going to pressure one way or the other, I just want to make sure we consider all options.

[Wrenna Robson]

No indeed. I think that's good.

[Wrenna Robson]

Having slept on it, I think I am alright to change stuff to eq_false.

[Wrenna Robson]

We should build mathlib again to check it still works.

[Wrenna Robson]

I am not sure how I retrigger a build

[Wrenna Robson]

I think I would need write permissions.

[Wrenna Robson]

https://github.com/leanprover-community/mathlib4-nightly-testing/actions/runs/18079454960/job/51440671329

[Wrenna Robson]

If someone could re-run this that would be good.

[Kevin Buzzard]

I have a "rerun all jobs" button on that link and I've just clicked it.

[Wrenna Robson]

Thanks Kevin

[François G. Dorais]

@Kim Morrison Please grant Wrenna (linesthatinterlace) write access to mathlib4-nightly-testing.

[Wrenna Robson]

As an aside by the way, I'd like to look at moving some of Mathlib.Data.Fin.SuccPred over to batteries as I think they have non-mathematical uses. In particular docs#Fin.forall_fin_succ' and docs#Fin.exists_fin_succ' though also stuff like docs#Fin.castSucc_le_castSucc_iff or docs#Fin.succ_le_castSucc_iff.

They come up when doing induction arguments on Fin quite a bit.

In particular I would like to consider providing Fin.findRev? and related things, and when arguing "from the top" that kinda thing does come up.

[Wrenna Robson]

Outside this PR though.

[Ruben Van de Velde]

@François G. Dorais Kim is unavailable for a while

[François G. Dorais]

@Ruben Van de Velde Thanks for the reminder! Do you know who else might have permissions to do that?

[Ruben Van de Velde]

If we're lucky, any of the mathlib maintainers

[Wrenna Robson]

Thanks!

[Mario Carneiro]

Wrenna Robson said:

Grand. I think we should get a third opinion on that maybe? I don't disagree with your perspective but I worry about deviating too much from the existing style.

FWIW I agree with François that the p = false normal form is bad, it means you have to duplicate all lemmas about boolean functions

[François G. Dorais]

@Mario Carneiro We've already given up to the upstream NF. I don't like it but it works for the time being...

[François G. Dorais]

Upstream changes are always too slow!

[Wrenna Robson]

Yes - personally I think "p = false" should normalise to "\not p = true". But that's going to be really annoying to change.

[Kim Morrison]

François G. Dorais said:

Kim Morrison Please grant Wrenna (linesthatinterlace) write access to mathlib4-nightly-testing.

@Wrenna Robson, please check your inbox for an invitation to the nightly-testing team, which will give you this access.

[Wrenna Robson]

Thank you.

[Wrenna Robson]

It says I'm now a member of leanprover-community, not specifically nightly-testing. I hope this is right.

[Ruben Van de Velde]

Yeah, it's a team within that organisation

[Wrenna Robson]

Right

[Wrenna Robson]

Well I think I accepted!

[Wrenna Robson]

Also, good to see you back (?) @Kim Morrison