module bin where

open import Data.Nat

open import Relation.Binary.PropositionalEquality 

{- \bn is too awkward to type, so let's define an alias -}

Nat = ℕ


-- Main data type of the day : binary number of N bits

data Binnum : Nat -> Set where
  eod : Binnum zero
  b0 : {n : Nat} -> Binnum n -> Binnum (suc n)
  b1 : {n : Nat} -> Binnum n -> Binnum (suc n)


-- bzero n = n bits of zero
bzero : (n : Nat) -> Binnum n
bzero zero = eod
bzero (suc n) = b0 (bzero n)

-- bzero n = n bits of 1
ball : (n : Nat) -> Binnum n
ball zero = eod
ball (suc n) = b1 (ball n)

-- bone : 1 in binary
bone : (n : Nat) -> Binnum n
bone zero = eod
bone (suc n) = b1 (bzero n)

-- invert all bits
invert : {n : Nat} -> Binnum n -> Binnum n
invert eod = eod
invert (b0 a) = b1 (invert a)
invert (b1 a) = b0 (invert a)

-- n + 1 % (2^n)
bsuc : {n : Nat} -> Binnum n -> Binnum n
bsuc eod = eod
bsuc (b0 n) = b1 n
bsuc (b1 n) = b0 (bsuc n)


-- For  testing
-- Let's check that suc is actually working

b0x0 = (b0 (b0 (b0 (b0 eod))))
b0x1 = (b1 (b0 (b0 (b0 eod))))
b0x2 = (b0 (b1 (b0 (b0 eod))))
b0x3 = (b1 (b1 (b0 (b0 eod))))
b0x4 = (b0 (b0 (b1 (b0 eod))))
b0x5 = (b1 (b0 (b1 (b0 eod))))
b0x6 = (b0 (b1 (b1 (b0 eod))))
b0x7 = (b1 (b1 (b1 (b0 eod))))
b0x8 = (b0 (b0 (b0 (b1 eod))))
b0x9 = (b1 (b0 (b0 (b1 eod))))
b0xA = (b0 (b1 (b0 (b1 eod))))
b0xB = (b1 (b1 (b0 (b1 eod))))
b0xC = (b0 (b0 (b1 (b1 eod))))
b0xD = (b1 (b0 (b1 (b1 eod))))
b0xE = (b0 (b1 (b1 (b1 eod))))
b0xF = (b1 (b1 (b1 (b1 eod))))

test_suc0 : (bsuc b0x0) ≡ (b0x1)
test_suc0 = refl

test_suc1 : (bsuc b0x1) ≡ (b0x2)
test_suc1 = refl

test_suc2 : (bsuc b0x2) ≡ (b0x3)
test_suc2 = refl

test_suc3 : (bsuc b0x3) ≡ (b0x4)
test_suc3 = refl

test_suc4 : (bsuc b0x4) ≡ (b0x5)
test_suc4 = refl

test_suc5 : (bsuc b0x5) ≡ (b0x6)
test_suc5 = refl

test_suc6 : (bsuc b0x6) ≡ (b0x7)
test_suc6 = refl

test_suc7 : (bsuc b0x7) ≡ (b0x8)
test_suc7 = refl

test_suc8 : (bsuc b0x8) ≡ (b0x9)
test_suc8 = refl

test_suc9 : (bsuc b0x9) ≡ (b0xA)
test_suc9 = refl

test_sucA : (bsuc b0xA) ≡ (b0xB)
test_sucA = refl

test_sucB : (bsuc b0xB) ≡ (b0xC)
test_sucB = refl

test_sucC : (bsuc b0xC) ≡ (b0xD)
test_sucC = refl

test_sucD : (bsuc b0xD) ≡ (b0xE)
test_sucD = refl

test_sucE : (bsuc b0xE) ≡ (b0xF)
test_sucE = refl

test_sucF : (bsuc b0xF) ≡ (b0x0)
test_sucF = refl


-- Now let's prove that one is a successor of zero
bone-is-suc0 : (n : Nat) -> (bsuc (bzero n)) ≡ (bone n)
bone-is-suc0 zero = refl
bone-is-suc0 (suc n) = refl

-- Main auxfunction of the day: (l1 ≡ l2) -> (f l1 ≡ f l2)
f-equal : {LHS RHS : Set} -> (f : LHS -> RHS) -> (l1 : LHS) -> (l2 : LHS) -> (l1 ≡ l2) -> (f l1 ≡ f l2)
f-equal f .l2 l2 refl = refl


-- Let's prove that overflow resets all bits to 0
overflow-to-zero : (n : Nat) -> (bsuc (ball n)) ≡ (bzero n)
overflow-to-zero zero = refl
overflow-to-zero (suc n) = f-equal b0 (bsuc (ball n)) (bzero n) (overflow-to-zero n)


-- Define xor
xor : {n : Nat} -> Binnum n -> Binnum n -> Binnum n
xor eod b = eod
xor (b0 a) (b0 b) = b0 (xor a b)
xor (b1 a) (b0 b) = b1 (xor a b)
xor (b0 a) (b1 b) = b1 (xor a b)
xor (b1 a) (b1 b) = b0 (xor a b)

-- Test that a ^ 0 = a
xor-zero : (n : Nat) -> (a : Binnum n) -> (xor a (bzero n)) ≡ a
xor-zero .0 eod = refl
xor-zero .(suc n) (b0 {n} a) = f-equal b0 (xor a (bzero n)) a (xor-zero n a)
xor-zero .(suc n) (b1 {n} a) = f-equal b1 (xor a (bzero n)) a (xor-zero n a)

-- Test that a ^ 0xfffff...ffff = a 
xor-ball : (n : Nat) -> (a : Binnum n) -> (xor a (ball n)) ≡ (invert a)
xor-ball .0 eod = refl
xor-ball .(suc n) (b0 {n} a) = f-equal b1 (xor a (ball n)) (invert a) (xor-ball n a)
xor-ball .(suc n) (b1 {n} a) = f-equal b0 (xor a (ball n)) (invert a) (xor-ball n a)


-- Define plus (which is not needed per se, but it's used to prove correctness of unary minus)
bplus : {n : Nat} -> Binnum n -> Binnum n -> Binnum n
bplus eod eod = eod
bplus (b0 a) (b0 b) = b0 (bplus a b)
bplus (b0 a) (b1 b) = b1 (bplus a b)
bplus (b1 a) (b0 b) = b1 (bplus a b)
bplus (b1 a) (b1 b) = b0 (bplus (bsuc a) b)



-- While we are at it, let's prove that a+0 = a
bplus-zero-r : (n : Nat) -> (a : Binnum n) -> bplus a (bzero n) ≡ a
bplus-zero-r .0 eod = refl
bplus-zero-r .(suc n) (b0 {n} a) = f-equal b0 (bplus a (bzero n)) a (bplus-zero-r n a)
bplus-zero-r .(suc n) (b1 {n} a) = f-equal b1 (bplus a (bzero n)) a (bplus-zero-r n a)

-- and that a + 1 is successor of a
bplus-one-r : (n : Nat) -> (a : Binnum n) -> (bplus a (bone n)) ≡ (bsuc a)
bplus-one-r .0 eod = refl
bplus-one-r .(suc n) (b0 {n} a) = f-equal b1 (bplus a (bzero n)) a (bplus-zero-r n a)
bplus-one-r .(suc n) (b1 {n} a) = f-equal b0 (bplus (bsuc a) (bzero n)) (bsuc a) (bplus-zero-r n (bsuc a)) 



-- Define and
band : {n : Nat} -> Binnum n -> Binnum n -> Binnum n
band eod b = eod
band (b0 a) (b0 b) = b0 (band a b)
band (b0 a) (b1 b) = b0 (band a b)
band (b1 a) (b0 b) = b0 (band a b)
band (b1 a) (b1 b) = b1 (band a b)

-- Prove that a & a = a
band-xx : {n : Nat} -> (a : Binnum n) -> (band a a) ≡ a
band-xx eod = refl
band-xx (b0 a) = f-equal b0 (band a a) a (band-xx a)
band-xx (b1 a) = f-equal b1 (band a a) a (band-xx a)

-- Prove that a & ~a = 0. 
-- We'll need this proof later.
band-invert : (n : Nat) -> (a : Binnum n) -> band a (invert a) ≡ bzero n
band-invert .0 eod = refl
band-invert .(suc n) (b0 {n} a) = f-equal b0 (band a (invert a)) (bzero n) (band-invert n a)
band-invert .(suc n) (b1 {n} a) = f-equal b0 (band a (invert a)) (bzero n) (band-invert n a) 


-- Negatives are hard. 
buminus : {n : Nat} -> Binnum n -> Binnum n
buminus a =  bsuc (invert a)

-- So let's proof that it's actually unary minus by proving
-- -a + a = 0
buminus-is-correct : (n : Nat) ->  (a : Binnum n) -> (bplus (buminus a) a) ≡ (bzero n)
buminus-is-correct .0 eod = refl
buminus-is-correct .(suc n) (b0 {n} a) = f-equal b0 (bplus (buminus a) a) (bzero n) (buminus-is-correct n a)
buminus-is-correct .(suc n) (b1 {n} a) = f-equal b0 (bplus (bsuc (invert a)) a) (bzero n) (buminus-is-correct n a)

-- Now let's define a function for extracting LSB
lsb : {n : Nat} -> Binnum n -> Binnum n
lsb eod = eod
lsb (b0  a) = b0 (lsb a)
lsb .{suc n} (b1 {n} a) = b1 (bzero n)

-- And now let's put all pieces together
main-theorem : (n : Nat) -> (a : Binnum n) -> (band a (buminus a)) ≡ (lsb a)
main-theorem .0 eod = refl
main-theorem .(suc n) (b0 {n} a) = f-equal b0 (band a (bsuc (invert a))) (lsb a) (main-theorem n a)
main-theorem .(suc n) (b1 {n} a) = f-equal b1 (band a (invert a)) (bzero n) (band-invert n a)

Nat = ℕ  -- это юникодовый знак натуральных чисел 

test_suc0 : (bsuc b0x0) ≡ (b0x1) -- 8801 это эквивалентность  (как равно=, но с тремя чертами)
test_suc0 = refl