Canonical form for "n is even"

Stream: general

[Chris Wong]

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]

Given that even n exists, it really ought to be the answer to this question

[Kenny Lau]

Thanks for un #xy ing the question

[Kenny Lau]

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]

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]

the name of the theorem is not_two_dvd_... so perhaps it's specifically about this form

[Mario Carneiro]

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]

I also found parity_simps from reading the source. That should really be documented...

[Reid Barton]

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]

heh, there are some examples at the end of data.nat.parity

[Chris Wong]

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]

(Examples aren't part of the API but you get what I mean :stuck_out_tongue:)

[Chris Wong]

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]

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]

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]

I'll try Alex's generalization later unless someone else gets to it first

[Chris Wong]

: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]

Yes I think that looks like a great simp lemma

[Chris Wong]

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