1.4. Beta Reduction🔗

A beta step contracts one redex or performs one such contraction inside an application or a lambda. The reflexive-transitive closure BetaStar is the many-step reduction relation.

\frac{}{(\lambda.\ e)\ e' \to_\beta [e'/0]e} \qquad \frac{e_1 \to_\beta e_1'}{e_1\ e_2 \to_\beta e_1'\ e_2} \qquad \frac{e_2 \to_\beta e_2'}{e_1\ e_2 \to_\beta e_1\ e_2'} \qquad \frac{e \to_\beta e'}{\lambda.\ e \to_\beta \lambda.\ e'}

The first rule is the actual contraction rule. The other three rules say that one contraction may happen in any immediate subterm.

\frac{}{e \to_\beta^* e} \qquad \frac{e \to_\beta e' \qquad e' \to_\beta^* e''}{e \to_\beta^* e''}

The many-step relation is Lean's reflexive-transitive closure of one beta step.

inductive BetaStep : L0 -> L0 -> Prop where
  | beta :
      BetaStep (.app (.lam body) arg) (subst 0 arg body)
  | app_left :
      BetaStep f f' ->
      BetaStep (.app f a) (.app f' a)
  | app_right :
      BetaStep a a' ->
      BetaStep (.app f a) (.app f a')
  | lam :
      BetaStep body body' ->
      BetaStep (.lam body) (.lam body')

infix:50 " →β₀ " => BetaStepabbrev BetaStar : L0 -> L0 -> Prop := Relation.ReflTransGen BetaStepinfix:50 " →β₀* " => BetaStardef NormalForm (t : L0) : Prop := ∀u, ¬(t →β₀ u)syntax "beta_step" : tacticmacro_rules | `(tactic| beta_step) => `(tactic| repeat' constructor)syntax "beta_steps" : tacticmacro_rules | `(tactic| beta_steps) => `(tactic| rt_repeat { beta_step })syntax "normal" : tacticmacro_rules | `(tactic| normal) => `(tactic| intro _ _; repeat' cases ‹BetaStep _ _›)