Commit 2023-06-28 14:58 5526fd89

View on Github →

feat: add reverse induction principle for Vector (#5400) Add a snoc pseudo-constructor, lemmas to reason about snoc, and a reverse induction principle for Vectors.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Vector/Basic.lean

added theorem Vector.mapAccumr_cons

added theorem Vector.mapAccumr₂_cons

Created Mathlib/Data/Vector/Snoc.lean

added theorem Vector.mapAccumr_nil

added theorem Vector.mapAccumr_snoc

added theorem Vector.mapAccumr₂_nil

added theorem Vector.mapAccumr₂_snoc

added theorem Vector.map_snoc

added theorem Vector.map₂_snoc

added theorem Vector.replicate_succ_to_snoc

added def Vector.revCasesOn

added def Vector.revInductionOn

added def Vector.revInductionOn₂

added theorem Vector.reverse_cons

added theorem Vector.reverse_snoc

added def Vector.snoc

added theorem Vector.snoc_cons

added theorem Vector.snoc_nil