Search code examples
coqcoq-tactic

How can I close this demonstration about opt_c in coq?


I'm reading Logical Foundation book. It introduces this Fixpoint and this 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.

I decided to define another optimization on bexp with sound theorem:

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.

Then I introduced another optimization on Imp comand (using the previously optimizations):

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.

Now I have to demonstrate this opt_c sound theorem, but I'm not able to close it:

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

How can I close this Theorem?


Solution

  • The problem is that you are performing induction on c, which doesn't yield a useful induction hypothesis for the WhileTrue case. To solve this issue, you need to perform induction on ceval (opt_c c) st st' with the remember tactic:

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