-- The correctness of CBN TDPE, tested on Agda 2.3.2.1, standard library 0.7 (Feb 2014)

module plpv14 where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
-- open Relation.Binary.PropositionalEquality.≡-Reasoning

-- functional extensionality
postulate
  extensionality : forall {A B : Set} {f g : A -> B} -> (∀ (a : A) -> f a ≡ g a) -> f ≡ g

-- type
data typ : Set where
  base : typ
  arrow : typ -> typ -> typ

-- term, normal form, neutral term
data tm (var : typ -> Set) : typ -> Set where
  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

TM : typ -> Set1
TM A = forall (var : typ -> Set) -> tm var A

mutual
  data nf (var : typ -> Set) : typ -> Set where
    nf-Lam : forall {A B} -> (var A -> nf var B) -> nf var (arrow A B)
    nf-ne  : ne var base -> nf var base

  data ne (var : typ -> Set) : typ -> Set where
    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

NF : typ -> Set1
NF A = forall {var} -> nf var A

NE : typ -> Set1
NE A = forall {var} -> ne var A

mutual 
  tm-of-nf : forall {var A} -> nf var A -> tm var A
  tm-of-nf (nf-Lam f') = tm-Lam (\ x -> tm-of-nf (f' x))
  tm-of-nf (nf-ne e') = tm-of-ne e'

  tm-of-ne : forall {var A} -> ne var A -> tm var A
  tm-of-ne (ne-Var x) = tm-Var x
  tm-of-ne (ne-App e' f') = tm-App (tm-of-ne e') (tm-of-nf f')

-- V
V : Set -> typ -> Set
V b base = b
V b (arrow A B) = V b A -> V b B

-- soundness
soundness : forall (b : Set) -> {A : typ} -> tm (V b) A -> V b A
soundness b (tm-Var x) = x
soundness b (tm-Lam t1) = \ x -> soundness b (t1 x)
soundness b (tm-App t1 t2) = (soundness b t1) (soundness b t2)

soundness2 : forall (b : Set) -> {A : typ} -> TM A -> V b A
soundness2 b T = soundness b (T (V b))

-- completeness
mutual
  reify : forall (var : typ -> Set) -> (A : typ) -> V (ne var base) A -> nf var A
  reify var base v = nf-ne v
  reify var (arrow A B) v = nf-Lam (\ x -> reify var B (v (reflect var A (ne-Var x))))

  reflect : forall (var : typ -> Set) -> (A : typ) -> ne var A -> V (ne var base) A
  reflect var base e = e
  reflect var (arrow A B) e = \ v -> reflect var B (ne-App e (reify var A v))

-- interp
interp-nf : forall (b : Set) -> {A : typ} -> nf (V b) A -> V b A -> Set
interp-nf b f v = soundness b (tm-of-nf f) ≡ v

interp-ne : forall (b : Set) -> {A : typ} -> ne (V b) A -> V b A -> Set
interp-ne b e v = soundness b (tm-of-ne e) ≡ v

-- meaning of term families
interp-nf-ne : forall (b : Set) -> (e : ne (V b) base) -> (v : V b base) ->
               interp-ne b e v -> interp-nf b (nf-ne e) v
interp-nf-ne b e .(soundness b (tm-of-ne e)) refl = refl

interp-nf-Lam : forall (b : Set) -> (A B : typ) ->
                (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 {A = A} f) v
interp-nf-Lam b A B f v H = extensionality (\ a -> H {a})

interp-ne-Var : forall (b : Set) -> (A : typ) -> (v : V b A) -> interp-ne b (ne-Var {A = A} v) v
interp-ne-Var b A v = refl

interp-ne-App : forall (b : Set) -> (A B : typ) ->
                (e : ne (V b) (arrow A B)) -> (e' : V b A -> V b B) ->
                (f : nf (V b) A) -> (f' : V b A) ->
                interp-ne b e e' ->
                interp-nf b f f' ->
                interp-ne b (ne-App e f) (e' f')
interp-ne-App b A B e e' f f' He Hf =
  subst₂ (\ e' f' -> soundness b (tm-of-ne e) (soundness b (tm-of-nf f)) ≡ e' f') He Hf refl

-- R
R : forall (b : Set) -> (A : typ) -> V (ne (V b) base) A -> V b A -> Set
R b base e v = interp-ne b e v
R b (arrow A B) e v =
  forall (e' : V (ne (V b) base) A) -> (v' : V b A) -> R b A e' v' -> R b B (e e') (v v')

-- completeness
mutual
  reify-R : forall (b : Set) -> (A : typ) -> (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
  reify-R b base v f H = H
  reify-R b (arrow A B) v f H = 
    interp-nf-Lam b A B (\ x -> reify (V b) B (v (reflect (V b) A (ne-Var x)))) f
                  (\ {v'} -> reify-R b B (v (reflect (V b) A (ne-Var v'))) (f v')
                                    (H (reflect (V b) A (ne-Var v')) v'
                                       (reflect-R b A (ne-Var v') v'
                                                  (interp-ne-Var b A v'))))

  reflect-R : forall (b : Set) -> (A : typ) -> (e : ne (V b) A) -> (v : V b A) ->
              interp-ne b e v -> R b A (reflect (V b) A e) v
  reflect-R b base e v H = H
  reflect-R b (arrow A B) e v H =
    \ e' v' X -> reflect-R b B (ne-App e (reify (V b) A e')) (v v')
                          (interp-ne-App b A B e v (reify (V b) A e') v' H
                                         (reify-R b A e' v' X))

-- soundness
data related-term (b : Set) : forall {A : typ} -> tm (V (ne (V b) base)) A -> tm (V b) A -> Set where
  related-Var : forall {A} v v' -> R b A v v' -> related-term b {A} (tm-Var v) (tm-Var v')
  related-Lam : forall {A B} t t' -> (forall v v' -> R b A v v' -> related-term b (t v) (t' v')) ->
                related-term b {arrow A B} (tm-Lam t) (tm-Lam t')
  related-App : forall {A B} t1 t1' t2 t2' -> related-term b {arrow A B} t1 t1' -> related-term b {A} t2 t2' ->
                related-term b (tm-App t1 t2) (tm-App t1' t2')

main' : forall b A t1 t2 -> related-term b {A} t1 t2 -> R b A (soundness (ne (V b) base) t1) (soundness b t2)
main' b A .(tm-Var v) .(tm-Var v') (related-Var v v' x) = x
main' b .(arrow A B) .(tm-Lam t) .(tm-Lam t') (related-Lam {A} {B} t t' x) =
  \ e' v' x1 -> main' b B (t e') (t' v') (x e' v' x1)
main' b A .(tm-App t1 t2) .(tm-App t1' t2') (related-App {B} {.A} t1 t1' t2 t2' H H1) =
  (main' b (arrow B A) t1 t1' H) (soundness (ne (V b) base) t2) (soundness b t2') (main' b B t2 t2' H1)

main : forall b A (T : TM A) -> related-term b {A} (T (V (ne (V b) base))) (T (V b)) ->
                            R b A (soundness (ne (V b) base) (T (V (ne (V b) base)))) (soundness b (T (V b)))
main b A T = main' b A (T (V (ne (V b) base))) (T (V b))

correctness : forall b A (T : TM A) ->
              related-term b {A} (T (V (ne (V b) base))) (T (V b)) ->
              interp-nf b (reify (V b) A (soundness2 (ne (V b) base) T)) (soundness2 b T)
correctness b A T H = reify-R b A (soundness2 (ne (V b) base) T) (soundness2 b T) (main b A T H)