306 lines
13 KiB
Text
306 lines
13 KiB
Text
/-
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Leonardo de Moura
|
|
-/
|
|
prelude
|
|
import init.data.Fin.basic init.platform
|
|
|
|
open Nat
|
|
|
|
def uint8Sz : Nat := 256
|
|
structure Uint8 :=
|
|
(val : Fin uint8Sz)
|
|
|
|
@[extern cpp "Lean::uint8_of_nat"]
|
|
def Uint8.ofNat (n : @& Nat) : Uint8 := ⟨Fin.ofNat n⟩
|
|
@[extern cpp "Lean::uint8_to_nat"]
|
|
def Uint8.toNat (n : Uint8) : Nat := n.val.val
|
|
@[extern cpp inline "#1 + #2"]
|
|
def Uint8.add (a b : Uint8) : Uint8 := ⟨a.val + b.val⟩
|
|
@[extern cpp inline "#1 - #2"]
|
|
def Uint8.sub (a b : Uint8) : Uint8 := ⟨a.val - b.val⟩
|
|
@[extern cpp inline "#1 * #2"]
|
|
def Uint8.mul (a b : Uint8) : Uint8 := ⟨a.val * b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
|
|
def Uint8.div (a b : Uint8) : Uint8 := ⟨a.val / b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
|
|
def Uint8.mod (a b : Uint8) : Uint8 := ⟨a.val % b.val⟩
|
|
@[extern cpp "Lean::uint8_modn"]
|
|
def Uint8.modn (a : Uint8) (n : @& Nat) : Uint8 := ⟨a.val %ₙ n⟩
|
|
@[extern cpp inline "#1 & #2"]
|
|
def Uint8.land (a b : Uint8) : Uint8 := ⟨Fin.land a.val b.val⟩
|
|
@[extern cpp inline "#1 | #2"]
|
|
def Uint8.lor (a b : Uint8) : Uint8 := ⟨Fin.lor a.val b.val⟩
|
|
def Uint8.lt (a b : Uint8) : Prop := a.val < b.val
|
|
def Uint8.le (a b : Uint8) : Prop := a.val ≤ b.val
|
|
|
|
instance : HasZero Uint8 := ⟨Uint8.ofNat 0⟩
|
|
instance : HasOne Uint8 := ⟨Uint8.ofNat 1⟩
|
|
instance : HasAdd Uint8 := ⟨Uint8.add⟩
|
|
instance : HasSub Uint8 := ⟨Uint8.sub⟩
|
|
instance : HasMul Uint8 := ⟨Uint8.mul⟩
|
|
instance : HasMod Uint8 := ⟨Uint8.mod⟩
|
|
instance : HasModn Uint8 := ⟨Uint8.modn⟩
|
|
instance : HasDiv Uint8 := ⟨Uint8.div⟩
|
|
instance : HasLt Uint8 := ⟨Uint8.lt⟩
|
|
instance : HasLe Uint8 := ⟨Uint8.le⟩
|
|
instance : Inhabited Uint8 := ⟨0⟩
|
|
|
|
@[extern cpp inline "#1 == #2"]
|
|
def Uint8.decEq (a b : Uint8) : Decidable (a = b) :=
|
|
Uint8.casesOn a $ λ n, Uint8.casesOn b $ λ m,
|
|
if h : n = m then isTrue (h ▸ rfl) else isFalse (λ h', Uint8.noConfusion h' (λ h', absurd h' h))
|
|
|
|
@[extern cpp inline "#1 < #2"]
|
|
def Uint8.decLt (a b : Uint8) : Decidable (a < b) :=
|
|
Uint8.casesOn a $ λ n, Uint8.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n < m))
|
|
|
|
@[extern cpp inline "#1 <= #2"]
|
|
def Uint8.decLe (a b : Uint8) : Decidable (a ≤ b) :=
|
|
Uint8.casesOn a $ λ n, Uint8.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n <= m))
|
|
|
|
instance : DecidableEq Uint8 := {decEq := Uint8.decEq}
|
|
instance Uint8.hasDecidableLt (a b : Uint8) : Decidable (a < b) := Uint8.decLt a b
|
|
instance Uint8.hasDecidableLe (a b : Uint8) : Decidable (a ≤ b) := Uint8.decLe a b
|
|
|
|
def uint16Sz : Nat := 65536
|
|
structure Uint16 :=
|
|
(val : Fin uint16Sz)
|
|
|
|
@[extern cpp "Lean::uint16_of_nat"]
|
|
def Uint16.ofNat (n : @& Nat) : Uint16 := ⟨Fin.ofNat n⟩
|
|
@[extern cpp "Lean::uint16_to_nat"]
|
|
def Uint16.toNat (n : Uint16) : Nat := n.val.val
|
|
@[extern cpp inline "#1 + #2"]
|
|
def Uint16.add (a b : Uint16) : Uint16 := ⟨a.val + b.val⟩
|
|
@[extern cpp inline "#1 - #2"]
|
|
def Uint16.sub (a b : Uint16) : Uint16 := ⟨a.val - b.val⟩
|
|
@[extern cpp inline "#1 * #2"]
|
|
def Uint16.mul (a b : Uint16) : Uint16 := ⟨a.val * b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
|
|
def Uint16.div (a b : Uint16) : Uint16 := ⟨a.val / b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
|
|
def Uint16.mod (a b : Uint16) : Uint16 := ⟨a.val % b.val⟩
|
|
@[extern cpp "Lean::uint16_modn"]
|
|
def Uint16.modn (a : Uint16) (n : @& Nat) : Uint16 := ⟨a.val %ₙ n⟩
|
|
@[extern cpp inline "#1 & #2"]
|
|
def Uint16.land (a b : Uint16) : Uint16 := ⟨Fin.land a.val b.val⟩
|
|
@[extern cpp inline "#1 | #2"]
|
|
def Uint16.lor (a b : Uint16) : Uint16 := ⟨Fin.lor a.val b.val⟩
|
|
def Uint16.lt (a b : Uint16) : Prop := a.val < b.val
|
|
def Uint16.le (a b : Uint16) : Prop := a.val ≤ b.val
|
|
|
|
instance : HasZero Uint16 := ⟨Uint16.ofNat 0⟩
|
|
instance : HasOne Uint16 := ⟨Uint16.ofNat 1⟩
|
|
instance : HasAdd Uint16 := ⟨Uint16.add⟩
|
|
instance : HasSub Uint16 := ⟨Uint16.sub⟩
|
|
instance : HasMul Uint16 := ⟨Uint16.mul⟩
|
|
instance : HasMod Uint16 := ⟨Uint16.mod⟩
|
|
instance : HasModn Uint16 := ⟨Uint16.modn⟩
|
|
instance : HasDiv Uint16 := ⟨Uint16.div⟩
|
|
instance : HasLt Uint16 := ⟨Uint16.lt⟩
|
|
instance : HasLe Uint16 := ⟨Uint16.le⟩
|
|
instance : Inhabited Uint16 := ⟨0⟩
|
|
|
|
@[extern cpp inline "#1 == #2"]
|
|
def Uint16.decEq (a b : Uint16) : Decidable (a = b) :=
|
|
Uint16.casesOn a $ λ n, Uint16.casesOn b $ λ m,
|
|
if h : n = m then isTrue (h ▸ rfl) else isFalse (λ h', Uint16.noConfusion h' (λ h', absurd h' h))
|
|
|
|
@[extern cpp inline "#1 < #2"]
|
|
def Uint16.decLt (a b : Uint16) : Decidable (a < b) :=
|
|
Uint16.casesOn a $ λ n, Uint16.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n < m))
|
|
|
|
@[extern cpp inline "#1 <= #2"]
|
|
def Uint16.decLe (a b : Uint16) : Decidable (a ≤ b) :=
|
|
Uint16.casesOn a $ λ n, Uint16.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n <= m))
|
|
|
|
instance : DecidableEq Uint16 := {decEq := Uint16.decEq}
|
|
instance Uint16.hasDecidableLt (a b : Uint16) : Decidable (a < b) := Uint16.decLt a b
|
|
instance Uint16.hasDecidableLe (a b : Uint16) : Decidable (a ≤ b) := Uint16.decLe a b
|
|
|
|
def uint32Sz : Nat := 4294967296
|
|
structure Uint32 :=
|
|
(val : Fin uint32Sz)
|
|
|
|
@[extern cpp "Lean::uint32_of_nat"]
|
|
def Uint32.ofNat (n : @& Nat) : Uint32 := ⟨Fin.ofNat n⟩
|
|
@[extern cpp "Lean::uint32_to_nat"]
|
|
def Uint32.toNat (n : Uint32) : Nat := n.val.val
|
|
@[extern cpp inline "#1 + #2"]
|
|
def Uint32.add (a b : Uint32) : Uint32 := ⟨a.val + b.val⟩
|
|
@[extern cpp inline "#1 - #2"]
|
|
def Uint32.sub (a b : Uint32) : Uint32 := ⟨a.val - b.val⟩
|
|
@[extern cpp inline "#1 * #2"]
|
|
def Uint32.mul (a b : Uint32) : Uint32 := ⟨a.val * b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
|
|
def Uint32.div (a b : Uint32) : Uint32 := ⟨a.val / b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
|
|
def Uint32.mod (a b : Uint32) : Uint32 := ⟨a.val % b.val⟩
|
|
@[extern cpp "Lean::uint32_modn"]
|
|
def Uint32.modn (a : Uint32) (n : @& Nat) : Uint32 := ⟨a.val %ₙ n⟩
|
|
@[extern cpp inline "#1 & #2"]
|
|
def Uint32.land (a b : Uint32) : Uint32 := ⟨Fin.land a.val b.val⟩
|
|
@[extern cpp inline "#1 | #2"]
|
|
def Uint32.lor (a b : Uint32) : Uint32 := ⟨Fin.lor a.val b.val⟩
|
|
def Uint32.lt (a b : Uint32) : Prop := a.val < b.val
|
|
def Uint32.le (a b : Uint32) : Prop := a.val ≤ b.val
|
|
|
|
instance : HasZero Uint32 := ⟨Uint32.ofNat 0⟩
|
|
instance : HasOne Uint32 := ⟨Uint32.ofNat 1⟩
|
|
instance : HasAdd Uint32 := ⟨Uint32.add⟩
|
|
instance : HasSub Uint32 := ⟨Uint32.sub⟩
|
|
instance : HasMul Uint32 := ⟨Uint32.mul⟩
|
|
instance : HasMod Uint32 := ⟨Uint32.mod⟩
|
|
instance : HasModn Uint32 := ⟨Uint32.modn⟩
|
|
instance : HasDiv Uint32 := ⟨Uint32.div⟩
|
|
instance : HasLt Uint32 := ⟨Uint32.lt⟩
|
|
instance : HasLe Uint32 := ⟨Uint32.le⟩
|
|
instance : Inhabited Uint32 := ⟨0⟩
|
|
|
|
@[extern cpp inline "#1 == #2"]
|
|
def Uint32.decEq (a b : Uint32) : Decidable (a = b) :=
|
|
Uint32.casesOn a $ λ n, Uint32.casesOn b $ λ m,
|
|
if h : n = m then isTrue (h ▸ rfl) else isFalse (λ h', Uint32.noConfusion h' (λ h', absurd h' h))
|
|
|
|
@[extern cpp inline "#1 < #2"]
|
|
def Uint32.decLt (a b : Uint32) : Decidable (a < b) :=
|
|
Uint32.casesOn a $ λ n, Uint32.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n < m))
|
|
|
|
@[extern cpp inline "#1 <= #2"]
|
|
def Uint32.decLe (a b : Uint32) : Decidable (a ≤ b) :=
|
|
Uint32.casesOn a $ λ n, Uint32.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n <= m))
|
|
|
|
instance : DecidableEq Uint32 := {decEq := Uint32.decEq}
|
|
instance Uint32.hasDecidableLt (a b : Uint32) : Decidable (a < b) := Uint32.decLt a b
|
|
instance Uint32.hasDecidableLe (a b : Uint32) : Decidable (a ≤ b) := Uint32.decLe a b
|
|
|
|
def uint64Sz : Nat := 18446744073709551616
|
|
structure Uint64 :=
|
|
(val : Fin uint64Sz)
|
|
|
|
@[extern cpp "Lean::uint64_of_nat"]
|
|
def Uint64.ofNat (n : @& Nat) : Uint64 := ⟨Fin.ofNat n⟩
|
|
@[extern cpp "Lean::uint64_to_nat"]
|
|
def Uint64.toNat (n : Uint64) : Nat := n.val.val
|
|
@[extern cpp inline "#1 + #2"]
|
|
def Uint64.add (a b : Uint64) : Uint64 := ⟨a.val + b.val⟩
|
|
@[extern cpp inline "#1 - #2"]
|
|
def Uint64.sub (a b : Uint64) : Uint64 := ⟨a.val - b.val⟩
|
|
@[extern cpp inline "#1 * #2"]
|
|
def Uint64.mul (a b : Uint64) : Uint64 := ⟨a.val * b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
|
|
def Uint64.div (a b : Uint64) : Uint64 := ⟨a.val / b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
|
|
def Uint64.mod (a b : Uint64) : Uint64 := ⟨a.val % b.val⟩
|
|
@[extern cpp "Lean::uint64_modn"]
|
|
def Uint64.modn (a : Uint64) (n : @& Nat) : Uint64 := ⟨a.val %ₙ n⟩
|
|
@[extern cpp inline "#1 & #2"]
|
|
def Uint64.land (a b : Uint64) : Uint64 := ⟨Fin.land a.val b.val⟩
|
|
@[extern cpp inline "#1 | #2"]
|
|
def Uint64.lor (a b : Uint64) : Uint64 := ⟨Fin.lor a.val b.val⟩
|
|
def Uint64.lt (a b : Uint64) : Prop := a.val < b.val
|
|
def Uint64.le (a b : Uint64) : Prop := a.val ≤ b.val
|
|
|
|
instance : HasZero Uint64 := ⟨Uint64.ofNat 0⟩
|
|
instance : HasOne Uint64 := ⟨Uint64.ofNat 1⟩
|
|
instance : HasAdd Uint64 := ⟨Uint64.add⟩
|
|
instance : HasSub Uint64 := ⟨Uint64.sub⟩
|
|
instance : HasMul Uint64 := ⟨Uint64.mul⟩
|
|
instance : HasMod Uint64 := ⟨Uint64.mod⟩
|
|
instance : HasModn Uint64 := ⟨Uint64.modn⟩
|
|
instance : HasDiv Uint64 := ⟨Uint64.div⟩
|
|
instance : HasLt Uint64 := ⟨Uint64.lt⟩
|
|
instance : HasLe Uint64 := ⟨Uint64.le⟩
|
|
instance : Inhabited Uint64 := ⟨0⟩
|
|
|
|
@[extern cpp inline "#1 == #2"]
|
|
def Uint64.decEq (a b : Uint64) : Decidable (a = b) :=
|
|
Uint64.casesOn a $ λ n, Uint64.casesOn b $ λ m,
|
|
if h : n = m then isTrue (h ▸ rfl) else isFalse (λ h', Uint64.noConfusion h' (λ h', absurd h' h))
|
|
|
|
@[extern cpp inline "#1 < #2"]
|
|
def Uint64.decLt (a b : Uint64) : Decidable (a < b) :=
|
|
Uint64.casesOn a $ λ n, Uint64.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n < m))
|
|
|
|
@[extern cpp inline "#1 <= #2"]
|
|
def Uint64.decLe (a b : Uint64) : Decidable (a ≤ b) :=
|
|
Uint64.casesOn a $ λ n, Uint64.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n <= m))
|
|
|
|
instance : DecidableEq Uint64 := {decEq := Uint64.decEq}
|
|
instance Uint64.hasDecidableLt (a b : Uint64) : Decidable (a < b) := Uint64.decLt a b
|
|
instance Uint64.hasDecidableLe (a b : Uint64) : Decidable (a ≤ b) := Uint64.decLe a b
|
|
|
|
def usizeSz : Nat := (2:Nat) ^ System.platform.nbits
|
|
structure Usize :=
|
|
(val : Fin usizeSz)
|
|
|
|
@[extern cpp "Lean::usize_of_nat"]
|
|
def Usize.ofNat (n : @& Nat) : Usize := ⟨Fin.ofNat n⟩
|
|
@[extern cpp "Lean::usize_to_nat"]
|
|
def Usize.toNat (n : Usize) : Nat := n.val.val
|
|
@[extern cpp inline "#1 + #2"]
|
|
def Usize.add (a b : Usize) : Usize := ⟨a.val + b.val⟩
|
|
@[extern cpp inline "#1 - #2"]
|
|
def Usize.sub (a b : Usize) : Usize := ⟨a.val - b.val⟩
|
|
@[extern cpp inline "#1 * #2"]
|
|
def Usize.mul (a b : Usize) : Usize := ⟨a.val * b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 / #2"]
|
|
def Usize.div (a b : Usize) : Usize := ⟨a.val / b.val⟩
|
|
@[extern cpp inline "#2 == 0 ? 0 : #1 % #2"]
|
|
def Usize.mod (a b : Usize) : Usize := ⟨a.val % b.val⟩
|
|
@[extern cpp "Lean::usize_modn"]
|
|
def Usize.modn (a : Usize) (n : @& Nat) : Usize := ⟨a.val %ₙ n⟩
|
|
@[extern cpp inline "#1 & #2"]
|
|
def Usize.land (a b : Usize) : Usize := ⟨Fin.land a.val b.val⟩
|
|
@[extern cpp inline "#1 | #2"]
|
|
def Usize.lor (a b : Usize) : Usize := ⟨Fin.lor a.val b.val⟩
|
|
@[extern cpp inline "#1"]
|
|
def Usize.ofUint32 (a : Uint32) : Usize := Usize.ofNat (Uint32.toNat a)
|
|
@[extern cpp inline "((Lean::Usize)#1)"]
|
|
def Usize.ofUint64 (a : Uint64) : Usize := Usize.ofNat (Uint64.toNat a)
|
|
def Usize.lt (a b : Usize) : Prop := a.val < b.val
|
|
def Usize.le (a b : Usize) : Prop := a.val ≤ b.val
|
|
|
|
instance : HasZero Usize := ⟨Usize.ofNat 0⟩
|
|
instance : HasOne Usize := ⟨Usize.ofNat 1⟩
|
|
instance : HasAdd Usize := ⟨Usize.add⟩
|
|
instance : HasSub Usize := ⟨Usize.sub⟩
|
|
instance : HasMul Usize := ⟨Usize.mul⟩
|
|
instance : HasMod Usize := ⟨Usize.mod⟩
|
|
instance : HasModn Usize := ⟨Usize.modn⟩
|
|
instance : HasDiv Usize := ⟨Usize.div⟩
|
|
instance : HasLt Usize := ⟨Usize.lt⟩
|
|
instance : HasLe Usize := ⟨Usize.le⟩
|
|
instance : Inhabited Usize := ⟨0⟩
|
|
|
|
@[extern cpp inline "#1 == #2"]
|
|
def Usize.decEq (a b : Usize) : Decidable (a = b) :=
|
|
Usize.casesOn a $ λ n, Usize.casesOn b $ λ m,
|
|
if h : n = m then isTrue (h ▸ rfl) else isFalse (λ h', Usize.noConfusion h' (λ h', absurd h' h))
|
|
|
|
@[extern cpp inline "#1 < #2"]
|
|
def Usize.decLt (a b : Usize) : Decidable (a < b) :=
|
|
Usize.casesOn a $ λ n, Usize.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n < m))
|
|
|
|
@[extern cpp inline "#1 <= #2"]
|
|
def Usize.decLe (a b : Usize) : Decidable (a ≤ b) :=
|
|
Usize.casesOn a $ λ n, Usize.casesOn b $ λ m,
|
|
inferInstanceAs (Decidable (n <= m))
|
|
|
|
instance : DecidableEq Usize := {decEq := Usize.decEq}
|
|
instance Usize.hasDecidableLt (a b : Usize) : Decidable (a < b) := Usize.decLt a b
|
|
instance Usize.hasDecidableLe (a b : Usize) : Decidable (a ≤ b) := Usize.decLe a b
|
|
|
|
theorem Usize.modnLt {m : Nat} : ∀ (u : Usize), m > 0 → Usize.toNat (u %ₙ m) < m
|
|
| ⟨u⟩ h := Fin.modnLt u h
|