lambda.v

From Coq Require Fin.

Definition ifun (X Y : nat -> Type) : Type := forall i, X i -> Y i.
Definition δ (X : nat -> Type) (n : nat) := X (S n).
Definition prod (X Y : nat -> Type) (n : nat) := (X n * Y n)%type.
Definition sum (X Y : nat -> Type) (n : nat) := (X n + Y n)%type.

Definition TermF' (X : nat -> Type) := sum (δ X) (prod X X).

Variant TermF (X : nat -> Type) : nat -> Type :=
| lam {n : nat} : X (S n) -> TermF X n
| app {n : nat} : X n -> X n -> TermF X n
.

Inductive Term (X : nat -> Type): nat -> Type :=
| var {n : nat} : X n -> Term X n
| cons {n : nat} : TermF (Term X) n -> Term X n
.

Arguments lam {_ _} t.
Arguments app {_ _} t1 t2.
Arguments var {_ _} x.
Arguments cons {_ _} t.

Definition map_TermF {X Y} (f : forall n, X n -> Y n) : forall n, TermF X n -> TermF Y n :=
  fun n t =>
    match t with
    | lam t1 => lam (f _ t1)
    | app t1 t2 => app (f _ t1) (f _ t2)
    end.

Fixpoint map_Term {X Y} (f : forall n, X n -> Y n) (n : nat) (t : Term X n) : Term Y n :=
  match t with
  | var x => var (f _ x)
  | cons t => cons (map_TermF (map_Term f) _ t)
  end.

Definition ret_Term {X} (n : nat) : X n -> Term X n :=
  fun x => var x.

Fixpoint μ_Term {X} (n : nat) (t : Term (Term X) n) : Term X n :=
  match t with
  | var x => x
  | cons t => cons (map_TermF μ_Term _ t)
  end.

Definition icompose {X Y Z : nat -> Type} (f : forall i, X i -> Y i) (g : forall i, Y i -> Z i) : forall i, X i -> Z i :=
  fun i x => g _ (f _ x).

Definition bind_Term {X Y} (f : forall n, X n -> Term Y n) : forall n, Term X n -> Term Y n :=
  icompose (map_Term f) μ_Term.

Definition Tm (n : nat) : Type := Term Fin.t n.

(* λx. x *)
Definition tm_id (n : nat) : Tm n :=
  cons (lam (var Fin.F1)).

(* x *)
Definition tm_x (n : nat) : Tm (S n) :=
  var Fin.F1.

(* λx. x x *)
Definition tm_ω (n : nat) : Tm n :=
  cons (lam (cons (app (var Fin.F1) (var Fin.F1)))).

(* ω ω *)
Definition tm_Ω (n : nat) : Tm n :=
  cons (app (tm_ω n) (tm_ω n)).