Normalization by Evaluation of Simply Typed Lambda Calculus including Sum and Empty Types.

NbE.v

(* This Normalization by Evaluation is based on mietek's <https://research.mietek.io/A201801.FullIPLNormalisation.html>.
   I've removed the continuations to give a purely tree-based implementation.
   This is operationally less efficent than using continuations, but it is hopefully easier to understand and potentially easier to verify correct.

   Checked with Coq 8.18.0
*)

Inductive Form :=
| Zero : Form
| One : Form
| Sum : Form -> Form -> Form
| Prod : Form -> Form -> Form
| Func : Form -> Form -> Form
.

Definition Ctx := list Form.

Inductive In {A : Set} (a : A) : list A -> Set :=
| here : forall {l}, In a (cons a l)
| there : forall {b l}, In a l -> In a (cons b l)
.

Definition Sub {A : Set} (x y : list A) : Set := forall i, In i x -> In i y.
Definition idSub {A : Set} (x : list A) : Sub x x := fun _ x => x.
Definition dropSub {A : Set} (a : A) (x : list A) : Sub x (cons a x) := fun _ x => there _ x.
Definition exSub {A : Set} (a : A) {x y : list A} (sub : Sub x y) : Sub (cons a x) (cons a y) := 
fun i p =>
match p with
| here _ => fun _ => here _
| there _ q => fun sub => there _ (sub _ q)
end sub.

Inductive nf (Gamma : Ctx) : Form -> Set :=
| star : nf Gamma One
| lin : forall {A B}, nf Gamma A -> nf Gamma (Sum A B)
| rin : forall {A B}, nf Gamma B -> nf Gamma (Sum A B)
| pair : forall {A B}, nf Gamma A -> nf Gamma B -> nf Gamma (Prod A B)
| lam : forall {A B}, nf (cons A Gamma) B -> nf Gamma (Func A B)
| case : forall {A B C}, ne Gamma (Sum A B) -> nf (cons A Gamma) C -> nf (cons B Gamma) C -> nf Gamma C
| abort : forall {C}, ne Gamma Zero -> nf Gamma C
with ne (Gamma : Ctx) : Form -> Set :=
| var : forall {A}, In A Gamma -> ne Gamma A
| pi1 : forall {A B}, ne Gamma (Prod A B) -> ne Gamma A
| pi2 : forall {A B}, ne Gamma (Prod A B) -> ne Gamma B
| apply : forall {A B}, ne Gamma (Func A B) -> nf Gamma A -> ne Gamma B
.

Inductive Tree Gamma a :=
| ret : a Gamma -> Tree Gamma a
| branch : forall {A B}, ne Gamma (Sum A B) -> Tree (cons A Gamma) a -> Tree (cons B Gamma) a -> Tree Gamma a
| null : ne Gamma Zero -> Tree Gamma a
.

Fixpoint bind {A B Gamma} (x : Tree Gamma A) (f : forall {Delta}, Sub Gamma Delta -> A Delta -> Tree Delta B) : Tree Gamma B :=
match x with 
| ret _ _ v => f (idSub Gamma) v
| branch _ _  n l r => branch _ _ n (bind l (fun Xi sub => f (fun _ i => sub _ (dropSub _ _ _ i))))
                                    (bind r (fun Xi sub => f (fun _ i => sub _ (dropSub _ _ _ i))))
| null _ _ n => null _ _ n
end. 

Definition map {A B Gamma} (x : Tree Gamma A) (f : forall {Delta}, Sub Gamma Delta -> A Delta -> B Delta) : Tree Gamma B := bind  x (fun _ sub a => ret _ _ (f sub a)).

Definition flip {A B C} := fun (f : A -> B -> C) x y => f y x.

Fixpoint run {Gamma A} (x : Tree Gamma (flip nf A)) : nf Gamma A :=
match x with
| ret _ _ v => v
| branch _ _ n l r => case _ n (run l) (run r)
| null _ _ n => abort _ n
end.

Fixpoint renameNf {Gamma Delta A} (sub : Sub Gamma Delta) (v : nf Gamma A) : nf Delta A :=
match v with
| star _ => star _
| lin _ v => lin _ (renameNf sub v)
| rin _ v => rin _ (renameNf sub v)
| pair _ v w => pair _ (renameNf sub v) (renameNf sub w)
| lam _ v => lam _ (renameNf (exSub _ sub) v)
| case _ v l r => case _ (renameNe sub v) (renameNf (exSub _ sub)  l) (renameNf (exSub _ sub)  r)
| abort _ v => abort _ (renameNe sub v)
end
with renameNe {Gamma Delta A} (sub : Sub Gamma Delta) (v : ne Gamma A) : ne Delta A :=
match v with
| var _ v => var _ (sub _ v)
| pi1 _ v => pi1 _ (renameNe sub v)
| pi2 _ v => pi2 _ (renameNe sub v)
| apply _ v w => apply _ (renameNe sub v) (renameNf sub w)
end.

