murec.v

Section MU_RECURSIVE.

#[local] Close Scope list_scope.
#[local] Open Scope vector_scope.

Let arity : Set := nat.

Inductive MuRec : arity -> Set :=
  | MR_succ : MuRec 1
  | MR_zero : MuRec 0
  | MR_proj (n : arity) (i : Fin.t n) : MuRec n
  | MR_compose (n : arity) (m : arity) (g : MuRecs n m) (h : MuRec m) : MuRec n
  | MR_primRec (n : arity) (g : MuRec n) (h : MuRec (S (S n))) : MuRec (S n)
  | MR_mu (n : arity) (g : MuRec (S n)) : MuRec n
with MuRecs : arity -> arity -> Set :=
  | MRs_nil (n : arity) : MuRecs n 0
  | MRs_cons (n : arity) (m : arity) (f : MuRec n) (fs : MuRecs n m) : MuRecs n (S m).

Inductive MuRecGraph : forall n, MuRec n -> Vector.t nat n -> nat -> Set :=
  | MRG_succ x
    : MuRecGraph 1 (MR_succ) [x] (S x)
  | MRG_zero
    : MuRecGraph 0 (MR_zero) [] (O)
  | MRG_proj n xs i
    : MuRecGraph n (MR_proj n i) xs (xs !! i)
  | MRG_compose n m g h xs ys z
    (g_spec : MuRecsGraph n m g xs ys)
    (h_spec : MuRecGraph m h ys z)
    : MuRecGraph n (MR_compose n m g h) xs z
  | MRG_primRec_O n g h xs z
    (g_spec : MuRecGraph n g xs z)
    : MuRecGraph (S n) (MR_primRec n g h) (O :: xs) z
  | MRG_primRec_S n g h xs a acc z
    (ACC : MuRecGraph (S n) (MR_primRec n g h) (a :: xs) acc)
    (h_spec : MuRecGraph (S (S n)) h (a :: acc :: xs) z)
    : MuRecGraph (S n) (MR_primRec n g h) (S a :: xs) z
  | MRG_mu n g xs z
    (MU : MuRecGraph (S n) g (z :: xs) 0)
    (* (MIN : forall y, MuRecGraph (S n) g (y :: xs) 0 -> y >= z) *)
    : MuRecGraph n (MR_mu n g) xs z
with MuRecsGraph : forall n, forall m, MuRecs n m -> Vector.t nat n -> Vector.t nat m -> Set :=
  | MRG_nil n xs
    : MuRecsGraph n 0 (MRs_nil n) xs []
  | MRG_cons n m f fs xs y ys
    (HEAD : MuRecGraph n f xs y)
    (TAIL : MuRecsGraph n m fs xs ys)
    : MuRecsGraph n (S m) (MRs_cons n m f fs) xs (y :: ys).

End MU_RECURSIVE.