feat(data/nat/basic): simp lemmas about inequalities with bit* (#2207)

* feat(data/nat/basic): `simp` lemmas about inequalities with `bit*`

* Fix compile of `computability/partrec_code`

* Fix `nat.bit_cases` to work for `Type*` too

* Generalize some lemmas to `linear_ordered_semiring`s

* Apply suggestions from code review

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

* Apply suggestions from code review

Co-Authored-By: Scott Morrison <scott@tqft.net>

* fixing a proof

Co-authored-by: Gabriel Ebner <gebner@gebner.org>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 4 people

src/algebra/ordered_ring.lean

@@ -37,6 +37,42 @@ by { rw [← zero_add (0:α), bit0], exact add_lt_add zero_lt_one zero_lt_one }
 ⟨lt_imp_lt_of_le_imp_le $ λ h', mul_le_mul_of_nonneg_right h' (le_of_lt h),
  λ h', mul_lt_mul_of_pos_right h' h⟩
 
+@[simp] lemma zero_le_mul_left {b c : α} (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b :=
+by { convert mul_le_mul_left h, simp }
+
+@[simp] lemma zero_le_mul_right {b c : α} (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b :=
+by { convert mul_le_mul_right h, simp }
+
+@[simp] lemma zero_lt_mul_left {b c : α} (h : 0 < c) : 0 < c * b ↔ 0 < b :=
+by { convert mul_lt_mul_left h, simp }
+
+@[simp] lemma zero_lt_mul_right {b c : α} (h : 0 < c) : 0 < b * c ↔ 0 < b :=
+by { convert mul_lt_mul_right h, simp }
+
+@[simp] lemma bit0_le_bit0 {a b : α} : bit0 a ≤ bit0 b ↔ a ≤ b :=
+by rw [bit0, bit0, ← two_mul, ← two_mul, mul_le_mul_left zero_lt_two]
+
+@[simp] lemma bit0_lt_bit0 {a b : α} : bit0 a < bit0 b ↔ a < b :=
+by rw [bit0, bit0, ← two_mul, ← two_mul, mul_lt_mul_left zero_lt_two]
+
+@[simp] lemma bit1_le_bit1 {a b : α} : bit1 a ≤ bit1 b ↔ a ≤ b :=
+(add_le_add_iff_right 1).trans bit0_le_bit0
+
+@[simp] lemma bit1_lt_bit1 {a b : α} : bit1 a < bit1 b ↔ a < b :=
+(add_lt_add_iff_right 1).trans bit0_lt_bit0
+
+@[simp] lemma one_le_bit1 {a : α} : (1 : α) ≤ bit1 a ↔ 0 ≤ a :=
+by rw [bit1, le_add_iff_nonneg_left, bit0, ← two_mul, zero_le_mul_left zero_lt_two]
+
+@[simp] lemma one_lt_bit1 {a : α} : (1 : α) < bit1 a ↔ 0 < a :=
+by rw [bit1, lt_add_iff_pos_left, bit0, ← two_mul, zero_lt_mul_left zero_lt_two]
+
+@[simp] lemma zero_le_bit0 {a : α} : (0 : α) ≤ bit0 a ↔ 0 ≤ a :=
+by rw [bit0, ← two_mul, zero_le_mul_left zero_lt_two]
+
+@[simp] lemma zero_lt_bit0 {a : α} : (0 : α) < bit0 a ↔ 0 < a :=
+by rw [bit0, ← two_mul, zero_lt_mul_left zero_lt_two]
+
 lemma mul_lt_mul'' {a b c d : α} (h1 : a < c) (h2 : b < d) (h3 : 0 ≤ a) (h4 : 0 ≤ b) :
        a * b < c * d :=
 (lt_or_eq_of_le h4).elim

src/computability/partrec_code.lean

@@ -136,8 +136,7 @@ theorem encode_lt_comp (cf cg) :
 begin
   suffices, exact (encode_lt_pair cf cg).imp
     (λ h, lt_trans h this) (λ h, lt_trans h this),
-  change _, simp [encode_code_eq, encode_code, -add_comm],
-  exact nat.bit0_lt (nat.lt_succ_self _),
+  change _, simp [encode_code_eq, encode_code]
 end
 
 theorem encode_lt_prec (cf cg) :
@@ -146,8 +145,7 @@ theorem encode_lt_prec (cf cg) :
 begin
   suffices, exact (encode_lt_pair cf cg).imp
     (λ h, lt_trans h this) (λ h, lt_trans h this),
-  change _, simp [encode_code_eq, encode_code, -add_comm],
-  exact nat.lt_succ_self _,
+  change _, simp [encode_code_eq, encode_code],
 end
 
 theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf) :=

src/data/nat/basic.lean

@@ -714,9 +714,46 @@ theorem bit_lt_bit0 : ∀ (b) {n m : ℕ}, n < m → bit b n < bit0 m
 theorem bit_lt_bit (a b) {n m : ℕ} (h : n < m) : bit a n < bit b m :=
 lt_of_lt_of_le (bit_lt_bit0 _ h) (bit0_le_bit _ (le_refl _))
 
+@[simp] lemma bit0_le_bit1_iff : bit0 k ≤ bit1 n ↔ k ≤ n :=
+⟨λ h, by rwa [← nat.lt_succ_iff, n.bit1_eq_succ_bit0, ← n.bit0_succ_eq,
+  bit0_lt_bit0, nat.lt_succ_iff] at h, λ h, le_of_lt (nat.bit0_lt_bit1 h)⟩
+
+@[simp] lemma bit0_lt_bit1_iff : bit0 k < bit1 n ↔ k ≤ n :=
+⟨λ h, bit0_le_bit1_iff.1 (le_of_lt h), nat.bit0_lt_bit1⟩
+
+@[simp] lemma bit1_le_bit0_iff : bit1 k ≤ bit0 n ↔ k < n :=
+⟨λ h, by rwa [k.bit1_eq_succ_bit0, succ_le_iff, bit0_lt_bit0] at h,
+  λ h, le_of_lt (nat.bit1_lt_bit0 h)⟩
+
+@[simp] lemma bit1_lt_bit0_iff : bit1 k < bit0 n ↔ k < n :=
+⟨λ h, bit1_le_bit0_iff.1 (le_of_lt h), nat.bit1_lt_bit0⟩
+
+@[simp] lemma one_le_bit0_iff : 1 ≤ bit0 n ↔ 0 < n :=
+by { convert bit1_le_bit0_iff, refl, }
+
+@[simp] lemma one_lt_bit0_iff : 1 < bit0 n ↔ 1 ≤ n :=
+by { convert bit1_lt_bit0_iff, refl, }
+
+@[simp] lemma bit_le_bit_iff : ∀ {b : bool}, bit b k ≤ bit b n ↔ k ≤ n
+| ff := bit0_le_bit0
+| tt := bit1_le_bit1
+
+@[simp] lemma bit_lt_bit_iff : ∀ {b : bool}, bit b k < bit b n ↔ k < n
+| ff := bit0_lt_bit0
+| tt := bit1_lt_bit1
+
+@[simp] lemma bit_le_bit1_iff : ∀ {b : bool}, bit b k ≤ bit1 n ↔ k ≤ n
+| ff := bit0_le_bit1_iff
+| tt := bit1_le_bit1
+
 lemma pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) : 0 < n :=
 by { cases n, cases h, apply succ_pos, }
 
+/-- Define a function on `ℕ` depending on parity of the argument. -/
+@[elab_as_eliminator]
+def bit_cases {C : ℕ → Sort u} (H : Π b n, C (bit b n)) (n : ℕ) : C n :=
+eq.rec_on n.bit_decomp (H (bodd n) (div2 n))
+
 /- partial subtraction -/
 
 /-- Partial predecessor operation. Returns `ppred n = some m`

src/data/real/pi.lean

@@ -91,7 +91,7 @@ end
         mul_div_cancel_left],
     norm_num, norm_num, norm_num,
     apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
-    apply le_of_lt, apply mul_pos, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
+    apply le_of_lt, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
     { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
       apply div_pos pi_pos, apply pow_pos, norm_num },
     apply div_lt_div' (le_refl pi) _ pi_pos _,