# Library STLCImpl

``` Require Import Arith. Require Import Axioms. Require Import AuxLib. Require Import Nominal. Require Import STLC. Require Import Wf_nat. Module MakeSTLC <: STLC. ```

## Basic definitions

``` ```
 Term variables.
``` Definition tmvar := mkAtomRec 0. Definition tmvarP := mkAtomPset tmvar. ```
 STLC types.
``` Inductive ty : Set :=   | unit : ty   | arrow : ty -> ty -> ty. Definition tyP := mkIdPset tmvar ty. ```
 `Phi n` is the set of all terms whose bound variables have index less than `n`. Thus, `Phi 0` corresponds to those terms with no dangling bound variables. Free variables are still represented using names.
``` Inductive Phi : nat -> Set :=   | pdot : forall (n : nat), Phi n   | pfree : forall (n : nat), tmvar -> Phi n   | pbound : forall (n i : nat), i < n -> Phi n   | papp : forall (n : nat), Phi n -> Phi n -> Phi n   | plam : forall (n : nat), ty -> Phi (S n) -> Phi n. ```
 We need to take advantage of proof irrelevance when considering equality on `Phi`.
``` Lemma pbound_eq :   forall (n i i': nat), (i = i') ->   forall (p : i < n) (q : i' < n),   pbound n i p = pbound n i' q. Hint Resolve pbound_eq : core nominal. ```
 Free variables.
``` Fixpoint Phi_fv (n : nat) (x : Phi n) {struct x} : aset tmvar :=   match x with     | pdot _ => empty     | pfree _ a => singleton a     | pbound _ _ _ => empty     | papp _ s t => union (Phi_fv _ s) (Phi_fv _ t)     | plam _ _ s => Phi_fv _ s   end. Implicit Arguments Phi_fv [n]. ```
 Size. The fact that `1 + x` converts to `S x` is helpful when defining the recursion combinator below, since it proceeds by induction on natural numbers (the initial value being the size of a term).
``` Fixpoint Phi_size (n : nat) (x : Phi n) {struct x} : nat :=   match x with     | pdot _ => 1     | pfree _ _ => 1     | pbound _ _ _ => 1     | papp _ s t => 1 + (Phi_size _ s) + (Phi_size _ t)     | plam _ _ s => 1 + (Phi_size _ s)   end. Implicit Arguments Phi_size [n]. Lemma Phi_size_eq_O :   forall (T : Type) (n : nat) (x : Phi n), Phi_size x = 0 -> T. Lemma Phi_size_lt_O :   forall (T : Type) (n : nat) (x : Phi n), Phi_size x <= 0 -> T. ```
 We need ``weakening'' on terms in order to define substitution: Any term in `Phi n` is also a term in `Phi (S n)` modulo the proofs carried by `pbound` subterms.
``` Fixpoint Phi_weaken (n : nat) (x : Phi n) {struct x} : Phi (S n) :=   match x in Phi n return Phi (S n) with     | pdot _ => pdot _     | pfree _ a => pfree _ a     | pbound _ i pf => pbound _ i (le_S _ _ pf)     | papp _ s t => papp _ (Phi_weaken _ s) (Phi_weaken _ t)     | plam _ T s => plam _ T (Phi_weaken _ s)   end. Implicit Arguments Phi_weaken [n]. ```
 Case analysis. This lemma is useful when built-in tactics fail to provide similar functionality, for example when you want to analyze `x : Phi (S n)` and `case` fails.
``` Lemma Phi_case :   forall (n : nat) (P : Phi n -> Type),   (P (pdot n)) ->   (forall a, P (pfree n a)) ->   (forall i pf, P (pbound n i pf)) ->   (forall s t, P (papp n s t)) ->   (forall T s, P (plam n T s)) ->   (forall x, P x). ```
 Well-founded induction on size.
``` Lemma Phi_ind_size_multi :   forall (P : forall (n : nat), Phi (S n) -> Type),   (forall n x, (forall m y, Phi_size y < Phi_size x -> P m y) -> P n x) ->   (forall n x, P n x). Lemma Phi_ind_size_single :   forall (n : nat) (P : Phi n -> Type),   (forall x, (forall y, Phi_size y < Phi_size x -> P y) -> P x) ->   (forall x, P x). ```

## Permutations

