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)
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.
induction T ; intros sigma sigma_val ; simpl ; auto using prod_realizable, possible_int_realizable, valuation_up.

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.

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.
  rewrite IHT, int_ty_feq_equiv.
  + reflexivity.
  + intros [|x] ; auto.

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.

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).
  rewrite int_ty_ren_equiv.
  now apply int_ty_feq_equiv.

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.

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.

The type interpretation respects the typing judgement

Lemma in_int_ty : adequacy Ftype int_ty f_ty.
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.

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