Bitwise operations using binary representation of integers #

Definitions #

bitwise operations for PosNum and Num,
SNum, a type that represents integers as a bit string with a sign bit at the end,
arithmetic operations for SNum.

source

def PosNum.lor :

PosNum → PosNum → PosNum

Bitwise "or" for PosNum.

Equations

PosNum.one.lor q.bit0 = q.bit1
PosNum.one.lor x✝ = x✝
p.bit0.lor PosNum.one = p.bit1
x✝.lor PosNum.one = x✝
p.bit0.lor q.bit0 = (p.lor q).bit0
p.bit0.lor q.bit1 = (p.lor q).bit1
p.bit1.lor q.bit0 = (p.lor q).bit1
p.bit1.lor q.bit1 = (p.lor q).bit1

source

instance PosNum.instOrOp :

OrOp PosNum

Equations

PosNum.instOrOp = { or := PosNum.lor }

source

@[simp]

theorem PosNum.lor_eq_or (p q : PosNum) :

p.lor q = p ||| q

source

def PosNum.land :

PosNum → PosNum → Num

Bitwise "and" for PosNum.

Equations

source

instance PosNum.instHAndNum :

HAnd PosNum PosNum Num

Equations

PosNum.instHAndNum = { hAnd := PosNum.land }

source

@[simp]

theorem PosNum.land_eq_and (p q : PosNum) :

p.land q = p &&& q

source

def PosNum.ldiff :

PosNum → PosNum → Num

Bitwise fun a b ↦ a && !b for PosNum. For example, ldiff 5 9 = 4:

 101
1001
----
 100

Equations

PosNum.one.ldiff a.bit0 = 1
PosNum.one.ldiff x✝ = 0
p.bit0.ldiff PosNum.one = Num.pos p.bit0
p.bit1.ldiff PosNum.one = Num.pos p.bit0
p.bit0.ldiff q.bit0 = (p.ldiff q).bit0
p.bit0.ldiff q.bit1 = (p.ldiff q).bit0
p.bit1.ldiff q.bit0 = (p.ldiff q).bit1
p.bit1.ldiff q.bit1 = (p.ldiff q).bit0

source

def PosNum.lxor :

PosNum → PosNum → Num

Bitwise "xor" for PosNum.

Equations

source

instance PosNum.instHXorNum :

HXor PosNum PosNum Num

Equations

PosNum.instHXorNum = { hXor := PosNum.lxor }

source

@[simp]

theorem PosNum.lxor_eq_xor (p q : PosNum) :

p.lxor q = p ^^^ q

source

def PosNum.testBit :

PosNum → ℕ → Bool

a.testBit n is true iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to false.

Equations

source

def PosNum.oneBits :

PosNum → ℕ → List ℕ

n.oneBits 0 is the list of indices of active bits in the binary representation of n.

Equations

PosNum.one.oneBits x✝ = [x✝]
p.bit0.oneBits x✝ = p.oneBits (x✝ + 1)
p.bit1.oneBits x✝ = x✝ :: p.oneBits (x✝ + 1)

source

def PosNum.shiftl :

PosNum → ℕ → PosNum

Left-shift the binary representation of a PosNum.

Equations

x✝.shiftl 0 = x✝
x✝.shiftl n.succ = x✝.bit0.shiftl n

source

instance PosNum.instHShiftLeftNat :

HShiftLeft PosNum ℕ PosNum

Equations

PosNum.instHShiftLeftNat = { hShiftLeft := PosNum.shiftl }

source

@[simp]

theorem PosNum.shiftl_eq_shiftLeft (p : PosNum) (n : ℕ) :

p.shiftl n = p <<< n

source

theorem PosNum.shiftl_succ_eq_bit0_shiftl (p : PosNum) (n : ℕ) :

p <<< n.succ = (p <<< n).bit0

source

def PosNum.shiftr :

PosNum → ℕ → Num

Right-shift the binary representation of a PosNum.

Equations

x✝.shiftr 0 = Num.pos x✝
PosNum.one.shiftr x✝ = 0
p.bit0.shiftr n.succ = p.shiftr n
p.bit1.shiftr n.succ = p.shiftr n

source

instance PosNum.instHShiftRightNatNum :

HShiftRight PosNum ℕ Num

Equations

PosNum.instHShiftRightNatNum = { hShiftRight := PosNum.shiftr }

source

@[simp]

theorem PosNum.shiftr_eq_shiftRight (p : PosNum) (n : ℕ) :

p.shiftr n = p >>> n

source

def Num.lor :

Num → Num → Num

Bitwise "or" for Num.

Equations

Num.zero.lor x✝ = x✝
x✝.lor Num.zero = x✝
(Num.pos p).lor (Num.pos q) = Num.pos (p ||| q)

source

instance Num.instOrOp :

OrOp Num

Equations

Num.instOrOp = { or := Num.lor }

source

@[simp]

theorem Num.lor_eq_or (p q : Num) :

p.lor q = p ||| q

source

def Num.land :

Num → Num → Num

Bitwise "and" for Num.

Equations

Num.zero.land x✝ = 0
x✝.land Num.zero = 0
(Num.pos p).land (Num.pos q) = p &&& q