``` Fixpoint Phi_perm   (n : nat) (p : permt tmvar) (x : Phi n) {struct x} : Phi n :=   match x in Phi n return Phi n with     | pdot _ => pdot _     | pfree _ a => pfree _ (perm tmvarP p a)     | pbound _ i pf => pbound _ i pf     | papp _ s t => papp _ (Phi_perm _ p s) (Phi_perm _ p t)     | plam _ T s => plam _ T (Phi_perm _ p s)   end. Implicit Arguments Phi_perm [n]. Definition PhiPermR (n : nat) : PsetT tmvar (Phi n). ```
 Permutation preserves the size of a term.
``` Lemma Phi_size_perm :   forall (n : nat) (p : permt tmvar) (x : Phi n),   Phi_size (Phi_perm p x) = Phi_size x. ```

## Abstraction and instantiation

``` ```
 Turn a free variable into a bound variable (an index). We turn a term in `Phi n` into a term in `Phi (S n)` and choose `n` as the new index.
``` Fixpoint abs   (n : nat) (a : tmvar) (x : Phi n) {struct x}   : Phi (S n) :=   match x in Phi n return Phi (S n) with     | pdot _ => pdot _     | pfree i a' =>         if atom_eqdec tmvar a a' then pbound (S i) i (lt_n_Sn _)         else pfree _ a'     | pbound i m pf => pbound (S i) m (lt_S _ _ pf)     | papp _ s t => papp _ (abs _ a s) (abs _ a t)     | plam _ T s => plam _ T (abs _ a s)   end. Implicit Arguments abs [n]. ```
 Turn the greatest index (bound variable) in a term into a free variable. A more general version of this function would instantiate the index with an arbitrary term.
``` Definition inst_aux   (n' : nat) (a : tmvar) (x : Phi n') (n : nat) (wf : n' = S n) : Phi n. Definition inst (n : nat) (a : tmvar) (x : Phi (S n)) : Phi n :=   inst_aux (S n) a x n (refl_equal _). Implicit Arguments inst [n]. ```
 The following rewrites make it easier to work with `inst`. It is not usually helpful to unfold `inst` to `inst_aux`.
``` Lemma inst_papp :   forall (n : nat) (a : tmvar) (s t : Phi (S n)),   inst a (papp _ s t) = papp _ (inst a s) (inst a t). Lemma inst_plam :   forall (n : nat) (a : tmvar) (s : Phi (S (S n))) (T : ty),   inst a (plam _ T s) = plam _ T (inst a s). ```
 `abs` preserves the size of terms.
``` Lemma Phi_size_abs :   forall (n : nat) (x : Phi n) (a : tmvar),   Phi_size (abs a x) = Phi_size x. ```
 `inst` preserves the size of terms.
``` Lemma Phi_size_inst :   forall (n : nat) (x : Phi (S n)) (a : tmvar),   Phi_size (inst a x) = Phi_size x. ```
 Permutations commute with `abs`.
``` Lemma Phi_perm_abs :   forall n p c (s : Phi n),   Phi_perm p (abs c s) = abs (perm tmvarP p c) (Phi_perm p s). ```
 Swapping pseudo-commutes with `inst` under certain conditions.
``` Lemma Phi_swap_inst :   forall (n : nat) (x : Phi (S n)) (a c d : tmvar),   ~ In c (Phi_fv x) -> ~ In d (Phi_fv x) ->   perm (PhiPermR n) [(c, d)] (inst a x) = inst (perm tmvarP [(c, d)] a) x. ```
 Swapping commutes with `inst` under certain conditions.
``` Lemma Phi_swap_inst_commute :   forall (n : nat) (x : Phi (S n)) (a c d : tmvar),   a <> c -> a <> d ->   perm (PhiPermR n) [(c, d)] (inst a x) =   inst a (perm (PhiPermR (S n)) [(c, d)] x). ```
 `inst` is the inverse of `abs`.
``` Lemma inst_abs_inv :   forall (n : nat) (x : Phi n) (a : tmvar), inst a (abs a x) = x. ```
 `abs` is the inverse of `inst` under certain conditions.
``` Lemma abs_inst_inv :   forall (n : nat) (x : Phi (S n)) (a : tmvar),   ~ In a (Phi_fv x) -> abs a (inst a x) = x. ```
 The free variables of `abs a x` are the obvious ones.
``` Lemma Phi_fv_abs :   forall (n : nat) (x : Phi n) (a : tmvar),   Phi_fv (abs a x) = remove a (Phi_fv x). ```

## User-level abstraction for terms

``` Definition tm : Set := Phi 0. Definition tmP := PhiPermR 0. Definition dot : tm := pdot 0. Definition var (a : tmvar) : tm := pfree 0 a. Definition app (s t : tm) : tm:= papp 0 s t. Definition lam (x : tmvar) (T : ty) (b : tm) : tm := plam 0 T (abs x b). ```

