proposition: Lemma Triple_while_lexico: forall P variant1 variant2 b c, (forall v1 v2, [[ P //\\ atrue b //\\ aequal variant1 v1 //\\ aequal variant2 v2 ]] c [[ P //\\ (alessthan variant1 v1 \\// (aequal variant1 v1 //\\ alessthan variant2 v2)) ]]) -> [[P]] WHILE b c [[P //\\ afalse b]].
proof: Proof. intros P variant1 variant2 b c T. assert (REC: forall v1 v2 s, P s -> aeval variant1 s = v1 -> aeval variant2 s = v2 -> exists s', cexec s (WHILE b c) s' /\ (P s' /\ beval b s' = false)). Admitted. Module VCGEN. Inductive com: Type := | SKIP | ASSIGN (x: ident) (a: aexp) | SEQ (c1: com) (c2: com) | IFTHENELSE (b: bexp) (c1: com) (c2: com) | WHILE (Inv: assertion) (b: bexp) (c1: com). Fixpoint pre (c: com) (Q: assertion) : assertion := match c with | SKIP => Q | ASSIGN x a => aupdate x a Q | SEQ c1 c2 => pre c1 (pre c2 Q) | IFTHENELSE b c1 c2 => atrue b //\\ pre c1 Q \\// afalse b //\\ pre c2 Q | WHILE Inv b c => Inv end. Fixpoint vcg (c: com) (Q: assertion) : Prop := match c with | SKIP => True | ASSIGN x a => True | SEQ c1 c2 => vcg c1 (pre c2 Q) /\ vcg c2 Q | IFTHENELSE b c1 c2 => vcg c1 Q /\ vcg c2 Q | WHILE Inv b c => vcg c Inv /\ (afalse b //\\ Inv -->> Q) /\ (atrue b //\\ Inv -->> pre c Inv) end. Definition vcgen (P: assertion) (c: com) (Q: assertion) : Prop := (P -->> pre c Q) /\ vcg c Q. Fixpoint erase (c: com) : IMP.com := match c with | SKIP => IMP.SKIP | ASSIGN x a => IMP.ASSIGN x a | SEQ c1 c2 => IMP.SEQ (erase c1) (erase c2) | IFTHENELSE b c1 c2 => IMP.IFTHENELSE b (erase c1) (erase c2) | WHILE Inv b c => IMP.WHILE b (erase c) end. Lemma vcg_sound: forall c Q, vcg c Q -> {{pre c Q}} erase c {{Q}}. Proof. induction c; cbn; intros. - apply triple_skip. - apply triple_assign. - destruct H as (V1 & V2). apply triple_seq with (pre c2 Q); auto. - destruct H as (V1 & V2). apply triple_ifthenelse. + eapply triple_consequence. eapply IHc1; eauto. unfold aimp, aand, aor, atrue, afalse. intuition congruence. unfold aimp; auto. + eapply triple_consequence. eapply IHc2; eauto. unfold aimp, aand, aor, atrue, afalse. intuition congruence. unfold aimp; auto. - destruct H as (V1 & V2 & V3). eapply triple_consequence. + apply triple_while. eapply triple_consequence. apply IHc; eauto. eauto. red; auto. + red; auto. + auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)