From ebf5fbd294b379dcaf4a7a6da0a6934b035e61d4 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 5 Jun 2025 21:25:04 +1000 Subject: [PATCH] feat: complete `grind`'s `ToInt` framework (#8639) This PR completes the `ToInt` family of typeclasses which `grind` will use to embed types into the integers for `cutsat`. It contains instances for the usual concrete data types (`Fin`, `UIntX`, `IntX`, `BitVec`), and is extensible (e.g. for Mathlib's `PNat`). --- src/Init/Data/Fin/Lemmas.lean | 11 ++ src/Init/Grind/CommRing/BitVec.lean | 5 + src/Init/Grind/CommRing/Fin.lean | 3 + src/Init/Grind/CommRing/SInt.lean | 25 +++ src/Init/Grind/CommRing/UInt.lean | 25 +++ src/Init/Grind/Module/Basic.lean | 14 ++ src/Init/Grind/ToInt.lean | 258 ++++++++++++++++++++++++---- 7 files changed, 304 insertions(+), 37 deletions(-) diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean index 00daef752a..deb517c3a3 100644 --- a/src/Init/Data/Fin/Lemmas.lean +++ b/src/Init/Data/Fin/Lemmas.lean @@ -1079,6 +1079,17 @@ theorem val_neg {n : Nat} [NeZero n] (x : Fin n) : have := Fin.val_ne_zero_iff.mpr h omega +protected theorem sub_eq_add_neg {n : Nat} (x y : Fin n) : x - y = x + -y := by + by_cases h : n = 0 + · subst h + apply elim0 x + · replace h : NeZero n := ⟨h⟩ + ext + rw [Fin.coe_sub, Fin.val_add, val_neg] + split + · simp_all + · simp [Nat.add_comm] + /-! ### mul -/ theorem ofNat_mul [NeZero n] (x : Nat) (y : Fin n) : diff --git a/src/Init/Grind/CommRing/BitVec.lean b/src/Init/Grind/CommRing/BitVec.lean index 24e6bf20bc..d7e50780b3 100644 --- a/src/Init/Grind/CommRing/BitVec.lean +++ b/src/Init/Grind/CommRing/BitVec.lean @@ -34,4 +34,9 @@ instance : CommRing (BitVec w) where instance : IsCharP (BitVec w) (2 ^ w) where ofNat_eq_zero_iff {x} := by simp [BitVec.ofInt, BitVec.toNat_eq] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add (BitVec w) (some 0) (some (2^w)) := inferInstance +example : ToInt.Neg (BitVec w) (some 0) (some (2^w)) := inferInstance +example : ToInt.Sub (BitVec w) (some 0) (some (2^w)) := inferInstance + end Lean.Grind diff --git a/src/Init/Grind/CommRing/Fin.lean b/src/Init/Grind/CommRing/Fin.lean index d4b89115c4..47541890f7 100644 --- a/src/Init/Grind/CommRing/Fin.lean +++ b/src/Init/Grind/CommRing/Fin.lean @@ -100,6 +100,9 @@ instance (n : Nat) [NeZero n] : IsCharP (Fin n) n where simp only [Nat.zero_mod] simp only [Fin.mk.injEq] +example [NeZero n] : ToInt.Neg (Fin n) (some 0) (some n) := inferInstance +example [NeZero n] : ToInt.Sub (Fin n) (some 0) (some n) := inferInstance + end Fin end Lean.Grind diff --git a/src/Init/Grind/CommRing/SInt.lean b/src/Init/Grind/CommRing/SInt.lean index f5bff29224..a5c78a5a1e 100644 --- a/src/Init/Grind/CommRing/SInt.lean +++ b/src/Init/Grind/CommRing/SInt.lean @@ -45,6 +45,11 @@ instance : IsCharP Int8 (2 ^ 8) where simp [Int8.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add Int8 (some (-(2^7))) (some (2^7)) := inferInstance +example : ToInt.Neg Int8 (some (-(2^7))) (some (2^7)) := inferInstance +example : ToInt.Sub Int8 (some (-(2^7))) (some (2^7)) := inferInstance + instance : NatCast Int16 where natCast x := Int16.ofNat x @@ -76,6 +81,11 @@ instance : IsCharP Int16 (2 ^ 16) where simp [Int16.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add Int16 (some (-(2^15))) (some (2^15)) := inferInstance +example : ToInt.Neg Int16 (some (-(2^15))) (some (2^15)) := inferInstance +example : ToInt.Sub Int16 (some (-(2^15))) (some (2^15)) := inferInstance + instance : NatCast Int32 where natCast x := Int32.ofNat x @@ -107,6 +117,11 @@ instance : IsCharP Int32 (2 ^ 32) where simp [Int32.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add Int32 (some (-(2^31))) (some (2^31)) := inferInstance +example : ToInt.Neg Int32 (some (-(2^31))) (some (2^31)) := inferInstance +example : ToInt.Sub Int32 (some (-(2^31))) (some (2^31)) := inferInstance + instance : NatCast Int64 where natCast x := Int64.ofNat x @@ -138,6 +153,11 @@ instance : IsCharP Int64 (2 ^ 64) where simp [Int64.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add Int64 (some (-(2^63))) (some (2^63)) := inferInstance +example : ToInt.Neg Int64 (some (-(2^63))) (some (2^63)) := inferInstance +example : ToInt.Sub Int64 (some (-(2^63))) (some (2^63)) := inferInstance + instance : NatCast ISize where natCast x := ISize.ofNat x @@ -171,4 +191,9 @@ instance : IsCharP ISize (2 ^ numBits) where simp [ISize.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance +example : ToInt.Neg ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance +example : ToInt.Sub ISize (some (-(2^(numBits-1)))) (some (2^(numBits-1))) := inferInstance + end Lean.Grind diff --git a/src/Init/Grind/CommRing/UInt.lean b/src/Init/Grind/CommRing/UInt.lean index 1b69b81c42..54b2b89537 100644 --- a/src/Init/Grind/CommRing/UInt.lean +++ b/src/Init/Grind/CommRing/UInt.lean @@ -149,6 +149,11 @@ instance : IsCharP UInt8 256 where have : OfNat.ofNat x = UInt8.ofNat x := rfl simp [this, UInt8.ofNat_eq_iff_mod_eq_toNat] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add UInt8 (some 0) (some (2^8)) := inferInstance +example : ToInt.Neg UInt8 (some 0) (some (2^8)) := inferInstance +example : ToInt.Sub UInt8 (some 0) (some (2^8)) := inferInstance + instance : CommRing UInt16 where add_assoc := UInt16.add_assoc add_comm := UInt16.add_comm @@ -174,6 +179,11 @@ instance : IsCharP UInt16 65536 where have : OfNat.ofNat x = UInt16.ofNat x := rfl simp [this, UInt16.ofNat_eq_iff_mod_eq_toNat] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add UInt16 (some 0) (some (2^16)) := inferInstance +example : ToInt.Neg UInt16 (some 0) (some (2^16)) := inferInstance +example : ToInt.Sub UInt16 (some 0) (some (2^16)) := inferInstance + instance : CommRing UInt32 where add_assoc := UInt32.add_assoc add_comm := UInt32.add_comm @@ -199,6 +209,11 @@ instance : IsCharP UInt32 4294967296 where have : OfNat.ofNat x = UInt32.ofNat x := rfl simp [this, UInt32.ofNat_eq_iff_mod_eq_toNat] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add UInt32 (some 0) (some (2^32)) := inferInstance +example : ToInt.Neg UInt32 (some 0) (some (2^32)) := inferInstance +example : ToInt.Sub UInt32 (some 0) (some (2^32)) := inferInstance + instance : CommRing UInt64 where add_assoc := UInt64.add_assoc add_comm := UInt64.add_comm @@ -224,6 +239,11 @@ instance : IsCharP UInt64 18446744073709551616 where have : OfNat.ofNat x = UInt64.ofNat x := rfl simp [this, UInt64.ofNat_eq_iff_mod_eq_toNat] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add UInt64 (some 0) (some (2^64)) := inferInstance +example : ToInt.Neg UInt64 (some 0) (some (2^64)) := inferInstance +example : ToInt.Sub UInt64 (some 0) (some (2^64)) := inferInstance + instance : CommRing USize where add_assoc := USize.add_assoc add_comm := USize.add_comm @@ -251,4 +271,9 @@ instance : IsCharP USize (2 ^ numBits) where have : OfNat.ofNat x = USize.ofNat x := rfl simp [this, USize.ofNat_eq_iff_mod_eq_toNat] +-- Verify we can derive the instances showing how `toInt` interacts with operations: +example : ToInt.Add USize (some 0) (some (2^numBits)) := inferInstance +example : ToInt.Neg USize (some 0) (some (2^numBits)) := inferInstance +example : ToInt.Sub USize (some 0) (some (2^numBits)) := inferInstance + end Lean.Grind diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean index 3a2dc36b12..a06b33b8e4 100644 --- a/src/Init/Grind/Module/Basic.lean +++ b/src/Init/Grind/Module/Basic.lean @@ -7,6 +7,7 @@ module prelude import Init.Data.Int.Order +import Init.Grind.ToInt namespace Lean.Grind @@ -115,4 +116,17 @@ class NoNatZeroDivisors (α : Type u) [Zero α] [HMul Nat α α] where export NoNatZeroDivisors (no_nat_zero_divisors) +instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Zero α (some lo) (some hi)] [ToInt.Add α (some lo) (some hi)] : ToInt.Neg α (some lo) (some hi) where + toInt_neg x := by + have := (ToInt.Add.toInt_add (-x) x).symm + rw [IntModule.neg_add_cancel, ToInt.Zero.toInt_zero] at this + rw [ToInt.wrap_eq_wrap_iff] at this + simp at this + rw [← ToInt.wrap_toInt] + rw [ToInt.wrap_eq_wrap_iff] + simpa + +instance [ToInt α (some lo) (some hi)] [IntModule α] [ToInt.Add α (some lo) (some hi)] [ToInt.Neg α (some lo) (some hi)] : ToInt.Sub α (some lo) (some hi) := + ToInt.Sub.of_sub_eq_add_neg IntModule.sub_eq_add_neg + end Lean.Grind diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean index 602ec9d842..45068482de 100644 --- a/src/Init/Grind/ToInt.lean +++ b/src/Init/Grind/ToInt.lean @@ -27,9 +27,6 @@ The typeclass `ToInt.Add α lo? hi?` then asserts that `toInt (x + y) = wrap lo? There are many variants for other operations. These typeclasses are used solely in the `grind` tactic to lift linear inequalities into `Int`. - --- TODO: instances for `ToInt.Mod` (only exists for `Fin n` so far) --- TODO: typeclasses for LT, and other algebraic operations. -/ namespace Lean.Grind @@ -40,21 +37,73 @@ class ToInt (α : Type u) (lo? hi? : outParam (Option Int)) where le_toInt : lo? = some lo → lo ≤ toInt x toInt_lt : hi? = some hi → toInt x < hi -@[simp 500] +@[simp] def ToInt.wrap (lo? hi? : Option Int) (x : Int) : Int := match lo?, hi? with | some lo, some hi => (x - lo) % (hi - lo) + lo | _, _ => x +class ToInt.Zero (α : Type u) [Zero α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + toInt_zero : toInt (0 : α) = wrap lo? hi? 0 + +class ToInt.Add (α : Type u) [Add α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + toInt_add : ∀ x y : α, toInt (x + y) = wrap lo? hi? (toInt x + toInt y) + +class ToInt.Neg (α : Type u) [Neg α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + toInt_neg : ∀ x : α, toInt (-x) = wrap lo? hi? (-toInt x) + +class ToInt.Sub (α : Type u) [Sub α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + toInt_sub : ∀ x y : α, toInt (x - y) = wrap lo? hi? (toInt x - toInt y) + +class ToInt.Mod (α : Type u) [Mod α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + /-- One might expect a `wrap` on the right hand side, + but in practice this stronger statement is usually true. -/ + toInt_mod : ∀ x y : α, toInt (x % y) = toInt x % toInt y + +class ToInt.LE (α : Type u) [LE α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + le_iff : ∀ x y : α, x ≤ y ↔ toInt x ≤ toInt y + +class ToInt.LT (α : Type u) [LT α] (lo? hi? : outParam (Option Int)) [ToInt α lo? hi?] where + lt_iff : ∀ x y : α, x < y ↔ toInt x < toInt y + +/-! ## Helper theorems -/ + +theorem ToInt.wrap_add (lo? hi? : Option Int) (x y : Int) : + ToInt.wrap lo? hi? (x + y) = ToInt.wrap lo? hi? (ToInt.wrap lo? hi? x + ToInt.wrap lo? hi? y) := by + simp only [wrap] + split <;> rename_i lo hi + · dsimp + rw [Int.add_left_inj, Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.emod_def (x - lo), Int.emod_def (y - lo)] + have : (x + y - lo - + (x - lo - (hi - lo) * ((x - lo) / (hi - lo)) + lo + + (y - lo - (hi - lo) * ((y - lo) / (hi - lo)) + lo) - lo)) = + (hi - lo) * ((x - lo) / (hi - lo) + (y - lo) / (hi - lo)) := by + simp only [Int.mul_add] + omega + rw [this] + exact Int.mul_emod_right .. + · simp + +@[simp] +theorem ToInt.wrap_toInt (lo? hi? : Option Int) [ToInt α lo? hi?] (x : α) : + ToInt.wrap lo? hi? (ToInt.toInt x) = ToInt.toInt x := by + simp only [wrap] + split + · have := ToInt.le_toInt (x := x) rfl + have := ToInt.toInt_lt (x := x) rfl + rw [Int.emod_eq_of_lt (by omega) (by omega)] + omega + · rfl + theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) : ToInt.wrap (some (-i)) (some i) x = x.bmod ((2 * i).toNat) := by match i, h with | (i : Nat), _ => have : (2 * (i : Int)).toNat = 2 * i := by omega - simp only [this] + rw [this] simp [Int.bmod_eq_emod, ← Int.two_mul] have : (2 * (i : Int) + 1) / 2 = i := by omega - simp only [this] + rw [this] by_cases h : i = 0 · simp [h] split @@ -69,7 +118,7 @@ theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) : have : x - 2 * ↑i * (x / (2 * ↑i)) - ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i)) - 1) := by simp only [Int.mul_sub, Int.mul_neg] omega - simp only [this] + rw [this] exact Int.dvd_mul_right .. · rw [← Int.sub_eq_add_neg, Int.sub_eq_iff_eq_add, Int.natCast_zero, Int.sub_zero] rw [Int.emod_eq_iff (by omega)] @@ -81,17 +130,27 @@ theorem ToInt.wrap_eq_bmod {i : Int} (h : 0 ≤ i) : have : x - 2 * ↑i * (x / (2 * ↑i)) + ↑i - (x + ↑i) = (2 * (i : Int)) * (- (x / (2 * i))) := by simp only [Int.mul_neg] omega - simp only [this] + rw [this] exact Int.dvd_mul_right .. -class ToInt.Add (α : Type u) [Add α] (lo? hi? : Option Int) [ToInt α lo? hi?] where - toInt_add : ∀ x y : α, toInt (x + y) = wrap lo? hi? (toInt x + toInt y) +theorem ToInt.wrap_eq_wrap_iff : + ToInt.wrap (some lo) (some hi) x = ToInt.wrap (some lo) (some hi) y ↔ (x - y) % (hi - lo) = 0 := by + simp only [wrap] + rw [Int.add_left_inj] + rw [Int.emod_eq_emod_iff_emod_sub_eq_zero] + have : x - lo - (y - lo) = x - y := by omega + rw [this] -class ToInt.Mod (α : Type u) [Mod α] (lo? hi? : Option Int) [ToInt α lo? hi?] where - toInt_mod : ∀ x y : α, toInt (x % y) = wrap lo? hi? (toInt x % toInt y) +/-- Construct a `ToInt.Sub` instance from a `ToInt.Add` and `ToInt.Neg` instance and +a `sub_eq_add_neg` assumption. -/ +def ToInt.Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α] + (sub_eq_add_neg : ∀ x y : α, x - y = x + -y) + {lo? hi? : Option Int} [ToInt α lo? hi?] [Add α lo? hi?] [Neg α lo? hi?] : ToInt.Sub α lo? hi? where + toInt_sub x y := by + rw [sub_eq_add_neg, ToInt.Add.toInt_add, ToInt.Neg.toInt_neg, Int.sub_eq_add_neg] + conv => rhs; rw [ToInt.wrap_add, ToInt.wrap_toInt] -class ToInt.LE (α : Type u) [LE α] (lo? hi? : Option Int) [ToInt α lo? hi?] where - le_iff : ∀ x y : α, x ≤ y ↔ toInt x ≤ toInt y +/-! ## Instances for concrete types-/ instance : ToInt Int none none where toInt := id @@ -104,9 +163,21 @@ instance : ToInt Int none none where instance : ToInt.Add Int none none where toInt_add := by simp +instance : ToInt.Neg Int none none where + toInt_neg x := by simp + +instance : ToInt.Sub Int none none where + toInt_sub x y := by simp + +instance : ToInt.Mod Int none none where + toInt_mod x y := by simp + instance : ToInt.LE Int none none where le_iff x y := by simp +instance : ToInt.LT Int none none where + lt_iff x y := by simp + instance : ToInt Nat (some 0) none where toInt := Nat.cast toInt_inj x y := Int.ofNat_inj.mp @@ -118,9 +189,15 @@ instance : ToInt Nat (some 0) none where instance : ToInt.Add Nat (some 0) none where toInt_add := by simp +instance : ToInt.Mod Nat (some 0) none where + toInt_mod x y := by simp + instance : ToInt.LE Nat (some 0) none where le_iff x y := by simp +instance : ToInt.LT Nat (some 0) none where + lt_iff x y := by simp + -- Mathlib will add a `ToInt ℕ+ (some 1) none` instance. instance : ToInt (Fin n) (some 0) (some n) where @@ -134,17 +211,21 @@ instance : ToInt (Fin n) (some 0) (some n) where instance : ToInt.Add (Fin n) (some 0) (some n) where toInt_add x y := by rfl +instance [NeZero n] : ToInt.Zero (Fin n) (some 0) (some n) where + toInt_zero := by rfl + +-- The `ToInt.Neg` and `ToInt.Sub` instances are generated automatically from the `IntModule (Fin n)` instance. + instance : ToInt.Mod (Fin n) (some 0) (some n) where toInt_mod x y := by - simp only [toInt_fin, Fin.mod_val, Int.natCast_emod, ToInt.wrap, Int.sub_zero, Int.add_zero] - rw [Int.emod_eq_of_lt (b := n)] - · omega - · rw [Int.ofNat_mod_ofNat, ← Fin.mod_val] - exact Int.ofNat_lt.mpr (x % y).isLt + simp only [toInt_fin, Fin.mod_val, Int.natCast_emod] instance : ToInt.LE (Fin n) (some 0) (some n) where le_iff x y := by simpa using Fin.le_def +instance : ToInt.LT (Fin n) (some 0) (some n) where + lt_iff x y := by simpa using Fin.lt_def + instance : ToInt UInt8 (some 0) (some (2^8)) where toInt x := (x.toNat : Int) toInt_inj x y w := UInt8.toNat_inj.mp (Int.ofNat_inj.mp w) @@ -156,9 +237,18 @@ instance : ToInt UInt8 (some 0) (some (2^8)) where instance : ToInt.Add UInt8 (some 0) (some (2^8)) where toInt_add x y := by simp +instance : ToInt.Zero UInt8 (some 0) (some (2^8)) where + toInt_zero := by simp + +instance : ToInt.Mod UInt8 (some 0) (some (2^8)) where + toInt_mod x y := by simp + instance : ToInt.LE UInt8 (some 0) (some (2^8)) where le_iff x y := by simpa using UInt8.le_iff_toBitVec_le +instance : ToInt.LT UInt8 (some 0) (some (2^8)) where + lt_iff x y := by simpa using UInt8.lt_iff_toBitVec_lt + instance : ToInt UInt16 (some 0) (some (2^16)) where toInt x := (x.toNat : Int) toInt_inj x y w := UInt16.toNat_inj.mp (Int.ofNat_inj.mp w) @@ -170,9 +260,18 @@ instance : ToInt UInt16 (some 0) (some (2^16)) where instance : ToInt.Add UInt16 (some 0) (some (2^16)) where toInt_add x y := by simp +instance : ToInt.Zero UInt16 (some 0) (some (2^16)) where + toInt_zero := by simp + +instance : ToInt.Mod UInt16 (some 0) (some (2^16)) where + toInt_mod x y := by simp + instance : ToInt.LE UInt16 (some 0) (some (2^16)) where le_iff x y := by simpa using UInt16.le_iff_toBitVec_le +instance : ToInt.LT UInt16 (some 0) (some (2^16)) where + lt_iff x y := by simpa using UInt16.lt_iff_toBitVec_lt + instance : ToInt UInt32 (some 0) (some (2^32)) where toInt x := (x.toNat : Int) toInt_inj x y w := UInt32.toNat_inj.mp (Int.ofNat_inj.mp w) @@ -184,9 +283,18 @@ instance : ToInt UInt32 (some 0) (some (2^32)) where instance : ToInt.Add UInt32 (some 0) (some (2^32)) where toInt_add x y := by simp +instance : ToInt.Zero UInt32 (some 0) (some (2^32)) where + toInt_zero := by simp + +instance : ToInt.Mod UInt32 (some 0) (some (2^32)) where + toInt_mod x y := by simp + instance : ToInt.LE UInt32 (some 0) (some (2^32)) where le_iff x y := by simpa using UInt32.le_iff_toBitVec_le +instance : ToInt.LT UInt32 (some 0) (some (2^32)) where + lt_iff x y := by simpa using UInt32.lt_iff_toBitVec_lt + instance : ToInt UInt64 (some 0) (some (2^64)) where toInt x := (x.toNat : Int) toInt_inj x y w := UInt64.toNat_inj.mp (Int.ofNat_inj.mp w) @@ -198,9 +306,18 @@ instance : ToInt UInt64 (some 0) (some (2^64)) where instance : ToInt.Add UInt64 (some 0) (some (2^64)) where toInt_add x y := by simp +instance : ToInt.Zero UInt64 (some 0) (some (2^64)) where + toInt_zero := by simp + +instance : ToInt.Mod UInt64 (some 0) (some (2^64)) where + toInt_mod x y := by simp + instance : ToInt.LE UInt64 (some 0) (some (2^64)) where le_iff x y := by simpa using UInt64.le_iff_toBitVec_le +instance : ToInt.LT UInt64 (some 0) (some (2^64)) where + lt_iff x y := by simpa using UInt64.lt_iff_toBitVec_lt + instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where toInt x := (x.toNat : Int) toInt_inj x y w := USize.toNat_inj.mp (Int.ofNat_inj.mp w) @@ -216,9 +333,18 @@ instance : ToInt USize (some 0) (some (2^System.Platform.numBits)) where instance : ToInt.Add USize (some 0) (some (2^System.Platform.numBits)) where toInt_add x y := by simp +instance : ToInt.Zero USize (some 0) (some (2^System.Platform.numBits)) where + toInt_zero := by simp + +instance : ToInt.Mod USize (some 0) (some (2^System.Platform.numBits)) where + toInt_mod x y := by simp + instance : ToInt.LE USize (some 0) (some (2^System.Platform.numBits)) where le_iff x y := by simpa using USize.le_iff_toBitVec_le +instance : ToInt.LT USize (some 0) (some (2^System.Platform.numBits)) where + lt_iff x y := by simpa using USize.lt_iff_toBitVec_lt + instance : ToInt Int8 (some (-2^7)) (some (2^7)) where toInt x := x.toInt toInt_inj x y w := Int8.toInt_inj.mp w @@ -232,9 +358,22 @@ instance : ToInt.Add Int8 (some (-2^7)) (some (2^7)) where simp [Int.bmod_eq_emod] split <;> · simp; omega +instance : ToInt.Zero Int8 (some (-2^7)) (some (2^7)) where + toInt_zero := by + -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error! + change (0 : Int8).toInt = _ + rw [Int8.toInt_zero] + decide + +-- Note that we can not define `ToInt.Mod` instances for `Int8`, +-- because the condition does not hold unless `0 ≤ x.toInt ∨ y.toInt ∣ x.toInt ∨ y = 0`. + instance : ToInt.LE Int8 (some (-2^7)) (some (2^7)) where le_iff x y := by simpa using Int8.le_iff_toInt_le +instance : ToInt.LT Int8 (some (-2^7)) (some (2^7)) where + lt_iff x y := by simpa using Int8.lt_iff_toInt_lt + instance : ToInt Int16 (some (-2^15)) (some (2^15)) where toInt x := x.toInt toInt_inj x y w := Int16.toInt_inj.mp w @@ -248,9 +387,19 @@ instance : ToInt.Add Int16 (some (-2^15)) (some (2^15)) where simp [Int.bmod_eq_emod] split <;> · simp; omega +instance : ToInt.Zero Int16 (some (-2^15)) (some (2^15)) where + toInt_zero := by + -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error! + change (0 : Int16).toInt = _ + rw [Int16.toInt_zero] + decide + instance : ToInt.LE Int16 (some (-2^15)) (some (2^15)) where le_iff x y := by simpa using Int16.le_iff_toInt_le +instance : ToInt.LT Int16 (some (-2^15)) (some (2^15)) where + lt_iff x y := by simpa using Int16.lt_iff_toInt_lt + instance : ToInt Int32 (some (-2^31)) (some (2^31)) where toInt x := x.toInt toInt_inj x y w := Int32.toInt_inj.mp w @@ -264,9 +413,19 @@ instance : ToInt.Add Int32 (some (-2^31)) (some (2^31)) where simp [Int.bmod_eq_emod] split <;> · simp; omega +instance : ToInt.Zero Int32 (some (-2^31)) (some (2^31)) where + toInt_zero := by + -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error! + change (0 : Int32).toInt = _ + rw [Int32.toInt_zero] + decide + instance : ToInt.LE Int32 (some (-2^31)) (some (2^31)) where le_iff x y := by simpa using Int32.le_iff_toInt_le +instance : ToInt.LT Int32 (some (-2^31)) (some (2^31)) where + lt_iff x y := by simpa using Int32.lt_iff_toInt_lt + instance : ToInt Int64 (some (-2^63)) (some (2^63)) where toInt x := x.toInt toInt_inj x y w := Int64.toInt_inj.mp w @@ -280,31 +439,44 @@ instance : ToInt.Add Int64 (some (-2^63)) (some (2^63)) where simp [Int.bmod_eq_emod] split <;> · simp; omega +instance : ToInt.Zero Int64 (some (-2^63)) (some (2^63)) where + toInt_zero := by + -- simp -- FIXME: succeeds, but generates a `(kernel) application type mismatch` error! + change (0 : Int64).toInt = _ + rw [Int64.toInt_zero] + decide + instance : ToInt.LE Int64 (some (-2^63)) (some (2^63)) where le_iff x y := by simpa using Int64.le_iff_toInt_le -instance : ToInt (BitVec 0) (some 0) (some 1) where - toInt x := 0 - toInt_inj x y w := by simp at w; exact BitVec.eq_of_zero_length rfl - le_toInt {lo x} w := by simp at w; subst w; exact Int.zero_le_ofNat 0 - toInt_lt {hi x} w := by simp at w; subst w; exact Int.one_pos +instance : ToInt.LT Int64 (some (-2^63)) (some (2^63)) where + lt_iff x y := by simpa using Int64.lt_iff_toInt_lt -@[simp] theorem toInt_bitVec_0 (x : BitVec 0) : ToInt.toInt x = 0 := rfl +instance : ToInt (BitVec v) (some 0) (some (2^v)) where + toInt x := (x.toNat : Int) + toInt_inj x y w := + BitVec.eq_of_toNat_eq (Int.ofNat_inj.mp w) + le_toInt {lo x} w := by simp at w; subst w; exact Int.natCast_nonneg x.toNat + toInt_lt {hi x} w := by + simp at w; subst w; + simpa using Int.ofNat_lt.mpr (BitVec.isLt x) -instance [NeZero v] : ToInt (BitVec v) (some (-2^(v-1))) (some (2^(v-1))) where - toInt x := x.toInt - toInt_inj x y w := BitVec.toInt_inj.mp w - le_toInt {lo x} w := by simp at w; subst w; exact BitVec.le_toInt x - toInt_lt {hi x} w := by simp at w; subst w; exact BitVec.toInt_lt +@[simp] theorem toInt_bitVec (x : BitVec v) : ToInt.toInt x = (x.toNat : Int) := rfl -@[simp] theorem toInt_bitVec [NeZero v] (x : BitVec v) : ToInt.toInt x = x.toInt := rfl +instance : ToInt.Add (BitVec v) (some 0) (some (2^v)) where + toInt_add x y := by simp -instance [i : NeZero v] : ToInt.Add (BitVec v) (some (-2^(v-1))) (some (2^(v-1))) where - toInt_add x y := by - rw [toInt_bitVec, BitVec.toInt_add, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))] - have : ((2 : Int) * 2 ^ (v - 1)).toNat = 2 ^ v := by - match v, i with | v + 1, _ => simp [← Int.pow_succ', Int.toNat_pow_of_nonneg] - simp [this] +instance : ToInt.Zero (BitVec v) (some 0) (some (2^v)) where + toInt_zero := by simp + +instance : ToInt.Mod (BitVec v) (some 0) (some (2^v)) where + toInt_mod x y := by simp + +instance : ToInt.LE (BitVec v) (some 0) (some (2^v)) where + le_iff x y := by simpa using BitVec.le_def + +instance : ToInt.LT (BitVec v) (some 0) (some (2^v)) where + lt_iff x y := by simpa using BitVec.lt_def instance : ToInt ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where toInt x := x.toInt @@ -326,4 +498,16 @@ instance : ToInt.Add ISize (some (-2^(System.Platform.numBits-1))) (some (2^(Sys simp simp [p₁, p₂] +instance : ToInt.Zero ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where + toInt_zero := by + rw [toInt_isize] + rw [ISize.toInt_zero, ToInt.wrap_eq_bmod (Int.pow_nonneg (by decide))] + simp + +instance instToIntLEISize : ToInt.LE ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where + le_iff x y := by simpa using ISize.le_iff_toInt_le + +instance instToIntLTISize : ToInt.LT ISize (some (-2^(System.Platform.numBits-1))) (some (2^(System.Platform.numBits-1))) where + lt_iff x y := by simpa using ISize.lt_iff_toInt_lt + end Lean.Grind