The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Cedric,

 

>  Does "eapply H_Consequence_pre; [eauto with HDBhoare|eauto with HDBhoare]." works any better ?
> (If so, I know this would not help you much, but it has some interest for me, as some tactics like "abstract" require one-liners.)

 

No, this also doesn’t work.

 

But your explanation sheds quite some light on this. I didn’t think that Coq tries to solve the two goals independently, so that variables instantiations done by one sub goal might be missing in the other one. The second sub goal does actually change by solving the first one. Before I solve the first sub goal

 

    hoare_proof ?2055 (i ::= a) (fun _ : state => True)

 

the second sub goal looks like this:

 

    forall st : state, P st -> ?2055 st

 

After I solve the first sub goal, the second sub goal looks like this:

 

   forall st : state, P st -> ((fun _ : state => True) [i |-> a]) st

 

So ?2055 got instantiated by something by solving the first sub goal. It is obvious that the second sub goal cannot be solved without this instantiation.

 

Is there anything like “;” which works sequentially on sub goals? I can of cause use repeat to get this effect …

 

Best regards,

 

Michael