feat(archive/imo): add IMO 2019 problem 4 (#4482)

archive/imo/imo2019_q4.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import tactic.interval_cases
+import algebra.big_operators.order
+import algebra.big_operators.enat
+import data.nat.multiplicity
+
+/-!
+# IMO 2019 Q4
+
+Find all pairs `(k, n)` of positive integers such that
+```
+  k! = (2 ^ n − 1)(2 ^ n − 2)(2 ^ n − 4)···(2 ^ n − 2 ^ (n − 1))
+```
+We show in this file that this property holds iff `(k, n) = (1, 1) ∨ (k, n) = (3, 2)`.
+
+Proof sketch:
+The idea of the proof is to count the factors of 2 on both sides. The LHS has less than `k` factors
+of 2, and the RHS has exactly `n * (n - 1) / 2` factors of 2. So we know that `n * (n - 1) / 2 < k`.
+Now for `n ≥ 6` we have `RHS < 2 ^ (n ^ 2) < (n(n-1)/2)! < k!`. We then treat the cases `n < 6`
+individually.
+-/
+
+open_locale nat big_operators
+open finset multiplicity nat (hiding zero_le prime)
+
+theorem imo2019_q4_upper_bound {k n : ℕ} (hk : k > 0)
+  (h : (k! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i)) : n < 6 :=
+begin
+  have prime_2 : prime (2 : ℤ),
+  { exact prime_iff_prime_int.mp prime_two },
+  have h2 : n * (n - 1) / 2 < k,
+  { suffices : multiplicity 2 (k! : ℤ) = (n * (n - 1) / 2 : ℕ),
+    { rw [← enat.coe_lt_coe, ← this], change multiplicity ((2 : ℕ) : ℤ) _ < _,
+      simp_rw [int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] },
+    rw [h, multiplicity.finset.prod prime_2, ← sum_range_id, ← sum_nat_coe_enat],
+    apply sum_congr rfl, intros i hi,
+    rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime prime_2],
+    rwa [multiplicity_pow_self_of_prime prime_2, multiplicity_pow_self_of_prime prime_2,
+      enat.coe_lt_coe, ←mem_range] },
+  rw [←not_le], intro hn,
+  apply ne_of_lt _ h.symm,
+  suffices : (∏ i in range n, 2 ^ n : ℤ) < ↑k!,
+  { apply lt_of_le_of_lt _ this, apply prod_le_prod,
+    { intros, rw [sub_nonneg], apply pow_le_pow, norm_num, apply le_of_lt, rwa [← mem_range] },
+    { intros, apply sub_le_self, apply pow_nonneg, norm_num } },
+  suffices : 2 ^ (n * n) < (n * (n - 1) / 2)!,
+  { rw [prod_const, card_range, ← pow_mul], rw [← int.coe_nat_lt_coe_nat_iff] at this,
+    convert this.trans _, norm_cast, rwa [int.coe_nat_lt_coe_nat_iff, factorial_lt],
+    refine nat.div_pos _ (by norm_num),
+    refine le_trans _ (mul_le_mul hn (pred_le_pred hn) (zero_le _) (zero_le _)),
+    norm_num },
+  refine le_induction _ _ n hn, { norm_num },
+  intros n' hn' ih,
+  have h5 : 1 ≤ 2 * n', { linarith },
+  have : 2 ^ (2 + 2) ≤ (n' * (n' - 1) / 2).succ,
+  { change succ (6 * (6 - 1) / 2) ≤ _,
+    apply succ_le_succ, apply nat.div_le_div_right,
+    exact mul_le_mul hn' (pred_le_pred hn') (zero_le _) (zero_le _) },
+  rw [triangle_succ], apply lt_of_lt_of_le _ factorial_mul_pow_le_factorial,
+  refine lt_of_le_of_lt _ (mul_lt_mul ih (nat.pow_le_pow_of_le_left this _)
+    (pow_pos (by norm_num) _) (zero_le _)),
+  rw [← pow_mul, ← pow_add], apply pow_le_pow_of_le_right, norm_num,
+  rw [add_mul 2 2],
+  convert add_le_add_left (add_le_add_left h5 (2 * n')) (n' * n') using 1, ring
+end
+
+theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
+  (k! : ℤ) = (∏ i in range n, (2 ^ n - 2 ^ i)) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) :=
+begin
+  /- The implication `←` holds. -/
+  split, swap,
+  { rintro (h|h); simp [prod.ext_iff] at h; rcases h with ⟨rfl, rfl⟩;
+    norm_num [prod_range_succ, succ_mul] },
+  intro h,
+  /- We know that n < 6. -/
+  have := imo2019_q4_upper_bound hk h,
+  interval_cases n,
+  /- n = 1 -/
+  { left, congr, norm_num at h, norm_cast at h, rw [factorial_eq_one] at h, apply antisymm h,
+    apply succ_le_of_lt hk },
+  /- n = 2 -/
+  { right, congr, norm_num [prod_range_succ] at h, norm_cast at h, rw [← factorial_inj],
+    exact h, rw [h], norm_num },
+  all_goals { exfalso, norm_num [prod_range_succ] at h, norm_cast at h, },
+  /- n = 3 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h; norm_num },
+  /- n = 4 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 7 _ _ _ h; norm_num },
+  /- n = 5 -/
+  { refine monotone_factorial.ne_of_lt_of_lt_nat 10 _ _ _ h; norm_num },
+end

