prim_rec_prim_eval.lean

inductive prim_rec: nat -> Type
| zero: prim_rec 0
| succ: prim_rec 1
| proj: forall {n}, fin n -> prim_rec n
| comp: forall {k m}, prim_rec k -> (fin k -> prim_rec m) -> prim_rec m
| prec: forall {k}, prim_rec k -> prim_rec (k + 2) -> prim_rec (k + 1)


def curry {k} (v: nat) (a: fin k -> nat): fin (k + 1) -> nat :=
begin
  intro arg,
  cases arg with val is_lt,
  cases val with val',
  exact v, -- arg(0) = v
  apply a,
  existsi val',
  apply nat.lt_of_succ_lt_succ,
  exact is_lt,
end


def uncurry {k} (a: fin (k + 1) -> nat): prod nat (fin k -> nat) :=
begin
  split,
  exact a 0,
  intro arg,
  cases arg with val is_lt,
  apply a,
  split,
  show val + 1 < k + 1,
  apply nat.succ_lt_succ,
  exact is_lt,
end


def prim_eval : forall {k}, prim_rec k -> (fin k -> nat) -> nat
| 0 prim_rec.zero _arg := 0
| 1 prim_rec.succ arg := arg 0 + 1
| m (prim_rec.proj idx) arg := arg idx
| m (@prim_rec.comp k .(m) (f: prim_rec k) g) arg
  := prim_eval f (fun i, prim_eval (g i) arg)
| .(_) (@prim_rec.prec k f g) arg :=
  let h :=
  fun (v: nat) (arg: fin k -> nat),
  @nat.rec (fun _, nat) (prim_eval f arg)
    (fun (v': nat) (prev: nat), prim_eval g (curry prev (curry v' arg))) v in
  let ⟨x, y⟩ := uncurry arg in
  h x y