-- Project: Binary numbers
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Name: _______________________
--
-- ============================================================
--
-- Projects must be done individually. You may not collaborate with
-- other students, and you may not use AI tools. If you have questions
-- or are stuck, ask the instructor.
--
-- You may use, among other things, `rfl`, the equality rules from
-- Lecture 8 (`Eq.symm`, `Eq.trans`, `congrArg`, `calc`, ...), and the
-- basic arithmetic lemmas in `Nat` (type `Nat.` to explore them).
--
-- In many places, you will need additional lemmas. Some are suggested
-- below. Please state and prove your own lemmas as appropriate.
--
-- For full marks, complete Parts 0-4. Part 5 is a bonus.
--
-- ============================================================

set_option autoImplicit false
set_option linter.unusedVariables false

namespace Project_Binary

-- ============================================================
-- Introduction
--
-- Every positive integer can be written in binary, i.e., as a
-- sequence of binary digits 0 and 1 that starts with a 1. For
-- example, 13 is written `1101`, because 13 = 8 + 4 + 1. The goal of
-- this project is to define binary numbers as an inductive type, to
-- define some arithmetic on them, and to prove the following
-- theorem:
--
--   Every natural number has a unique binary representation.
--
-- We think of a binary number as being built from its most
-- significant digit (which is always 1) by repeatedly appending one
-- more digit on the right. Appending a 0 to the digits of a number
-- doubles the number; appending a 1 doubles it and adds 1. So `1101`
-- is built as follows:
--
--   1      = one
--   11     = bit1 one
--   110    = bit0 (bit1 one)
--   1101   = bit1 (bit0 (bit1 one))
--
-- Note that the *last* digit is the *outermost* constructor.

-- ============================================================
-- Part 0: An arithmetic toolkit
--
-- The proofs in Parts 1-5 below need a handful of facts about
-- doubling. It is a good idea to prove them once and for all here, so
-- that you do not need to do arithmetic in the middle of other
-- proofs. Prove the following. (Hint: remember that `x + (y + 1)` and
-- `(x + y) + 1` are equal by definition, but `(x + 1) + y` and
-- `(x + y) + 1` are not.)

-- 0.1
theorem succ_double (n : Nat) : (n + 1) + (n + 1) = (n + n + 1) + 1 :=
  sorry

-- 0.2
theorem double_add (a b : Nat) : (a + a) + (b + b) = (a + b) + (a + b) :=
  sorry

-- 0.3
theorem double_add_one (a b : Nat) :
    (a + a) + (b + b + 1) = (a + b) + (a + b) + 1 :=
  sorry

-- 0.4
theorem double_one_add (a b : Nat) :
    (a + a + 1) + (b + b) = (a + b) + (a + b) + 1 :=
  sorry

-- 0.5
theorem double_one_add_one (a b : Nat) :
    (a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1) :=
  sorry

-- ============================================================
-- Part 1: Positive binary numbers

-- In our formalization of binary numbers, we want to avoid the
-- problem of leading zeros. If leading zeros are permitted, then for
-- example, `101`, `0101`, and `00101` all represent the number `5`.
-- To make our binary representation unique, we therefore stipulate
-- that the leftmost digit must always be `1`. However, that does not
-- work for the number `0` itself!

-- For this reason, we start by first representing only *positive*
-- binary numbers. We will add the number `0` in Part 2 below.

-- The type of positive binary numbers.
inductive Pos : Type where
  | one : Pos             -- the number 1
  | bit0 : Pos → Pos      -- append the digit 0: p ↦ 2p
  | bit1 : Pos → Pos      -- append the digit 1: p ↦ 2p + 1

namespace Pos

  -- The string of binary digits of `p`. This is for testing and
  -- entertainment only.
  def digits : Pos → String
    | one => "1"
    | bit0 p => digits p ++ "0"
    | bit1 p => digits p ++ "1"

  #eval digits (bit1 (bit0 (bit1 one)))   --> "1101"

  -- The value of a binary number. We write `2 * n` as `n + n`, which
  -- makes the arithmetic a bit easier.
  def toNat : Pos → Nat
    | one => 1
    | bit0 p => toNat p + toNat p
    | bit1 p => toNat p + toNat p + 1

  example : toNat (bit1 (bit0 (bit1 one))) = 13 := rfl

  -- 1.1 Define the successor function on positive binary numbers.
  -- Think about how you add 1 to a binary number by hand: what
  -- happens to the last digit, and when is there a carry? Your
  -- definition should pass the tests below.
  def succ : Pos → Pos :=
    sorry

  -- Uncomment these tests when you have defined `succ`.
  -- example : succ one = bit0 one := rfl
  -- example : succ (bit0 (bit1 one)) = bit1 (bit1 one) := rfl
  -- example : succ (bit1 (bit1 one)) = bit0 (bit0 (bit0 one)) := rfl

  -- 1.2 Prove that `succ` is correct.
  theorem toNat_succ : ∀ p : Pos, toNat (succ p) = toNat p + 1 :=
    sorry

end Pos

-- ============================================================
-- Part 2: Binary numbers and existence of representations
--
-- It's time to add the number `0`, which we had excluded in Part 1.
-- A binary number is either zero, or a positive binary number.

inductive Bin : Type where
  | zero : Bin
  | pos : Pos → Bin

