我如何在coq中关闭关于opt_c的这个余量？

Question

我正在阅读Logical Foundation的书。它介绍了此Fixpoint和该定理：

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 comand进行了另一项优化（使用先前的优化）：

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情况，这不会产生有用的归纳假设。要解决此问题，您需要使用ceval (opt_c c) st st'策略在remember上进行归纳：

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