Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: order lemmas for UIntX types #854

Open
wants to merge 7 commits into
base: main
Choose a base branch
from
Open

feat: order lemmas for UIntX types #854

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d784c51
feat: order lemmas for `UIntX` types
fgdorais Jun 20, 2024
d5f198d
fix: naming convention
fgdorais Jun 20, 2024
fd4c2cb
feat: add `last`
fgdorais Jun 20, 2024
fc8d7fb
fix: naming convention
fgdorais Jun 20, 2024
182c8ba
fix: long lines
fgdorais Jun 20, 2024
033473a
chore: merge main
fgdorais Sep 27, 2024
3b0ca30
Merge branch 'main' into uint-order
fgdorais Nov 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
163 changes: 161 additions & 2 deletions Batteries/Data/UInt.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,38 @@ 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_toNat_compare_toNat (x y : UInt8) :
compare x y = compare x.toNat y.toNat := by
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

theorem UInt8.min_def (x y : UInt8) : min x y = if x ≤ y then x else y := rfl

theorem UInt8.toNat_max (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.toNat_min (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
Expand Down Expand Up @@ -73,6 +105,38 @@ 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_toNat_compare_toNat (x y : UInt16) :
compare x y = compare x.toNat y.toNat := by
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

theorem UInt16.min_def (x y : UInt16) : min x y = if x ≤ y then x else y := rfl

theorem UInt16.toNat_max (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.toNat_min (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
Expand Down Expand Up @@ -107,6 +171,38 @@ 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_toNat_compare_toNat (x y : UInt32) :
compare x y = compare x.toNat y.toNat := by
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

theorem UInt32.min_def (x y : UInt32) : min x y = if x ≤ y then x else y := rfl

theorem UInt32.toNat_max (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.toNat_min (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
Expand Down Expand Up @@ -141,6 +237,38 @@ 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_toNat_compare_toNat (x y : UInt64) :
compare x y = compare x.toNat y.toNat := by
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

theorem UInt64.min_def (x y : UInt64) : min x y = if x ≤ y then x else y := rfl

theorem UInt64.toNat_max (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.toNat_min (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
Expand All @@ -164,8 +292,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
Expand All @@ -187,3 +314,35 @@ 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_toNat_compare_toNat (x y : USize) :
compare x y = compare x.toNat y.toNat := by
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

theorem USize.min_def (x y : USize) : min x y = if x ≤ y then x else y := rfl

theorem USize.toNat_max (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.toNat_min (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)]