src/algebra/big_operators/default.lean

@@ -6,3 +6,4 @@ import algebra.big_operators.ring
 import algebra.big_operators.pi
 import algebra.big_operators.finsupp
 import algebra.big_operators.nat_antidiagonal
+import algebra.big_operators.enat

src/algebra/big_operators/enat.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import algebra.big_operators.basic
+import data.nat.enat
+
+/-!
+# Big operators in `enat`
+
+A simple lemma about sums in `enat`.
+-/
+open_locale big_operators
+variables {α : Type*}
+
+namespace finset
+lemma sum_nat_coe_enat (s : finset α) (f : α → ℕ) :
+  (∑ x in s, (f x : enat)) = (∑ x  in s, f x : ℕ) :=
+(enat.coe_hom.map_sum _ _).symm
+
+end finset

src/data/int/basic.lean

@@ -35,7 +35,7 @@ instance : comm_ring int :=
   right_distrib  := int.distrib_right,
   mul_comm       := int.mul_comm }
 
-/- Extra instances to short-circuit type class resolution -/
+/-! ### Extra instances to short-circuit type class resolution -/
 -- instance : has_sub int            := by apply_instance -- This is in core
 instance : add_comm_monoid int    := by apply_instance
 instance : add_monoid int         := by apply_instance
@@ -111,7 +111,7 @@ lemma coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := int.coe_nat_pos.2 (succ
 @[simp, norm_cast] theorem coe_nat_abs (n : ℕ) : abs (n : ℤ) = n :=
 abs_of_nonneg (coe_nat_nonneg n)
 
-/- succ and pred -/
+/-! ### succ and pred -/
 
 /-- Immediate successor of an integer: `succ n = n + 1` -/
 def succ (a : ℤ) := a + 1
@@ -194,7 +194,7 @@ begin
       exact Hp _ (le_of_lt (add_lt_of_neg_of_le (neg_succ_lt_zero _) (le_refl _))) ih } }
 end
 
-/- nat abs -/
+/-! ### nat abs -/
 
 attribute [simp] nat_abs nat_abs_of_nat nat_abs_zero nat_abs_one
 
@@ -240,7 +240,7 @@ begin
   simpa using w₂,
 end
 
-/- /  -/
+/-! ### `/`  -/
 
 @[simp] theorem of_nat_div (m n : ℕ) : of_nat (m / n) = (of_nat m) / (of_nat n) := rfl
 
@@ -358,7 +358,7 @@ by rw [mul_comm, int.mul_div_cancel _ H]
 @[simp] protected theorem div_self {a : ℤ} (H : a ≠ 0) : a / a = 1 :=
 by have := int.mul_div_cancel 1 H; rwa one_mul at this
 
