# Library Lib_Typed_Lambda

``` ```
An implementation of the simply-typed lambda calculus parameterized over a set of base types and base constants.

Author: Brian Aydemir.
``` Require Import Metatheory. ```
We parameterize the sorts (types) for our simply-typed lambda calculus over a set of base sorts. We define these sorts here in order to make it possible to define a signature for the base constants of the language.
``` Inductive lambda_sort (A : Set) : Set :=   | lt_base : A -> lambda_sort A   | lt_arrow : lambda_sort A -> lambda_sort A -> lambda_sort A. Implicit Arguments lt_base [A]. Implicit Arguments lt_arrow [A]. ```
We need the following in order to define the syntax of a language.

• `const`: A set of base constants defining the constructors of the language.

• `base_sort`: A set of base sorts defining the syntactic categories of the language. Equality on these sorts must be decidable.

• `signature`: Defines the arities/sorting of each of the base constants.
``` Module Type CONST.   Parameter const : Set.   Parameter base_sort : Set.   Axiom eq_base_sort_dec : forall A B : base_sort, {A = B} + {A <> B}.   Parameter signature : const -> lambda_sort base_sort.   Hint Resolve eq_base_sort_dec. End CONST. ```

# Parameterized lambda calculus

``` ```
We parameterize the lambda calculus over a set of base constants.
``` Module Lam (Const : CONST). Import Const. ```

## Preliminaries

``` Notation Local sort := (lambda_sort base_sort). ```
Equality on sorts is decidable.
``` Definition eq_sort_dec : forall (A B : sort), {A = B} + {A <> B}. Hint Resolve eq_sort_dec. ```

## Pre-terms

``` Inductive syntax : Set :=   | bvar : nat -> syntax   | fvar : atom -> syntax   | abs : sort -> syntax -> syntax   | app : syntax -> syntax -> syntax   | const : Const.const -> syntax. Coercion bvar : nat >-> syntax. Coercion fvar : atom >-> syntax. ```

## Basic operations

``` Fixpoint open_rec (k : nat) (u : syntax) (e : syntax) {struct e} : syntax :=   match e with     | bvar i => if k === i then u else (bvar i)     | fvar x => fvar x     | abs T e1 => abs T (open_rec (S k) u e1)     | app e1 e2 => app (open_rec k u e1) (open_rec k u e2)     | const v => e   end. Notation Local "{ k ~> u } t" := (open_rec k u t) (at level 67). Definition open e u := open_rec 0 u e. Fixpoint subst (z : atom) (u : syntax) (e : syntax) {struct e} : syntax :=   match e with     | bvar i => bvar i     | fvar x => if x == z then u else (fvar x)     | abs T e1 => abs T (subst z u e1)     | app e1 e2 => app (subst z u e1) (subst z u e2)     | _ => e   end. Notation Local "[ z ~> u ] e" := (subst z u e) (at level 68). Fixpoint fv (e : syntax) {struct e} : atoms :=   match e with     | bvar i => {}     | fvar x => singleton x     | abs T e1 => (fv e1)     | app e1 e2 => (fv e1) `union` (fv e2)     | _ => {}   end. Fixpoint close_rec (k : nat) (x : atom) (e : syntax) {struct e} : syntax :=   match e with     | bvar i => bvar i     | fvar y => if x == y then (bvar k) else (fvar y)     | abs T e1 => abs T (close_rec (S k) x e1)     | app e1 e2 => app (close_rec k x e1) (close_rec k x e2)     | const c => const c   end. Definition close e x := close_rec 0 x e. ```

## Local closure

``` Notation Local "[ x ]" := (x :: nil) (at level 68). Notation Local env := (list (atom * sort)). ```
The statement of `lc_const` is chosen such that it works well with Coq's automation facilities.
``` Inductive lc : env -> syntax -> sort -> Prop :=   | lc_const : forall E c T,       ok E ->       signature c = T ->       lc E (const c) T   | lc_var : forall E x T,       ok E ->       binds x T E ->       lc E (fvar x) T   | lc_app : forall E e1 e2 T1 T2,       lc E e1 (lt_arrow T1 T2) ->       lc E e2 T1 ->       lc E (app e1 e2) T2   | lc_abs : forall L E e T1 T2,       (forall x, x `notin` L -> lc ([(x,T1)] ++ E) (open e x) T2) ->       lc E (abs T1 e) (lt_arrow T1 T2). Hint Constructors lc. Definition lc' (s : syntax) : Prop :=   exists E, exists T, lc E s T. Hint Unfold lc'. Definition body (E : env) (e : syntax) (T1 T2 : sort) : Prop :=   exists L, forall x : atom, x `notin` L -> lc ([(x,T1)] ++ E) (open e x) T2. Hint Unfold body. Definition body' (e : syntax) : Prop :=   exists E, exists T1, exists T2, body E e T1 T2. Hint Unfold body'. Inductive level : nat -> syntax -> Prop :=   | level_bvar : forall n i,       i < n ->       level n (bvar i)   | level_fvar : forall n x,       level n (fvar x)   | level_abs : forall T n e,       level (S n) e ->       level n (abs T e)   | level_app : forall n e1 e2,       level n e1 ->       level n e2 ->       level n (app e1 e2)   | level_const : forall n c,       level n (const c). Hint Constructors level. ```

