Library STLC1

Simply typed lambda calculus in Curry style

Require Import Framework.
Implicit Types rho : type_context.

Implicit Types x y z : var.

Implicit Types u v : inttype -> Prop.

Simple type syntax

Inductive simpletype : Type :=
| base (x : var) : simpletype
| arr (A B : simpletype) : simpletype.

Implicit Types A B C : simpletype.

STLC uses contexts

Definition stlc_ctx := var -> simpletype.
Implicit Types Gamma Delta : stlc_ctx.

The typing rules of STLC

Inductive stlc_ty : stlc_ctx -> term -> simpletype -> Prop :=
| stlctyvar Gamma x : stlc_ty Gamma x (Gamma x)
| stlctyapp Gamma s t A B : stlc_ty Gamma s (arr A B) -> stlc_ty Gamma t A -> stlc_ty Gamma (s t) B
| stlctylam Gamma s A B : stlc_ty (A .: Gamma) s B -> stlc_ty Gamma (Lam s) (arr A B).

We interpret variables according to the valuation, arrows as functional products

Fixpoint int_ty A sigma := match A with
                           | base x => sigma x
                           | arr A B => prod (int_ty A sigma) (int_ty B sigma)
                           end.

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

This trivially preserves realizor predicates

Lemma int_ty_rp : rp_preservation simpletype int_ty.
hnf.
induction T ; simpl ; auto using prod_realizable.
Qed.

The type interpretation also easily respects the typing judgement

Lemma in_int_ty : adequacy simpletype int_ty stlc_ty.
hnf.
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 IHstlc_ty1 ; 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 ([s] (u .: rho)) ; eauto using int_ty_rp, int_lam, only_filter, valid_up, validates_up.
Qed.

STLC terminates

Corollary sn_stlc Gamma t A : stlc_ty Gamma t A -> SN t.
apply sn with int_ty ; auto using in_int_ty, int_ty_rp.
Qed.