[Merged by Bors] - feat: add reverse induction principle for Vector #5400
Conversation
alexkeizer
added
blocked-by-other-PR
semorrison
added
merge-conflict
alexkeizer
added
the
awaiting-review
semorrison
removed
the
merge-conflict
Mathlib/Data/Vector/Snoc.lean
Outdated
| (nil : C nil) | ||
| (snoc : ∀ {n : ℕ} (xs : Vector α n) (x : α), C xs → C (xs.snoc x)) | ||
| : C v := |
There was a problem hiding this comment.
This indentation style is not usual. We just indent the theorem statement with four spaces usually, with occasional extra two space indentations for readability.
These should now be addressed |
Mathlib/Data/Vector/Basic.lean
Outdated
|
|
||
| @[simp] | ||
| theorem mapAccumr_cons : mapAccumr f (x ::ᵥ xs) s | ||
| = let r := mapAccumr f xs s |
There was a problem hiding this comment.
I think this indentation is somewhat not in mathlib style as well.
|
✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with |
semorrison
added
delegated
and removed
awaiting-review
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
…4 into vector-snoc
|
bors merge |
Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.
Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.
Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.
Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.
Vector.snoc xs xis just a short-hand forxs ++ [x].The reverse induction principle uses
xs.snoc xfor it's recursive step, which makes it easier to reason about algorithms that work on aVectorright-to-left, such asfoldrormapAccumr.The PR also add some simplification rules for
snocwhich help with such backwards proofs.