如何在 coq 中关闭这个关于 opt_c 的演示？

Question

我正在阅读《逻辑基础》一书。它介绍了这个固定点和这个定理：

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
    | APlus (ANum 0) e2 => optimize_0plus e2
    | APlus  e1 e2 => APlus  (optimize_0plus e1) (optimize_0plus e2)
    | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
    | AMult  e1 e2 => AMult  (optimize_0plus e1) (optimize_0plus e2)
    | _ => a
  end.

Theorem optimize_0plus_sound: 
  forall a st,
  aeval st (optimize_0plus a) = aeval st a.

我决定用合理的定理对 bexp 定义另一个优化：

Fixpoint opt_b (b : bexp) : bexp :=
  match b with
    | BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2)
    | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2)
    | BNot b => BNot (opt_b b)
    | BAnd BTrue b2 => (opt_b b2)
    | BAnd BFalse _ => BFalse
    | BAnd b1 b2 => BAnd (opt_b b1) (opt_b b2)
    | _ => b
  end.
Theorem opt_b_sound: 
  forall b st,
  beval st (opt_b b) = beval st b.

然后我在 Imp 命令上引入了另一个优化（使用之前的优化）：

Fixpoint opt_c (c : com) : com := 
  match c with
    | CAss x a => CAss x (optimize_0plus a)
    | CSeq c1 c2 => CSeq (opt_c c1) (opt_c c2)
    | CIf b c1 c2 => CIf (opt_b b) (opt_c c1) (opt_c c2)
    | CWhile b c => CWhile (opt_b b) (opt_c c)
    | _ => c
  end.

现在我必须证明这个 opt_c 合理的定理，但我无法关闭它：

Theorem opt_c_sound: 
  forall c st st',
  ceval c st st' <-> ceval (opt_c c) st st'.  
Proof.
  intros.
  split. 
  {
    intros. induction H; simpl.
    - constructor.
    - constructor. rewrite optimize_0plus_sound. assumption.
    - apply E_Seq with st'; assumption.
    - apply E_IfTrue.
      + rewrite opt_b_sound. assumption.
      + assumption.
    - apply E_IfFalse.
      + rewrite opt_b_sound. assumption. 
      + assumption.
    - apply E_WhileFalse. rewrite opt_b_sound. assumption.
    - apply E_WhileTrue with st'.
      + rewrite opt_b_sound. assumption.
      + assumption.
      + simpl in IHceval2. assumption. 
  }
  {
    generalize dependent st'.
    generalize dependent st.
    induction c; intros; inversion H; subst.
    - constructor.
    - rewrite optimize_0plus_sound. constructor. trivial.
    - apply E_Seq with st'0. 
      + apply IHc1 in H2. assumption.
      + apply IHc2 in H5. assumption.
    - apply E_IfTrue.
      + rewrite opt_b_sound in H5. assumption.
      + apply IHc1 in H6. assumption.
    - apply E_IfFalse.
      + rewrite opt_b_sound in H5. assumption.
      + apply IHc2 in H6. assumption.
    - apply E_WhileFalse. rewrite opt_b_sound in H4. assumption.
    - apply E_WhileTrue with st'0.
      + rewrite opt_b_sound in H2. assumption.
      + apply IHc in H3. assumption.
      + (* I'm blocked here *)

如何关闭这个定理？

Answer 1

问题是您正在对 c 进行归纳，这不会为 WhileTrue 情况产生有用的归纳假设。为了解决这个问题，你需要使用 remember 策略对 ceval (opt_c c) st st' 进行归纳：

remember (opt_c c) as c'.
generalize dependent c.
induction H.

如何在 coq 中关闭这个关于 opt_c 的演示？

How can I close this demonstration about opt_c in coq?

coq

coq-tactic