Library T1

System T in curry style
Require Import Framework.
Require Import Freevars Types.
Implicit Types rho : type_context.

Implicit Types x y z : var.

Implicit Types u v : inttype -> Prop.

Even though we use curry style, the addition of the numeric primitives forces us to define a new term syntax

Inductive Tterm : Type :=
| Tvar (x : var)
| Tlam (a : {bind Tterm})
| Tapp (a b : Tterm)
| Tprec | TO | TS.

Implicit Types a b c : Tterm.
Coercion Tapp : Tterm >-> Funclass.
Coercion Tvar : var >-> Tterm.

Boilerplate for Autosubst

Instance Ids_Tterm : Ids Tterm. derive. Defined.
Instance Rename_Tterm : Rename Tterm. derive. Defined.
Instance Subst_Tterm : Subst Tterm. derive. Defined.
Instance SubstLemmas_Tterm : SubstLemmas Tterm. derive. Qed.

beta reduction

Inductive T_step : Tterm -> Tterm -> Prop :=
| Tbeta a b : T_step ((Tlam a) b) (a.[b /])
| TappL a a' b : T_step a a' -> T_step (a b) (a' b)
| TappR a b b' : T_step b b' -> T_step (a b) (a b')
| TprecO b c : T_step (Tprec TO b c) b
| TprecS a b c : T_step (Tprec (TS a) b c) (c a (Tprec a b c)).

Notation "' x" := (x : var) (at level 1).

We compile the primitives as their Church-Scott encoding, which means that n is encoded as the primitive recursor applied to n. Thus primitive recursion becomes the identity mapping.

Fixpoint compile a : term := match a with
                      | Tvar x => x
                      | Tlam a => Lam (compile a)
                      | Tapp a b => (compile a) (compile b)
                      | Tprec => Lam '0
                      | TO => Lam (Lam '1)
                      | TS => Lam (Lam (Lam ('0 '2 ((Lam '0) '2 '1 '0))))
                      end.

The compiler is stable under renaming
Lemma compile_ren_full a r : compile a.[ren r] = (compile a).[ren r].
revert r.
induction a ; intros r ; asimpl ; auto.
Qed.

The compiler is stable under compiled substitution
Lemma compile_subst_full a sT sS : (forall x, sS x = compile (sT x)) -> compile a.[sT] = (compile a).[sS].
revert sT sS.
induction a ; intros sT sS E ; asimpl ; auto.
- f_equal. apply IHa. intros [|x] ; asimpl ; auto. rewrite compile_ren_full; auto.
- rewrite IHa1 with sT sS, IHa2 with sT sS ; auto.
Qed.

The compiler is stable under compiled beta substitution
Corollary compile_subst a b : compile a.[b/] = (compile a).[compile b/].
apply compile_subst_full.
intros [|x] ; auto. Qed.

The compiler is consistent
Lemma TC_c : compiler_consistency _ compile T_step.
intros a b. induction 1 ; simpl.
- rewrite compile_subst. repeat constructor.
- now apply steps_appL.
- now apply steps_appR.
- econstructor 2. repeat constructor.
  econstructor 2. repeat constructor.
  repeat constructor.
  apply step_beta_eq. autosubst.
- econstructor 2. repeat constructor.
  econstructor 2. repeat constructor.
  econstructor 2. repeat constructor.
  constructor.
  asimpl. apply step_beta_eq.
  autosubst.
Qed.

System T has only NAT and the arrow types
Inductive Ttype : Type :=
| NAT
| arr (A B : Ttype).

Implicit Types A B C : Ttype.
Infix "-->" := arr.

System T uses contexts
Definition T_ctx := var -> Ttype.
Implicit Types Gamma Delta : T_ctx.

The typing judgements of System T
Inductive T_ty : T_ctx -> Tterm -> Ttype -> Prop :=
| Ttyvar Gamma x : T_ty Gamma x (Gamma x)
| Ttyapp Gamma a b A B : T_ty Gamma a (A --> B) -> T_ty Gamma b A -> T_ty Gamma (a b) B
| Ttylam Gamma a A B : T_ty (A .: Gamma) a B -> T_ty Gamma (Tlam a) (A --> B)
| Ttyprec Gamma A : T_ty Gamma Tprec (NAT --> A --> (NAT --> A --> A) --> A)
| TtyO Gamma : T_ty Gamma TO NAT
| TtyS Gamma : T_ty Gamma TS (NAT --> NAT)
.

The interpretation of the NAT type is inductively as follows:
  • the top filter is included
  • the term interpretation of TO is included
  • if v is included, so is the interpretation of TS applied to v
Inductive int_nat u : Prop :=
| top_nat : u ~ top -> int_nat u
| O_nat : u ~ [compile TO] top_rho -> int_nat u
| S_nat v : int_nat v -> u ~ [compile TS]top_rho @ v -> int_nat u.

The interpretation of NAT is a filter
Lemma int_nat_filter u : int_nat u -> IFilter u.
induction 1 as [ ? E | ? E | ? ? ? ? E ].
- now refine (equiv_filter _ _ _ (filter_equiv_sym E)).
- refine (equiv_filter _ _ _ (filter_equiv_sym E)). eauto using int_IF, top_rho_valid.
- refine (equiv_filter _ _ _ (filter_equiv_sym E)). apply closure_filter.
Qed.

Infix "==>" := Arr (at level 55, right associativity).
Coercion BASE : nat >-> basetype.

A filter includes a Ktype if it includes F ==> A ==> F for some A and F. Thus it is also not empty.
Inductive Ktype u : Prop :=
| inKtype (F : basetype) (A : inttype) : u (F ==> A ==> F) -> Ktype u.

The interpretation of TS maps Ktypes to Ktypes. Note that a Ktype also includes (F ==> A ==> F) o (F ==> A ==> F) since it is closed under intersection.

Lemma ty_S (A : inttype) (F : basetype) : [compile TS]top_rho (
  (F ==> A ==> F) o (F ==> A ==> F) ==>
  F ==>
  ((F ==> A ==> F) ==> F ==> F) o A ==>
  F)
.
exists (S ((S (0 + 0) + S (S (S(0 + 0) + 0) + 0)))) Empty.
{ cbv ; eauto. }
repeat constructor.
econstructor.
econstructor.
eapply (tyVarA _ (((F ==> A ==> F) ==> F ==> F : type) .: OMEGA .: OMEGA .: Empty)).
simpl ; reflexivity.
eapply (tyVarA _ (OMEGA .: OMEGA .: ((F ==> A ==> F) : type) .: Empty)).
simpl ; reflexivity.
intros [|x] ; auto.
econstructor.
econstructor.
econstructor.
econstructor.
eapply (tyVarA _ (((F ==> A ==> F) : type) .: Empty)).
simpl ; reflexivity.
eapply (tyVarA _ (OMEGA .: OMEGA .: (F ==> A ==> F : type) .: Empty)).
simpl ; reflexivity.
simpl ; reflexivity.
eapply (tyVarA _ (OMEGA .: (F : type) .: OMEGA .: Empty)).
simpl ; reflexivity.
reflexivity.
eapply (tyVarA _ ((A : type) .: OMEGA .: OMEGA .: Empty)).
simpl ; reflexivity.
reflexivity.
intros [| [| [|x] ] ] ; simpl ; auto.
Qed.

Consequently, filters in the interpretation of NAT are Ktypes
Lemma k_nat u : int_nat u -> Ktype u.
induction 1 as [ ? E | ? E | ? ? Nv [F A P] E ].
- exists (BASE 0) (BASE 1).
  now apply E.
- exists (BASE 0) (BASE 1).
  apply E.
  exists 0 Empty ; cbv ; eauto.
- exists F (((F ==> A ==> F) ==> F ==> F) o A).
  apply E.
  constructor.
  exists ((F ==> A ==> F) o (F ==> A ==> F)) ; eauto using ty_S.
  now apply int_nat_filter.
Qed.

And thus the interpretation of NAT is a realizor predicate
Lemma rp_nat : realizorPredicate int_nat.
constructor.
- intros u Nu. destruct (k_nat u Nu) ; eauto.
- eauto using top_nat, filter_equiv_refl.
- apply int_nat_filter.
- intros u v e Nu.
  induction Nu ; eauto using filter_equiv_sym, filter_equiv_trans, top_nat, O_nat, S_nat.
Qed.

Hint Resolve rp_nat.

We interpret NAT with the type we defined earlier and arrows as functional products

Fixpoint int_ty A (sigma : rc_ctx):= match A with
                           | NAT => int_nat
                           | arr A B => prod (int_ty A sigma) (int_ty B sigma)
                           end.

Notation "[[ A ]]" := (int_ty A) (at level 1).

This trivially preserves realizor candidates
Lemma int_ty_rp : rp_preservation Ttype int_ty.
hnf.
induction T ; simpl ; auto using prod_realizable, rp_nat.
Qed.

In order to recognize type contexts and valuations, they need to validate the context
Inductive val_ty rho sigma t T : Prop := val_ty_gamma tGamma : validates _ int_ty rho tGamma sigma -> T_ty tGamma t T -> val_ty rho sigma t T.

The compiler and interpretation are adequate with relation towards the typing relation
Lemma in_int_ty : cadequacy Ttype int_ty _ compile val_ty.
hnf.
intros rho sigma rho_val sigma_val a A [Gamma rho_sigma_val T].
revert rho sigma rho_val sigma_val rho_sigma_val.
induction T ; 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 ([compile a]rho @ [compile b]rho) ; eauto using int_ty_rp, filter_equiv_sym, int_st.
  apply IHT1 ; eauto.
- constructor ; auto using int_IF.
  intros u Au.
  assert (rpA := int_ty_rp A _ sigma_val).
  assert (exists C : inttype, u C) by now apply rpA.
  apply equiv_closed with ([compile a] (u .: rho)) ; eauto using int_ty_rp, filter_equiv_sym, int_lam, only_filter, valid_up, validates_up.
- split ; auto using int_IF.
  intros vn Hn.
  split ; eauto using closure_filter.
  intros vf Hf.
  split ; eauto using closure_filter.
  intros vx Hx.
  assert (realizorPredicate ([[A]]sigma)) by auto using int_ty_rp.
  assert (realizorPredicate (prod int_nat (prod ([[A]] sigma) ([[A]] sigma)))) by auto using prod_realizable.
  rewrite <- int_lam, int_x ; eauto using only_filter, valid_up, excl_bot.
  simpl.
  induction Hn as [ ? E | ? E | ? ? ? ? E ].
  + rewrite E, <- ! top_app ; eauto using excl_bot.
    now apply incl_top.
  + rewrite E. simpl.
    rewrite <- ! int_lam, int_x ; eauto using valid_up, only_filter, excl_bot, top_rho_valid.
  + rewrite E. simpl.
    rewrite <- ! int_lam, ! int_st, ! int_x ; eauto 7 using valid_up, only_filter, excl_bot, top_rho_valid.
    rewrite <- int_lam, int_x ; simpl ; eauto 9 using valid_up, only_filter, excl_bot, top_rho_valid.
    apply Hx ; eauto using equiv_refl.
- constructor 2. simpl. apply agree_equiv ; auto using top_rho_valid.
  intros x FH. repeat match goal with [ H : FV _ _ |- _] => inversion H ; clear H end.
- split ; auto using int_IF.
  econstructor 3. eassumption.
  rewrite agree_equiv ; eauto using filter_equiv_refl, top_rho_valid.
  intros x FH. repeat match goal with [ H : FV _ _ |- _] => inversion H ; clear H end.
Qed.

The typing recognizes type contexts and valuations
Definition typeable a A := exists Gamma, T_ty Gamma a A.

Lemma T_valid : validation _ _ typeable val_ty.
split.
- intros [Gamma ty]. exists top_rho, top_sigma.
  assert (validates _ int_ty top_rho Gamma top_sigma).
  { intros x. unfold top_rho. apply incl_top. eauto using top_sigma_valuation, int_ty_rp. }
  eauto 6 using top_rho_valid, top_sigma_valuation, val_ty_gamma.
- intros [_ [_ [_ [_ [ tGamma _ tty ] ] ] ] ].
  unfold typeable. eauto.
Qed.

System T terminates
Corollary sn_T Gamma a A : T_ty Gamma a A -> TSN _ T_step a.
intros tyt.
cut (typeable a A).
apply tsn with int_ty compile val_ty ; eauto using in_int_ty, int_ty_rp, TC_c, T_valid.
unfold typeable ; eauto.
Qed.