Fixpoint renameTree {a Gamma Delta} (rename : forall G D, Sub G D -> a G -> a D) (sub : Sub Gamma Delta) (t : Tree Gamma a) : Tree Delta a :=
match t with
| ret _ _ v => ret _ _ (rename _ _ sub v)
| branch _ _ n l r => branch _ _ (renameNe sub n) (renameTree rename (exSub _ sub) l) (renameTree rename (exSub _ sub) r) 
| null _ _ n => null _ _ (renameNe sub n)
end.

Fixpoint FInterp Gamma (f : Form) :=
match f with 
| Zero => Empty_set
| One => unit
| Sum x y => (Tree Gamma (flip FInterp x) + Tree Gamma (flip FInterp y))%type
| Prod x y => (Tree Gamma (flip FInterp x) * Tree Gamma (flip FInterp y))%type
| Func x y => (forall Delta, Sub Gamma Delta -> Tree Delta (flip FInterp x) -> Tree Delta (flip FInterp y))%type
end.

Fixpoint renameFInterp {A Gamma Delta} (sub : Sub Gamma Delta) : FInterp Gamma A -> FInterp Delta A :=
match A return FInterp Gamma A -> FInterp Delta A with 
| Zero => fun v => match v with end
| One => fun _ => tt
| Sum x y => fun v => match v with inl v0 => inl (renameTree (@renameFInterp _) sub v0) | inr v1 => inr (renameTree (@renameFInterp _) sub v1) end
| Prod x y => fun v => (renameTree (@renameFInterp _) sub (fst v), renameTree (@renameFInterp _) sub (snd v))
| Func x y => fun v Xi subXi tXi => v _ (fun _ i => subXi _ (sub _ i)) tXi
end.

Fixpoint reify {Gamma A} : (FInterp Gamma A) -> nf Gamma A :=
match A return (FInterp Gamma A) -> nf Gamma A with 
| Zero => fun v => match v with end
| One => fun v => star _
| Sum x y => fun v => match v with inl a => lin _ (run (map a (fun Delta sub => @reify Delta _))) | inr b => rin _ (run (map b (fun Delta sub => @reify Delta _))) end
| Prod x y => fun v => pair _ (run (map (fst v) (fun Delta sub => @reify Delta _))) (run (map (snd v) (fun Delta sub => @reify Delta _)))
| Func x y => fun v => lam _ (run (map (v _ (dropSub x Gamma) (reflect (var _ (here _)))) (fun Delta sub => @reify Delta _)))
end
with reflect {Gamma A} : ne Gamma A -> Tree Gamma (flip FInterp A) :=
match A return ne Gamma A -> Tree Gamma (flip FInterp A)  with
| Zero => fun v => null _ _ v
| One => fun v => ret _ _ tt
| Sum x y => fun v => branch _ (flip FInterp (Sum x y)) v (map (reflect (var _ (here _))) (fun Delta sub (a : FInterp Delta x) => inl (ret _ _ a) : FInterp Delta (Sum x y)))
                                                          (map (reflect (var _ (here _))) (fun Delta sub (a : FInterp Delta y) => inr (ret _ _ a) : FInterp Delta (Sum x y)))
| Prod x y => fun v => ret _ _ (reflect (pi1 _ v), reflect (pi2 _ v))
| Func x y => fun v => ret _ (flip FInterp (Func x y)) (fun Delta sub a => reflect (apply _ (renameNe sub v) (run (map a (fun Delta sub => @reify Delta _)))))
end
.

Definition reifyTree {Gamma A} (t : Tree Gamma (flip FInterp A)) : nf Gamma A :=
  run (map t (fun Delta sub => @reify Delta _)).

Module Syntax.

