feat(data/nat/digits): Add lemmas#7813
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
left a comment
eric-wieser
left a comment
There was a problem hiding this comment.
This looks good to me now, thanks. I'll leave it a day or two in case another reviewer has suggestions for shortening the proof
eric-wieser
added
the
awaiting-review
ericrbg
left a comment
ericrbg
left a comment
There was a problem hiding this comment.
this looks really good! fantastic first PR
| /-- | ||
| Applying `(digits b ∘ of_digits b)` will create a prefix of the original list if it has proper | ||
| digits; it removes trailing zeros. | ||
| -/ | ||
| lemma digits_of_digits_prefix {b : ℕ} {L : list ℕ} (hlt : ∀ a ∈ L, a < b) : | ||
| digits b (of_digits b L) <+: L := |
There was a problem hiding this comment.
As stated, it feels like this is not a very useful lemma. Surely we want to know what is actually stated in the doc-string, i.e. that you get exactly L with trailing zeros removed?
Given that saying "L with trailing zeroes removed" is perhaps slightly cumbersome, why not instead add the hypothesis that L does not end with 0, and then strengthen the conclusion?
A separate lemma could say that of_digits b (L ++ [0]) = of_digits b L.
There was a problem hiding this comment.
(I'm also happy to be convinced that this lemma is useful as is, although I have to say that I'm skeptical that Kaprekar's routine counts as an application. :-)
There was a problem hiding this comment.
(Also --- thanks for the PR! Sorry if the above comment sounds grumpy, I'm just wondering what lemma you actually want.)
jcommelin
added
awaiting-author
|
@Pazzaz gentle ping. Feel free to ask here or on Zulip if you need help with the suggestion above. |
6 participants
Add some lemmas about
nat.digitsandnat.of_digits, including thatdigits b (of_digits b L)is a prefix ofLI found the need for these lemmas while formalizing properties of Kaprekar's routine.
(Note: this is my first PR 🙂)