source

instance Num.instAndOp :

AndOp Num

Equations

Num.instAndOp = { and := Num.land }

source

@[simp]

theorem Num.land_eq_and (p q : Num) :

p.land q = p &&& q

source

def Num.ldiff :

Num → Num → Num

Bitwise fun a b ↦ a && !b for Num. For example, ldiff 5 9 = 4:

 101
1001
----
 100

Equations

Num.zero.ldiff x✝ = 0
x✝.ldiff Num.zero = x✝
(Num.pos p).ldiff (Num.pos q) = p.ldiff q

source

def Num.lxor :

Num → Num → Num

Bitwise "xor" for Num.

Equations

Num.zero.lxor x✝ = x✝
x✝.lxor Num.zero = x✝
(Num.pos p).lxor (Num.pos q) = p ^^^ q

source

instance Num.instXor :

Xor Num

Equations

Num.instXor = { xor := Num.lxor }

source

@[simp]

theorem Num.lxor_eq_xor (p q : Num) :

p.lxor q = p ^^^ q

source

def Num.shiftl :

Num → ℕ → Num

Left-shift the binary representation of a Num.

Equations

Num.zero.shiftl x✝ = 0
(Num.pos p).shiftl x✝ = Num.pos (p <<< x✝)

source

instance Num.instHShiftLeftNat :

HShiftLeft Num ℕ Num

Equations

Num.instHShiftLeftNat = { hShiftLeft := Num.shiftl }

source

@[simp]

theorem Num.shiftl_eq_shiftLeft (p : Num) (n : ℕ) :

p.shiftl n = p <<< n

source

def Num.shiftr :

Num → ℕ → Num

Right-shift the binary representation of a Num.

Equations

Num.zero.shiftr x✝ = 0
(Num.pos p).shiftr x✝ = p >>> x✝

source

instance Num.instHShiftRightNat :

HShiftRight Num ℕ Num

Equations

Num.instHShiftRightNat = { hShiftRight := Num.shiftr }

source

@[simp]

theorem Num.shiftr_eq_shiftRight (p : Num) (n : ℕ) :

p.shiftr n = p >>> n

source

def Num.testBit :

Num → ℕ → Bool

a.testBit n is true iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to false.

Equations

Num.zero.testBit x✝ = false
(Num.pos p).testBit x✝ = p.testBit x✝

source

def Num.oneBits :

Num → List ℕ

n.oneBits is the list of indices of active bits in the binary representation of n.

Equations

Num.zero.oneBits = []
(Num.pos p).oneBits = p.oneBits 0

source

inductive NzsNum :

Type

This is a nonzero (and "non minus one") version of SNum. See the documentation of SNum for more details.

msb : Bool → NzsNum
bit : Bool → NzsNum → NzsNum
Add a bit at the end of a NzsNum.

source

instance instDecidableEqNzsNum :

DecidableEq NzsNum

Equations

instDecidableEqNzsNum = decEqNzsNum✝

source

inductive SNum :

Type

Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, with all higher bits set to the negation of this sign. The result is interpreted in two's complement.

13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true)))) -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))

As with Num, a special case must be added for zero, which has no msb, but by two's complement symmetry there is a second special case for -1. Here the Bool field indicates the sign of the number.

0 = ..0000000(base 2) = zero false -1 = ..1111111(base 2) = zero true

zero : Bool → SNum
nz : NzsNum → SNum

source

instance instDecidableEqSNum :

DecidableEq SNum

Equations

instDecidableEqSNum = decEqSNum✝

source

instance instCoeNzsNumSNum :

Coe NzsNum SNum

Equations

instCoeNzsNumSNum = { coe := SNum.nz }

source

instance instZeroSNum :

Zero SNum

Equations

instZeroSNum = { zero := SNum.zero false }

source

instance instOneNzsNum :

One NzsNum

Equations

instOneNzsNum = { one := NzsNum.msb true }

source

instance instOneSNum :

One SNum

Equations

instOneSNum = { one := SNum.nz 1 }

source

instance instInhabitedNzsNum :

Inhabited NzsNum

Equations

instInhabitedNzsNum = { default := 1 }

source

instance instInhabitedSNum :

Inhabited SNum

Equations

instInhabitedSNum = { default := 0 }

The SNum representation uses a bit string, essentially a list of 0 (false) and 1 (true) bits, and the negation of the MSB is sign-extended to all higher bits.

source

def NzsNum.«term_::_» :

Lean.TrailingParserDescr

Add a bit at the end of a NzsNum.

Equations

NzsNum.«term_::_» = Lean.ParserDescr.trailingNode `NzsNum.«term_::_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::") (Lean.ParserDescr.cat `term 0))

source

def NzsNum.sign :

NzsNum → Bool

Sign of a NzsNum.

Equations

(NzsNum.msb b).sign = !b
(NzsNum.bit a p).sign = p.sign

source

@[match_pattern]

def NzsNum.not :

NzsNum → NzsNum

Bitwise not for NzsNum.

Equations

(NzsNum.msb b).not = NzsNum.msb (decide ¬b = true)
(NzsNum.bit a p).not = NzsNum.bit (decide ¬a = true) p.not

