From 27a4f60b7089c6949d1674aa310debb551efc755 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 11 Oct 2024 12:07:34 +0200
Subject: [PATCH] address review

---
 src/Init/Data/BitVec/Basic.lean    |  8 ++++----
 src/Init/Data/BitVec/BasicAux.lean |  5 +++++
 src/Init/Data/UInt/BasicAux.lean   |  7 +++++++
 src/Init/Data/UInt/Lemmas.lean     | 16 ++++------------
 4 files changed, 20 insertions(+), 16 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 915f2876ee1d..3d4b311d1218 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -11,10 +11,10 @@ import Init.Data.Int.Bitwise
 import Init.Data.BitVec.BasicAux
 
 /-!
-We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
-(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
-with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
-representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
+others for its relative efficiency (Lean has special support for `Nat`),  and the fact that bitwise
+operations on `Fin` are already defined. Some other possible representations are `List Bool`,
+`{ l : List Bool // l.length = w }`, `Fin w → Bool`.
 
 We define many of the bitvector operations from the
 [`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean
index c2ac3097a77f..6e6eccc157cf 100644
--- a/src/Init/Data/BitVec/BasicAux.lean
+++ b/src/Init/Data/BitVec/BasicAux.lean
@@ -8,6 +8,11 @@ import Init.Data.Fin.Basic
 
 set_option linter.missingDocs true
 
+/-!
+This module exists to provide the very basic `BitVec` definitions required for
+`Init.Data.UInt.BasicAux`.
+-/
+
 namespace BitVec
 
 section Nat
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index f181e2645154..b751f6f3d932 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -7,6 +7,13 @@ prelude
 import Init.Data.Fin.Basic
 import Init.Data.BitVec.BasicAux
 
+/-!
+This module exists to provide the very basic `UInt8` etc. definitions required for
+`Init.Data.Char.Basic` and `Init.Data.Array.Basic`. These are very important as they are used in
+meta code that is then (transitively) used in `Init.Data.UInt.Basic` and `Init.Data.BitVec.Basic`.
+This file thus breaks the import cycle that would be created by this dependency.
+-/
+
 open Nat
 
 def UInt8.val (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index b1f5da4c1609..ff376e15ccc0 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -45,21 +45,13 @@ theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
 
 @[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 := by
-  simp only [le_def, lt_def]
-  apply BitVec.le_trans
+protected theorem le_trans {a b c : $typeName} : a ≤ b → b ≤ c → a ≤ c := BitVec.le_trans
 
-protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := by
-  simp only [le_def, lt_def]
-  apply BitVec.lt_trans
+protected theorem lt_trans {a b c : $typeName} : a < b → b < c → a < c := BitVec.lt_trans
 
-protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := by
-  simp only [le_def, lt_def]
-  apply BitVec.le_total
+protected theorem le_total (a b : $typeName) : a ≤ b ∨ b ≤ a := BitVec.le_total ..
 
-protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := by
-  simp only [le_def, lt_def]
-  apply BitVec.lt_asymm
+protected theorem lt_asymm {a b : $typeName} : a < b → ¬ b < a := BitVec.lt_asymm
 
 protected theorem toBitVec_eq_of_eq {a b : $typeName} (h : a = b) : a.toBitVec = b.toBitVec := h ▸ rfl