Как я могу закрыть эту демонстрацию о opt_ c в coq? - PullRequest
Новая
       9

Как я могу закрыть эту демонстрацию о opt_ c в coq?

0 голосов
/ 05 января 2020

Я читаю книгу «Логическое основание». Он вводит эту точку фиксации и эту теорему: 

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

Как мне закрыть эту теорему

1 Ответ

1 голос
/ 05 января 2020

Проблема в том, что вы выполняете индукцию для c, что не дает полезной гипотезы индукции для случая WhileTrue. Чтобы решить эту проблему, вам нужно выполнить индукцию на ceval (opt_c c) st st' с remember tacti c: 

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