feat(data/list/big_operators): More lemmas about alternating product (#…

…13195)

A few more lemmas about `list.alternating_prod` and `list.alternating_sum` and a proof that 11 divides even length base 10 palindromes.

Also rename `palindrome` to `list.palindrome` (as it should have been).

Co-authored-by: Chris Wong



Co-authored-by: Chris Wong <lambda.fairy@gmail.com>

src/data/list/big_operators.lean

@@ -3,16 +3,18 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 -/
+import algebra.group_power
 import data.list.basic
 
 /-!
 # Sums and products from lists
 
-This file provides basic results about `list.prod` and `list.sum`, which calculate the product and
-sum of elements of a list. These are defined in [`data.list.defs`](./data/list/defs).
+This file provides basic results about `list.prod`, `list.sum`, which calculate the product and sum
+of elements of a list and `list.alternating_prod`, `list.alternating_sum`, their alternating
+counterparts. These are defined in [`data.list.defs`](./defs).
 -/
 
-variables {ι M N P M₀ G R : Type*}
+variables {ι α M N P M₀ G R : Type*}
 
 namespace list
 section monoid
@@ -482,19 +484,51 @@ lemma tail_sum (L : list ℕ) : L.tail.sum = L.sum - L.head :=
 by rw [← head_add_tail_sum L, add_comm, add_tsub_cancel_right]
 
 section alternating
