Apply suggestions from code review

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Init/Data/Char.lean

@@ -5,3 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Char.Basic
+import Init.Data.Char.Lemmas

src/Init/Data/Char/Lemmas.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Char.Basic
+import Init.Data.UInt.Lemmas
+
+namespace Char
+
+theorem le_def {a b : Char} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
+theorem lt_def {a b : Char} : a < b ↔ a.1 < b.1 := .rfl
+theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
+@[simp] protected theorem not_le {a b : Char} : ¬ a ≤ b ↔ b < a := UInt32.not_le
+@[simp] protected theorem not_lt {a b : Char} : ¬ a < b ↔ b ≤ a := UInt32.not_lt
+@[simp] protected theorem le_refl (a : Char) : a ≤ a := by simp [le_def]
+@[simp] protected theorem lt_irrefl (a : Char) : ¬ a < a := by simp
+protected theorem le_trans {a b c : Char} : a ≤ b → b ≤ c → a ≤ c := UInt32.le_trans
+protected theorem lt_trans {a b c : Char} : a < b → b < c → a < c := UInt32.lt_trans
+protected theorem le_total (a b : Char) : a ≤ b ∨ b ≤ a := UInt32.le_total a.1 b.1
+protected theorem lt_asymm {a b : Char} (h : a < b) : ¬ b < a := UInt32.lt_asymm h
+protected theorem ne_of_lt {a b : Char} (h : a < b) : a ≠ b := Char.ne_of_val_ne (UInt32.ne_of_lt h)
+
+end Char

src/Init/Data/Fin/Lemmas.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
+Authors: Mario Carneiro, Leonardo de Moura
 -/
 prelude
 import Init.Data.Fin.Basic
@@ -94,6 +94,18 @@ theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ a.val < b.val := Iff.rfl
 
 @[simp] protected theorem not_lt {a b : Fin n} : ¬ a < b ↔ b ≤ a := Nat.not_lt
 
+@[simp] protected theorem le_refl (a : Fin n) : a ≤ a := by simp [le_def]
+
+@[simp] protected theorem lt_irrefl (a : Fin n) : ¬ a < a := by simp
+
+protected theorem le_trans {a b c : Fin n} : a ≤ b → b ≤ c → a ≤ c := Nat.le_trans
+
+protected theorem lt_trans {a b c : Fin n} : a < b → b < c → a < c := Nat.lt_trans
+
+protected theorem le_total (a b : Fin n) : a ≤ b ∨ b ≤ a := Nat.le_total a b
+
+protected theorem lt_asymm {a b : Fin n} (h : a < b) : ¬ b < a := Nat.lt_asymm h
+
 protected theorem ne_of_lt {a b : Fin n} (h : a < b) : a ≠ b := Fin.ne_of_val_ne (Nat.ne_of_lt h)
 
 protected theorem ne_of_gt {a b : Fin n} (h : a < b) : b ≠ a := Fin.ne_of_val_ne (Nat.ne_of_gt h)
@@ -823,27 +835,3 @@ protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
   simp [ext_iff, mul_def]
 
 end Fin
-
-namespace USize
-
-@[simp] theorem lt_def {a b : USize} : a < b ↔ a.toNat < b.toNat := .rfl
-
-@[simp] theorem le_def {a b : USize} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
-
-@[simp] theorem zero_toNat : (0 : USize).toNat = 0 := Nat.zero_mod _
-
-@[simp] theorem mod_toNat (a b : USize) : (a % b).toNat = a.toNat % b.toNat :=
-  Fin.mod_val ..
-
-@[simp] theorem div_toNat (a b : USize) : (a / b).toNat = a.toNat / b.toNat :=
-  Fin.div_val ..
-
-@[simp] theorem modn_toNat (a : USize) (b : Nat) : (a.modn b).toNat = a.toNat % b :=
-  Fin.modn_val ..
-
-theorem mod_lt (a b : USize) (h : 0 < b) : a % b < b := USize.modn_lt _ (by simp at h; exact h)
-
-theorem toNat.inj : ∀ {a b : USize}, a.toNat = b.toNat → a = b
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-
-end USize

src/Init/Data/Int/Order.lean

@@ -96,7 +96,7 @@ protected theorem le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a
   have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm
   rw [← hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]
 
-protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
+@[simp] protected theorem lt_irrefl (a : Int) : ¬a < a := fun H =>
   let ⟨n, hn⟩ := lt.dest H
   have : (a+Nat.succ n) = a+0 := by
     rw [hn, Int.add_zero]

src/Init/Data/String.lean

@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.String.Basic
 import Init.Data.String.Extra
+import Init.Data.String.Lemmas

