Binary representation of integers using inductive types #
Note: Unlike in Coq, where this representation is preferred because of
the reliance on kernel reduction, in Lean this representation is discouraged
in favor of the "Peano" natural numbers Nat
, and the purpose of this
collection of theorems is to show the equivalence of the different approaches.
Addition of two PosNum
s.
Equations
- PosNum.add PosNum.one x = PosNum.succ x
- PosNum.add x PosNum.one = PosNum.succ x
- PosNum.add (PosNum.bit0 a) (PosNum.bit0 b) = PosNum.bit0 (PosNum.add a b)
- PosNum.add (PosNum.bit1 a) (PosNum.bit1 b) = PosNum.bit0 (PosNum.succ (PosNum.add a b))
- PosNum.add (PosNum.bit0 a) (PosNum.bit1 b) = PosNum.bit1 (PosNum.add a b)
- PosNum.add (PosNum.bit1 a) (PosNum.bit0 b) = PosNum.bit1 (PosNum.add a b)
Instances For
The predecessor of a PosNum
as a Num
.
Equations
- PosNum.pred' PosNum.one = 0
- PosNum.pred' (PosNum.bit0 n) = Num.pos (Num.casesOn (PosNum.pred' n) 1 PosNum.bit1)
- PosNum.pred' (PosNum.bit1 n) = Num.pos (PosNum.bit0 n)
Instances For
The number of bits of a PosNum
, as a PosNum
.
Equations
- PosNum.size PosNum.one = 1
- PosNum.size (PosNum.bit0 n) = PosNum.succ (PosNum.size n)
- PosNum.size (PosNum.bit1 n) = PosNum.succ (PosNum.size n)
Instances For
Multiplication of two PosNum
s.
Equations
- PosNum.mul a PosNum.one = a
- PosNum.mul a (PosNum.bit0 n) = PosNum.bit0 (PosNum.mul a n)
- PosNum.mul a (PosNum.bit1 n) = PosNum.bit0 (PosNum.mul a n) + a
Instances For
Ordering of PosNum
s.
Equations
- PosNum.cmp PosNum.one PosNum.one = Ordering.eq
- PosNum.cmp x PosNum.one = Ordering.gt
- PosNum.cmp PosNum.one x = Ordering.lt
- PosNum.cmp (PosNum.bit0 a) (PosNum.bit0 b) = PosNum.cmp a b
- PosNum.cmp (PosNum.bit0 a) (PosNum.bit1 b) = Ordering.casesOn (PosNum.cmp a b) Ordering.lt Ordering.lt Ordering.gt
- PosNum.cmp (PosNum.bit1 a) (PosNum.bit0 b) = Ordering.casesOn (PosNum.cmp a b) Ordering.lt Ordering.gt Ordering.gt
- PosNum.cmp (PosNum.bit1 a) (PosNum.bit1 b) = PosNum.cmp a b
Instances For
@[deprecated]
castPosNum
casts a PosNum
into any type which has 1
and +
.
Equations
- ↑PosNum.one = 1
- ↑(PosNum.bit0 n) = bit0 ↑n
- ↑(PosNum.bit1 n) = bit1 ↑n
Instances For
bitm1 x
appends a 1
to the end of x
, mapping x
to 2 * x - 1
.
Instances For
Subtraction of two PosNum
s, producing a ZNum
.
Equations
- PosNum.sub' x PosNum.one = Num.toZNum (PosNum.pred' x)
- PosNum.sub' PosNum.one x = Num.toZNumNeg (PosNum.pred' x)
- PosNum.sub' (PosNum.bit0 a) (PosNum.bit0 b) = ZNum.bit0 (PosNum.sub' a b)
- PosNum.sub' (PosNum.bit0 a) (PosNum.bit1 b) = ZNum.bitm1 (PosNum.sub' a b)
- PosNum.sub' (PosNum.bit1 a) (PosNum.bit0 b) = ZNum.bit1 (PosNum.sub' a b)
- PosNum.sub' (PosNum.bit1 a) (PosNum.bit1 b) = ZNum.bit0 (PosNum.sub' a b)
Instances For
Auxiliary definition for PosNum.divMod
.
Instances For
divMod x y = (y / x, y % x)
.
Equations
- PosNum.divMod d (PosNum.bit0 n) = match PosNum.divMod d n with | (q, r₁) => PosNum.divModAux d q (Num.bit0 r₁)
- PosNum.divMod d (PosNum.bit1 n) = match PosNum.divMod d n with | (q, r₁) => PosNum.divModAux d q (Num.bit1 r₁)
- PosNum.divMod d PosNum.one = PosNum.divModAux d 0 1
Instances For
Auxiliary definition for Num.gcd
.
Equations
- Num.gcdAux 0 x x = x
- Num.gcdAux (Nat.succ n) Num.zero x = x
- Num.gcdAux (Nat.succ n) x x = Num.gcdAux n (x % x) x