# Library Lib_Untyped_Lambda

``` Require Import Metatheory. Module Type CONST.   Parameter const : Set. End CONST. ```

# Parameterized lambda calculus

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

## Pre-terms

``` Inductive syntax : Set :=   | bvar : nat -> syntax   | fvar : atom -> syntax   | abs : 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 e1 => abs (open_rec (S k) u e1)     | app e1 e2 => app (open_rec k u e1) (open_rec k u e2)     | const c => const c   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 e1 => abs (subst z u e1)     | app e1 e2 => app (subst z u e1) (subst z u e2)     | const c => const c   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 e1 => (fv e1)     | app e1 e2 => (fv e1) `union` (fv e2)     | const c => {}   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 e1 => abs (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

``` Inductive lc : syntax -> Prop :=   | lc_var : forall x,       lc (fvar x)   | lc_abs : forall L e,       (forall x : atom, x `notin` L -> lc (open e x)) ->       lc (abs e)   | lc_app : forall e1 e2,       lc e1 ->       lc e2 ->       lc (app e1 e2)   | lc_const : forall s,       lc (const s). Hint Constructors lc. Definition body (e : syntax) :=   exists L, forall x : atom, x `notin` L -> lc (open e x). 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 n e,       level (S n) e ->       level n (abs 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 subst_lc : forall (x : atom) u e,   lc e ->   lc u ->   lc ([x ~> u] e). Lemma subst_fresh : forall (x : atom) u e,   x `notin` fv e ->   e = [x ~> u] e. Lemma lc_open_from_body : forall e1 e2,   body e1 ->   lc e2 ->   lc (open e1 e2). Lemma lc_open_from_abs : forall e1 e2,   lc (abs e1) ->   lc e2 ->   lc (open e1 e2). Lemma lc_abs_from_body : forall e,   body e ->   lc (abs e). Lemma body_from_lc_abs : forall e,   lc (abs e) ->   body e. 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_open_from_abs   lc_abs_from_body body_from_lc_abs   level_of_lc close_fresh_rec close_fresh. Hint Extern 1 (body ?e) =>   match goal with     | H : lc (app ?e _) |- _ => inversion_clear H     | H : lc (app _ ?e) |- _ => inversion_clear H   end. End Lam. ```