max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: strengthen finIdxOf? lemmas (#8678)

Browse source 
This PR makes the LHS of `isSome_finIdxOf?` and `isNone_finIdxOf?` more
general.
This commit is contained in:
Eric Wieser 2025-06-11 08:32:01 +01:00 • committed by GitHub
parent a92890ec84
commit 44e36dec6f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/Array/Find.lean
View file

@ -743,13 +743,15 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
simp [List.finIdxOf?_eq_some_iff]
@[simp]
theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
(xs.finIdxOf? a).isSome ↔ a ∈ xs := by
theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
(xs.finIdxOf? a).isSome = xs.contains a := by
rcases xs with ⟨xs⟩
simp [Array.size]
theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
(xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
simp
@[simp]
theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
(xs.finIdxOf? a).isNone = !xs.contains a := by
rcases xs with ⟨xs⟩
simp [Array.size]
end Array

13
src/Init/Data/List/Find.lean
View file

@ -1097,17 +1097,18 @@ theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
@[simp]
theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.finIdxOf? a).isSome ↔ a ∈ l := by
theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
(l.finIdxOf? a).isSome = l.contains a := by
induction l with
| nil => simp
| cons x xs ih =>
simp only [finIdxOf?_cons]
split <;> simp_all [@eq_comm _ x a]
split <;> simp_all [BEq.comm]
theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
(l.finIdxOf? a).isNone = ¬ a ∈ l := by
simp
@[simp]
theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
(l.finIdxOf? a).isNone = !l.contains a := by
rw [← isSome_finIdxOf?, Option.not_isSome]
/-! ### idxOf?