Library Autosubst.sem

Normalization of Call-By-Value System F


Require Export axioms.
Require Export SystemFCBV.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import CommaNotation.

Call-by value reduction


Inductive eval {m n} : tm m n vl m n Prop :=
| eval_app (A : ty m) s t u (v1 v2 : vl m n) :
    eval s (lam A u) eval t v1 eval (u [var_ty ; v1 .: var_vl]) v2
    eval (app s t) v2
| eval_tapp (A : ty m) s u v :
    eval s (tlam u) eval u[A .: var_ty; var_vl] v
    eval (tapp s A) v
| eval_val (v : vl m n) :
    eval (vt v) v.
Hint Resolve eval_val.

Syntactic typing


Definition ctx (m n : nat) := fin n ty m.

Unset Elimination Schemes.
Inductive tm_ty m n (Gamma : ctx m n) : tm m n ty m Prop :=
| ty_app (A B : ty m) (s t : tm m n) :
    tm_ty Gamma s (arr A B)
    tm_ty Gamma t A
    tm_ty Gamma (app s t) B
| ty_tapp A A' B (s : tm m n) :
    tm_ty Gamma s (all A) A' = A[B .: var_ty]
    tm_ty Gamma (tapp s B) A'
| ty_val (A : ty m) (v : vl m n) :
    vl_ty Gamma v A
    tm_ty Gamma (vt v) A
with vl_ty m n (Gamma : ctx m n) : vl m n ty m Prop :=
     | ty_var (x : fin n) s :
         s = Gamma x
 vl_ty Gamma (var_vl x) s
| ty_lam A B (s : tm m (S n)) :
    @tm_ty m (S n) (A, Gamma) s B
    vl_ty Gamma (lam A s) (arr A B)
| ty_tlam A (s : tm (S m) n) :
    @tm_ty (S m) n (Gamma >> ) s A
    vl_ty Gamma (tlam s) (all A).
Set Elimination Schemes.

Scheme tm_ty_ind := Minimality for tm_ty Sort Prop
with vl_ty_ind := Minimality for vl_ty Sort Prop.
Combined Scheme has_ty_ind from tm_ty_ind, vl_ty_ind.

Hint Constructors tm_ty vl_ty.

 Definition lt_ctx_ren {m n m' n'} (Gamma : ctx m n) (Delta : ctx m' n') (xi: fin m fin m') (zeta: fin n fin n') :=
    x, (Gamma x)⟨xi= Delta (zeta x).

Lemma typing_ren m n (Gamma : ctx m n):
  ( s A, tm_ty Gamma s A m' n' (Delta : ctx m' n') (sigma : fin m fin m') (tau : fin n fin n'),
lt_ctx_ren Gamma Delta sigma tau tm_ty Delta (ssigma;tau) (Asigma))
( s A, vl_ty Gamma s A m' n' (Delta : ctx m' n') (sigma : fin m fin m') (tau : fin n fin n') A',
          A' = Asigma lt_ctx_ren Gamma Delta sigma tau vl_ty Delta (ssigma;tau) A').
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl; eauto.
  - econstructor. asimpl in H0. eapply H0. eauto. now asimpl.
  - constructor. eapply H0. unfold lt_ctx_ren.
    auto_case.
  - constructor. eapply H0. unfold lt_ctx_ren. intros z. asimpl. unfold funcomp.
    rewrite <- H2. now asimpl.
Qed.

Definition lt_ctx {m n m' n'} (Gamma : ctx m n) (Delta : ctx m' n') sigma tau :=
   x, vl_ty Delta (tau x) (Gamma x)[sigma].

