# System F CBV Typing Relation

From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype.
Require Import Examples.sysf_wn.
Set Implicit Arguments.
Unset Strict Implicit.

Local Ltac asimpl :=
repeat progress (cbn; fsimpl; gsimpl; ty_simpl; vt_simpl).

## Typing traversal

Definition type_of_traversal : TmVl.traversal ty ty (constl ty)
(constl (pred1 ty)) (constl (pred1 ty)) := FCBV.Traversal
(* Variables i *)
(fun m _ (A B : ty m) => A = B)
(* Lambda \A. s *)
(fun m n (An : ty m) (F : (fun m _ => ty m -> ty m -> Prop) m n) (AB : ty m) =>
if AB is Ty.arr A B then An = A /\ F m n idren idren A B else False)
(* Type Lambda /\. s *)
(fun m n (F : (fun m _ => ty m -> ty m -> Prop) m n) (FA : ty m) =>
if FA is Ty.all A then F m.+1 n shift idren (Ty.var (n:=m.+1) bound) A else False)
(* Value as term v *)
(fun m n (P : ty m -> Prop) => P)
(* Application s t *)
(fun m n (P Q : ty m -> Prop) (B : ty m) =>
exists2 A : ty m, P (Ty.arr A B) & Q A)
(* Type Application *)
(fun m n (P : ty m -> Prop) (A : ty m) (IA : ty m) =>
exists2 B : ty m.+1, P (Ty.all B) & IA = B.[A .: Ty.var (n:=m)]%ty).

Notation vl_type := (@Vl.eval _ _ _ _ _ Ty.inst_traversal type_of_traversal _ _ _ 0 (@Ty.var _)).
Notation tm_type := (@Tm.eval _ _ _ _ _ Ty.inst_traversal type_of_traversal _ _ _ 0 (@Ty.var _)).

Notation "[ 'vl' ctx ⊢ v : A ]" := (vl_type ctx v A).
Notation "[ 'tm' ctx ⊢ s : A ]" := (tm_type ctx s A).

Notation vl_frel := (@Vl.eval _ _ _ _ _ Ty.inst_traversal (FCBV.lift Ty.inst_traversal type_of_traversal) _ _ _ 0).
Notation tm_frel := (Tm.eval Ty.inst_traversal (FCBV.lift Ty.inst_traversal type_of_traversal) (n2 := 0)).

Notation vl_rel := (vl_frel Ty.var).
Notation tm_rel := (tm_frel Ty.var).

## Equations for recursive typing

Lemma type_of_var {m n : nat} (ctx : fin n -> ty m) (i : fin n) (A : ty m) :
vl_type ctx (TmVl.var i) A = (ctx i = A).
Proof. by []. Qed.