source

def NzsNum.«term~_» :

Lean.ParserDescr

Bitwise not for NzsNum.

Equations

NzsNum.«term~_» = Lean.ParserDescr.node `NzsNum.«term~_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))

source

def NzsNum.bit0 :

NzsNum → NzsNum

Add an inactive bit at the end of a NzsNum. This mimics PosNum.bit0.

Equations

NzsNum.bit0 = NzsNum.bit false

source

def NzsNum.bit1 :

NzsNum → NzsNum

Add an active bit at the end of a NzsNum. This mimics PosNum.bit1.

Equations

NzsNum.bit1 = NzsNum.bit true

source

def NzsNum.head :

NzsNum → Bool

The head of a NzsNum is the boolean value of its LSB.

Equations

(NzsNum.msb b).head = b
(NzsNum.bit a p).head = a

source

def NzsNum.tail :

NzsNum → SNum

The tail of a NzsNum is the SNum obtained by removing the LSB. Edge cases: tail 1 = 0 and tail (-2) = -1.

Equations

(NzsNum.msb b).tail = SNum.zero (decide ¬b = true)
(NzsNum.bit a p).tail = SNum.nz p

source

def SNum.sign :

SNum → Bool

Sign of a SNum.

Equations

(SNum.zero z).sign = z
(SNum.nz p).sign = p.sign

source

@[match_pattern]

def SNum.not :

SNum → SNum

Bitwise not for SNum.

Equations

(SNum.zero z).not = SNum.zero (decide ¬z = true)
(SNum.nz p).not = SNum.nz p.not

source

def SNum.«term~_» :

Lean.ParserDescr

Bitwise not for SNum.

Equations

SNum.«term~_» = Lean.ParserDescr.node `SNum.«term~_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))

source

@[match_pattern]

def SNum.bit :

Bool → SNum → SNum

Add a bit at the end of a SNum. This mimics NzsNum.bit.

Equations

SNum.bit x✝ (SNum.zero z) = if x✝ = z then SNum.zero x✝ else SNum.nz (NzsNum.msb x✝)
SNum.bit x✝ (SNum.nz p) = SNum.nz (NzsNum.bit x✝ p)

source

def SNum.«term_::_» :

Lean.TrailingParserDescr

Add a bit at the end of a SNum. This mimics NzsNum.bit.

Equations

SNum.«term_::_» = Lean.ParserDescr.trailingNode `SNum.«term_::_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::") (Lean.ParserDescr.cat `term 0))

source

def SNum.bit0 :

SNum → SNum

Add an inactive bit at the end of a SNum. This mimics ZNum.bit0.

Equations

SNum.bit0 = SNum.bit false

source

def SNum.bit1 :

SNum → SNum

Add an active bit at the end of a SNum. This mimics ZNum.bit1.

Equations

SNum.bit1 = SNum.bit true

source

theorem SNum.bit_zero (b : Bool) :

bit b (zero b) = zero b

source

theorem SNum.bit_one (b : Bool) :

bit b (zero (decide ¬b = true)) = nz (NzsNum.msb b)

source

def NzsNum.drec' {C : SNum → Sort u_1} (z : (b : Bool) → C (SNum.zero b)) (s : (b : Bool) → (p : SNum) → C p → C (SNum.bit b p)) (p : NzsNum) :

C (SNum.nz p)

A dependent induction principle for NzsNum, with base cases 0 : SNum and (-1) : SNum.

Equations

NzsNum.drec' z s (NzsNum.msb b) = ⋯.mpr (s b (SNum.zero (decide ¬b = true)) (z (decide ¬b = true)))
NzsNum.drec' z s (NzsNum.bit a p) = s a (SNum.nz p) (NzsNum.drec' z s p)

source

def SNum.head :

SNum → Bool

The head of a SNum is the boolean value of its LSB.

Equations

(SNum.zero z).head = z
(SNum.nz p).head = p.head

source

def SNum.tail :

SNum → SNum

The tail of a SNum is obtained by removing the LSB. Edge cases: tail 1 = 0, tail (-2) = -1, tail 0 = 0 and tail (-1) = -1.

Equations

(SNum.zero z).tail = SNum.zero z
(SNum.nz p).tail = p.tail

source

def SNum.drec' {C : SNum → Sort u_1} (z : (b : Bool) → C (zero b)) (s : (b : Bool) → (p : SNum) → C p → C (bit b p)) (p : SNum) :

C p

A dependent induction principle for SNum which avoids relying on NzsNum.

Equations

SNum.drec' z s (SNum.zero z_1) = z z_1
SNum.drec' z s (SNum.nz p) = NzsNum.drec' z s p

source

def SNum.rec' {α : Sort u_1} (z : Bool → α) (s : Bool → SNum → α → α) :

SNum → α

An induction principle for SNum which avoids relying on NzsNum.

Equations

SNum.rec' z s = SNum.drec' z s

source

def SNum.testBit :

ℕ → SNum → Bool

SNum.testBit n a is true iff the n-th bit (starting from the LSB) of a is active. If the size of a is less than n, this evaluates to false.

Equations