时间戳

首页 > 解决方案 > 如何在 coq 中关闭有关 opt_c 的演示？

coq - 如何在 coq 中关闭有关 opt_c 的演示？

问题描述

我正在读逻辑基础的书。它介绍了这个 Fixpoint 和这个 Theorem：

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 *)

我怎样才能关闭这个定理？

标签： coqcoq-tactic

解决方案

问题是您正在对 执行归纳c，这不会为WhileTrue案例产生有用的归纳假设。要解决此问题，您需要ceval (opt_c c) st st'使用以下remember策略进行归纳：

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

推荐阅读