Lemma typing_subst m n (Gamma : ctx m n):
  ( s A, tm_ty Gamma s A m' n' (Delta : ctx m' n') (sigma : fin m ty m') (tau : fin n vl m' n'),
lt_ctx Gamma Delta sigma tau tm_ty Delta (s[sigma;tau]) (A[sigma]))
( s A, vl_ty Gamma s A m' n' (Delta : ctx m' n') (sigma : fin m ty m') (tau : fin n vl m' n'),
lt_ctx Gamma Delta sigma tau vl_ty Delta (s[sigma;tau]) (A[sigma])).
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl; eauto.
  - econstructor. asimpl in H0. apply H0. eauto. now asimpl.
  - econstructor. apply H0.
    unfold lt_ctx. intros [|].
    + cbn. eapply typing_ren. eapply H1. now asimpl.
      unfold lt_ctx_ren. intros x. now asimpl.
    + cbn. constructor. now asimpl.
  - econstructor. apply H0.
    unfold lt_ctx. intros. asimpl.
    unfold funcomp. eapply typing_ren. eapply H1. now asimpl.
    unfold lt_ctx_ren. now asimpl.
Qed.

Semantic typing


Definition L {m n} (P : vl m n Prop) (s : tm m n) :=
   v, eval s v P v.

Fixpoint V {m m' n'} (A : ty m) (rho : fin m vl m' n' Prop) (v : vl m' n' ) {struct A} : Prop :=
  match A with
  | var_ty Xrho X v
  | arr A B
    match v with
    | lam C s u, V A rho u L (V B rho) s[var_ty; u .: var_vl]
    | _False
    end
  | all A
    match v with
    | tlam s B i, (v: vl m' n'), eval (s[B..; ids]) v
                                                                   V A (i .: rho) v
    | _False
    end
  end.
Notation E A rho := (L (V A rho)).

Lemma V_ren m m' m'' n' (A: ty m) (rho: fin m'' vl m' n' Prop) (xi: fin m fin m'') :
  V Axi rho = V A (xi >> rho).
Proof.
  revert m' m'' n' rho xi. induction A; intros; eauto.
  - fext. intros [| |]; eauto.
    simpl. fext. intros v. asimpl. now rewrite IHA1, IHA2.
  - fext. intros [| |]; eauto.
    simpl. fext. intros. asimpl. rewrite IHA. now asimpl.
Qed.

Lemma V_weak m m' n' A d (rho: fin m vl m' n' Prop) :
  V (ren_ty A) (d .: rho) = V A rho.
Proof. eapply V_ren. Qed.

Lemma V_subst m m' n' m'' (A : ty m) (rho: fin m'' vl m' n' Prop) (sigma: fin m ty m'') :
  V (subst_ty sigma A) rho = V A (fun xV (sigma x) rho).
Proof.
  revert m' m'' n' rho sigma. induction A; intros; eauto.
  - fext. intros [| |]; eauto.
    simpl. fext. intros v. asimpl. now rewrite IHA1, IHA2.
  - fext. intros [| |]; eauto.
    simpl. fext. intros. asimpl.
    rewrite IHA.
    f_equal. fext. intros. repeat f_equal. fext. auto_case.
    intros. asimpl. now rewrite V_weak.
Qed.

Lemma E_subst1 m m' n' (A : ty (S m)) B (rho: fin m vl m' n' Prop) :
  E (subst_ty (B .: var_ty) A) rho = E A (V B rho .: rho).
Proof.
  unfold E. fext. intros. f_equal. fext. intros.
  f_equal. rewrite V_subst. repeat f_equal. fext. auto_case.
Qed.

Definition VG {m n m' n'} (Gamma : ctx m n) (rho : fin m vl m' n' Prop) (sigma : fin n vl m' n') :=
   x, V (Gamma x) rho (sigma x).

Theorem soundness m n (Gamma : ctx m n) :
  ( (s : tm m n) (A : ty m), tm_ty Gamma s A
     m' n' (sigma: fin m ty m') (tau: fin n vl m' n') rho, VG Gamma rho tau E A rho s[sigma;tau])
  ( (v : vl m n) (A : ty m), vl_ty Gamma v A
     m' n' (sigma: fin m ty m') (tau: fin n vl m' n') rho, VG Gamma rho tau V A rho v[sigma;tau]).
Proof.
  revert m n Gamma. apply has_ty_ind; intros; subst; asimpl in *; eauto.
  - destruct (H0 _ _ sigma _ rho H3) as ([]&ev1&h1); simpl in h1; try contradiction.
    destruct (H2 _ _ sigma _ rho H3) as (v1&ev2&h2).
    destruct (h1 _ h2) as (v2&ev3&h3).
     v2. split; eauto using eval_app.
  - rewrite E_subst1.
    destruct (H0 _ _ sigma _ rho H2) as ([]&ev1&h1); simpl in h1; try contradiction.
    destruct (h1 (B[sigma]) (V B rho)) as (v&ev2&h2).
     v. eauto using eval_tapp.
  - eexists; asimpl; eauto.
  - simpl. intros. asimpl. apply H0.
    intros [|]; cbn; asimpl; eauto.
  - simpl. intros. asimpl. asimpl in H0. apply H0.
    intros x. asimpl. rewrite V_weak. apply H1.
Qed.

Applications


Definition nilA {m n}: fin m vl m n Prop := fun _ _False.

Definition empty {m} : fin 0 ty m := fun xmatch x with end.

Corollary soundness_nil m (s: tm m 0) A :
  tm_ty empty s A E A nilA s.
Proof.
  intros H.
  replace s with (s[ids;ids]) by now asimpl.
  eapply soundness; eauto.
  intros x. now destruct x.
Qed.

Corollary normalization m (s: tm m 0) A :
  tm_ty empty s A v, eval s v.
Proof.
  intros H. apply soundness_nil in H.
  destruct H. eexists; eauto. eapply H.
Qed.

Corollary consistency (s: tm 0 0) :
  ¬tm_ty empty s (all (var_ty var_zero)).
Proof.
  intros H. eapply soundness_nil in H.
  destruct H as (?&?&?). simpl in H0. destruct x; eauto.
  now destruct (H0 (all (var_ty var_zero)) (fun _False)) as (?&?&?) .
Qed.