[Merged by Bors] - feat: Add to List.finRange and Fin.castLE APIs
#8306
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Mathlib/Data/List/FinRange.lean
Outdated
| /-- Folding over a list obtained from a function `g : Fin n → α` is equivalent to | ||
| folding over the list of indices `0, 1, ..., n-1` and invoking `g` for each index -/ | ||
| theorem foldl_ofFn {α β n} (f : α → β → α) (init : α) (g : Fin n → β) : | ||
| (List.ofFn g).foldl f init = (List.finRange n).foldl (fun a i => f a (g i)) init := by | ||
| rw [ofFn_eq_map, foldl_map] | ||
|
|
||
| /-- Folding over a list obtained from a function `g : Fin n → α` is equivalent to | ||
| folding over the list of indices `0, 1, ..., n-1` and invoking `g` for each index -/ | ||
| theorem foldr_ofFn {α β n} (f : β → α → α) (init : α) (g : Fin n → β) : | ||
| (List.ofFn g).foldr f init = (List.finRange n).foldr (fun i a => f (g i) a) init := by | ||
| rw [ofFn_eq_map, foldr_map] |
There was a problem hiding this comment.
With these new proofs in mind, it's not really clear to me that we want these lemmas at all; I think it makes more sense for the user to go via ofFn_eq_map, because then the whole API for map is at their fingertips. The trail you're blazing ends in us repeating the entire map API for ofFn!
Maybe the documentation for ofFn should more prominently display ofFn_eq_map.
There was a problem hiding this comment.
Fair point.
Maybe the documentation for ofFn should more prominently display ofFn_eq_map.
This is slightly complicated, since List.ofFn is defined in Std, while ofFn_eq_map is from Mathlib.
In any case, now that I know about ofFn_eq_map, I can just use these simpler proofs in #5920
There was a problem hiding this comment.
ofFn_eq_map could probably be upstreamed to Std (unless finRange is only in mathlib...)
There was a problem hiding this comment.
finRange is indeed also only in mathlib. The definition of finRange depends only on stuff in std, so we could upstream ofFn_eq_map and finRange together, if desired
alexkeizer
changed the title
List.finRange APIList.finRange and Fin.castLE APIs
|
I've now removed the fold lemmas, but kept the others |
|
✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
bors r+ |
Add a lemma that unfolds `finRange n.succ` in terms of `List.concat`, and add a few simp-lemmas for `Fin.castLE`
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
List.finRange and Fin.castLE APIsList.finRange and Fin.castLE APIs
Add a lemma that unfolds `finRange n.succ` in terms of `List.concat`, and add a few simp-lemmas for `Fin.castLE`
Add a lemma that unfolds `finRange n.succ` in terms of `List.concat`, and add a few simp-lemmas for `Fin.castLE`
Add a lemma that unfolds
finRange n.succin terms ofList.concat, and add a few simp-lemmas forFin.castLEThe PRed lemmas seem unrelated. This PR exists because they were both used in a different proof, which was decided against, but these lemmas were deemed useful enough to keep the PR