(* (c) 2017, Jonas Kaiser, based on major contributions from Tobias Tebbi *)

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 its theory. The definitions are those from our 2017 CPP paper.

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

Require Import Decidable lib.

Set Implicit Arguments.


Inductive typeF : Type :=
| TyVarF (x : var)
| ImpF (A B : typeF)
| AllF (A : {bind typeF}).

Inductive termF : Type :=
| TmVarF (x : var)
| AppF (s t : termF)
| LamF (A : typeF) (s : {bind termF})
| TySpecF (s : termF) (A : typeF)
| TyAbsF (s : {bind typeF in termF}).

Decidable Equality on the type and term syntax
Instance decide_eq_typeF (A B : typeF) : Dec (A = B). derive. Defined.
Instance decide_eq_termF (s t : termF) : Dec (s = t). derive. Defined.

Autosubst machinery
Instance Ids_typeF : Ids typeF. derive. Defined.
Instance Rename_typeF : Rename typeF. derive. Defined.
Instance Subst_typeF : Subst typeF. derive. Defined.
Instance SubstLemmas_typeF : SubstLemmas typeF. derive. Qed.
Instance HSubst_termF : HSubst typeF termF. derive. Defined.
Instance Ids_termF : Ids termF. derive. Defined.
Instance Rename_termF : Rename termF. derive. Defined.
Instance Subst_termF : Subst termF. derive. Defined.
Instance HSubstLemmas_termF : HSubstLemmas typeF termF. derive. Qed.
Instance SubstHSubstComp_typeF_termF : SubstHSubstComp typeF termF. derive. Qed.
Instance SubstLemmas_termF : SubstLemmas termF. derive. Qed.

Illustration of heterogeneos subst s.|tau.sigma (also written stau,sigma) reduction rules for reference
Goal forall x sigma tau, (TmVarF x).|[tau].[sigma] = sigma(x). autosubst. Qed.
Goal forall s t sigma tau, (AppF s t).|[tau].[sigma] = AppF s.|[tau].[sigma] t.|[tau].[sigma]. autosubst. Qed.
Goal forall A s sigma tau, (LamF A s).|[tau].[sigma] = LamF A.[tau] s.|[tau].[up sigma]. autosubst. Qed.
Goal forall s A sigma tau, (TySpecF s A).|[tau].[sigma] = TySpecF s.|[tau].[sigma] A.[tau]. autosubst. Qed.
Goal forall s sigma tau, (TyAbsF s).|[tau].[sigma] = TyAbsF s.|[up tau].[sigma >>| (ren (+1))]. autosubst. Qed.

Type System

Type Formation Judgement
Inductive istyF (N : nat) : typeF -> Prop :=
| istyF_var x : x < N -> istyF N (TyVarF x)
| istyF_imp A B : istyF N A -> istyF N B -> istyF N (ImpF A B)
| istyF_all A : istyF (1+N) A -> istyF N (AllF A).

Typing Judgment
Inductive typingF (N : nat) (Gamma : list typeF) : termF -> typeF -> Prop :=
| typingF_var x A :
    atn Gamma x A -> istyF N A ->
    typingF N Gamma (TmVarF x) A
| typingF_app s t A B :
    typingF N Gamma s (ImpF A B) -> typingF N Gamma t A ->
    typingF N Gamma (AppF s t) B
| typingF_lam s A B :
    istyF N A -> typingF N (A :: Gamma) s B ->
    typingF N Gamma (LamF A s) (ImpF A B)
| typingF_tyspec s A A' B :
    istyF N B -> typingF N Gamma s (AllF A) -> A' = A.[B/] ->
    typingF N Gamma (TySpecF s B) A'
| typingF_tyabs s A :
    typingF (1 + N) Gamma..[ren (+1)] s A ->
    typingF N Gamma (TyAbsF s) (AllF A).

Definition cr_istyF (rho xi : var -> var) N M := forall x, istyF N (TyVarF (rho x)) -> istyF M (TyVarF (xi x)).

Lemma cr_istyF_id N : cr_istyF id id N N.
Proof. intros n. auto. Qed.

