Library F1

Require Import Framework.
Implicit Types rho : type_context.

Implicit Types x y z : var.

Implicit Types u v : inttype -> Prop.

System F in Lambda-Curry style

Type syntax of System F

Inductive Ftype : Type :=
| tvar (x : var)
| arr (S T : Ftype)
| pi (T : {bind Ftype }).

Boilerplate for Autosubst

Instance Ids_ftype : Ids Ftype. derive. Defined.
Instance Rename_ftype : Rename Ftype. derive. Defined.
Instance Subst_ftype : Subst Ftype. derive. Defined.
Instance SubstLemmas_ftype : SubstLemmas Ftype. derive. Qed.

System F uses contexts

Definition f_ctx := t_ctx Ftype.
Implicit Types Gamma Delta : f_ctx.

System F typing judgement

Inductive f_ty : f_ctx -> term -> Ftype -> Prop :=
| fvar Gamma x : f_ty Gamma x (Gamma x)
| fapp Gamma s t S T : f_ty Gamma s (arr T S) ->
  f_ty Gamma t T ->
    f_ty Gamma (s t) S
| flam Gamma s S T : f_ty (S .: Gamma) s T ->
  f_ty Gamma (Lam s) (arr S T)
| fgen Gamma s T :
  f_ty (fun x => (Gamma x ).[ren (+1)]) s T
  -> f_ty Gamma s (pi T)
| fspec Gamma s S T :
  f_ty Gamma s (pi T)
  -> f_ty Gamma s (T .[S /]).

We interpret variables according to the valuation. For generalized types, we interpret the generalized variable as any realizor predicate. We interpret the arrow as the functional product.

Fixpoint int_ty T sigma := match T with
                           | tvar x => sigma x
                           | pi T => possible_int (fun X=> int_ty T (X .: sigma))
                           | arr T1 T2 => prod (int_ty T1 sigma) (int_ty T2 sigma)
                           end.
Notation "[[ T ]] sigma" := (int_ty T sigma) (at level 1).

This interpretation trivially preserves realizor predicates

Lemma int_ty_rp : rp_preservation Ftype int_ty.
hnf.
induction T ; intros sigma sigma_val ; simpl ; auto using prod_realizable, possible_int_realizable, valuation_up.
Qed.

Extensionally equal valuations yield equivalent interpretations

Lemma int_ty_feq_equiv {T} sigma1 sigma2 : (forall x, sigma1 x = sigma2 x) -> [[T ]]sigma1 =R = [[T ]]sigma2.
revert sigma1 sigma2.
induction T ; intros sigma1 sigma2 feq ; simpl in *.
- now rewrite feq.
- now rewrite IHT1, IHT2.
- apply int_equiv.
  intros X pX.
  apply IHT.
  intros [|x] ; auto.
Qed.

Renamings can be performed in either the type or in the valuation

Lemma int_ty_ren_equiv T sigma (r : var -> var) : [[ T .[ren r ] ]]sigma =R = [[T ]] (fun x => sigma (r x)).
revert sigma r.
induction T ; simpl ; intros sigma r.
- asimpl. reflexivity.
- now rewrite IHT1, IHT2.
- apply int_equiv.
  intros X pX.
  asimpl.
  rewrite IHT, int_ty_feq_equiv.
  + reflexivity.
  + intros [|x] ; auto.
Qed.

Variables that are not used can be interpreted any way

Corollary validates_skip rho tGamma sigma : validates Ftype int_ty rho tGamma sigma -> forall X, validates Ftype int_ty rho (fun x => (tGamma x ).[ren (+1)]) (X .: sigma).
intros rho_sigma_val X x.
now apply int_ty_ren_equiv.
Qed.

A substitution translates one valuation to another if they interpret variables equivalently

Definition translates s sigma1 sigma2 := forall x, [[ tvar x ]] sigma1 =R = [[s x ]]sigma2.

Extending two valuations equally preserves translations between them, as long as the substitution does not affect the additional variable

Lemma translates_skip {s sigma1 sigma2} : forall X,
translates s sigma1 sigma2 -> translates (up s) (X .: sigma1) (X .: sigma2).
intros X t [|x] ; simpl.
- reflexivity.
- rewrite (t x).
  asimpl.
  rewrite int_ty_ren_equiv.
  asimpl.
  now apply int_ty_feq_equiv.
Qed.

If a substitution translates all variables, it also translates all terms

Lemma int_ty_subst_equiv T : forall s sigma1 sigma2,
  translates s sigma1 sigma2 -> [[T ]] sigma1 =R = [[ T .[s ] ]] sigma2.
induction T ; intros s sigma1 sigma2 t ; eauto ; simpl.
- now rewrite IHT1, IHT2.
- apply int_equiv.
  intros X pX.
  rewrite IHT ; eauto using translates_skip.
  reflexivity.
Qed.

The type interpretation respects specialization

Lemma int_ty_beta T S sigma u : [[T ]]([[S ]]sigma .: sigma ) u -> [[ T .[S /] ]]sigma u.
apply int_ty_subst_equiv.
intros [|x] ; simpl ; reflexivity.
Qed.

The type interpretation respects the typing judgement

Lemma in_int_ty : adequacy Ftype int_ty f_ty.
hnf.
induction 1 ; intros rho sigma rho_val sigma_val rho_sigma_val ; simpl in *.
- apply equiv_closed with (rho x) ; eauto using int_ty_rp, filter_equiv_sym, int_x.
- apply equiv_closed with ([s]rho @ [t]rho) ; eauto using int_ty_rp, filter_equiv_sym, int_st.
  apply IHf_ty1 ; eauto.
- constructor ; auto using int_IF.
  intros u Au.
  assert (rpS := int_ty_rp S _ sigma_val).
  assert (exists A : inttype , u A) by now apply rpS.
  apply equiv_closed with ([s] (u .: rho)) ; eauto using int_ty_rp, filter_equiv_sym, int_lam, only_filter, valid_up, validates_up.
- intros [X HX] ; simpl. apply IHf_ty ; eauto using valuation_up, possible_int_realizable, validates_skip.
- apply int_ty_beta.
  pattern [[S]]sigma, [s]rho.
  apply possible_int_specialize ; eauto using int_ty_rp.
Qed.

System F terminates

Corollary sn_F {tGamma t T} : f_ty tGamma t T -> SN t.
apply (sn _ _ _ int_ty_rp in_int_ty).
Qed.