# Untyped lambda-calculus, terms and substitutions

Require Export Base.

Notation "f '=1' g" := (forall x, f x = g x) (at level 70).

Definitions

Inductive term := Var (n : nat) | App (s t : term) | Lam (s : term).

Coercion App : term >-> Funclass.

Implicit Types s t : term.

Definition renaming := nat -> nat.

Definition substitution := nat -> term.

Implicit Types xi zeta : renaming.

Implicit Types sigma tau : substitution.

Definition sub xi := Var o xi.

Definition upr : renaming -> renaming :=
fun xi n => match n with
| 0 => 0
| S n => S (xi n)
end.

Fixpoint apply_ren (xi : renaming) (s : term) : term :=
match s with
| Var n => Var (xi n)
| App s t => App (apply_ren xi s) (apply_ren xi t)
| Lam s => Lam (apply_ren (upr xi) s)
end.

Notation "xi '!!' s" := (apply_ren xi s) (at level 52, right associativity).

Definition up : substitution -> substitution :=
fun sigma n => match n with
| 0 => Var 0
| S n => S !! sigma n
end.

Fixpoint apply_subst (sigma : substitution) (s : term) : term :=
match s with
| Var n => sigma n
| App s t => App (apply_subst sigma s) (apply_subst sigma t)
| Lam s => Lam (apply_subst (up sigma) s)
end.

Notation "sigma '!' s" := (apply_subst sigma s) (at level 52, right associativity).

Equivalence of substitutions

Let ren_eq xi zeta s :
xi =1 zeta -> xi !! s = zeta !! s.

Proof.

intros A.
revert xi zeta A.
induction s as [n |s IHs t IHt|s IHs];
intros xi zeta A; simpl; f_equal; auto.

- apply IHs.
intros [|n]; simpl; f_equal; auto.
Qed.

Lemma subst_eq sigma tau s :
sigma =1 tau -> sigma ! s = tau ! s.

Proof.

intros A.
revert sigma tau A.
induction s as [n |s IHs t IHt|s IHs];
intros sigma tau A; simpl; f_equal; auto.

- apply IHs.
intros [|n]; simpl; f_equal; auto.
Qed.

Agreement

Lemma subst_ren xi s :
xi !! s = sub xi ! s.

Proof.

revert xi.

induction s as [n |s IHs t IHt|s IHs];
intros xi; simpl; f_equal; auto.

- rewrite IHs.
apply subst_eq.
intros [|n]; reflexivity.

Qed.

Identity laws

Lemma subst_var s :
Var ! s = s.

Proof.

induction s as [n |s IHs t IHt|s IHs] ;
simpl; f_equal; auto.

- rewrite <- IHs at 2.

apply subst_eq.
intros [|n]; reflexivity.
Qed.

Lemma subst_id sigma s :
sigma =1 Var -> sigma ! s = s.

Proof.

intros A.
rewrite <- subst_var. apply subst_eq, A.
Qed.

Composition laws

Definition comp_subst sigma tau n := sigma ! tau n.

Arguments comp_subst sigma tau n /.

Notation "sigma '#' tau" := (comp_subst sigma tau) (at level 51).

Lemma subst_S sigma s :
sub S # sigma =1 up sigma # sub S.

Proof.

intros n.
simpl. rewrite subst_ren. reflexivity.
Qed.

Let subst_comp_ren sigma xi s :
sigma ! xi !! s = sigma # sub xi ! s.

Proof.

revert sigma xi.

induction s as [n|s IHs t IHt|s IHs];
intros sigma xi ; simpl; f_equal; auto.

- rewrite IHs.
apply subst_eq.
intros [|n]; reflexivity.

Qed.

Let ren_comp_subst xi sigma s :
xi !! sigma ! s = sub xi # sigma ! s.

Proof.

revert xi sigma.

induction s as [n|s IHs t IHt|s IHs]; intros xi sigma; simpl.

- apply subst_ren.

- congruence.

- f_equal.
rewrite IHs. apply subst_eq.
intros [|n]; simpl.
reflexivity.
rewrite subst_comp_ren.

rewrite <- subst_ren.
rewrite subst_ren.
rewrite subst_comp_ren.
reflexivity.
Qed.

Let up_distri sigma tau :
up (sigma # tau) =1 up sigma # up tau.

Proof.

intros [|n]; simpl.
reflexivity.
rewrite subst_comp_ren, ren_comp_subst.

apply subst_eq.
simpl.
symmetry; apply subst_ren.

Qed.

Lemma subst_comp sigma tau s :
sigma ! tau ! s = sigma # tau ! s.

Proof.

revert sigma tau.

induction s as [n |s IHs t IHt|s IHs];
intros sigma tau; simpl; f_equal; auto.

- rewrite IHs.
apply subst_eq.
symmetry; apply up_distri.

Qed.

Beta reduction

Definition beta (t : term) : substitution :=
fun n => match n with
| 0 => t
| S n' => Var n'
end.

Inductive step : term -> term -> Prop :=
| stepB s t :
step ((Lam s) t) (beta t ! s)
| stepAL s s' t :
step s s' -> step (s t) (s' t)
| stepAR (s t t' : term) :
step t t' -> step (s t) (s t')
| stepL s s' :
step s s' -> step (Lam s) (Lam s').

Lemma subst_beta_S t s :
beta t ! S !! s = s.

Proof.

rewrite subst_ren, subst_comp.
apply subst_var.
Qed.

Lemma subst_beta_com sigma t s :
sigma ! beta t ! s = beta (sigma ! t) ! up sigma ! s.

Proof.

repeat rewrite subst_comp.
apply subst_eq. intros [|n]; simpl.
- reflexivity.

- now rewrite subst_beta_S.

Qed.

Lemma step_substitutive sigma s t :
step s t -> step (sigma ! s) (sigma ! t).

Proof.

intros A.
revert sigma.
induction A as [s t|s s' t _ IHs | s t t' _ IHt | s s' _ IHs];
simpl; intros sigma; auto using step.

- rewrite subst_beta_com.
constructor.
Qed.

Closed Terms

Inductive dclosed (d : nat) : term -> Prop :=
| dclosedV n : n < d -> dclosed d (Var n)
| dclosedA s t : dclosed d s -> dclosed d t -> dclosed d (App s t)
| dclosedL s : dclosed (S d) s -> dclosed d (Lam s).

Definition closed s := dclosed 0 s.

Arguments closed / s.

Lemma dclosed_mono d d' s :
d <= d' -> dclosed d s -> dclosed d' s.

Proof.

intros A B.
revert d' A.
induction B; intros d' A; constructor; intuition; omega.

Qed.

Let subst_dclosed d sigma s :
dclosed d s -> (forall n, n < d -> sigma n = Var n) -> sigma ! s = s.

Proof.

intros A.
revert sigma.
induction A; intros sigma B; simpl; f_equal; auto.

- apply IHA.
intros [|n] C; simpl. reflexivity.
rewrite B; simpl.
reflexivity. omega.
Qed.

Lemma subst_closed s sigma :
closed s -> sigma!s = s.

Proof.

intros A.
apply (subst_dclosed A). intros n B. inv B.
Qed.

Arguments subst_closed {s sigma} _.