Lemma cr_istyF_up rho xi N M : cr_istyF rho xi N M -> cr_istyF (upren rho) (upren xi) (1 + N) (1 + M).
  intros CR [|n] L; asimpl in *.
  - constructor. omega.
  - ainv. cut (rho n < N); [intros H|omega]. aspec. constructor. ainv. omega.

Lemma istyF_ren N A rho:
  istyF N A.[ren rho] -> forall M xi, cr_istyF rho xi N M -> istyF M A.[ren xi].
  intros H. depind H; intros M xi CR; destruct A; ainv.
  - apply CR. now constructor.
  - constructor; eauto.
  - constructor. asimpl. eapply IHistyF; eauto using cr_istyF_up. autosubst.

Lemma cr_istyF_shift N : cr_istyF id (+1) N (1 + N).
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.

Lemma cr_istyF_ushift N : cr_istyF (+1) id (1 + N) N.
Proof. intros n H. asimpl in *. ainv. constructor. omega. Qed.

Corollary istyF_weaken N A: istyF N A -> istyF (1 + N) A.[ren (+1)].
Proof. intros H. eapply istyF_ren; eauto using cr_istyF_shift. now asimpl. Qed.

Corollary istyF_strengthen N A: istyF (1 + N) A.[ren (+1)] -> istyF N A.
Proof. intros H. eapply istyF_ren in H; eauto using cr_istyF_ushift. now asimpl in *. Qed.

Definition cm_istyF (sigma : var -> typeF) N M := forall x, istyF N (TyVarF x) -> istyF M (sigma x).

Lemma cm_istyF_up sigma N M : cm_istyF sigma N M -> cm_istyF (up sigma) (1 + N) (1 + M).
  intros CM [|x] T; ainv; asimpl.
  - constructor. omega.
  - apply lt_S_n in H0. apply istyF_weaken. apply CM. now constructor.

Lemma istyF_subst N A : istyF N A -> forall M sigma, cm_istyF sigma N M -> istyF M A.[sigma].
  intros H. induction H; intros M sigma CM.
  - apply CM. now constructor.
  - constructor; auto.
  - constructor; auto using cm_istyF_up.

Lemma cm_istyF_beta N B : istyF N B -> cm_istyF (B .: ids) (1 + N) N.
Proof. intros T [|x] H; asimpl; trivial. now apply istyF_strengthen. Qed.

Theorem istyF_beta N A B : istyF N B -> istyF (1 + N) A -> istyF N A.[B/].
Proof. intros H T. eapply istyF_subst; eauto using cm_istyF_beta. Qed.

Definition cr_typingF zeta N Gamma Delta := forall x A, typingF N Gamma (TmVarF x) A -> typingF N Delta (TmVarF (zeta x)) A.

Lemma cr_typingF_id N Gamma : cr_typingF id N Gamma Gamma.
Proof. intros n A. auto. Qed.

Lemma cr_typingF_up A zeta N Gamma Delta :
  cr_typingF zeta N Gamma Delta -> cr_typingF (upren zeta) N (A :: Gamma) (A :: Delta).
  intros CR [|n] B L; ainv; asimpl.
  - constructor; trivial. constructor.
  - constructor; trivial. constructor.
    cut (typingF N Gamma (TmVarF n) B); [intros J| now constructor]. apply CR in J. ainv.

