The Coq mailing list

[троль <vuvupik AT gmail.com>]

No, it's not a counterexample:

Theorem example_hoare_proof :
 hoare_proof example_P example_prog example_Q.
Proof.
 unfold example_prog, example_P, example_Q. eapply H_Consequence.
    apply (H_While (fun st => st X = 3 \/ st X = 4)). eapply 
H_Consequence_pre.
       apply H_Asgn.
       unfold assn_sub, bassn, update. simpl. intros. inversion H.
        right. apply beq_nat_true in H1. omega.
    simpl. intros. omega.
    unfold bassn, update. simpl. intros. inversion H. inversion H0.
       rewrite not_true_iff_false in H1. apply beq_nat_false in H1.
rewrite H2 in H1. intuition.
       assumption.
Qed.

My question is actually this: if {{ P }} WHILE b DO c END {{ Q }} is
valid hoare triple, does it implies, that you can prove it with
hoare_while? Since H_While is just a relation version of hoare_while.
I suppose, that you can't prove such a thing with an arbitrary loop
due to undecidability of loop's invariants inference. Am I right? Or
maybe someone has a solution to hoare_proof_complete?

2013/12/20, 
vuvupik AT gmail.com
 
<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.
>