Library Reduction
Reduction
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).
| 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.
(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.
| one : step s t -> steps s t
| more s' : step s s' -> steps s' t -> steps s t.
General termination
Termination of One Step Beta Reduction
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.
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