Lemma cr_typingF_ren zeta N Gamma Delta :
  cr_typingF zeta N Gamma Delta ->
  forall M xi, cr_istyF xi id M N -> cr_typingF zeta M Gamma..[ren xi] Delta..[ren xi].
  intros CR2 M xi CR1. intros x B L. inversion L; subst.
  destruct (mmap_atn H0) as [B' [EB' L']]; subst.
  assert (H2' : istyF N B'). eapply istyF_ren in H1; eauto. now asimpl in *.
  assert (H3 : typingF N Gamma (TmVarF x) B') by now constructor.
  apply CR2 in H3. inversion H3; subst.
  constructor; trivial. eapply atn_mmap; eauto.

Corollary cr_typingF_ren_ushift zeta N Gamma Delta :
  cr_typingF zeta N Gamma Delta -> cr_typingF zeta (1 + N) Gamma..[ren (+1)] Delta..[ren (+1)].
Proof. intros CR. eapply cr_typingF_ren; eauto using cr_istyF_ushift. Qed.

Lemma typingF_ren N Gamma s A:
  typingF N Gamma s A ->
  forall M Delta xi zeta,
    cr_istyF id xi N M ->
    cr_typingF zeta N Gamma Delta ->
    typingF M Delta..[ren xi] s.[ren zeta].|[ren xi] A.[ren xi].
  intros H. induction H; intros M Delta xi zeta CR1 CR2; subst; asimpl.
  - constructor.
    + eapply atn_mmap; eauto.
      cut (typingF N Gamma (TmVarF x) A); [intros J | now constructor].
      apply CR2 in J. ainv.
    + eapply istyF_ren; eauto. now asimpl.
  - econstructor.
    + specialize (IHtypingF1 _ _ _ _ CR1 CR2); asimpl in *; eauto.
    + specialize (IHtypingF2 _ _ _ _ CR1 CR2); asimpl in *; eauto.
  - constructor.
    + eapply istyF_ren; eauto. now asimpl.
    + apply cr_typingF_up with (A:=A) in CR2.
      specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
  - econstructor.
    + eapply istyF_ren; eauto. now asimpl.
    + specialize (IHtypingF _ _ _ _ CR1 CR2). asimpl in *; eauto.
    + autosubst.
  - constructor. asimpl.
    replace (Delta..[ren (xi >>> (+1))]) with (Delta..[ren (+1)]..[ren (upren xi)]) by autosubst.
    replace (s.|[ren (upren xi)].[ren zeta]) with (s.[ren zeta].|[ren (upren xi)]) by autosubst.
    apply IHtypingF.
    + apply cr_istyF_up in CR1. now asimpl in *.
    + now apply cr_typingF_ren_ushift.

Lemma cr_typingF_shift B N Gamma : cr_typingF (+1) N Gamma (B :: Gamma).
Proof. intros n A H. ainv. constructor; trivial. now constructor. Qed.

Corollary typingF_weaken B N Gamma s A:
  typingF N Gamma s A -> typingF N (B :: Gamma) s.[ren (+1)] A.
  intros H.
  pose proof (typingF_ren H (@cr_istyF_id N) (@cr_typingF_shift B N Gamma)) as J.
  asimpl in *. now replace (mmap id Gamma) with Gamma in J by autosubst.

Corollary typingF_ren_ty N Gamma s A:
  typingF N Gamma s A ->
  forall M xi, cr_istyF id xi N M ->
         typingF M Gamma..[ren xi] s.|[ren xi] A.[ren xi].
  intros H M xi CR. pose proof (typingF_ren H CR (@cr_typingF_id N Gamma)) as J.
  now asimpl in *.

Corollary typingF_weaken_ty N Gamma s A :
  typingF N Gamma s A -> typingF (1 + N) Gamma..[ren (+1)] s.|[ren (+1)] A.[ren (+1)].
Proof. intros H. eapply typingF_ren_ty; eauto using cr_istyF_shift. Qed.

Internalising contexts

Fixpoint internF_ty (N : nat) (s : termF) (A : typeF) : (termF * typeF) :=
  match N with
  | 0 => (s,A)
  | (S M) => internF_ty M (TyAbsF s) (AllF A)

Fixpoint internF (N : nat) (Gamma : list typeF) (s : termF) (A : typeF) : (termF * typeF) :=
  match Gamma with
  | nil => internF_ty N s A
  | (B :: Delta) => internF N Delta (LamF B s) (ImpF B A)

Inductive wfF : nat -> list typeF -> Prop :=
| wfF_empty : wfF 0 nil
| wfF_ext_ty N : wfF N nil -> wfF (S N) nil (* note: restriction to nil *)
| wfF_ext_tm N Gamma A : istyF N A -> wfF N Gamma -> wfF N (A :: Gamma).

Lemma internF_correct N Gamma s A t B: wfF N Gamma -> internF N Gamma s A = (t,B) -> (typingF N Gamma s A <-> typingF 0 nil t B).
  intros H. revert s A t B. induction H; intros; simpl in *.
  - inversion H; firstorder.
  - apply IHwfF in H0. eapply iff_trans; eauto. split.
    + intros. econstructor. eauto.
    + intros. now inversion H1.
  - apply IHwfF in H1. eapply iff_trans; eauto. split.
    + intros. econstructor; eauto.
    + intros. now inversion H2.