# Plain.Demo

# Autosubst Tutorial

## Syntax and the substitution operation

Now we can automatically derive the substitution operations and lemmas.
This is done by generating instances for the following typeclasses:

- Ids term provides the generic identity substitution ids for term. It is always equivalent to the variable constructor of term, i.e. to the unique constructor having a single argument of type var. In this example, ids is convertible to Var.
- Rename term provides the renaming operation on term.
- Subst term provides the substitution operation on term and needs a Rename instance in the presence of binders.
- SubstLemmas term contains proofs for the basic lemmas.

Instance Ids_term : Ids term. derive. Defined.

Instance Rename_term : Rename term. derive. Defined.

Instance Subst_term : Subst term. derive. Defined.

Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

At this point we can use the notations:
Let us test the simplification behavior of s.[sigma].

- s.[sigma] for the application of the substitution sigma to a term s.
- sigma >> tau for the composition of sigma and tau, i.e., the substitution fun x => (sigma x).[tau].

Eval simpl in fun sigma x => (Var x).[sigma].

(* simplifies to sigma x*)

Eval simpl in fun sigma s t => (App s t).[sigma].

(* simplifies to App s.[sigma] t.[sigma]*)

Eval simpl in fun sigma s => (Lam s).[sigma].

(* simplifies to Lam s.[up sigma]*)

The operator up adapts a substitution when going below a binder.
It does not simplify with simpl, but we can use our tactic asimpl
to perform the simplification.

Goal forall sigma,

(Lam (App (Var 0) (Var 3))).[sigma] = Lam (App (Var 0) (sigma 2).[ren(+1)]).

intros. asimpl. reflexivity. Qed.

(Lam (App (Var 0) (Var 3))).[sigma] = Lam (App (Var 0) (sigma 2).[ren(+1)]).

intros. asimpl. reflexivity. Qed.

## Reduction and substitutivity

Inductive step : term -> term -> Prop :=

| Step_beta (s1 s2 t : term) :

s1.[t/] = s2 -> step (App (Lam s1) t) s2

| Step_appL (s1 s2 t : term) :

step s1 s2 -> step (App s1 t) (App s2 t)

| Step_appR (s t1 t2 : term) :

step t1 t2 -> step (App s t1) (App s t2)

| Step_lam (s1 s2 : term) :

step s1 s2 -> step (Lam s1) (Lam s2).

The proof of substitutivity proceeds by induction on the reduction relation.
In every case we apply the respective constructor of step.
Apart from Step_beta, every case is trivial.
For Step_beta, we have to show the equation
Since both sides of the equation are simplified to s1.[t.[sigma] .: sigma] using
asimpl, this goal can be solved using autosubst.

Lemma substitutivity s1 s2 :

step s1 s2 -> forall sigma, step s1.[sigma] s2.[sigma].

Proof.

induction 1; constructor; subst; autosubst.

Restart.

induction 1; intros; simpl; eauto using step; subst.

constructor. asimpl. reflexivity.

Qed.

For simplicity, the typing relation uses infinite contexts, that is, substitutions
Thus we can reuse the primitives and tactics for substitutions.

Inductive ty (Gamma : var -> type) : term -> type -> Prop :=

| Ty_Var x A : Gamma x = A ->

ty Gamma (Var x) A

| Ty_Lam s A B : ty (A .: Gamma) s B ->

ty Gamma (Lam s) (Arr A B)

| Ty_App s t A B : ty Gamma s (Arr A B) -> ty Gamma t A ->

ty Gamma (App s t) B.

| Ty_Var x A : Gamma x = A ->

ty Gamma (Var x) A

| Ty_Lam s A B : ty (A .: Gamma) s B ->

ty Gamma (Lam s) (Arr A B)

| Ty_App s t A B : ty Gamma s (Arr A B) -> ty Gamma t A ->

ty Gamma (App s t) B.

This lemma is a generalization of the usual weakening lemma and a specialization
of ty_subst, which we will prove next.

Lemma ty_ren Gamma s A:

ty Gamma s A -> forall Delta xi,

Gamma = xi >>> Delta ->

ty Delta s.[ren xi] A.

Proof.

induction 1; intros; subst; asimpl; econstructor; eauto.

- eapply IHty. autosubst.

Qed.

ty Gamma s A -> forall Delta xi,

Gamma = xi >>> Delta ->

ty Delta s.[ren xi] A.

Proof.

induction 1; intros; subst; asimpl; econstructor; eauto.

- eapply IHty. autosubst.

Qed.

By generalizing ty_ren to substitutions, we obtain that we preserve typing
if we replace variables by terms of the same type.

Lemma ty_subst Gamma s A:

ty Gamma s A -> forall sigma Delta,

(forall x, ty Delta (sigma x) (Gamma x)) ->

ty Delta s.[sigma] A.

Proof.

induction 1; intros; subst; asimpl; eauto using ty.

- econstructor. eapply IHty.

intros [|]; asimpl; eauto using ty, ty_ren.

Qed.

ty Gamma s A -> forall sigma Delta,

(forall x, ty Delta (sigma x) (Gamma x)) ->

ty Delta s.[sigma] A.

Proof.

induction 1; intros; subst; asimpl; eauto using ty.

- econstructor. eapply IHty.

intros [|]; asimpl; eauto using ty, ty_ren.

Qed.

To show type preservation of the simply typed lambda calculus, we use ty_subst to
justify the typing of the result of the beta reduction.

Lemma ty_pres Gamma s A :

ty Gamma s A -> forall s',

step s s' ->

ty Gamma s' A.

Proof.

induction 1; intros s' H_step; asimpl;

inversion H_step; ainv; eauto using ty.

- eapply ty_subst; try eassumption.

intros [|]; simpl; eauto using ty.

Qed.

(* Local Variables: *)

(* coq-load-path: (("." "Plain") ("../../theories" "Autosubst")) *)

(* End: *)

ty Gamma s A -> forall s',

step s s' ->

ty Gamma s' A.

Proof.

induction 1; intros s' H_step; asimpl;

inversion H_step; ainv; eauto using ty.

- eapply ty_subst; try eassumption.

intros [|]; simpl; eauto using ty.

Qed.

(* Local Variables: *)

(* coq-load-path: (("." "Plain") ("../../theories" "Autosubst")) *)

(* End: *)