From 2a04ec03f17ad178e2e1e596973f7eb4c9838d1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 9 Apr 2022 00:02:05 +0000 Subject: [PATCH] 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 --- src/data/list/big_operators.lean | 58 +++++++++++++++++++++++++------- src/data/list/palindrome.lean | 9 +++-- src/data/nat/digits.lean | 17 ++++++++-- 3 files changed, 68 insertions(+), 16 deletions(-) diff --git a/src/data/list/big_operators.lean b/src/data/list/big_operators.lean index 0f59f9571de4d..f1b6b382975a9 100644 --- a/src/data/list/big_operators.lean +++ b/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 diff --git a/src/data/list/palindrome.lean b/src/data/list/palindrome.lean index aab0958efe135..e38cc03ddc2d8 100644 --- a/src/data/list/palindrome.lean +++ b/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 diff --git a/src/data/nat/digits.lean b/src/data/nat/digits.lean index 1558ebc6020b1..26b302621474e 100644 --- a/src/data/nat/digits.lean +++ b/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