# Library Stlc.Lec1

# Language specification and variable binding

- First, we would like to work up to
*alpha-equivalence*. In other words, we would like our reasoning about lambda terms to not depend on the names that we use for free variables. - Second, substitution should be
*capture avoiding*. When we substitute terms with free variables, those free variables should never become bound by the terms they are being substituted into. This means that sometimes we need to rename bound variables to avoid capture. For example,

## Approaches to variable binding

*old*problem. The issue isn't that we don't know how to solve this problem, in fact there are

*many*,

*many*different ways to solve this problem and they all have their trade offs. I won't include an entire taxonomy of solutions here, but before we go further, I want to mention a few relevant alternatives.

- Only working with closed terms, never reasoning about equivalence

*open*term, then we never have to worry about variable capture. We can represent binding variables in lambda terms using names in a straightforward manner. This approach is the simplest and side-steps the two problems shown above. For example, it can be used to show type soundness, as is done in Software Foundations.

- Named terms, with swapping

*define*alpha equivalence and substitution appropriately. There are, again, many approaches to these definitions. However, the most elegant approach is inspired by Nominal Logic.

- Locally nameless representation (LN)

*definitionally*equivalent. LN does this while still providing an interface that is mostly similar to paper proofs.

## Overview

- Use a locally nameless representation to
*specify*and reason about the semantics - Use a named representation to
*implement*environment-based interpreters for lambda calculus terms. If binders are mostly unique, then this implementation avoids additional work. - The definitions, lemmas and proofs that are needed to work with lambda-calculus terms are highly automatable.

*preservation*and

*progress*as in Software Foundations.

*nominal representation*but specify the semantics using an abstract machine. This abstract machine is given as a Coq function from machine configurations to machine configurations, and can be used as an efficient interpreter. This abstract machine features a heap (i.e. runtime environment for variables) so we will not need to define capture-avoiding substitution as part of our semantics.

## Tool support

# The simply-typed lambda calculus in Coq.

Require Import Metalib.Metatheory.

Next, we import the definitions of the simply-typed lambda calculus.
If you haven't skimmed this file yet, you should do so now. You don't
need to understand everything in the file at first, but you will need to
refer back to it in the material below.

And some notations (defined in `Stlc.Definitions`), but not automatically
brought into scope.

Import StlcNotations.

For the examples below, we introduce some sample variable names to
play with.

Definition X : atom := fresh nil.

Definition Y : atom := fresh (X :: nil).

Definition Z : atom := fresh (X :: Y :: nil).

## Encoding STLC terms

Finally, here is an example where the same bound variable has two
different indices, and the same index refers to two different
bound variables.
\y. ((\x. (x y)) y)

### Exercise: term representation

There are two important advantages of the locally nameless
representation:
Weighed against these advantages are two drawbacks:
The substitution function replaces a free variable with a term. For
simplicity, we define a notation for free variable substitution that
mimics standard mathematical notation.

- Alpha-equivalent terms have a unique representation. We're always working up to alpha-equivalence.
- Operations such as free variable substitution and free variable calculation have simple recursive definitions (and therefore are simple to reason about).

- The exp datatype admits terms, such as abs 3, where indices are unbound. A term is called "locally closed" when it contains no unbound indices.
- We must define *both* bound variable & free variable substitution and reason about how these operations interact with each other.

## Substitution

To demonstrate how free variable substitution works, we need to
reason about var equality.

The decidable var equality function returns a sum. If the two
vars are equal, the left branch of the sum is returned, carrying
a proof of the proposition that the vars are equal. If they are
not equal, the right branch includes a proof of the disequality.
The demo below uses three new tactics:

Example demo_subst1:

[Y ~> var_f Z] (abs (app (var_b 0) (var_f Y))) = (abs (app (var_b 0) (var_f Z))).

Proof.

simpl.

destruct (Y==Y).

- auto.

- destruct n. auto.

Qed.

### Exercise subst_eq_var

### Exercise subst_neq_var

### Exercise subst_same

## Free variables

### Recommended Exercise subst_exp_fresh_eq

- You will need to use simpl in many cases. You can simpl everything
everywhere (including hypotheses) with the pattern simpl in ×.
- Part of this proof includes a false assumption about free variables.
Destructing this hypothesis produces a goal about finite set membership
that is solvable by fsetdec.
- The f_equal tactic converts a goal of the form f e1 = f e1' in to one of the form e1 = e1', and similarly for f e1 e2 = f e1' e2', etc.

## Additional Exercises

Lemma fv_exp_subst_exp_notin : ∀ x y u e,

x `notin` fv_exp e →

x `notin` fv_exp u →

x `notin` fv_exp ([y ~> u]e).

Proof.

intros x y u e Fr1 Fr2.

induction e; simpl in ×.

- Case "var_b".

assumption.

- Case "var_f".

destruct (x0 == y).

assumption.

simpl. assumption.

- Case "abs".

apply IHe. assumption.

- Case "app".

destruct_notin.

apply notin_union.

apply IHe1.

assumption.

apply IHe2.

assumption.

Qed.

x `notin` fv_exp e →

x `notin` fv_exp u →

x `notin` fv_exp ([y ~> u]e).

Proof.

intros x y u e Fr1 Fr2.

induction e; simpl in ×.

