RSC.sysf

Traditional, 2-sorted System F with explicits type variable contexts, a la Harper

We define a de Bruijn presentation of traditional, 2-sorted System F and develop part of its theory. System F has no need for base types due to its quantification/abstraction over type variables We also do not consider reductions as the typing judgment does not have a conversion rule.

Require Import Omega List Program.Equality Relations.
From Autosubst Require Export Autosubst.

From RSC Require Import Decidable lib.

Set Implicit Arguments.

Syntax

Types

Inductive ty : Type :=
| TyVar (n : var)
| Imp (A B : ty)
| All (A : {bind ty }).

Terms

Inductive tm : Type :=
| Var (n : var)
| App (s t : tm)
| Lam (A : ty) (s : {bind tm })
| TyApp (s : tm) (A : ty)
| TyLam (s : {bind ty in tm }).

Decidable Equality on the type and term syntax

Instance decide_eq_ty (A B : ty) : Dec (A = B). derive. Defined.
Instance decide_eq_tm (s t : tm) : Dec (s = t). derive. Defined.

Autosubst machinery, check if the heterogeneous stuff is needed ...

Instance Ids_ty : Ids ty. derive. Defined.
Instance Rename_ty : Rename ty. derive. Defined.
Instance Subst_ty : Subst ty. derive. Defined.
Instance SubstLemmas_ty : SubstLemmas ty. derive. Qed.
Instance HSubst_termF : HSubst ty tm. derive. Defined.
Instance Ids_tm : Ids tm. derive. Defined.
Instance Rename_tm : Rename tm. derive. Defined.
Instance Subst_tm : Subst tm. derive. Defined.
Instance HSubstLemmas_termF : HSubstLemmas ty tm. derive. Qed.
Instance SubstHSubstComp_typeF_termF : SubstHSubstComp ty tm. derive. Qed.
Instance SubstLemmas_tm : SubstLemmas tm. derive. Qed.

Illustration of heterogeneos subst s.|tau.sigma (also written stau,sigma) reduction rules for reference.

Goal forall n sigma tau, (Var n ).|[tau ].[sigma ] = sigma(n). autosubst. Qed.
Goal forall s t sigma tau, (App s t ).|[tau ].[sigma ] = App s .|[tau ].[sigma ] t .|[tau ].[sigma ]. autosubst. Qed.
Goal forall A s sigma tau, (Lam A s ).|[tau ].[sigma ] = Lam A .[tau ] s .|[tau ].[up sigma ]. autosubst. Qed.
Goal forall s A sigma tau, (TyApp s A ).|[tau ].[sigma ] = TyApp s .|[tau ].[sigma ] A .[tau ]. autosubst. Qed.
Goal forall s sigma tau, (TyLam s ).|[tau ].[sigma ] = TyLam s .|[up tau ].[sigma >>| (ren (+1))]. autosubst. Qed.

Type System

Type Formation Judgement

Inductive istype (N : nat) : ty -> Prop :=
| istype_tyvar n : n < N -> istype N (TyVar n)
| istype_imp A B : istype N A -> istype N B -> istype N (Imp A B)
| istype_all A : istype (1 + N) A -> istype N (All A).

Typing Judgment; Note the context lookup is non-dependent since the free variables in a typing context are all type variables, referencing a separate context.

Inductive hastype (N : nat) (Gamma : list ty) : tm -> ty -> Prop :=
| hastype_var x A : atn Gamma x A -> istype N A -> hastype N Gamma (Var x) A
| hastype_app s t A B : hastype N Gamma s (Imp A B) -> hastype N Gamma t A -> hastype N Gamma (App s t) B
| hastype_lam s A B : hastype N (A :: Gamma) s B -> istype N A -> hastype N Gamma (Lam A s) (Imp A B)
| hastype_tyapp s A A' B : istype N B -> hastype N Gamma s (All A) -> A' = A .[B /] -> hastype N Gamma (TyApp s B) A'
| hastype_tylam s A : hastype (1 + N) Gamma..[ren (+1)] s A -> hastype N Gamma (TyLam s) (All A).

Theory

Note that we have beta substitutions on types in the typing judgment, hence we clearly require that at least type formation is compatible with such beta substituions. This is new with respect to the stlc case!

For Type Formation. As for the STLC we only map lookups. Note that we also need the full substitution CML

Definition istype_cr (xi : var -> var) N M := forall n, n < N -> (xi n ) < M.