## Essential properties

``` Lemma open_rec_lc_core : forall e j v i u,   i <> j ->   {j ~> v} e = {i ~> u} ({j ~> v} e) ->   e = {i ~> u} e. Lemma open_rec_lc : forall k u e,   lc' e ->   e = {k ~> u} e. Lemma subst_open_rec : forall (x : atom) e1 e2 u k,   lc' u ->   [x ~> u] ({k ~> e2} e1) = {k ~> [x ~> u] e2} ([x ~> u] e1). Lemma subst_open : forall (x : atom) e1 e2 u,   lc' u ->   [x ~> u] (open e1 e2) = open ([x ~> u] e1) ([x ~> u] e2). Lemma subst_open_var : forall (x y : atom) u e,   y <> x ->   lc' u ->   open ([x ~> u] e) y = [x ~> u] (open e y). Lemma subst_intro_rec : forall (x : atom) e u k,   x `notin` fv e ->   {k ~> u} e = [x ~> u] ({k ~> x} e). Lemma subst_intro : forall x e u,   x `notin` fv e ->   open e u = subst x u (open e x). Lemma lc_regular : forall E e T,   lc E e T ->   ok E. Hint Local Resolve lc_regular. Lemma lc_weakening : forall E F G e T,   lc (F ++ E) e T ->   ok (F ++ G ++ E) ->   lc (F ++ G ++ E) e T. Lemma lc_weakening_head : forall E F e T,   lc E e T ->   ok (F ++ E) ->   lc (F ++ E) e T. Lemma subst_lc : forall E F T U e u x,   lc (F ++ [(x,U)] ++ E) e T ->   lc E u U ->   lc (F ++ E) ([x ~> u] e) T. Lemma subst_fresh : forall (x : atom) u e,   x `notin` fv e ->   e = [x ~> u] e. Lemma lc_open_from_body : forall L E e1 e2 T1 T2,   (forall x : atom, x `notin` L -> lc ([(x,T1)] ++ E) (open e1 x) T2) ->   lc E e2 T1 ->   lc E (open e1 e2) T2. Lemma open_injective_rec : forall (x : atom) e1 e2 k,   x `notin` (fv e1 `union` fv e2) ->   open_rec k x e1 = open_rec k x e2 ->   e1 = e2. Lemma open_injective : forall (x : atom) e1 e2,   x `notin` (fv e1 `union` fv e2) ->   open e1 x = open e2 x ->   e1 = e2. Lemma level_promote : forall n e,   level n e ->   level (S n) e. Lemma level_open : forall e n (x : atom),   level n (open_rec n x e) ->   level (S n) e. Lemma level_of_lc : forall e,   lc' e -> level 0 e. Lemma open_close_inv_rec : forall e k (x : atom),   level k e ->   open_rec k x (close_rec k x e) = e. Lemma open_close_inv : forall e (x : atom),   lc' e ->   open (close e x) x = e. Lemma close_fresh_rec : forall e k x,   x `notin` fv (close_rec k x e). Lemma close_fresh : forall e x,   x `notin` fv (close e x). ```

## Automation

``` ```
NOTE: "`Hint Constructors lc`" is declared above.
``` ```
NOTE: `lc_open_from_body` interacts poorly with `lc_abs`.
``` Hint Resolve   subst_lc   lc_weakening lc_weakening_head   level_of_lc close_fresh_rec close_fresh. ```
NOTE: The following hint is specifically for aiding applications of `lc_const`.
``` Hint Extern 1 (signature _ = _) =>   simpl signature; try eapply refl_equal. End Lam. ```