-- This focuses more on the programming and type and programming
-- side of lean than proving type.  All done here can be done in haskell.

-- Pat = Pranshu's nat
inductive Pat where
  | zero : Pat
  | succ (p : Pat) : Pat

-- ntp stands for nat to pat
def ntp (n : Nat) : Pat :=
 match n with
  | 0 => Pat.zero
  | n'+1 => Pat.succ (ntp n')

-- ptn = pat to nat
def ptn (p : Pat) : Nat :=
 match p with
  | Pat.zero => 0
  | Pat.succ n => 1 + ptn n

-- True
#eval let a := 10 ; (ptn (ntp a)) == a
-- TODO prove properly using theorem or something

-- in haskell this would be
-- data Pat = Zero | Succ Pat

def isZero (p : Pat) : Bool :=
 match p with
  | Pat.zero => true
  | Pat.succ _ => false

-- This is true
#eval isZero Pat.zero

------- Now I make basic functions -------

def plus (l : Pat) (r : Pat) : Pat :=
 match l with
  | Pat.zero => r
  | Pat.succ p => plus p (Pat.succ r)

-- (Pat.succ Pat.zero)
#eval plus Pat.zero (Pat.succ Pat.zero)

-- (Pat.succ Pat.zero)
#eval plus (Pat.succ Pat.zero) Pat.zero

-- (Pat.succ (Pat.succ Pat.zero))
#eval plus (Pat.succ Pat.zero) (Pat.succ Pat.zero)

-- Pred is like `- 1`
def pred (p : Pat) : Pat :=
  match p with
  | Pat.zero => Pat.zero
  | Pat.succ k => k

def sub (l : Pat) (r : Pat) : Pat :=
 match r with
  | Pat.zero => l
  | Pat.succ p => pred (sub l p)

def greater_than (p : Pat) (k : Pat) : Bool :=
 match sub p k with
   | Pat.zero => false
   | _ => true

-- False
#eval greater_than (ntp 2) (ntp 3)

-- -- ERROR 'failed to prove termination'
-- def div (n : Pat) (k : Pat) : Pat :=
--   if greater_than k n 
--     then Pat.zero
--   else Pat.succ (div (sub n k) k)
-- termination_by?