-/- mod -/
+/-! ### mod -/
 
 theorem of_nat_mod (m n : nat) : (m % n : ℤ) = of_nat (m % n) := rfl
 
@@ -513,7 +513,7 @@ begin
   rw [sub_add_cancel, ← add_mod_mod, sub_add_cancel, mod_mod]
 end
 
-/- properties of / and % -/
+/-! ### properties of `/` and `%` -/
 
 @[simp] theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : 0 < a) : a * b / (a * c) = b / c :=
 suffices ∀ (m k : ℕ) (b : ℤ), (m.succ * b / (m.succ * k) : ℤ) = b / k, from
@@ -584,7 +584,7 @@ match (n % 2), h, h₁ with
 | -[1+ a] := λ _ h₁, absurd h₁ dec_trivial
 end
 
-/- dvd -/
+/-! ### dvd -/
 
 @[norm_cast] theorem coe_nat_dvd {m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n :=
 ⟨λ ⟨a, ae⟩, m.eq_zero_or_pos.elim
@@ -771,7 +771,22 @@ end
 lemma dvd_of_pow_dvd {p k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p^k) ∣ m) : ↑p ∣ m :=
 by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
-/- / and ordering -/
+/-- If `n > 0` then `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)`
+  for some `k`. -/
+lemma exists_lt_and_lt_iff_not_dvd (m : ℤ) {n : ℤ} (hn : 0 < n) :
+  (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬ n ∣ m :=
+begin
+  split,
+  { rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩, rw [mul_lt_mul_left hn] at h1k h2k,
+    rw [lt_add_one_iff, ← not_lt] at h2k, exact h2k h1k },
+  { intro h, rw [dvd_iff_mod_eq_zero, ← ne.def] at h,
+    have := (mod_nonneg m hn.ne.symm).lt_of_ne h.symm,
+    simp only [← mod_add_div m n] {single_pass := tt},
+    refine ⟨m / n, lt_add_of_pos_left _ this, _⟩,
+    rw [add_comm _ (1 : ℤ), left_distrib, mul_one], exact add_lt_add_right (mod_lt_of_pos _ hn) _ }
+end
+
+/-! ### `/` and ordering -/
 
 protected theorem div_mul_le (a : ℤ) {b : ℤ} (H : b ≠ 0) : a / b * b ≤ a :=
 le_of_sub_nonneg $ by rw [mul_comm, ← mod_def]; apply mod_nonneg _ H
@@ -877,7 +892,7 @@ end
 
 @[simp] theorem neg_add_neg (m n : ℕ) : -[1+m] + -[1+n] = -[1+nat.succ(m+n)] := rfl
 
-/- to_nat -/
+/-! ### to_nat -/
 
 theorem to_nat_eq_max : ∀ (a : ℤ), (to_nat a : ℤ) = max a 0
 | (n : ℕ) := (max_eq_left (coe_zero_le n)).symm
@@ -942,7 +957,7 @@ lemma to_nat_zero_of_neg : ∀ {z : ℤ}, z < 0 → z.to_nat = 0
 | (-[1+n]) _ := rfl
 | (int.of_nat n) h := (not_le_of_gt h $ int.of_nat_nonneg n).elim
 
-/- units -/
+/-! ### units -/
 
 @[simp] theorem units_nat_abs (u : units ℤ) : nat_abs u = 1 :=
 units.ext_iff.1 $ nat.units_eq_one ⟨nat_abs u, nat_abs ↑u⁻¹,
@@ -955,7 +970,7 @@ by simpa only [units.ext_iff, units_nat_abs] using nat_abs_eq u
 lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
 
-/- bitwise ops -/
+/-! ### bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl
 @[simp] lemma bodd_one : bodd 1 = tt := rfl
@@ -1189,7 +1204,7 @@ congr_arg coe (nat.one_shiftl _)
 
 @[simp] lemma zero_shiftr (n) : shiftr 0 n = 0 := zero_shiftl _
 
-/- Least upper bound property for integers -/
+/-! ### Least upper bound property for integers -/
 
 section classical
 open_locale classical

src/data/nat/basic.lean

@@ -777,6 +777,9 @@ protected lemma div_eq_zero_iff {a b : ℕ} (hb : 0 < b) : a / b = 0 ↔ a < b :
   λ h, by rw [← nat.mul_right_inj hb, ← @add_left_cancel_iff _ _ (a % b), mod_add_div,
     mod_eq_of_lt h, mul_zero, add_zero]⟩
 
+protected lemma div_eq_zero {a b : ℕ} (hb : a < b) : a / b = 0 :=
+(nat.div_eq_zero_iff $ (zero_le a).trans_lt hb).mpr hb
+
 lemma eq_zero_of_le_div {a b : ℕ} (hb : 2 ≤ b) (h : a ≤ a / b) : a = 0 :=
 eq_zero_of_mul_le hb $
   by rw mul_comm; exact (nat.le_div_iff_mul_le' (lt_of_lt_of_le dec_trivial hb)).1 h
@@ -1202,6 +1205,19 @@ dvd_trans this hdiv
 lemma dvd_of_pow_dvd {p k m : ℕ} (hk : 1 ≤ k) (hpk : p^k ∣ m) : p ∣ m :=
 by rw ←pow_one p; exact pow_dvd_of_le_of_pow_dvd hk hpk
 
+/-- `m` is not divisible by `n` iff it is between `n * k` and `n * (k + 1)` for some `k`. -/
+lemma exists_lt_and_lt_iff_not_dvd (m : ℕ) {n : ℕ} (hn : 0 < n) :
+  (∃ k, n * k < m ∧ m < n * (k + 1)) ↔ ¬ n ∣ m :=
+begin
+  split,
+  { rintro ⟨k, h1k, h2k⟩ ⟨l, rfl⟩, rw [mul_lt_mul_left hn] at h1k h2k,
+    rw [lt_succ_iff, ← not_lt] at h2k, exact h2k h1k },
+  { intro h, rw [dvd_iff_mod_eq_zero, ← ne.def, ← pos_iff_ne_zero] at h,
+    simp only [← mod_add_div m n] {single_pass := tt},
+    refine ⟨m / n, lt_add_of_pos_left _ h, _⟩,
+    rw [add_comm _ 1, left_distrib, mul_one], exact add_lt_add_right (mod_lt _ hn) _ }
+end
+
 /-! ### `find` -/
 section find
 

src/data/nat/bitwise.lean

@@ -35,6 +35,9 @@ namespace nat
 @[simp] lemma bit_ff : bit ff = bit0 := rfl
 @[simp] lemma bit_tt : bit tt = bit1 := rfl
 
+@[simp] lemma bit_eq_zero {n : ℕ} {b : bool} : n.bit b = 0 ↔ n = 0 ∧ b = ff :=
+by { cases b; norm_num [bit0_eq_zero, nat.bit1_ne_zero] }
+
 lemma zero_of_test_bit_eq_ff {n : ℕ} (h : ∀ i, test_bit n i = ff) : n = 0 :=
 begin
   induction n using nat.binary_rec with b n hn,

src/data/nat/enat.lean

@@ -109,6 +109,9 @@ roption.ext' (iff_of_true trivial h) (λ _ _, rfl)
 lemma dom_of_le_some {x : enat} {y : ℕ} : x ≤ y → x.dom :=
 λ ⟨h, _⟩, h trivial
 
+/-- The coercion `ℕ → enat` preserves `0` and addition. -/
+def coe_hom : ℕ →+ enat := ⟨coe, enat.coe_zero, enat.coe_add⟩
+
 instance : partial_order enat :=
 { le          := (≤),
   le_refl     := λ x, ⟨id, λ _, le_refl _⟩,
@@ -127,6 +130,9 @@ lemma get_le_get {x y : enat} {hx : x.dom} {hy : y.dom} :
   x.get hx ≤ y.get hy ↔ x ≤ y :=
 by conv { to_lhs, rw [← coe_le_coe, coe_get, coe_get]}
 
+protected lemma zero_lt_one : (0 : enat) < 1 :=
+by { norm_cast, norm_num }
+
 instance semilattice_sup_bot : semilattice_sup_bot enat :=
 { sup := (⊔),
   bot := (⊥),