The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-08-20 9:41 GMT+02:00 <michael.soegtrop AT intel.com>:

Dear Coq users,

testing the Coq automation features I came accross a behaviour of eauto I
don't understand. Unfortunately I couldn't boil this down to a simple use
case. It is an exercise from the HoareAsLogic chapter from the Software
Foundations course, I try to proof with automation.
<…>
The thing I don't understand is that the following steps solve the first goal.
H_Consequence_pre results in 2 subgoals, both of which can be solved with
eauto.

    eapply H_Consequence_pre.
          eauto with HDBhoare.
          eauto with HDBhoare.

But strangely, this doesn't solve the first goal

    eapply H_Consequence_pre; eauto with HDBhoare.

I assumed that this is exactly the same as the above, but this solves only the
first subgoal, but not the second one. The second subgoal looks exactly the
same as when I execute only the first eauto step above.
Also consequently this doesn't work

    eauto 6 with HDBhoare.

which should work, because H_Consequence_pre is in the hint database.


Does someone have an explanation and a work around for this behaviour?

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.)

My guess is that "eapply H_Consequence_pre; eauto with HDBhoare." tries both "eauto with HDBhoare" branches in parallel, and the second branch fails since there is too many existentials and they cannot be inferred. While in your first attempt, both branches are tried one after the other and the first branch instantiates evars in the second branch making the second branch solvable.

I do not have Coq nor Software Foundations installed, and cannot try this. If I am correct, A. Spiwack works on the proof engine and things may be different in the trunk version.
 

Thanks & best regards,

Michael

P.S.:

I am using Coq 8.4pl4

--
.../Sedrikov\...