76 lines
1.6 KiB
Text
76 lines
1.6 KiB
Text
-- 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?
|