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 examples 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