Lemma type_of_lam {m n : nat} (ctx : fin n -> ty m) (s : tm m n.+1) (A A' B : ty m) :
vl_type ctx (TmVl.lam A' s) (Ty.arr A B) = (A' = A /\ tm_type (A .: ctx) s B).
Proof. by asimpl. Qed.

Lemma type_of_Lam {m n : nat} (ctx : fin n -> ty m) (s : tm m.+1 n) (A : ty m.+1) :
vl_type ctx (TmVl.Lam s) (Ty.all A) = tm_type (ctx >> th1 shift) s A.
Proof. by asimpl. Qed.

Lemma type_of_tvl {m n : nat} (ctx : fin n -> ty m) (v : vl m n) (A : ty m) :
tm_type ctx (TmVl.tvl v) A = vl_type ctx v A.
Proof. by []. Qed.

Lemma type_of_app {m n : nat} (ctx : fin n -> ty m) (s t : tm m n) (B : ty m) :
tm_type ctx (TmVl.app s t) B =
(exists2 A, tm_type ctx s (Ty.arr A B) & tm_type ctx t A).
Proof. by []. Qed.

Lemma type_of_App {m n : nat} (ctx : fin n -> ty m) (s : tm m n) (A B : ty m) :
tm_type ctx (TmVl.App s A) B =
(exists2 F, tm_type ctx s (Ty.all F) & B = Ty.inst (A .: @Ty.var m) F).
Proof. by asimpl. Qed.

Corollary shift_typing {m n : nat} (ctx : fin n -> ty m) (v : vl m n) (A B : ty m) :
vl_type (B .: ctx) (v (id,shift))%vl A = vl_type ctx v A.
Proof. by asimpl. Qed.

## Naturality

Lemma im_eq {X Y} (f : X -> Y) (x : X) :
im f (eq x) = (eq (f x)).
Proof. fext=> y. apply: pext; split=> [[z <- <-//]|<-]. by exists x. Qed.

Lemma im_exists2 {X Y} (f : X -> Y) (P Q : X -> X -> Prop) (x : Y) :
injective f ->
im f (fun x => exists2 y : X, P y x & Q y x) x =
exists2 y, im f (P y) x & im f (Q y) x.
Proof.
move=> fP. apply: pext; split.
case=> y [x' pxy qxy <-]. eexists; eexists; eauto.
case=> y [x' pxy E1] [x'' pxy' E2]. subst. move: E2 => /fP E2. subst.
eexists. eexists. eassumption. eassumption. reflexivity.
Qed.

Lemma type_of_is_natural : FCBV.is_natural type_of_traversal.
Proof.
constructor => //.
- move=> m1 m2 n1 n2 f g /= i. asimpl. by rewrite im_eq.
- move=> m1 n1 A F ih m2 n2 f g. asimpl. fext=> AB /=. apply: pext; split.
+ move=> [/=AB']. case: AB' => //A' B' [e1 H] e2; subst=> /=. asimpl. split=>//.
rewrite -(ih _ _ _ _ idren f idren g A'). hnf. eexists. exact H. by [].
+ case: AB => // A' B' [eqn H]; subst => /=. move: H. asimpl.
rewrite -(ih _ _ _ _ idren f idren g A) => -[/=C H <-]. by exists (Ty.arr A C).
- move=> m1 n1 F ih m2 n2 f g. fext=> A. asimpl. apply: pext; split.
+ move=> [/=[]//B H <-{A}/=]. asimpl.
move: (ih _ m2.+1 _ n2 shift (up f) idren g (Ty.var bound)). asimpl.
rewrite shift_up. move<-. rewrite im_inj //. exact: th_inj1.
+ case: A => //= A. move: (ih _ m2.+1 _ n2 shift (up f) idren g (Ty.var bound)). asimpl.
rewrite shift_up. move<-. case=> /=B H <-. by exists (Ty.all B).
- move=> m1 m2 n1 n2 f g P Q. asimpl. fext=>/=B. rewrite im_exists2; last first.
exact: th_inj1. apply: pext; split.
+ case=> /= A [B' H1 <- {B}] [_ QA _]. eexists; by repeat (eexists; eauto).
+ case=> /=C[/=[]//D1 D2 H1]. asimpl=> -[e1 e2]. subst=> -[E H2 /th_inj1 e]. subst.
eexists; by repeat (eexists; eauto).
- move=> m1 m2 n1 n2 f g P A. fext=> B. asimpl. apply: pext; split.
+ move=> [/=C [/=D H E1] E2]. subst. eexists. eexists. eassumption. cbn. reflexivity.
by asimpl.
+ move=> [/=C [/=D H E1] E2]. subst. destruct D; cbn in * => //.
move: E1 => [E1]. subst C. eexists. eexists. eassumption. reflexivity.
by asimpl.
Qed.

Canonical type_of_model := TmVl.Model type_of_is_natural.

Corollary vl_tvar_shift {m n : nat} (ctx : fin n -> ty m) (v : vl m n) (A : ty m) :
vl_type (ctx >> Ty.ren shift) (v (shift,idren))%vl (A shift)%ty = vl_type ctx v A.
Proof.
asimpl. rewrite -(Vl.naturality (TyTerms.lift_model TyTerms.ren_model) type_of_model (Ty.var (n:=m)) ctx shift idren). asimpl. rewrite im_inj //. exact: th_inj1.
Qed.

## Relational Typing & Preservation

Lemma tv_monotone :
forall m1 n : nat,
(forall (v : vl m1 n) {m2} (f : fin m1 -> ty m2)
(c1 : fin n -> ty m1 -> Prop) (c2 : fin n -> ty m2 -> Prop) (A : ty m1),
(forall i B, c1 i B -> c2 i B.[f]%ty) -> vl_rel c1 v A -> vl_frel f c2 v A.[f]%ty) /\
(forall (s : tm m1 n) {m2} (f : fin m1 -> ty m2)
(c1 : fin n -> ty m1 -> Prop) (c2 : fin n -> ty m2 -> Prop) (A : ty m1),
(forall i B, c1 i B -> c2 i B.[f]%ty) -> tm_rel c1 s A -> tm_frel f c2 s A.[f]%ty).
Proof.
apply TmVl.tv_ind => //=[m1 n i|m1 n A b ih|m1 n b ih|m1 n s ihs t iht|m1 n s ih A] m2 f c1 c2 T le /=.
- exact: le.
- case: T => // B C. asimpl=> -[<-{B} H]. split=>//. by apply: ih H => -[]//=B <-.
- case: T => // A. asimpl. apply: ih => i B /=[/=C H<-]. asimpl.
rewrite -Ty.inst_ren im_inj. exact: le. exact: th_inj1.
- cbn; move=> [/=A h1 h2]. exists A.[f]%ty. exact: ihs h1. exact: iht h2.
- cbn; move=> [/=B h1 ->{T}]. exists B.[Ty.var bound .: f >> th1 shift]%ty.
exact: ih h1. by asimpl.
Qed.

Lemma tm_frel_mono {m1 m2 n} (c1 : fin n -> ty m1 -> Prop) (c2 : fin n -> ty m2 -> Prop)
(f : fin m1 -> ty m2) (s : tm m1 n) (A : ty m1) :
(forall i B, c1 i B -> c2 i B.[f]%ty) ->
tm_rel c1 s A -> tm_frel f c2 s A.[f]%ty.
Proof. case: (tv_monotone m1 n) => _ H. exact: H. Qed.

Lemma tm_rel_mono {m n} (c1 c2 : fin n -> ty m -> Prop) (s : tm m n) (A : ty m) :
(forall i B, c1 i B -> c2 i B) -> tm_rel c1 s A -> tm_rel c2 s A.
Proof. move: (@tm_frel_mono m m n c1 c2 Ty.var). asimpl. exact. Qed.

Lemma rel_preservation {m n} (s : tm m n) (v : vl m n) :
eval s v -> forall (Gamma : fin n -> ty m -> Prop) (A : ty m),
tm_rel Gamma s A -> vl_rel Gamma v A.
Proof.
elim=> //{s v}[s t A b u v _ ih1 _ ih2 _ ih3|s A b v _ ih1 _ ih2] Gamma T.
- asimpl=> -[/=C /ih1]. asimpl=> -[E]. subst=> h1 /ih2 h2.
apply: ih3. asimpl=>/=. by apply: tm_rel_mono h1 => /=-[]//=B<-.
- asimpl=> -[/=B /ih1]. asimpl=> h1 ->{T}. apply: ih2. asimpl.
apply: tm_frel_mono h1 => i C' [/=C h <-{C'}]. by asimpl.
Qed.

Corollary preservation {m n} (Gamma : fin n -> ty m) (s : tm m n) (v : vl m n) (A : ty m) :
eval s v -> tm_type Gamma s A -> vl_type Gamma v A.
Proof.
move=> ev. rewrite Tm.embed Vl.embed. exact: rel_preservation.
Qed.

Lemma context_morphism {l m n k} (Gamma : fin n -> ty l) (Delta : fin k -> ty m) (f : fin l -> ty m) (g : fin n -> vl m k) :
(forall x, vl_type Delta (g x) (Gamma x).[f]%ty) ->
(forall s A, tm_type Gamma s A -> tm_type Delta s.[f,g]%tm A.[f]%ty).
Proof.
move=> h1 s A. rewrite Tm.embed => h2. asimpl. apply: tm_frel_mono; last first.
exact: h2. move=> i B /= <-. exact: h1.
Qed.