The Coq mailing list

[vuvupik AT gmail.com]

It's in HoareAsLogic.v:
Theorem hoare_proof_complete : forall P c Q,
  {{P}} c {{Q}} -> hoare_proof P c Q.
By placing admit in the end of available proof, i've got this context:

Case := "WHILE" : String.string
  b : bexp
  c : com
  IHc : forall P Q : Assertion, ({{P}} c {{Q}}) -> hoare_proof P c Q
  P : Assertion
  Q : Assertion
  HT : {{P}} WHILE b DO c END {{Q}}
  ============================
   hoare_proof P (WHILE b DO c END) Q

But isn't it a counterexample? :

Definition example_prog :=
 WHILE BEq (AId X) (ANum 3) DO
    X ::= APlus (AId X) (ANum 1)
 END.
Definition example_P := fun st => st X = 3.
Definition example_Q := fun st => st X = 4.

Theorem example_hoare_triple :
 {{ example_P }} example_prog {{ example_Q }}.
Proof.
 unfold example_prog, example_P, example_Q, hoare_triple. intros. inversion H;
subst.
    simpl in H5. rewrite H0 in H5. inversion H5.
    inversion H4. inversion H7; subst.
       rewrite <- H12. simpl. unfold update. simpl. rewrite H0. reflexivity.
       simpl in H11. unfold update in H11. simpl in H11. rewrite H0 in H11.
inversion H11.
Qed.

Theorem example_hoare_proof :
 hoare_proof example_P example_prog example_Q.
Proof.
 unfold example_prog, example_P, example_Q. eapply H_Consequence_post.
    apply H_While.
    eapply H_Consequence_pre.
       apply H_Asgn.
       unfold assn_sub, bassn, update. simpl. intros. (* stuck *)
Abort.