Zulip Chat Archive
Stream: general
Topic: Canonical form for "n is even"
Chris Wong (Aug 15 2020 at 14:12):
What's the canonical way to say that a natural number is even? I see 2 \dvd n
, n % 2 = 0
, even n
...
Context: I'd like to prove that alternating_sum
and ++
commute when the first list has even length.
Reid Barton (Aug 15 2020 at 14:15):
Given that even n
exists, it really ought to be the answer to this question
Kenny Lau (Aug 15 2020 at 17:21):
Thanks for un #xy ing the question
Kenny Lau (Aug 15 2020 at 17:22):
you might want to also consider the more general statement alternating_sum (L1 ++ L2) = alternating_sum L1 + (-1) ^ L1.length * alternating_sum L2
Chris Wong (Aug 16 2020 at 01:04):
Thanks @Reid Barton. I guess my source of confusion was this lemma, and the one below it:
https://leanprover-community.github.io/mathlib_docs/data/nat/parity.html#nat.two_not_dvd_two_mul_add_one
What's the reason for using 2 \dvd
here – especially in the module where even
is defined?
Mario Carneiro (Aug 16 2020 at 01:14):
the name of the theorem is not_two_dvd_...
so perhaps it's specifically about this form
Mario Carneiro (Aug 16 2020 at 01:15):
especially in the module where even and odd are defined you are more likely to find alternative representations, because that's where you would prove equivalence of the alternative representations
Chris Wong (Aug 16 2020 at 01:18):
I also found parity_simps
from reading the source. That should really be documented...
Reid Barton (Aug 16 2020 at 01:23):
data.nat.parity
is a 100 line file--even if someone were to write documentation for it, the most efficient way to find out what's in it would still be to just read the whole thing.
Mario Carneiro (Aug 16 2020 at 01:31):
heh, there are some example
s at the end of data.nat.parity
Chris Wong (Aug 16 2020 at 01:42):
Even (hehe) so, when reading the docs I think that there's an expectation that what's listed is the complete public interface for that module. That defs and lemmas are shown, but custom simp sets and examples are not, seems like a bug to me.
Chris Wong (Aug 16 2020 at 01:47):
(Examples aren't part of the API but you get what I mean :stuck_out_tongue:)
Chris Wong (Aug 16 2020 at 02:38):
Regarding the (-1) ^ L1.length
formulation – that requires a ring
, whereas the specialized approach only needs add_comm_group
(like the other alternating_sum
lemmas). And it gets more complicated when we consider alternating_prod
. So perhaps both statements are useful?
And un- #xy -ing further, I'm using this to prove "a palindromic number of even length is divisible by 11", so the specialized version would be more useful to me. (I should have mentioned that first whoops)
Alex J. Best (Aug 16 2020 at 02:48):
What about
import data.list.basic
import algebra.group_power
open list
example {α : Type} [add_group α] (L1 L2 : list α) :
alternating_sum (L1 ++ L2) = alternating_sum L1 + (-1) ^ L1.length •ℤ alternating_sum L2
:= sorry
for the general version, no ring required (in the statement at least).
Chris Wong (Aug 16 2020 at 03:23):
Here's what I've got so far:
import data.list.basic
import data.nat.parity
open list nat
lemma alternating_sum_append_of_even_length {α : Type*} [add_comm_group α] :
∀ (l₁ l₂ : list α), even (length l₁) → alternating_sum (l₁ ++ l₂) = alternating_sum l₁ + alternating_sum l₂
| [] l₂ _ := by simp
| [_] l₂ h := by simpa using h
| (x :: y :: l₁) l₂ h := by simp [alternating_sum_append_of_even_length l₁ l₂ (by simpa [even_succ] using h), add_assoc]
lemma alternating_sum_reverse_of_even_length {α : Type*} [add_comm_group α] :
∀ (l : list α), even (length l) → alternating_sum (reverse l) = -alternating_sum l
| [] _ := by simp
| [_] h := by simpa using h
| (x :: y :: l) h :=
begin
replace h : even (length l), by simpa [even_succ] using h,
simp [alternating_sum_append_of_even_length (reverse l) [y, x] ((length_reverse l).symm ▸ h),
alternating_sum_reverse_of_even_length l h]
end
Chris Wong (Aug 16 2020 at 03:23):
I'll try Alex's generalization later unless someone else gets to it first
Chris Wong (Aug 21 2020 at 13:53):
:octopus:
import data.list.basic
import algebra.group_power
open list
@[simp]
lemma alternating_sum_nil {α : Type*} [has_zero α] [has_add α] [has_neg α] : alternating_sum (@nil α) = 0 := rfl
lemma alternating_sum_cons {α : Type*} [add_comm_group α] : ∀ (x : α) (l : list α), alternating_sum (x :: l) = x - alternating_sum l
| x [] := (sub_zero x).symm
| x (y :: l) := by rw [alternating_sum_cons_cons, alternating_sum_cons y l, sub_add]
lemma alternating_sum_append {α : Type*} [add_comm_group α] :
∀ (l₁ l₂ : list α), alternating_sum (l₁ ++ l₂) = alternating_sum l₁ + (-1) ^ l₁.length •ℤ alternating_sum l₂
| [] l₂ := by simp
| (x :: l₁) l₂ :=
begin
have h := alternating_sum_append l₁ l₂,
simp [alternating_sum_cons, pow_succ, sub_add, h]
end
Now I wonder if it's safe to put @[simp]
on alternating_sum_cons
...
Kevin Buzzard (Aug 21 2020 at 14:19):
Yes I think that looks like a great simp lemma
Chris Wong (Aug 22 2020 at 02:26):
I agree! My concern is about this existing lemma:
@[simp]
theorem alternating_sum_cons_cons' {G : Type*} [add_comm_group G] (g h : G) (l : list G) :
(g :: h :: l).alternating_sum = g + -h + l.alternating_sum := rfl
That'll probably conflict with alternating_sum_cons
, right? I guess I'll have to try and see
Last updated: Dec 20 2023 at 11:08 UTC