Lemma istype_cr_up xi N M : istype_cr xi N M -> istype_cr (upren xi) (1 + N) (1 + M).
Proof.
  intros CR [|n] Ln; asimpl in *; try omega. cut (n < N); [intros H|omega]. apply CR in H. omega.
Qed.

Lemma istype_ren N A: istype N A -> forall M xi, istype_cr xi N M -> istype M A .[ren xi ].
Proof. intros H. induction H; intros M xi CR; asimpl; auto using istype, istype_cr_up. Qed.

Lemma istype_cr_shift N : istype_cr (+1) N (1 + N).
Proof. intros n H. asimpl in *. omega. Qed.

Corollary istype_weaken N A: istype N A -> istype (1 + N) A .[ren (+1)].
Proof. intros H. eapply istype_ren; eauto using istype_cr_shift. Qed.

Definition istype_cm (sigma : var -> ty) N M := forall n, n < N -> istype M (sigma n).

Lemma istype_cm_up sigma N M : istype_cm sigma N M -> istype_cm (up sigma) (1 + N) (1 + M).
Proof.
  intros CM [|n] T; asimpl.
  - constructor. omega.
  - apply istype_weaken. apply CM. omega.
Qed.

Lemma istype_subst N A : istype N A -> forall M sigma, istype_cm sigma N M -> istype M A .[sigma ].
Proof.
  intros H. induction H; intros M sigma CM.
  - now apply CM.
  - constructor; auto.
  - constructor; auto using istype_cm_up.
Qed.

Lemma istype_cm_beta N B : istype N B -> istype_cm (B .: ids) (1 + N) N.
Proof. intros T [|n] H; asimpl; trivial. constructor. omega. Qed.

Corollary istype_beta N A B : istype N B -> istype (1 + N) A -> istype N A .[B /].
Proof. intros H T. eapply istype_subst; eauto using istype_cm_beta. Qed.

Validity of contexts

Inductive valid : nat -> list ty -> Prop :=
| valid_empty : valid 0 nil
| valid_ext_ty N : valid N nil -> valid (1 + N) nil
| valid_ext_tm N Gamma A : istype N A -> valid N Gamma -> valid N (A :: Gamma).

Lemma valid_N_nil N : valid N nil.
Proof. induction N; auto using valid. Qed.

alternative characterisation of validity with less structure

Inductive valid' (N : nat): list ty -> Prop :=
| valid'_nil : valid' N nil
| valid'_ext_tm Gamma A : istype N A -> valid' N Gamma -> valid' N (A :: Gamma).

Lemma valid_valid' N Gamma : valid N Gamma <-> valid' N Gamma.
Proof.
  split; intros H.
  - induction H; eauto using valid'.
  - induction H; eauto using valid, valid_N_nil.
Qed.

Lemma valid_ren N Gamma : valid N Gamma -> forall M xi, istype_cr xi N M -> valid M Gamma..[ren xi ].
Proof.
  intros H. induction H; intros M xi CR.
  - apply valid_N_nil.
  - apply valid_N_nil.
  - asimpl. constructor; auto. eapply istype_ren; eauto.
Qed.

Corollary valid_shift N Gamma: valid N Gamma -> valid (1 + N) Gamma..[ren (+1)].
Proof. intros H. eapply valid_ren; eauto using istype_cr_shift. Qed.

Internalising valid contexts, staged: first terms then types

Fixpoint intern_ty (N : nat) (s : tm) (A : ty) : (tm * ty) :=
  match N with
  | 0 => (s ,A )
  | (S M) => intern_ty M (TyLam s) (All A)
  end.

Fixpoint intern (N : nat) (Gamma : list ty) (s : tm) (A : ty) : (tm * ty) :=
  match Gamma with
  | nil => intern_ty N s A
  | (B :: Delta) => intern N Delta (Lam B s) (Imp B A)
  end.

Lemma intern_correct N Gamma s A t B: valid N Gamma -> intern N Gamma s A = (t ,B ) -> (istype N A <-> istype 0 B ) /\ (hastype N Gamma s A <-> hastype 0 nil t B ).
Proof.
  intros H. revert s A t B. induction H; intros s C t B E; simpl in *.
  - inv E. firstorder.
  - apply IHvalid in E as [IHty IHtm]. split; eapply iff_trans; eauto; split; intros K.
    + now constructor.
    + now inv K.
    + constructor. now asimpl.
    + inv K. now asimpl in H2.
  - apply IHvalid in E as [IHty IHtm]. split; eapply iff_trans; eauto; split; intros K.
    + now constructor.
    + now inv K.
    + now constructor.
    + now inv K.
Qed.