src/Init/Data/String/Lemmas.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Char.Lemmas
+
+namespace String
+
+protected theorem data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data :=
+  h ▸ rfl
+protected theorem ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b :=
+  fun h' => absurd (String.data_eq_of_eq h') h
+@[simp] protected theorem lt_irrefl (s : String) : ¬ s < s :=
+  List.lt_irrefl' Char.lt_irrefl s.data
+protected theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b := by
+  have := String.lt_irrefl a
+  intro h; subst h; contradiction
+
+end String

src/Init/Data/UInt.lean

@@ -6,3 +6,4 @@ Authors: Henrik Böving
 prelude
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
+import Init.Data.UInt.Lemmas

src/Init/Data/UInt/Basic.lean

@@ -364,6 +364,3 @@ instance (a b : USize) : Decidable (a < b) := USize.decLt a b
 instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe
-
-theorem USize.modn_lt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u % m) < m
-  | ⟨u⟩, h => Fin.modn_lt u h

src/Init/Data/UInt/Lemmas.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.UInt.Basic
+import Init.Data.Fin.Lemmas
+
+set_option hygiene false in
+macro "declare_uint_theorems" typeName:ident : command =>
+`(
+namespace $typeName
+
+instance : Inhabited $typeName where
+  default := 0
+
+theorem zero_def : (0 : $typeName) = ⟨0⟩ := rfl
+theorem one_def : (1 : $typeName) = ⟨1⟩ := rfl
+theorem sub_def (a b : $typeName) : a - b = ⟨a.val - b.val⟩ := rfl
+theorem mul_def (a b : $typeName) : a * b = ⟨a.val * b.val⟩ := rfl
+theorem mod_def (a b : $typeName) : a % b = ⟨a.val % b.val⟩ := rfl
+theorem add_def (a b : $typeName) : a + b = ⟨a.val + b.val⟩ := rfl
+
+@[simp] theorem mk_val_eq : ∀ (a : $typeName), mk a.val = a
+  | ⟨_, _⟩ => rfl
+theorem val_eq_of_lt {a : Nat} : a < size → ((ofNat a).val : Nat) = a :=
+  Nat.mod_eq_of_lt
+
+theorem le_def {a b : $typeName} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
+theorem lt_def {a b : $typeName} : a < b ↔ a.1 < b.1 := .rfl
+theorem lt_iff_val_lt_val {a b : $typeName} : a < b ↔ a.val < b.val := .rfl
+@[simp] protected theorem not_le {a b : $typeName} : ¬ a ≤ b ↔ b < a := Fin.not_le
+@[simp] protected theorem not_lt {a b : $typeName} : ¬ a < b ↔ b ≤ a := Fin.not_lt
+@[simp] protected theorem le_refl (a : $typeName) : a ≤ a := by simp [le_def]
+@[simp] protected theorem lt_irrefl (a : $typeName) : ¬ a < a := by simp
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := Fin.le_trans
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := Fin.lt_trans
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := Fin.le_total a.1 b.1
+protected theorem lt_asymm {a b : $typeName} (h : a < b) : ¬ b < a := Fin.lt_asymm h
+protected theorem val_eq_of_eq {a b : $typeName} (h : a = b) : a.val = b.val := h ▸ rfl
+protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by cases a; cases b; simp at h; simp [h]
+open $typeName (val_eq_of_eq) in
+protected theorem ne_of_val_ne {a b : $typeName} (h : a.val ≠ b.val) : a ≠ b := fun h' => absurd (val_eq_of_eq h') h
+open $typeName (ne_of_val_ne) in
+protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := ne_of_val_ne (Fin.ne_of_lt h)
+
+@[simp] protected theorem zero_toNat : (0 : $typeName).toNat = 0 := Nat.zero_mod _
+@[simp] protected theorem mod_toNat (a b : $typeName) : (a % b).toNat = a.toNat % b.toNat := Fin.mod_val ..
+@[simp] protected theorem div_toNat (a b : $typeName) : (a / b).toNat = a.toNat / b.toNat := Fin.div_val ..
+@[simp] protected theorem modn_toNat (a : $typeName) (b : Nat) : (a.modn b).toNat = a.toNat % b := Fin.modn_val ..
+protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m
+  | ⟨u⟩, h => Fin.modn_lt u h
+open $typeName (modn_lt) in
+protected theorem mod_lt (a b : $typeName) (h : 0 < b) : a % b < b := modn_lt _ (by simp [lt_def] at h; exact h)
+protected theorem toNat.inj : ∀ {a b : $typeName}, a.toNat = b.toNat → a = b
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+end $typeName
+)
+
+declare_uint_theorems UInt8
+declare_uint_theorems UInt16
+declare_uint_theorems UInt32
+declare_uint_theorems UInt64
+declare_uint_theorems USize