(* The correctness of CBN TDPE, tested on Coq 8.4pl2 (Oct 2013) ****)

Require Import FunctionalExtensionality.

(* type ************************************************************)
Inductive typ : Set :=
| base  : typ
| arrow : typ -> typ -> typ.

(* term, normal form, neutral term *********************************)
Inductive tm (var: typ -> Type) : typ -> Type :=
| tm_Var : forall A, var A -> tm var A
| tm_Lam : forall A B, (var A -> tm var B) -> tm var (arrow A B)
| tm_App : forall A B, tm var (arrow A B) -> tm var A -> tm var B.

Arguments tm_Var [var A] _.
Arguments tm_Lam [var A B] _.
Arguments tm_App [var A B] _ _.

Definition TM A := forall var, tm var A.

Inductive nf (var: typ -> Type) : typ -> Type :=
| nf_Lam : forall A B, (var A -> nf var B) -> nf var (arrow A B)
| nf_ne  : ne var base -> nf var base
with ne (var: typ -> Type) : typ -> Type :=
| ne_Var : forall A, var A -> ne var A
| ne_App : forall A B, ne var (arrow A B) -> nf var A -> ne var B.

Arguments nf_Lam [var A B] _.
Arguments nf_ne  [var] _.
Arguments ne_Var [var A] _.
Arguments ne_App [var A B] _ _.

Definition NF A := forall var, nf var A.
Definition NE A := forall var, ne var A.

Fixpoint tm_of_nf {var A} (f: nf var A) : tm var A := match f with
| nf_Lam _ _ f' => tm_Lam (fun x => tm_of_nf (f' x))
| nf_ne e' => tm_of_ne e'
  end
with tm_of_ne {var A} (e: ne var A) : tm var A := match e with
| ne_Var _ x => tm_Var x
| ne_App _ _ e' f' => tm_App (tm_of_ne e') (tm_of_nf f')
  end.

(* examples ********************************************************)
Example TM_id : TM (arrow base base) := fun var =>
  tm_Lam (fun x => tm_Var x).

Example TM_id': TM (arrow base base) := fun var =>
  tm_Lam (fun x => tm_App (tm_Lam (fun y => tm_Var y)) (tm_Var x)).

Example TM_id2 : TM (arrow (arrow base base) (arrow base base)) := fun var =>
  tm_Lam (fun x => tm_Var x).

Example TM_id3 : TM (arrow base base) := fun var =>
  tm_App (TM_id2 var) (TM_id var).

Example TM_s : TM (arrow (arrow base (arrow base base))
                         (arrow (arrow base base)
                                (arrow base base))) := fun var =>
  tm_Lam (fun x => tm_Lam (fun y => tm_Lam (fun z =>
    tm_App (tm_App (tm_Var x) (tm_Var z))
           (tm_App (tm_Var y) (tm_Var z))))).

Example TM_k : TM (arrow base (arrow base base)) := fun var =>
  tm_Lam (fun x => tm_Lam (fun y => tm_Var x)).

(* V ***************************************************************)
Fixpoint V b (A: typ) : Type := match A with
| base => b
| arrow A B => V b A -> V b B
  end.

(* soundness *******************************************************)
Theorem soundness': forall b {A}, tm (V b) A -> V b A.
Proof.
intros b A t.
induction t.
(**) assumption.
(**) simpl.
     intros.
     apply X.
     assumption.
(**) apply IHt1.
     apply IHt2.
Qed.

Fixpoint soundness b {A} (t: tm (V b) A) : V b A :=
  match t with
| tm_Var _ x => x
| tm_Lam _ _ t1 => fun x => soundness b (t1 x)
| tm_App _ _ t1 t2 => (soundness b t1) (soundness b t2)
  end.

Theorem soundness2': forall b (A: typ) (T: TM A), V b A.
Proof.
intros.
apply soundness.
unfold TM in T.
apply T.
Qed.

Definition soundness2 b {A} (T: TM A) := soundness b (T (V b)).

(* completeness ****************************************************)
Theorem reify': forall var A, V (ne var base) A -> nf var A
with  reflect': forall var A, ne var A -> V (ne var base) A.
Proof.
(* reify *)
induction A; intros; simpl in X.
(**) apply nf_ne.
     assumption.
(**) apply nf_Lam.
     intros.
     apply IHA2.
     apply X.
     apply reflect'.
     apply ne_Var.
     assumption.
(* reflect *)
induction A; intros; simpl.
(**) assumption.
(**) intros.
     apply IHA2.
     apply (@ne_App _ A1).
     assumption.
     apply reify'.
     assumption.
Qed.

Fixpoint reify (var: typ -> Type) (A: typ) :=
  match A return V (ne var base) A -> nf var A with
| base => fun v => nf_ne v
| arrow A B => fun v =>
    nf_Lam (fun x => reify var B (v (reflect var A (ne_Var x))))
  end
with reflect (var: typ -> Type) (A: typ) :=
  match A return ne var A -> V (ne var base) A with
| base => fun e => e
| arrow A B => fun e v => reflect var B (ne_App e (reify var A v))
  end.

