Bitwise "or" for PosNum
.
Equations
- PosNum.lor PosNum.one (PosNum.bit0 q) = PosNum.bit1 q
- PosNum.lor PosNum.one x = x
- PosNum.lor (PosNum.bit0 p) PosNum.one = PosNum.bit1 p
- PosNum.lor x PosNum.one = x
- PosNum.lor (PosNum.bit0 p) (PosNum.bit0 q) = PosNum.bit0 (PosNum.lor p q)
- PosNum.lor (PosNum.bit0 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)
- PosNum.lor (PosNum.bit1 p) (PosNum.bit0 q) = PosNum.bit1 (PosNum.lor p q)
- PosNum.lor (PosNum.bit1 p) (PosNum.bit1 q) = PosNum.bit1 (PosNum.lor p q)
Bitwise "and" for PosNum
.
Equations
- PosNum.land PosNum.one (PosNum.bit0 q) = 0
- PosNum.land PosNum.one x = 1
- PosNum.land (PosNum.bit0 p) PosNum.one = 0
- PosNum.land x PosNum.one = 1
- PosNum.land (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit0 (PosNum.land p q)
- PosNum.land (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit1 (PosNum.land p q)
Bitwise fun a b ↦ a && !b↦ a && !b
for PosNum
. For example, ldiff 5 9 = 4
:
101
1001
----
100
Equations
- PosNum.ldiff PosNum.one (PosNum.bit0 a) = 1
- PosNum.ldiff PosNum.one x = 0
- PosNum.ldiff (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.ldiff (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.ldiff (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.ldiff p q)
- PosNum.ldiff (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.ldiff p q)
Bitwise "xor" for PosNum
.
Equations
- PosNum.lxor PosNum.one PosNum.one = 0
- PosNum.lxor PosNum.one (PosNum.bit0 q) = Num.pos (PosNum.bit1 q)
- PosNum.lxor PosNum.one (PosNum.bit1 q) = Num.pos (PosNum.bit0 q)
- PosNum.lxor (PosNum.bit0 p) PosNum.one = Num.pos (PosNum.bit1 p)
- PosNum.lxor (PosNum.bit1 p) PosNum.one = Num.pos (PosNum.bit0 p)
- PosNum.lxor (PosNum.bit0 p) (PosNum.bit0 q) = Num.bit0 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit0 p) (PosNum.bit1 q) = Num.bit1 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit1 p) (PosNum.bit0 q) = Num.bit1 (PosNum.lxor p q)
- PosNum.lxor (PosNum.bit1 p) (PosNum.bit1 q) = Num.bit0 (PosNum.lxor p q)
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
- PosNum.testBit PosNum.one 0 = true
- PosNum.testBit PosNum.one x = false
- PosNum.testBit (PosNum.bit0 a) 0 = false
- PosNum.testBit (PosNum.bit0 p) (Nat.succ n) = PosNum.testBit p n
- PosNum.testBit (PosNum.bit1 a) 0 = true
- PosNum.testBit (PosNum.bit1 p) (Nat.succ n) = PosNum.testBit p n
n.oneBits 0
is the list of indices of active bits in the binary representation of n
.
Equations
- PosNum.oneBits PosNum.one x = [x]
- PosNum.oneBits (PosNum.bit0 p) x = PosNum.oneBits p (x + 1)
- PosNum.oneBits (PosNum.bit1 p) x = x :: PosNum.oneBits p (x + 1)
Left-shift the binary representation of a PosNum
.
Equations
- PosNum.shiftl x 0 = x
- PosNum.shiftl x (Nat.succ n) = PosNum.shiftl (PosNum.bit0 x) n
Right-shift the binary representation of a PosNum
.
Equations
- PosNum.shiftr x 0 = Num.pos x
- PosNum.shiftr PosNum.one x = 0
- PosNum.shiftr (PosNum.bit0 p) (Nat.succ n) = PosNum.shiftr p n
- PosNum.shiftr (PosNum.bit1 p) (Nat.succ n) = PosNum.shiftr p n
Left-shift the binary representation of a Num
.
Equations
- Num.shiftl x x = match x, x with | Num.zero, x => 0 | Num.pos p, n => Num.pos (PosNum.shiftl p n)
Right-shift the binary representation of a Num
.
Equations
- Num.shiftr x x = match x, x with | Num.zero, x => 0 | Num.pos p, n => PosNum.shiftr p n
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.testBit x x = match x, x with | Num.zero, x => false | Num.pos p, n => PosNum.testBit p n
n.oneBits
is the list of indices of active bits in the binary representation of n
.
Equations
- Num.oneBits x = match x with | Num.zero => [] | Num.pos p => PosNum.oneBits p 0
Equations
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
Instances For
Equations
- instInhabitedNzsNum = { default := 1 }
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.
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))
Sign of a NzsNum
.
Equations
- NzsNum.sign (NzsNum.msb b) = !b
- NzsNum.sign (NzsNum.bit a p) = NzsNum.sign p
Equations
- NzsNum.not (NzsNum.msb b) = NzsNum.msb (decide ¬b = true)
- NzsNum.not (NzsNum.bit a p) = NzsNum.bit (decide ¬a = true) (NzsNum.not p)
Equations
- NzsNum.«term~_» = Lean.ParserDescr.node `NzsNum.term~_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))
Add an inactive bit at the end of a NzsNum
. This mimics PosNum.bit0
.
Equations
Add an active bit at the end of a NzsNum
. This mimics PosNum.bit1
.
Equations
The head
of a NzsNum
is the boolean value of its LSB.
Equations
- NzsNum.head x = match x with | NzsNum.msb b => b | NzsNum.bit b a => b
The tail
of a NzsNum
is the SNum
obtained by removing the LSB.
Edge cases: tail 1 = 0
and tail (-2) = -1
.
Equations
- NzsNum.tail x = match x with | NzsNum.msb b => SNum.zero (decide ¬b = true) | NzsNum.bit a p => SNum.nz p
Equations
- SNum.«term~_» = Lean.ParserDescr.node `SNum.term~_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 100))
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))
A dependent induction principle for NzsNum
, with base cases
0 : SNum
and (-1) : SNum
.
Equations
- NzsNum.drec' z s (NzsNum.msb b) = Eq.mpr (_ : C (SNum.nz (NzsNum.msb b)) = C (SNum.bit b (SNum.zero (decide ¬b = true)))) (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)
A dependent induction principle for SNum
which avoids relying on NzsNum
.
Equations
- SNum.drec' z s x = match x with | SNum.zero b => z b | SNum.nz p => NzsNum.drec' z s p
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
- SNum.testBit 0 x = SNum.head x
- SNum.testBit (Nat.succ n) x = SNum.testBit n (SNum.tail x)
SNum.czAdd a b n
is n + a - b
(where a
and b
should be read as either 0 or 1).
This is useful to implement the carry system in cAdd
.