From d784c51eb3ea86c7aa9c19e53a96e2ea85ddeb5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Thu, 20 Jun 2024 00:20:44 -0400 Subject: [PATCH 1/6] feat: order lemmas for `UIntX` types --- Batteries/Data/UInt.lean | 155 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 155 insertions(+) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index a7c2a4cbaa..64b2aa2fc7 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -42,6 +42,37 @@ theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm +theorem UInt8.le_iff_toNat_le_toNat {x y : UInt8} : x ≤ y ↔ x.toNat ≤ y.toNat := .rfl + +theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} : x < y ↔ x.toNat < y.toNat := .rfl + +theorem UInt8.compare_eq_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + +theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl + +theorem UInt8.min_def (x y : UInt8) : min x y = if x ≤ y then x else y := rfl + +theorem UInt8.max_toNat (x y : UInt8) : (max x y).toNat = max x.toNat y.toNat := by + rw [max_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_right h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_left (Nat.le_of_not_ge h)] + +theorem UInt8.min_toNat (x y : UInt8) : (min x y).toNat = min x.toNat y.toNat := by + rw [min_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_left h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_right (Nat.le_of_not_ge h)] + /-! ### UInt16 -/ @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y @@ -79,6 +110,37 @@ theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm +theorem UInt16.le_iff_toNat_le_toNat {x y : UInt16} : x ≤ y ↔ x.toNat ≤ y.toNat := .rfl + +theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} : x < y ↔ x.toNat < y.toNat := .rfl + +theorem UInt16.compare_eq_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + +theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rfl + +theorem UInt16.min_def (x y : UInt16) : min x y = if x ≤ y then x else y := rfl + +theorem UInt16.max_toNat (x y : UInt16) : (max x y).toNat = max x.toNat y.toNat := by + rw [max_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_right h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_left (Nat.le_of_not_ge h)] + +theorem UInt16.min_toNat (x y : UInt16) : (min x y).toNat = min x.toNat y.toNat := by + rw [min_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_left h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_right (Nat.le_of_not_ge h)] + /-! ### UInt32 -/ @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y @@ -116,6 +178,37 @@ theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm +theorem UInt32.le_iff_toNat_le_toNat {x y : UInt32} : x ≤ y ↔ x.toNat ≤ y.toNat := .rfl + +theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} : x < y ↔ x.toNat < y.toNat := .rfl + +theorem UInt32.compare_eq_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + +theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rfl + +theorem UInt32.min_def (x y : UInt32) : min x y = if x ≤ y then x else y := rfl + +theorem UInt32.max_toNat (x y : UInt32) : (max x y).toNat = max x.toNat y.toNat := by + rw [max_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_right h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_left (Nat.le_of_not_ge h)] + +theorem UInt32.min_toNat (x y : UInt32) : (min x y).toNat = min x.toNat y.toNat := by + rw [min_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_left h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_right (Nat.le_of_not_ge h)] + /-! ### UInt64 -/ @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y @@ -153,6 +246,37 @@ theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm +theorem UInt64.le_iff_toNat_le_toNat {x y : UInt64} : x ≤ y ↔ x.toNat ≤ y.toNat := .rfl + +theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} : x < y ↔ x.toNat < y.toNat := .rfl + +theorem UInt64.compare_eq_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + +theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rfl + +theorem UInt64.min_def (x y : UInt64) : min x y = if x ≤ y then x else y := rfl + +theorem UInt64.max_toNat (x y : UInt64) : (max x y).toNat = max x.toNat y.toNat := by + rw [max_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_right h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_left (Nat.le_of_not_ge h)] + +theorem UInt64.min_toNat (x y : UInt64) : (min x y).toNat = min x.toNat y.toNat := by + rw [min_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_left h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_right (Nat.le_of_not_ge h)] + /-! ### USize -/ @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y @@ -203,3 +327,34 @@ theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := instance : Batteries.LawfulOrd USize := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm + +theorem USize.le_iff_toNat_le_toNat {x y : USize} : x ≤ y ↔ x.toNat ≤ y.toNat := .rfl + +theorem USize.lt_iff_toNat_lt_toNat {x y : USize} : x < y ↔ x.toNat < y.toNat := .rfl + +theorem USize.compare_eq_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + +theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl + +theorem USize.min_def (x y : USize) : min x y = if x ≤ y then x else y := rfl + +theorem USize.max_toNat (x y : USize) : (max x y).toNat = max x.toNat y.toNat := by + rw [max_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_right h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.max_eq_left (Nat.le_of_not_ge h)] + +theorem USize.min_toNat (x y : USize) : (min x y).toNat = min x.toNat y.toNat := by + rw [min_def] + split + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_left h] + · next h => + rw [le_iff_toNat_le_toNat] at h + rw [Nat.min_eq_right (Nat.le_of_not_ge h)] From d5f198d4a902046574ed05a4b32e869db85d1673 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Thu, 20 Jun 2024 01:29:55 -0400 Subject: [PATCH 2/6] fix: naming convention --- Batteries/Data/UInt.lean | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index 64b2aa2fc7..32a240e915 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -53,7 +53,7 @@ theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl theorem UInt8.min_def (x y : UInt8) : min x y = if x ≤ y then x else y := rfl -theorem UInt8.max_toNat (x y : UInt8) : (max x y).toNat = max x.toNat y.toNat := by +theorem UInt8.toNat_max (x y : UInt8) : (max x y).toNat = max x.toNat y.toNat := by rw [max_def] split · next h => @@ -63,7 +63,7 @@ theorem UInt8.max_toNat (x y : UInt8) : (max x y).toNat = max x.toNat y.toNat := rw [le_iff_toNat_le_toNat] at h rw [Nat.max_eq_left (Nat.le_of_not_ge h)] -theorem UInt8.min_toNat (x y : UInt8) : (min x y).toNat = min x.toNat y.toNat := by +theorem UInt8.toNat_min (x y : UInt8) : (min x y).toNat = min x.toNat y.toNat := by rw [min_def] split · next h => @@ -121,7 +121,7 @@ theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rf theorem UInt16.min_def (x y : UInt16) : min x y = if x ≤ y then x else y := rfl -theorem UInt16.max_toNat (x y : UInt16) : (max x y).toNat = max x.toNat y.toNat := by +theorem UInt16.toNat_max (x y : UInt16) : (max x y).toNat = max x.toNat y.toNat := by rw [max_def] split · next h => @@ -131,7 +131,7 @@ theorem UInt16.max_toNat (x y : UInt16) : (max x y).toNat = max x.toNat y.toNat rw [le_iff_toNat_le_toNat] at h rw [Nat.max_eq_left (Nat.le_of_not_ge h)] -theorem UInt16.min_toNat (x y : UInt16) : (min x y).toNat = min x.toNat y.toNat := by +theorem UInt16.toNat_min (x y : UInt16) : (min x y).toNat = min x.toNat y.toNat := by rw [min_def] split · next h => @@ -189,7 +189,7 @@ theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rf theorem UInt32.min_def (x y : UInt32) : min x y = if x ≤ y then x else y := rfl -theorem UInt32.max_toNat (x y : UInt32) : (max x y).toNat = max x.toNat y.toNat := by +theorem UInt32.toNat_max (x y : UInt32) : (max x y).toNat = max x.toNat y.toNat := by rw [max_def] split · next h => @@ -199,7 +199,7 @@ theorem UInt32.max_toNat (x y : UInt32) : (max x y).toNat = max x.toNat y.toNat rw [le_iff_toNat_le_toNat] at h rw [Nat.max_eq_left (Nat.le_of_not_ge h)] -theorem UInt32.min_toNat (x y : UInt32) : (min x y).toNat = min x.toNat y.toNat := by +theorem UInt32.toNat_min (x y : UInt32) : (min x y).toNat = min x.toNat y.toNat := by rw [min_def] split · next h => @@ -257,7 +257,7 @@ theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rf theorem UInt64.min_def (x y : UInt64) : min x y = if x ≤ y then x else y := rfl -theorem UInt64.max_toNat (x y : UInt64) : (max x y).toNat = max x.toNat y.toNat := by +theorem UInt64.toNat_max (x y : UInt64) : (max x y).toNat = max x.toNat y.toNat := by rw [max_def] split · next h => @@ -267,7 +267,7 @@ theorem UInt64.max_toNat (x y : UInt64) : (max x y).toNat = max x.toNat y.toNat rw [le_iff_toNat_le_toNat] at h rw [Nat.max_eq_left (Nat.le_of_not_ge h)] -theorem UInt64.min_toNat (x y : UInt64) : (min x y).toNat = min x.toNat y.toNat := by +theorem UInt64.toNat_min (x y : UInt64) : (min x y).toNat = min x.toNat y.toNat := by rw [min_def] split · next h => @@ -339,7 +339,7 @@ theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl theorem USize.min_def (x y : USize) : min x y = if x ≤ y then x else y := rfl -theorem USize.max_toNat (x y : USize) : (max x y).toNat = max x.toNat y.toNat := by +theorem USize.toNat_max (x y : USize) : (max x y).toNat = max x.toNat y.toNat := by rw [max_def] split · next h => @@ -349,7 +349,7 @@ theorem USize.max_toNat (x y : USize) : (max x y).toNat = max x.toNat y.toNat := rw [le_iff_toNat_le_toNat] at h rw [Nat.max_eq_left (Nat.le_of_not_ge h)] -theorem USize.min_toNat (x y : USize) : (min x y).toNat = min x.toNat y.toNat := by +theorem USize.toNat_min (x y : USize) : (min x y).toNat = min x.toNat y.toNat := by rw [min_def] split · next h => From fd4c2cb4d2a3b25cb8b6e8eb053b7c8832bbc0ec Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 20 Jun 2024 07:29:57 -0400 Subject: [PATCH 3/6] feat: add `last` --- Batteries/Data/UInt.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index 32a240e915..d0c22c0736 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -304,8 +304,7 @@ theorem USize.size_le : USize.size ≤ 2 ^ 64 := by apply Nat.pow_le_pow_of_le_right (by decide) cases System.Platform.numBits_eq <;> simp_arith [*] -theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by - rw [←USize.size_eq]; exact x.val.isLt +theorem USize.toNat_lt (x : USize) : x.toNat < USize.size := x.val.isLt @[simp] theorem USize.toUInt64_toNat (x : USize) : x.toUInt64.toNat = x.toNat := by simp only [USize.toUInt64, UInt64.toNat]; rfl From fc8d7fbb3abd738f293df4592dec03a450909501 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 20 Jun 2024 09:49:01 -0400 Subject: [PATCH 4/6] fix: naming convention --- Batteries/Data/UInt.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index d0c22c0736..2bed854a98 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -46,7 +46,7 @@ theorem UInt8.le_iff_toNat_le_toNat {x y : UInt8} : x ≤ y ↔ x.toNat ≤ y.to theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt8.compare_eq_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by +theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl @@ -114,7 +114,7 @@ theorem UInt16.le_iff_toNat_le_toNat {x y : UInt16} : x ≤ y ↔ x.toNat ≤ y. theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt16.compare_eq_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by +theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rfl @@ -182,7 +182,7 @@ theorem UInt32.le_iff_toNat_le_toNat {x y : UInt32} : x ≤ y ↔ x.toNat ≤ y. theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt32.compare_eq_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by +theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rfl @@ -250,7 +250,7 @@ theorem UInt64.le_iff_toNat_le_toNat {x y : UInt64} : x ≤ y ↔ x.toNat ≤ y. theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt64.compare_eq_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by +theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rfl @@ -331,7 +331,7 @@ theorem USize.le_iff_toNat_le_toNat {x y : USize} : x ≤ y ↔ x.toNat ≤ y.to theorem USize.lt_iff_toNat_lt_toNat {x y : USize} : x < y ↔ x.toNat < y.toNat := .rfl -theorem USize.compare_eq_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by +theorem USize.compare_eq_toNat_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl From 182c8bafb987e53de3298f61dd2bb4d8c6b2b3a7 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 20 Jun 2024 09:53:18 -0400 Subject: [PATCH 5/6] fix: long lines --- Batteries/Data/UInt.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index 2bed854a98..b95b077b8f 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -46,7 +46,8 @@ theorem UInt8.le_iff_toNat_le_toNat {x y : UInt8} : x ≤ y ↔ x.toNat ≤ y.to theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by +theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) : + compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl @@ -114,7 +115,8 @@ theorem UInt16.le_iff_toNat_le_toNat {x y : UInt16} : x ≤ y ↔ x.toNat ≤ y. theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by +theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) : + compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rfl @@ -182,7 +184,8 @@ theorem UInt32.le_iff_toNat_le_toNat {x y : UInt32} : x ≤ y ↔ x.toNat ≤ y. theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by +theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) : + compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rfl @@ -250,7 +253,8 @@ theorem UInt64.le_iff_toNat_le_toNat {x y : UInt64} : x ≤ y ↔ x.toNat ≤ y. theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} : x < y ↔ x.toNat < y.toNat := .rfl -theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by +theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) : + compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rfl @@ -331,7 +335,8 @@ theorem USize.le_iff_toNat_le_toNat {x y : USize} : x ≤ y ↔ x.toNat ≤ y.to theorem USize.lt_iff_toNat_lt_toNat {x y : USize} : x < y ↔ x.toNat < y.toNat := .rfl -theorem USize.compare_eq_toNat_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by +theorem USize.compare_eq_toNat_compare_toNat (x y : USize) : + compare x y = compare x.toNat y.toNat := by simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl From 033473ac112ea8078197943f7960f8c5184a31cb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Fri, 27 Sep 2024 15:39:49 -0400 Subject: [PATCH 6/6] chore: merge main --- Batteries/Data/UInt.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean index b95b077b8f..e8ca78bb05 100644 --- a/Batteries/Data/UInt.lean +++ b/Batteries/Data/UInt.lean @@ -48,7 +48,7 @@ theorem UInt8.lt_iff_toNat_lt_toNat {x y : UInt8} : x < y ↔ x.toNat < y.toNat theorem UInt8.compare_eq_toNat_compare_toNat (x y : UInt8) : compare x y = compare x.toNat y.toNat := by - simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, UInt8.ext_iff] theorem UInt8.max_def (x y : UInt8) : max x y = if x ≤ y then y else x := rfl @@ -117,7 +117,7 @@ theorem UInt16.lt_iff_toNat_lt_toNat {x y : UInt16} : x < y ↔ x.toNat < y.toNa theorem UInt16.compare_eq_toNat_compare_toNat (x y : UInt16) : compare x y = compare x.toNat y.toNat := by - simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, UInt16.ext_iff] theorem UInt16.max_def (x y : UInt16) : max x y = if x ≤ y then y else x := rfl @@ -186,7 +186,7 @@ theorem UInt32.lt_iff_toNat_lt_toNat {x y : UInt32} : x < y ↔ x.toNat < y.toNa theorem UInt32.compare_eq_toNat_compare_toNat (x y : UInt32) : compare x y = compare x.toNat y.toNat := by - simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, UInt32.ext_iff] theorem UInt32.max_def (x y : UInt32) : max x y = if x ≤ y then y else x := rfl @@ -255,7 +255,7 @@ theorem UInt64.lt_iff_toNat_lt_toNat {x y : UInt64} : x < y ↔ x.toNat < y.toNa theorem UInt64.compare_eq_toNat_compare_toNat (x y : UInt64) : compare x y = compare x.toNat y.toNat := by - simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, UInt64.ext_iff] theorem UInt64.max_def (x y : UInt64) : max x y = if x ≤ y then y else x := rfl @@ -337,7 +337,7 @@ theorem USize.lt_iff_toNat_lt_toNat {x y : USize} : x < y ↔ x.toNat < y.toNat theorem USize.compare_eq_toNat_compare_toNat (x y : USize) : compare x y = compare x.toNat y.toNat := by - simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, ext_iff] + simp only [compare, compareOfLessAndEq, lt_iff_toNat_lt_toNat, USize.ext_iff] theorem USize.max_def (x y : USize) : max x y = if x ≤ y then y else x := rfl