feat(Data/Nat/Digits): digits_head and ofDigits_mod_eq_head (#11129)

Co-authored-by: Moritz Firsching <[email protected]>
leanprover-community · May 16, 2024 · 3d67461 · 3d67461
1 parent 1121911
commit 3d67461
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 3 deletions.
diff --git a/Mathlib/Algebra/BigOperators/List/Basic.lean b/Mathlib/Algebra/BigOperators/List/Basic.lean
@@ -574,7 +574,7 @@ If desired, we could add a class stating that `default = 0`.
 
 /-- This relies on `default ℕ = 0`. -/
 theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by
-  cases L <;> simp; rfl
+  cases L <;> simp
 #align list.head_add_tail_sum List.headI_add_tail_sum
 
 /-- This relies on `default ℕ = 0`. -/

diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean
@@ -1182,7 +1182,6 @@ def trNat (n : ℕ) : List Γ' :=
 theorem trNat_zero : trNat 0 = [] := by rw [trNat, Nat.cast_zero]; rfl
 #align turing.partrec_to_TM2.tr_nat_zero Turing.PartrecToTM2.trNat_zero
 
-@[simp]
 theorem trNat_default : trNat default = [] :=
   trNat_zero
 #align turing.partrec_to_TM2.tr_nat_default Turing.PartrecToTM2.trNat_default
@@ -1550,7 +1549,6 @@ theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s',
   rcases v with (_ | ⟨_ | n, v⟩)
   · refine' ⟨none, TransGen.single _⟩
     simp
-    rfl
   · refine' ⟨some Γ'.cons, TransGen.single _⟩
     simp
   refine' ⟨none, _⟩

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -764,6 +764,9 @@ theorem getLast?_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?)
 
 /-! ### head(!?) and tail -/
 
+@[simp]
+theorem head!_nil [Inhabited α] : ([] : List α).head! = default := rfl
+
 @[simp] theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by
   cases x <;> simp at h ⊢
 

diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean
@@ -66,6 +66,8 @@ variable {a b c d m n k : ℕ} {p q : ℕ → Prop}
 
 instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩
 
+@[simp] theorem default_eq_zero : default = 0 := rfl
+
 attribute [gcongr] Nat.succ_le_succ
 attribute [simp] Nat.not_lt_zero Nat.succ_ne_zero Nat.succ_ne_self Nat.zero_ne_one Nat.one_ne_zero
   Nat.min_eq_left Nat.min_eq_right Nat.max_eq_left Nat.max_eq_right

diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
@@ -192,6 +192,9 @@ theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) :
       Or.inl hl
 #align nat.of_digits_eq_sum_map_with_index Nat.ofDigits_eq_sum_mapIdx
 
+@[simp]
+theorem ofDigits_nil {b : ℕ} : ofDigits b [] = 0 := rfl
+
 @[simp]
 theorem ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n := by simp [ofDigits]
 #align nat.of_digits_singleton Nat.ofDigits_singleton
@@ -660,6 +663,19 @@ theorem ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b
   ofDigits_modEq b k L
 #align nat.of_digits_mod Nat.ofDigits_mod
 
+theorem ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b := by
+  induction l <;> simp [Nat.ofDigits, Int.ModEq]
+
+theorem head!_digits {b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b := by
+  by_cases hb : 1 < b
+  · rcases n with _ | n
+    · simp
+    · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]
+      rw [Nat.ofDigits_mod_eq_head! _ _]
+      exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
+          Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm
+  · rcases n with _ | _ <;> simp_all [show b = 0 by omega]
+
 theorem ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) :
     ofDigits b L ≡ ofDigits b' L [ZMOD k] := by
   induction' L with d L ih