The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-08-20 12:06 GMT+02:00 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 …

None that I have heard of. In fact, I never wondered if subgoals were solved independently or not. Evars are hardly ever used in my proofs, so that for me, "tac1; tac2." and "tac1. tac2. tac2." does the same thing when tac1 generates two goals. In fact if you had asked me before sending this mail, I would have told you that those two were equivalent.

For your problem, you could use the "instantiate" tactic, but it will kill the point of using evars. Once again, I am not familiar with evars, but something like "eapply H_Consequence_pre; (try instantiate 1 ((fun _ => True) [i|->a])); eauto." might work.
 

 

Best regards,

 

Michael

--
.../Sedrikov\...