## Permutations

``` Section STLCPermutations. Variable p : permt tmvar. Variable c : tmvar. Variable T : ty. Variables s t : tm. Theorem perm_dot : perm tmP p dot = dot. Theorem perm_var : perm tmP p (var c) = var (perm tmvarP p c). Theorem perm_app :   perm tmP p (app s t) = app (perm tmP p s) (perm tmP p t). Theorem perm_lam :   perm tmP p (lam c T s) = lam (perm tmvarP p c) T (perm tmP p s). End STLCPermutations. ```

## Free variables

``` Definition fvar : tm -> aset tmvar := Phi_fv (n:= 0). Theorem fvar_dot : fvar dot = empty. Theorem fvar_var : forall a, fvar (var a) = singleton a. Theorem fvar_app : forall s t, fvar (app s t) = union (fvar s) (fvar t). Theorem fvar_lam : forall a T s, fvar (lam a T s) = remove a (fvar s). ```

## Alpha-equality

``` Lemma swap_in_abs :   forall (n : nat) (s : Phi n) (a b : tmvar),   b <> a ->   ~ In a (Phi_fv (Phi_perm [(a, b)] s)) ->   abs b (Phi_perm [(a, b)] s) = abs a s. Lemma eq_lam_diff :   forall a b T T' s s',   T = T' ->   a <> b ->    ~ In b (fvar s) ->   s = perm tmP [(a, b)] s' ->   lam a T s = lam b T' s'. Theorem eq_lam :   forall a b T s,    ~ In b (fvar s) ->   lam a T s = lam b T (perm tmP [(a, b)] s). ```

## Structural induction

``` Theorem tm_induction_weak :   forall (P : tm -> Type),   (P dot) ->   (forall a, P (var a)) ->   (forall s, P s -> forall t, P t -> P (app s t)) ->   (forall a T s, P s -> P (lam a T s)) ->   forall x : tm, P x. Theorem tm_induction :   forall (P : tm -> Type) (F : aset tmvar),   (P dot) ->   (forall a, P (var a)) ->   (forall s, P s -> forall t, P t -> P (app s t)) ->   (forall a, ~ In a F -> forall T, forall s, P s -> P (lam a T s)) ->   forall x : tm, P x. ```

## Recursion

``` Section Recursion. Variables (R : Set) (RP : PsetT tmvar R). Variable (f_dot : R). Variable (f_var : tmvar -> R). Variable (f_app : tm -> R -> tm -> R -> R). Variable (f_lam : tmvar -> ty -> tm -> R -> R). Variable (F : aset tmvar). Variable (supp_dot : supports RP F f_dot). Variable (supp_var : supports (tmvarP ^-> RP) F f_var). Variable (supp_app : supports (tmP ^-> RP ^-> tmP ^-> RP ^-> RP) F f_app). Variable (supp_lam : supports (tmvarP ^-> tyP ^-> tmP ^-> RP ^-> RP) F f_lam). Variable (fcb :   exists b, ~ In b F /\ forall x y z, freshP RP b (f_lam b x y z)). Derive Dependent Inversion tm_inv with (Phi 0) Sort Set. Lemma Phi_size_lt_papp_fun :   forall n m s t, Phi_size (papp n s t) <= S m -> Phi_size s <= m. Implicit Arguments Phi_size_lt_papp_fun [n m s t]. Lemma Phi_size_lt_papp_arg :   forall n m s t, Phi_size (papp n s t) <= S m -> Phi_size t <= m. Implicit Arguments Phi_size_lt_papp_arg [n m s t]. Lemma Phi_size_lt_plam :   forall n m a T s, Phi_size (plam n T s) <= S m -> Phi_size (inst a s) <= m. Implicit Arguments Phi_size_lt_plam [n m a T s]. ```
 Our goal here is to define recursive functions over terms by induction on their size. This translates to induction on a natural number which bounds the size of the term. All the arguments here are important: `n` is required since the function is defined by induction on the structure of `n`, `x` is the term we actually care about, and the proof ensures that we don't have to deal with non-sensical combinations of `n` and `x`. The proof is of an `le` relation and not an `eq` relation due to how `recF` makes recursive calls. We could, in theory, use an `eq` relation if we were willing to define `recF` by well-founded induction on `n`, but that seems to pose its own problems.
``` Definition recF :   forall (n : nat) (x : Phi 0), Phi_size x <= n -> R. ```
 The particular `n` and proof supplied to `recF` don't matter.
