phoas.v

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)
| there : forall y xs, elem x xs -> elem x (y :: xs).

Arguments here  {A x xs}.
Arguments there {A x y xs} _.

Fixpoint hlist {A: Type} (I: A -> Type) (is: list A): Type :=
  match is with
    | nil => unit
    | cons j js => (I j * hlist I js) % type
  end.

Fixpoint hat {A: Type} {I: A -> Type} {is} {x} (p: elem x is): hlist I is -> I x :=
  match p with
    | here  _     => fun xs => fst xs
    | there _ _ q => fun xs => hat q (snd xs)
  end.

Module fo.

  Inductive term (g : list type): type -> Type :=
  | lam : forall s t, term (s::g) t -> term g (s ==> t)
  | app : forall s t, term g (s ==> t) -> term g s -> term g t
  | var : forall t, elem t g -> term g t.

  Arguments lam {g s t} _.
  Arguments app {g s t} _ _.
  Arguments var {g t} _.

End fo.

Module ho.

  Inductive term (v: type -> Type): type -> Type :=
  | lam : forall s t, (v s -> term v t) -> term v (s ==> t)
  | app : forall s t, term v (s ==> t) -> term v s -> term v t
  | var : forall t, v t -> term v t.

  Arguments lam {v s t} _.
  Arguments app {v s t} _ _.
  Arguments var {v t} _.
  
End ho.

Definition term t := forall v, ho.term v t.

Notation "[ t ]" := (fun _ => t).
Notation "^ v" :=
  (ho.var v) (format "^ v", at level 49).
Notation "'lambda' x -> e" :=
  (ho.lam (fun x => e)) (no associativity, at level 51, x at level 0).
Infix "@" :=
  ho.app (left associativity, at level 50).

Definition twice t : term ((t ==> t) ==> (t ==> t)) :=
  [ lambda f -> (lambda g -> lambda y -> ^f @ (^g @ ^y)) @ (lambda x -> ^f @ ^x) ].

Module wf.

  Inductive wf (g: list type) (u v: type -> Type) (i: hlist u g) (j: hlist v g):
    forall t, ho.term u t -> ho.term v t -> Prop :=
  | lam :
      forall s t (e: u s -> ho.term u t) (f: v s -> ho.term v t),
        (forall x y, wf (s::g) u v (x,i) (y,j) t (e x) (f y)) ->
        wf g u v i j (s ==> t) (lambda x -> e x) (lambda y -> f y)
  | app :
      forall s t
        (f1: ho.term u (s ==> t))
        (f2: ho.term v (s ==> t))
        (a1: ho.term u s)
        (a2: ho.term v s),
        wf g u v i j (s ==> t) f1 f2 ->
        wf g u v i j s a1 a2 ->
        wf g u v i j t (f1 @ a1) (f2 @ a2)
  | var :
      forall t (p: elem t g) x y,
        x = hat p i ->
        y = hat p j ->
        wf g u v i j t (^x) (^y).

End wf.
  
Definition wf {t} (e: term t) := forall u v, wf.wf nil u v tt tt t (e u) (e v).

Lemma hat_here:
  forall A (I: A -> Type) i is (x: I i) (xs: hlist I is), x = hat here (x,xs).
Proof.
  trivial.
Qed.

Lemma hat_there:
  forall A (I: A -> Type) i j is (x: I i) (y: I j) (xs: hlist I is) (p: elem _ is),
    x = hat p xs ->
    x = hat (there p) (y,xs).
Proof.
  trivial.
Qed.

Ltac show_wf :=
  repeat econstructor;
  repeat match goal with
           | |- ?x = hat _ (?x,_) => eapply hat_here
           | |- ?x = hat _ (?y,_) => eapply hat_there
         end.

Theorem wf_twice: forall t, wf (twice t).
  show_wf.
Qed.

Module equiv.

  Inductive equiv (g: list type) (u: type -> Type) (i: hlist u g):
    forall t, ho.term u t -> fo.term g t -> Prop :=
  | lam :
      forall s t (e: u s -> ho.term u t) y,
        (forall x, equiv (s::g) u (x,i) t (e x) y) ->
        equiv g u i (s ==> t) (lambda x -> e x) (fo.lam y)
  | app :
      forall s t (f: ho.term u (s ==> t)) (a: ho.term u s) e b,
        equiv g u i (s ==> t) f e ->
        equiv g u i s a b ->
        equiv g u i t (f @ a) (fo.app e b)
  | var :
      forall t (p: elem t g) x,
        x = hat p i ->
        equiv g u i t (^x) (fo.var p).

End equiv.

Definition equiv {t} (e: term t) (f: fo.term nil t) :=
  forall u, equiv.equiv nil u tt t (e u) f.

Definition lower_equiv {t} (e: term t) := { f | equiv e f }.

Definition twice_lower_equiv t: lower_equiv (twice t).
  show_wf.
Defined.

Definition twice_lower t := proj1_sig (twice_lower_equiv t).

Fixpoint raise_impl {t g u} (f: fo.term g t) (e: hlist u g): ho.term u t :=
  match f with
    | fo.lam s r b   => ho.lam (fun x => raise_impl b (x,e))
    | fo.app s r k a => ho.app (raise_impl k e) (raise_impl a e)
    | fo.var v p     => ho.var (hat p e)
  end.

Definition raise {t} (e: fo.term nil t): term t :=
  fun _ => raise_impl e tt.

Definition twice_raised t := raise (twice_lower t).

Eval compute in twice_raised base.