Coq中算术表达式的小步与大步语义等价性证明求助

1. 基础定义对齐 #

先给出标准的算术表达式、小步/大步语义定义，确保语境一致：

(* 算术表达式归纳类型 *)
Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (e1 e2 : aexp)
  | AMinus (e1 e2 : aexp)
  | AMult (e1 e2 : aexp).

(* 单步小步归约关系 *)
Inductive step : aexp -> aexp -> Prop :=
  | step_plus_l : forall e1 e1' e2, step e1 e1' -> step (APlus e1 e2) (APlus e1' e2)
  | step_plus_r : forall n1 e2 e2', step e2 e2' -> step (APlus (ANum n1) e2) (APlus (ANum n1) e2')
  | step_plus_num : forall n1 n2, step (APlus (ANum n1) (ANum n2)) (ANum (n1 + n2))
  | step_minus_l : forall e1 e1' e2, step e1 e1' -> step (AMinus e1 e2) (AMinus e1' e2)
  | step_minus_r : forall n1 e2 e2', step e2 e2' -> step (AMinus (ANum n1) e2) (AMinus (ANum n1) e2')
  | step_minus_num : forall n1 n2, step (AMinus (ANum n1) (ANum n2)) (ANum (n1 - n2))
  | step_mult_l : forall e1 e1' e2, step e1 e1' -> step (AMult e1 e2) (AMult e1' e2)
  | step_mult_r : forall n1 e2 e2', step e2 e2' -> step (AMult (ANum n1) e2) (AMult (ANum n1) e2')
  | step_mult_num : forall n1 n2, step (AMult (ANum n1) (ANum n2)) (ANum (n1 * n2)).

(* 多步小步归约（自反传递闭包） *)
Inductive star {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
  | star_refl : forall x, star R x x
  | star_step : forall x y z, R x y -> star R y z -> star R x z.

Notation "e1 ->* e2" := (star step e1 e2) (at level 40).

(* 大步求值关系 *)
Inductive eval : aexp -> nat -> Prop :=
  | eval_num : forall n, eval (ANum n) n
  | eval_plus : forall e1 e2 n1 n2, eval e1 n1 -> eval e2 n2 -> eval (APlus e1 e2) (n1 + n2)
  | eval_minus : forall e1 e2 n1 n2, eval e1 n1 -> eval e2 n2 -> eval (AMinus e1 e2) (n1 - n2)
  | eval_mult : forall e1 e2 n1 n2, eval e1 n1 -> eval e2 n2 -> eval (AMult e1 e2) (n1 * n2).

2. 等价性证明的两个核心方向 #

等价性需证明双向蕴含：

• 方向1：eval e n → e ->* ANum n（大步可求值的表达式，必能多步归约到对应数值）
• 方向2：e ->* ANum n → eval e n（多步归约到数值的表达式，必能被大步语义求值到该数值）

方向1证明：大步推多步小步 #

对eval的推导做归纳：

• 基例eval_num：直接用star_refl，因为ANum n ->* ANum n
• 归纳例eval_plus：假设eval e1 n1推出e1 ->* ANum n1，eval e2 n2推出e2 ->* ANum n2，构造路径：
  1. 先归约左子表达式：APlus e1 e2 ->* APlus (ANum n1) e2（依赖辅助引理step_plus_l_star）
  2. 再归约右子表达式：APlus (ANum n1) e2 ->* APlus (ANum n1) (ANum n2)（依赖辅助引理step_plus_r_star）
  3. 最后一步归约到结果：step_plus_num结合star_step完成链

辅助引理示例：

Lemma step_plus_l_star : forall e1 e1' e2,
  star step e1 e1' -> star step (APlus e1 e2) (APlus e1' e2).
Proof. induction 1; constructor; eauto. Qed.

Lemma step_plus_r_star : forall n1 e2 e2',
  star step e2 e2' -> star step (APlus (ANum n1) e2) (APlus (ANum n1) e2').
Proof. induction 1; constructor; eauto. Qed.

eval_minus、eval_mult的归纳逻辑与eval_plus完全一致。

方向2证明：多步小步推大步 #

先证两个关键辅助引理，再对star的推导做归纳：

1. 数值规范性：数值无法再归约

Lemma normal_form_num : forall n e', ~ step (ANum n) e'.
Proof. intros n e' H; inversion H. Qed.

2. 单步归约保持可求值性：若e单步归约到e'且e'可求值到n，则e也可求值到n

Lemma step_preserves_eval : forall e e' n,
  step e e' -> eval e' n -> eval e n.
Proof.
  intros e e' n Hstep Heval; inversion Hstep; inversion Heval; eauto.
  (* 按step构造子逐一处理，比如step_plus_l的情况：
     由eval (APlus e1' e2) n反推出eval e1' n1、eval e2 n2，再用归纳假设得eval e1 n1，最终构造eval (APlus e1 e2) n *)
Qed.

对star的推导归纳：

• 基例star_refl：e = ANum n，直接用eval_num
• 归纳例star_step：已知step e e'且e' ->* ANum n，由归纳假设得eval e' n，再用step_preserves_eval直接推出eval e n

3. 常见坑点及解决 #

• 忽略star的归纳结构：必须同时处理自反和单步扩展两种情况，不能只覆盖单步归约
• 缺失上下文辅助引理：比如step_plus_l_star这类上下文保持引理，会导致主证明中归约链无法拼接
• 未证数值规范性：在方向2的归纳中，若不排除数值继续归约的可能，会出现矛盾分支无法闭合

内容的提问来源于stack exchange，提问作者Samuel Novotný