(* interp **********************************************************)
Definition interp_nf b {A} (f: nf (V b) A) (v: V b A) :=
  soundness b (tm_of_nf f) = v.

Definition interp_ne b {A} (e: ne (V b) A) (v: V b A) :=
  soundness b (tm_of_ne e) = v.

(* meaning of term families (Lemma 3 of Filinski PPDP'99) **********)
Proposition interp_nf_ne: forall b (e: ne (V b) base) v,
  interp_ne b e v -> interp_nf b (nf_ne e) v.
Proof.
  auto.
Qed.

Proposition interp_nf_Lam: forall b A B
        (f: V b A -> nf (V b) B) (v: V b (arrow A B)),
  (forall v', interp_nf b (f v') (v v')) ->
  interp_nf b (nf_Lam f) v.
Proof.
  intros.
  unfold interp_nf.
  simpl.
  extensionality x.
  unfold interp_nf in H.
  apply H.
Qed.

Proposition interp_ne_Var: forall b A (v: V b A),
  interp_ne b (ne_Var v) v.
Proof.
  intros.
  unfold interp_ne.
  simpl.
  reflexivity.
Qed.

Proposition interp_ne_App: forall b A B
        (e: ne (V b) (arrow A B)) e' f f',
  interp_ne b e e' ->
  interp_nf b f f' ->
  interp_ne b (ne_App e f) (e' f').
Proof.
  intros.
  unfold interp_ne.
  unfold interp_ne in H.
  unfold interp_nf in H0.
  simpl.
  rewrite H.
  rewrite H0.
  reflexivity.
Qed.

(* R (Definition 8) ************************************************)
Fixpoint R b (A: typ) :=
  match A return V (ne (V b) base) A -> V b A -> Type with
| base => fun e v => interp_ne b e v
| arrow A B => fun e v => forall e' v',
    R b A e' v' -> R b B (e e') (v v')
  end.

(* completeness (Lemma 6) ******************************************)
Lemma reify_R: forall b A (v: V (ne (V b) base) A) (f: V b A),
  R b A v f -> interp_nf b (reify (V b) A v) f
with reflect_R: forall b A (e: ne (V b) A) (v: V b A),
  interp_ne b e v -> R b A (reflect (V b) A e) v.
Proof.
(* reify *)
induction A; intros; simpl.
(**) apply interp_nf_ne.
     simpl in X.
     assumption.
(**) apply interp_nf_Lam; intros.
     apply IHA2.
     simpl in X.
     apply X.
     apply reflect_R.
     apply interp_ne_Var.
(* reflect *)
induction A; intros; simpl.
(**) assumption.
(**) intros.
     apply IHA2.
     apply interp_ne_App.
     (**) assumption.
     (**) apply reify_R.
          assumption.
Qed.

(* soundness (Lemma 7) *********************************************)
Inductive related_term b : forall {A},
                tm (V (ne (V b) base)) A -> tm (V b) A -> Type :=
| related_Var : forall A (v: V (ne (V b) base) A) (v': V b A),
                R b A v v' ->
                related_term b (tm_Var v) (tm_Var v')
| related_Lam : forall A B
                (t: V (ne (V b) base) A -> tm (V (ne (V b) base)) B)
                (t': V b A -> tm (V b) B),
                (forall v v', R b A v v' ->
                              related_term b (t v) (t' v')) ->
                related_term b (tm_Lam t) (tm_Lam t')
| related_App : forall A B (t1: tm (V (ne (V b) base)) (arrow A B))
                           (t1': tm (V b) (arrow A B)) t2 t2',
                related_term b t1 t1' ->
                related_term b t2 t2' ->
                related_term b (tm_App t1 t2) (tm_App t1' t2').

Axiom T_related: forall b A (T: TM A),
  related_term b (T (V (ne (V b) base))) (T (V b)).

Lemma main': forall b A t1 t2,
  related_term b t1 t2 ->
  R b A (soundness (ne (V b) base) t1) (soundness b t2).
Proof.
intros.
induction X; simpl.
(**) assumption.
(**) intros.
     apply X. assumption.
(**) simpl in IHX1.
     apply IHX1.
     assumption.
Qed.

Lemma main: forall b A (T: TM A),
  R b A (soundness2 (ne (V b) base) T) (soundness2 b T).
Proof.
intros.
unfold soundness2.
apply main'.
apply T_related.
Qed.

Theorem correctness: forall b A (T: TM A),
  interp_nf b (reify (V b) A (soundness2 (ne (V b) base) T))
              (soundness2 b T).
Proof.
intros.
apply reify_R.
apply main.
Qed.

(* example *********************************************************)
Axiom var: typ -> Type.

Lemma TM_id'_related: forall b,
  related_term b (TM_id' (V (ne (V b) base))) (TM_id' (V b)).
Proof.
repeat intro; repeat (constructor; simpl; intuition).
Qed.

Eval compute in (reify var (arrow base base)
                           (soundness2 (ne var base) TM_id')).

Eval compute in (reify var _ (soundness2 _ TM_id')).

(* vim: set tw=0 columns=140: *)