namespace Bin
  open Pos (one bit0 bit1)

  def digits : Bin → String
    | zero => "0"
    | pos p => p.digits

  def toNat : Bin → Nat
    | zero => 0
    | pos p => p.toNat

  -- 2.1 Define the successor function on binary numbers.
  def succ : Bin → Bin :=
    sorry

  -- 2.2
  theorem toNat_succ : ∀ b : Bin, toNat (succ b) = toNat b + 1 :=
    sorry

  -- 2.3 Define the function that converts a natural number to
  -- binary. (Hint: use `succ`.)
  def fromNat : Nat → Bin :=
    sorry

  -- Uncomment this when you have defined `fromNat`.
  -- #eval (fromNat 2026).digits     --> "11111101010"

  -- 2.4
  theorem toNat_fromNat : ∀ n : Nat, toNat (fromNat n) = n :=
    sorry

  -- 2.5 Every natural number has a binary representation.
  theorem existence : ∀ n : Nat, ∃ b : Bin, toNat b = n :=
    sorry

-- ============================================================
-- Part 3: Uniqueness of representations
--
-- In this part, we will prove that our binary representation is
-- unique, i.e., if two binary numbers represent the same natural
-- number, then they are literally equal.

-- The main step is to prove that `fromNat (toNat b) = b`. This is
-- harder than 2.4, because `fromNat` builds a number by counting up
-- one step at a time, whereas `toNat` works digit by digit. To
-- connect the two, you need to understand what `fromNat` does to a
-- number of the form `n + n`. Here are some suggested definitions and
-- lemmas.

  -- 3.1 Define the doubling function on binary numbers. It should
  -- not use `toNat` or `fromNat`.
  def double : Bin → Bin :=
    sorry

  -- 3.2
  theorem double_succ : ∀ b : Bin, double (succ b) = succ (succ (double b)) :=
    sorry

  -- 3.3
  theorem fromNat_double : ∀ n : Nat, fromNat (n + n) = double (fromNat n) :=
    sorry

  -- 3.4
  theorem fromNat_toNat_pos : ∀ p : Pos, fromNat p.toNat = pos p :=
    sorry

  -- 3.5
  theorem fromNat_toNat : ∀ b : Bin, fromNat (toNat b) = b :=
    sorry

  -- 3.6 Different binary numbers represent different natural numbers.
  theorem uniqueness : ∀ b c : Bin, toNat b = toNat c → b = c :=
    sorry

  -- 3.7 The main theorem: every natural number has a unique binary
  -- representation.
  theorem unique_representation :
      ∀ n : Nat, ∃ b : Bin, toNat b = n ∧ ∀ c : Bin, toNat c = n → c = b :=
    sorry

end Bin

-- ============================================================
-- Part 4: Addition
--
-- In this part, we will teach our binary numbers how to add. Of
-- course, we could just convert to `Nat`, add, and convert back. But
-- that would not be in the spirit of binary numbers. Instead, we add
-- digit by digit, the way you learned in elementary school, but in
-- base 2.

namespace Pos

  -- 4.1 Define addition of positive binary numbers. Do not use
  -- `toNat`. Hint: you may use `Pos.succ` to deal with carries. You
  -- will need to pattern match on both arguments at once, and it is
  -- fine for some cases to overlap; Lean uses the first case that
  -- applies.
  def add : Pos → Pos → Pos :=
    sorry

  -- Uncomment these tests when you have defined `add`.
  -- example : add one one = bit0 one := rfl
  -- example : add (bit1 (bit1 one)) (bit1 (bit0 one)) = bit0 (bit0 (bit1 one)) := rfl
  -- example : add (bit0 (bit1 one)) (bit1 (bit1 one)) = bit1 (bit0 (bit1 one)) := rfl

  -- 4.2 Prove that addition is correct. (Hint: follow the structure
  -- of your definition of `add`. This is where the toolkit pays off.)
  theorem toNat_add : ∀ p q : Pos, toNat (add p q) = toNat p + toNat q :=
    sorry

end Pos

namespace Bin

  -- 4.3 Define addition of binary numbers, using `Pos.add`.
  def add : Bin → Bin → Bin :=
    sorry

  -- 4.4 Prove the correctness of your addition function.
  theorem toNat_add : ∀ b c : Bin, toNat (add b c) = toNat b + toNat c :=
    sorry

  -- 4.5 Conversely, prove that adding natural numbers and then
  -- converting to binary gives the same result as converting to
  -- binary and then adding. (Hint: use `uniqueness`.)
  theorem fromNat_add (m n : Nat) : fromNat (m + n) = add (fromNat m) (fromNat n) :=
    sorry

end Bin

-- ============================================================
-- Part 5 (bonus): Multiplication

namespace Pos

  -- 5.1 Define multiplication of positive binary numbers. Do not use
  -- `toNat`. (Hint: recurse on the first argument only.)
  def mul : Pos → Pos → Pos :=
    sorry

  -- Uncomment this test when you have defined `mul`.
  -- example : mul (bit1 one) (bit1 (bit0 one)) = bit1 (bit1 (bit1 one)) := rfl

  -- 5.2 Prove that multiplication is correct.
  theorem toNat_mul : ∀ p q : Pos, toNat (mul p q) = toNat p * toNat q :=
    sorry

end Pos

end Project_Binary