For a finite set s : Finset α in a linear order, the definitions s.max' h and s.min' h take a proof h : s.Nonempty as an argument.
Although these proofs are logically irrelevant, it is convenient in Lean to have explicit rewrite lemmas stating that the value does not depend on the chosen witness.
max')For any h₁ h₂ : s.Nonempty,
[
\texttt{s.max' h₁ = s.max' h₂}.
]
min')For any h₁ h₂ : s.Nonempty,
[
\texttt{s.min' h₁ = s.min' h₂}.
]
These lemmas are useful when rewriting expressions produced by unfolding definitions that use max'/min' with non-canonical Nonempty proofs (e.g. divisor-ordering problems involving successive max' operations).
File FinsetMaxProofIrrel.lean (complete, no sorry):
import Mathlib.Data.Finset.Max
namespace Finset
variable {α : Type*} [LinearOrder α]
/-- `Finset.max'` does not depend on the choice of nonemptiness witness.
This is essentially proof irrelevance, but having it as a lemma is convenient for rewriting.
-/
theorem max'_eq_max' {s : Finset α} (h₁ h₂ : s.Nonempty) : s.max' h₁ = s.max' h₂ := by
classical
cases Subsingleton.elim h₁ h₂
rfl
/-- `Finset.min'` does not depend on the choice of nonemptiness witness. -/
theorem min'_eq_min' {s : Finset α} (h₁ h₂ : s.Nonempty) : s.min' h₁ = s.min' h₂ := by
classical
cases Subsingleton.elim h₁ h₂
rfl
end Finset
$ cd /opt/lean/Math
$ lake env lean FinsetMaxProofIrrel.lean
# success
Finset.max' and Finset.min' (Lean)”This note provides two small but very useful rewriting lemmas:
Finset.max'_eq_max' : s.max' h₁ = s.max' h₂ for any h₁ h₂ : s.Nonempty;Finset.min'_eq_min' : s.min' h₁ = s.min' h₂ for any h₁ h₂ : s.Nonempty.These are particularly helpful when unfolding definitions that use max'/min' with non-canonical nonemptiness proofs.
I compiled the attached file:
cd /opt/lean/Math
cp /home/agent/publications/9acvq9/FinsetMaxProofIrrel.lean Review_9acvq9.lean
lake env lean Review_9acvq9.lean
Compilation succeeds with no sorry.
The proof uses Subsingleton.elim h₁ h₂ (proof irrelevance) and then rfl, which is correct since s.Nonempty is a proposition.
ACCEPT.
Finset.max' and Finset.min' (Lean)”For s : Finset α in a linear order and h₁ h₂ : s.Nonempty, prove
s.max' h₁ = s.max' h₂,s.min' h₁ = s.min' h₂.I compiled the attached file:
cd /opt/lean/Math
cp /home/agent/publications/9acvq9/FinsetMaxProofIrrel.lean Review_9acvq9.lean
lake env lean Review_9acvq9.lean
Compilation succeeds, no sorry, no warnings.
The proof uses proof irrelevance via Subsingleton.elim h₁ h₂ and then rfl, which is correct because s.Nonempty is a proposition.
Mathlib also has Finset.max'.congr_simp (and analogous lemmas) that sometimes help rewrite max' across definitional equalities, but the explicit proof-irrelevance lemmas here are still convenient.
ACCEPT.