``` Lemma recF_stable :   forall (n m : nat) (x : tm) (pfn : Phi_size x <= n) (pfm : Phi_size x <= m),   recF n x pfn = recF m x pfm. Lemma recF_stable_gen :   forall (n m : nat) (x y : tm), x = y ->   forall (pfn : Phi_size x <= n) (pfm : Phi_size y <= m),   recF n x pfn = recF m y pfm. Hint Resolve recF_stable_gen : core. ```
 Define the recursion combinator, as seen by the user. Most of the cases for how it evaluates are straightforward.
``` Definition tm_rec (x : tm) : R := recF (Phi_size x) x (le_n _). Theorem tm_rec_dot : tm_rec dot = f_dot. Theorem tm_rec_var : forall a, tm_rec (var a) = f_var a. Theorem tm_rec_app :   forall s t, tm_rec (app s t) = f_app s (tm_rec s) t (tm_rec t). ```
 Proving the rewrite rule for the `lam` case requires that we prove the following two properties simultaneously. There may be an easier way, but at least it doesn't seem that this particular method is specific to the object-language at hand. It's only at this point where we need to know the support of `f_dot`, `f_var`, `f_app`, and `f_lam`, and know that `fcb` holds.
``` Let rewrite_prop (n : nat) :=   forall a T s, Phi_size (lam a T s) <= n ->   ~ In a F -> tm_rec (lam a T s) = f_lam a T s (tm_rec s). Let swap_prop (n : nat) :=   forall x c d pf pf', ~ In c F -> ~ In d F ->   perm RP [(c, d)] (recF n x pf) = recF n (perm tmP [(c, d)] x) pf'. Lemma rewrite_to_swap :   forall (n : nat), (forall m, m <= n -> rewrite_prop m) -> swap_prop n. Lemma swap_to_rewrite :   forall (n : nat), (forall m, m < n -> swap_prop m) -> rewrite_prop n. Lemma rewrite_and_swap : forall m, rewrite_prop m /\ swap_prop m. Theorem tm_rec_lam :   forall a T s, ~ In a F -> tm_rec (lam a T s) = f_lam a T s (tm_rec s). Theorem tm_rec_supp :   supports (tmP ^-> RP) F tm_rec. End Recursion. ```

## Constructor distinctness

``` Section Distinctness. Variables a b : tmvar. Variables T : ty. Variables s t q r : tm. Theorem distinctness_dot_var: dot <> var a. Theorem distinctness_dot_app : dot <> app s t. Theorem distinctness_dot_lam : dot <> lam a T s. Theorem distinctness_var_dot : var a <> dot. Theorem distinctness_var_app : var a <> app s t. Theorem distinctness_var_lam : var a <> lam b T s. Theorem distinctness_app_dot : app s t <> dot. Theorem distinctness_app_var : app s t <> var a. Theorem distinctness_app_lam : app s t <> lam a T q. Theorem distinctness_lam_dot : lam a T s <> dot. Theorem distinctness_lam_var : lam a T s <> var b. Theorem distinctness_lam_app : lam a T s <> app q r. End Distinctness. ```

## Injectivity for constructors

``` ```
 Some of the lemmas in this section are needed because the `injection` tactic fails to produce useful hypotheses.
``` Theorem injection_var : forall a b, var a = var b -> a = b. Lemma injection_papp_fun :   forall n s s' t t', papp n s t = papp n s' t' -> s = s'. Theorem injection_app_fun : forall s s' t t', app s t = app s' t' -> s = s'. Lemma injection_papp_arg :   forall n s s' t t', papp n s t = papp n s' t' -> t = t'. Theorem injection_app_arg : forall s s' t t', app s t = app s' t' -> t = t'. Theorem injection_lam_ty :   forall a a' T T' s s',   lam a T s = lam a' T' s' ->   (T = T'). Lemma injection_plam :   forall (n : nat) (T T' : ty) (s s' : Phi (S n)),   plam n T s = plam n T' s' -> s = s'. Lemma abs_eq :   forall (n : nat) (a : tmvar) (s s' : Phi n),   abs a s = abs a s' -> s = s'. Lemma abs_neq :   forall (n : nat) (a a' : tmvar) (s s' : Phi n),   a <> a' ->   abs a s = abs a' s' ->   ~ In a (Phi_fv s') /\ s = Phi_perm [(a, a')] s'. Theorem injection_lam_body :   forall a a' T T' s s',   lam a T s = lam a' T' s' ->   (a = a' /\ s = s') \/   (a <> a' /\ ~ In a (fvar s') /\ s = perm tmP [(a, a')] s'). End MakeSTLC. ```
Index