-variables [comm_group G]
+section
+variables [has_one α] [has_mul α] [has_inv α]
+
+@[simp, to_additive] lemma alternating_prod_nil : alternating_prod ([] : list α) = 1 := rfl
+@[simp, to_additive] lemma alternating_prod_singleton (a : α) : alternating_prod [a] = a := rfl
+
+@[to_additive] lemma alternating_prod_cons_cons' (a b : α) (l : list α) :
+  alternating_prod (a :: b :: l) = a * b⁻¹ * alternating_prod l := rfl
+
+end
+
+@[to_additive] lemma alternating_prod_cons_cons [div_inv_monoid α] (a b : α) (l : list α) :
+  alternating_prod (a :: b :: l) = a / b * alternating_prod l :=
+by rw [div_eq_mul_inv, alternating_prod_cons_cons']
 
-@[simp, to_additive] lemma alternating_prod_nil : alternating_prod ([] : list G) = 1 := rfl
+variables [comm_group α]
 
-@[simp, to_additive] lemma alternating_prod_singleton (g : G) : alternating_prod [g] = g := rfl
+@[to_additive] lemma alternating_prod_cons' :
+  ∀ (a : α) (l : list α), alternating_prod (a :: l) = a * (alternating_prod l)⁻¹
+| a [] := by rw [alternating_prod_nil, one_inv, mul_one, alternating_prod_singleton]
+| a (b :: l) :=
+by rw [alternating_prod_cons_cons', alternating_prod_cons' b l, mul_inv, inv_inv, mul_assoc]
 
-@[simp, to_additive alternating_sum_cons_cons']
-lemma alternating_prod_cons_cons (g h : G) (l : list G) :
-  alternating_prod (g :: h :: l) = g * h⁻¹ * alternating_prod l := rfl
+@[simp, to_additive] lemma alternating_prod_cons (a : α) (l : list α) :
+  alternating_prod (a :: l) = a / alternating_prod l :=
+by rw [div_eq_mul_inv, alternating_prod_cons']
 
-lemma alternating_sum_cons_cons {G : Type*} [add_comm_group G] (g h : G) (l : list G) :
-  alternating_sum (g :: h :: l) = g - h + alternating_sum l :=
-by rw [sub_eq_add_neg, alternating_sum]
+@[to_additive]
+lemma alternating_prod_append : ∀ l₁ l₂ : list α,
+  alternating_prod (l₁ ++ l₂) = alternating_prod l₁ * alternating_prod l₂ ^ (-1 : ℤ) ^ length l₁
+| [] l₂ := by simp
+| (a :: l₁) l₂ := by simp_rw [cons_append, alternating_prod_cons, alternating_prod_append,
+  length_cons, pow_succ, neg_mul, one_mul, zpow_neg, ←div_eq_mul_inv, div_div]
+
+@[to_additive]
+lemma alternating_prod_reverse :
+  ∀ l : list α, alternating_prod (reverse l) = alternating_prod l ^ (-1 : ℤ) ^ (length l + 1)
+| [] := by simp only [alternating_prod_nil, one_zpow, reverse_nil]
+| (a :: l) :=
+begin
+  simp_rw [reverse_cons, alternating_prod_append, alternating_prod_reverse,
+    alternating_prod_singleton, alternating_prod_cons, length_reverse, length, pow_succ, neg_mul,
+    one_mul, zpow_neg, inv_inv],
+  rw [mul_comm, ←div_eq_mul_inv, div_zpow],
+end
 
 end alternating
 

src/data/list/palindrome.lean

@@ -25,9 +25,9 @@ principle. Also provided are conversions to and from other equivalent definition
 palindrome, reverse, induction
 -/
 
-open list
+variables {α β : Type*}
 
-variables {α : Type*}
+namespace list
 
 /--
 `palindrome l` asserts that `l` is a palindrome. This is defined inductively:
@@ -42,6 +42,7 @@ inductive palindrome : list α → Prop
 | cons_concat : ∀ x {l}, palindrome l → palindrome (x :: (l ++ [x]))
 
 namespace palindrome
+variables {l : list α}
 
 lemma reverse_eq {l : list α} (p : palindrome l) : reverse l = l :=
 palindrome.rec_on p rfl (λ _, rfl) (λ x l p h, by simp [h])
@@ -62,7 +63,11 @@ iff.intro reverse_eq of_reverse_eq
 lemma append_reverse (l : list α) : palindrome (l ++ reverse l) :=
 by { apply of_reverse_eq, rw [reverse_append, reverse_reverse] }
 
+protected lemma map (f : α → β) (p : palindrome l) : palindrome (map f l) :=
+of_reverse_eq $ by rw [← map_reverse, p.reverse_eq]
+
 instance [decidable_eq α] (l : list α) : decidable (palindrome l) :=
 decidable_of_iff' _ iff_reverse_eq
 
 end palindrome
+end list

src/data/nat/digits.lean

@@ -5,7 +5,9 @@ Authors: Scott Morrison, Shing Tak Lam, Mario Carneiro
 -/
 import data.int.modeq
 import data.nat.log
+import data.nat.parity
 import data.list.indexes
+import data.list.palindrome
 import tactic.interval_cases
 import tactic.linarith
 
@@ -23,6 +25,7 @@ A basic `norm_digits` tactic is also provided for proving goals of the form
 -/
 
 namespace nat
+variables {n : ℕ}
 
 /-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding. -/
 def digits_aux_0 : ℕ → list ℕ
@@ -585,14 +588,24 @@ begin
     (zmodeq_of_digits_digits b b' c (int.modeq_iff_dvd.2 h).symm _).symm.dvd,
 end
 
-lemma eleven_dvd_iff (n : ℕ) :
-  11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map (λ n : ℕ, (n : ℤ))).alternating_sum :=
+lemma eleven_dvd_iff : 11 ∣ n ↔ (11 : ℤ) ∣ ((digits 10 n).map (λ n : ℕ, (n : ℤ))).alternating_sum :=
 begin
   have t := dvd_iff_dvd_of_digits 11 10 (-1 : ℤ) (by norm_num) n,
   rw of_digits_neg_one at t,
   exact t,
 end
 
+lemma eleven_dvd_of_palindrome (p : (digits 10 n).palindrome) (h : even (digits 10 n).length) :
+  11 ∣ n :=
+begin
+  let dig := (digits 10 n).map (coe : ℕ → ℤ),
+  replace h : even dig.length := by rwa list.length_map,
+  refine eleven_dvd_iff.2 ⟨0, (_ : dig.alternating_sum = 0)⟩,
+  have := dig.alternating_sum_reverse,
+  rw [(p.map _).reverse_eq, pow_succ, neg_one_pow_of_even h, mul_one, neg_one_zsmul] at this,
+  exact eq_zero_of_neg_eq this.symm,
+end
+
 /-! ### `norm_digits` tactic -/
 
 namespace norm_digits