Inductive STLC (Gamma : Ctx) : Form -> Set :=
| var : forall {A}, In A Gamma -> STLC Gamma A
| pi1 : forall {A B}, STLC Gamma (Prod A B) -> STLC Gamma A
| pi2 : forall {A B}, STLC Gamma (Prod A B) -> STLC Gamma B
| apply : forall {A B}, STLC Gamma (Func A B) -> STLC Gamma A -> STLC Gamma B
| star : STLC Gamma One
| lin : forall {A B}, STLC Gamma A -> STLC Gamma (Sum A B)
| rin : forall {A B}, STLC Gamma B -> STLC Gamma (Sum A B)
| pair : forall {A B}, STLC Gamma A -> STLC Gamma B -> STLC Gamma (Prod A B)
| lam : forall {A B}, STLC (cons A Gamma) B -> STLC Gamma (Func A B)
| case : forall {A B C}, STLC Gamma (Sum A B) -> STLC (cons A Gamma) C -> STLC (cons B Gamma) C -> STLC Gamma C
| abort : forall {C}, STLC Gamma Zero -> STLC Gamma C
.

End Syntax.
Import Syntax(STLC).

Fixpoint CtxFold (F : Form -> Set) (Gamma : Ctx) :=
match Gamma with 
| nil => unit
| cons A Gamma0 => (CtxFold F Gamma0 * F A)%type
end.

Fixpoint getFold {F Gamma A} (i : In A Gamma) : CtxFold F Gamma -> F A :=
match i in In _ G return CtxFold F G -> F A with 
| here _ => fun env => snd env
| there _ j => fun env => getFold j (fst env)
end.

Fixpoint mapFold {F G : Form -> Set} {Gamma} (f : forall A, F A -> G A) : CtxFold F Gamma -> CtxFold G Gamma :=
match Gamma return  CtxFold F Gamma -> CtxFold G Gamma with
| nil => fun _ => tt
| cons A Gamma0 => fun env => (mapFold f (fst env), f _ (snd env))
end.

Fixpoint renameFold {F Gamma Delta} (f : Sub Delta Gamma) (env : CtxFold F Gamma) : CtxFold F Delta :=
match Delta return Sub Delta Gamma -> CtxFold F Delta with
| nil => fun _ => tt
| cons A Delta0 => fun f => (renameFold (fun _ i => f _ (there _ i)) env, getFold (f _ (here _)) env)
end f.

Definition Sem Gamma A := forall Delta, CtxFold (fun A => Tree Delta (flip FInterp A)) Gamma -> Tree Delta (flip FInterp A).

Definition getSem {Gamma A} (i : In A Gamma) : Sem Gamma A := fun _ env => getFold i env.

Definition renameEnv {Gamma Delta Xi} (sub : Sub Gamma Delta) (env : CtxFold (fun A => Tree Gamma (flip FInterp A)) Xi) : CtxFold (fun A => Tree Delta (flip FInterp A)) Xi :=
mapFold (fun A => renameTree (@renameFInterp _) sub) env.

Fixpoint idEnv {Gamma} : CtxFold (fun A => Tree Gamma (flip FInterp A)) Gamma :=
match Gamma return CtxFold (fun A => Tree Gamma (flip FInterp A)) Gamma with
| nil => tt
| cons A Gamma0 => (renameEnv (dropSub _ _) idEnv, reflect (var _ (here _)))
end.

Fixpoint Eval {Gamma A} (e : STLC Gamma A) : Sem Gamma A :=
match e with
| Syntax.var _ i => getSem i
| Syntax.pi1 _ e1 => fun Delta env => bind (Eval e1 Delta env) (fun _ _ => fst)
| Syntax.pi2 _ e1 => fun Delta env => bind (Eval e1 Delta env) (fun _ _ => snd)
| Syntax.apply _ e1 e2 => fun Delta env => bind (Eval e1 Delta env) (fun _ sub f => f _ (idSub _) (Eval e2 _ (renameEnv sub env)))
| Syntax.star _ => fun Delta env => ret _ _ tt
| Syntax.lin _ e1 => fun Delta env => ret _ _ (inl (Eval e1 Delta env))
| Syntax.rin _ e1 => fun Delta env => ret _ _ (inr (Eval e1 Delta env))
| Syntax.pair _ e1 e2 => fun Delta env => ret _ _ (Eval e1 Delta env, Eval e2 Delta env)
| Syntax.lam _ e1 => fun Delta env => ret _ _ (fun _ sub t => Eval e1 _ (renameEnv sub env, t))
| Syntax.case _ e1 e2 e3 => fun Delta env => bind (Eval e1 Delta env) (fun _ sub v1 => match v1 with inl vl => Eval e2 _ (renameEnv sub env, vl) 
                                                                                                   | inr vr => Eval e3 _ (renameEnv sub env, vr)  end)
| Syntax.abort _ e1 => fun Delta env => bind (Eval e1 Delta env) (fun _ _ v1 => match v1 with end)
end.

Definition NbE {Gamma A} (e : STLC Gamma A) : nf Gamma A := reifyTree (Eval e _ idEnv).