# Library Reduction

Reduction

Require Export Definitions.
Implicit Types x y z : var.
Implicit Types s t u : term.

One Step Beta Reduction
Inductive step : term -> term -> Prop :=
| step_beta (s t : term) :
step ((Lam s) t) (s.[t/])
| step_appL (s1 s2 t : term) :
step s1 s2 -> step (s1 t) (s2 t)
| step_appR (s t1 t2 : term) :
step t1 t2 -> step (s t1) (s t2)
| step_lam (s1 s2 : term) :
step s1 s2 -> step (Lam s1) (Lam s2).

Replacing definitional equality with propositional equality eases automatic theorem proving (e.g., auto)
Lemma step_beta_eq (s t u : term) :
(s.[t/]) = u -> step ((Lam s) t) u.
intros [] ; auto using step_beta. Qed.

Many Step Beta Reduction is the transitive closure of One Step Beta Reduction
Inductive steps s t : Prop :=
| one : step s t -> steps s t
| more s' : step s s' -> steps s' t -> steps s t.

General termination
Inductive GSN {X : Type} R (x : X) : Prop := gsn : (forall y : X, R x y -> GSN R y) -> GSN R x.

Termination of One Step Beta Reduction
Definition SN := GSN step.

Many Step Beta Reduction is compatible with term application
Lemma steps_appL s s' : steps s s' -> forall t, steps (s t) (s' t).
induction 1 ; eauto using one, more, step_appL. Qed.

Lemma steps_appR s s' : steps s s' -> forall t, steps (t s) (t s').
induction 1 ; intros ; eauto using one, more, step_appR. Qed.

Termination of One Step Beta Reduction implies termination of Many Step Beta Reduction
Lemma sn_gsn t : SN t -> GSN steps t.
induction 1 as [? SN' IH].
constructor.
intros t'.
inversion 1 as [ | ? st1 ? ] ; subst ; auto.
specialize (IH _ st1).
inversion IH ; auto.
Qed.