From 23bec25fce432258c1646d6d8dd7574a0609060c Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 26 Nov 2024 18:42:23 -0500 Subject: [PATCH] feat: `Nat.lt_pow_self` (#6200) This PR upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib and uses them to prove the simp theorem `Nat.mod_two_pow`. This simplifies expressions like `System.Platform.numBits % 2 ^ System.Platform.numBits = System.Platform.numBits`, which is needed for #6188. --- src/Init/Data/Nat/Lemmas.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index b956ca8712..4b9bad521f 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -846,6 +846,18 @@ protected theorem pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) : rw [←Nat.pow_add_one, Nat.pow_le_pow_iff_right (by omega), Nat.pow_lt_pow_iff_right (by omega)] omega +protected theorem lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n := by + induction n with + | zero => exact Nat.zero_lt_one + | succ _ ih => exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h) + +protected theorem lt_two_pow_self : n < 2 ^ n := + Nat.lt_pow_self Nat.one_lt_two + +@[simp] +protected theorem mod_two_pow_self : n % 2 ^ n = n := + Nat.mod_eq_of_lt Nat.lt_two_pow_self + @[simp] theorem two_pow_pred_mul_two (h : 0 < w) : 2 ^ (w - 1) * 2 = 2 ^ w := by