[Merged by Bors] - feat: add reverse induction principle for Vector#5400
[Merged by Bors] - feat: add reverse induction principle for Vector#5400alexkeizer wants to merge 10 commits intomasterfrom
Conversation
ChrisHughes24
left a comment
There was a problem hiding this comment.
I think my main comments here are just style comments about indentation.
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 |
ChrisHughes24
left a comment
There was a problem hiding this comment.
You can merge after the small fixes
bors d+
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 |
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. |
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.