RSC.stlc

(* (c) 2018, Jonas Kaiser *)

Traditional, 2-sorted STLC with one abstract base type, derived from 2-sorted SysF of the CPP paper

We define a de Bruijn presentation of traditional, 2-sorted STLC and develop its theory. Note that we handle base types via type variables, which cannot be abstracted over. 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 (x : var)
| Imp (A B : ty).

Terms
Inductive tm : Type :=
| Var (x : var)
| App (s t : tm)
| Lam (A : ty) (s : {bind 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, no heterogeneous instantiation necessary ...
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 Ids_tm : Ids tm. derive. Defined.
Instance Rename_tm : Rename tm. derive. Defined.
Instance Subst_tm : Subst tm. derive. Defined.
Instance SubstLemmas_tm : SubstLemmas tm. derive. Qed.

Type System

Type Formation Judgement: Ensures that a type is constructed from the base types/vars and implication.
Inductive istype (N : nat) : ty -> Prop :=
| istype_tyvar x : x < N -> istype N (TyVar x)
| istype_imp A B : istype N A -> istype N B -> istype N (Imp A B).

Typing Judgment; Note the context lookup is non-dependent since the free variables in a typing context are all type variabels, 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).

Theory

We need a small bit of renaming infrastructure to ensure that context validity is preserved under renaming.
Definition istype_cr (xi : var -> var) (N M : nat) := forall n, n < N -> (xi n) < M.

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. Qed.

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

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

The rest of the theory is not relevant to the correspondence proof, which in particular allows to obtain beta subsitutivity from the corresponding PTS. It is still an instructive example of the CML proof pattern.

Definition hastype_cr zeta (Gamma Delta : list ty) := forall x A, atn Gamma x A -> atn Delta (zeta x) A.

Lemma hastype_cr_id Gamma : hastype_cr id Gamma Gamma.
Proof. intros n A. auto. Qed.

Lemma hastype_cr_up A zeta Gamma Delta :
  hastype_cr zeta Gamma Delta -> hastype_cr (upren zeta) (A :: Gamma) (A :: Delta).
Proof.
  intros CR [|n] B L; inv L; asimpl.
  - constructor.
  - constructor; auto.
Qed.

Lemma hastype_ren N Gamma s A:
  hastype N Gamma s A -> forall Delta zeta, hastype_cr zeta Gamma Delta -> hastype N Delta s.[ren zeta] A.
Proof.
  intros H. induction H; intros Delta zeta CR; subst; asimpl.
  - constructor; trivial. now apply CR.
  - econstructor; eauto.
  - constructor; eauto using hastype_cr_up.
Qed.

Lemma hastype_cr_shift B Gamma : hastype_cr (+1) Gamma (B :: Gamma).
Proof. intros n A H. now constructor. Qed.

Corollary hastype_weaken B N Gamma s A:
  hastype N Gamma s A -> hastype N (B :: Gamma) s.[ren (+1)] A.
Proof. intros H. eapply hastype_ren; eauto using hastype_cr_shift. Qed.

Definition hastype_cm tau N (Gamma Delta : list ty) := forall x A, hastype N Gamma (Var x) A -> hastype N Delta (tau x) A.

Lemma hastype_cm_id N Gamma : hastype_cm ids N Gamma Gamma.
Proof. intros n A. auto. Qed.

Lemma hastype_cm_up A tau N Gamma Delta :
  hastype_cm tau N Gamma Delta -> hastype_cm (up tau) N (A :: Gamma) (A :: Delta).
Proof.
  intros CM [|n] B L; inv L; asimpl.
  - inv H0. constructor; trivial. constructor.
  - inv H0. apply hastype_weaken, CM. now constructor.
Qed.

Lemma hastype_subst N Gamma s A:
  hastype N Gamma s A -> forall Delta tau, hastype_cm tau N Gamma Delta -> hastype N Delta s.[tau] A.
Proof.
  intros H. induction H; intros Delta tau CM; subst; asimpl.
  - apply CM. now constructor.
  - econstructor; eauto.
  - constructor; eauto using hastype_cm_up.
Qed.

Lemma hastype_cm_beta t B N Gamma : hastype N Gamma t B -> hastype_cm (t .: ids) N (B :: Gamma) Gamma.
Proof. intros T [|n] A H; inv H; asimpl; inv H1; trivial. now constructor. Qed.

Corollary hastype_beta t B N Gamma s A:
  hastype N Gamma t B -> hastype N (B :: Gamma) s A -> hastype N Gamma s.[t/] A.
Proof. intros H1 H2. eapply hastype_subst; eauto using hastype_cm_beta. Qed.

Propagation

Theorem propagation N Gamma s A : hastype N Gamma s A -> istype N A.
Proof.
  intros H; induction H; trivial.
  - now inv IHhastype1.
  - now constructor.
Qed.

Validity of Contexts

Inductive valid (N : nat) : list ty -> Prop :=
| valid_nil : valid N nil
| valid_ext A Gamma : istype N A -> valid N Gamma -> valid N (A :: Gamma).

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.
  - constructor.
  - asimpl. constructor; auto. eapply istype_ren; eauto.
Qed.

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

Internalising contexts

Note that the STLC can internalise its term variabel context but not its type variabel context.

Fixpoint intern_ctx (Gamma : list ty) (s : tm) (A : ty) : (tm * ty) :=
  match Gamma with
  | nil => (s,A)
  | (B :: Delta) => intern_ctx Delta (Lam B s) (Imp B A)
  end.

Lemma intern_ctx_correct N Gamma s A t B:
  valid N Gamma -> intern_ctx Gamma s A = (t,B) -> (istype N A <-> istype N B) /\ (hastype N Gamma s A <-> hastype N nil t B).
Proof.
  intros V; revert s A t B. induction V; intros; simpl in *.
  - inversion H; firstorder.
  - apply IHV in H0 as [E1 E2]. split; eapply iff_trans; eauto; split; intros J.
    + now constructor.
    + now inv J.
    + now constructor.
    + now inv J.
Qed.