- Case "var_b".

assumption.

- Case "var_f".

destruct (x0 == y).

assumption.

simpl. assumption.

- Case "abs".

apply IHe. assumption.

- Case "app".

destruct_notin.

apply notin_union.

apply IHe1.

assumption.

apply IHe2.

assumption.

Qed.

Lemma subst_exp_fresh_same :

∀ u e x,

x `notin` fv_exp e →

x `notin` fv_exp ([x ~> u] e).

Proof.

Admitted.

### Exercise fv_exp_subst_exp_fresh

Lemma fv_exp_subst_exp_fresh :

∀ e u x,

x `notin` fv_exp e →

fv_exp ([x ~> u] e) [=] fv_exp e.

Proof.

Admitted.

### Exercise fv_exp_subst_exp_upper

Lemma fv_exp_subst_exp_upper :

∀ e1 e2 x1,

fv_exp (subst_exp e2 x1 e1) [<=] fv_exp e2 `union` remove x1 (fv_exp e1).

Proof.

Admitted.

# LN specific operations and relations

## Opening

*without*the outer abstraction, we need to replace the indices that refer to that abstraction with a name. Therefore, we show that we can open the body of the abs above with Y to produce app (abs (app Y 0)) Y).

Lemma demo_open :

(app (abs (app (var_b 1) (var_b 0))) (var_b 0)) ^ Y =

(app (abs (app (var_f Y) (var_b 0))) (var_f Y)).

Proof.

cbn. auto.

Qed.

## Local closure

*no*dangling indices.

Lemma demo_lc :

lc_exp (app (abs (app (var_f Y) (var_b 0))) (var_f Y)).

Proof.

eapply lc_app.

eapply lc_abs.

intro x. cbn.

auto.

auto.

Qed.

## Properties about basic operations

Lemma subst_exp_open_exp_wrt_exp :

∀ e3 e1 e2 x1,

lc_exp e1 →

[x1 ~> e1] (open e3 e2) = open ([x1 ~> e1] e3) ([x1 ~> e1] e2).

Proof.

Admitted.

### Exercise subst_var

Lemma subst_var : ∀ (x y : var) u e,

y ≠ x →

lc_exp u →

([x ~> u] e) ^ y = [x ~> u] (e ^ y).

Proof.

Admitted.

### Exercise subst_exp_intro

Lemma subst_exp_intro : ∀ (x : var) u e,

x `notin` (fv_exp e) →

open e u = [x ~> u](e ^ x).

Proof.

intros x u e FV_EXP.

unfold open.

generalize 0.

induction e; intro n0; simpl.

Admitted.

### Exercise fv_exp_open_exp_wrt_exp_upper

Lemma fv_exp_open_exp_wrt_exp_upper :

∀ e1 e2,

fv_exp (open_exp_wrt_exp e1 e2) [<=] fv_exp e2 `union` fv_exp e1.

Proof.

Admitted.

The induction principle for the lc_exp relation is particularly strong
in the abs case.
This principle says that to prove that a property holds for an abstraction,
we can assume that the property holds for the body of the abstraction,
opened with *any* variable that we like.

forall P : exp -> Prop, ... (forall e : exp, (forall x : atom, lc_exp (e ^ x)) -> (forall x : atom, P (e ^ x)) -> P (abs e)) -> ... forall e : exp, lc_exp e -> P e

However, on the other hand, when we show that an abstraction is locally
closed, we need to show that its body is locally closed, when
opened by any variable.
That can sometimes be a problem.

Lemma subst_lc0 : ∀ (x : var) u e,

lc_exp e →

lc_exp u →

lc_exp ([x ~> u] e).

Proof.

intros x u e He Hu.

induction He.

- Case "lc_var_f".

simpl.

destruct (x0 == x).

auto.

auto.

- Case "lc_abs".

simpl.

eapply lc_abs.

intros x0.

rewrite subst_var.

apply H0.

Abort.

Here we are stuck. We don't know that x0 is not equal to x,
which is a preconduction for subst_var.
The solution is to prove an alternative introduction rule for
local closure for abstractions. In the current rule, we need
to show that the body of the abstraction is locally closed,
no matter what variable we choose for the binder.
An easier to use lemma requires us to only show that the body
of the abstraction is locally closed for a
As before, we won't prove this lemma as part of the tutorial,
(it too is proved in Lemmas.v) but we will use it as part of
our reasoning.

| lc_abs : forall e, (forall x:var, lc_exp (open e x)) -> lc_exp (abs e)

*single*variable.
For example, with this addition, we can complete the proof above.

Lemma subst_exp_lc_exp : ∀ (x : var) u e,

lc_exp e →

lc_exp u →

lc_exp ([x ~> u] e).

Proof.

intros x u e He Hu.

induction He.

- Case "lc_var_f".

simpl.

destruct (x0 == x); auto.

- Case "lc_abs".

simpl.

pick fresh x0 for {{x}}. apply (lc_abs_exists x0).

rewrite subst_var; auto.

- Case "lc_app".

simpl. eauto.

Qed.

## Local closure and relations

Lemma step_lc_exp1 : ∀ e1 e2, step e1 e2 → lc_exp e1.

Proof. intros e1 e2 H. induction H; auto. Qed.

### Exercise step_lc_exp2

*also*locally closed.