The Coq mailing list

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

I am in the following situation:

===== Executed proof script =====

Theorem H_Post_True_deriv':
  forall c P, hoare_proof P c (fun _ => True).
Proof.
  intro c.
  com_cases (induction c) Case; eauto with HDBhoare.
    intro P.

===== Context after executing this =====

2 subgoal
Case := "::=" : String.string
i : id
a : aexp
P : Assertion
______________________________________(1/2)
hoare_proof P (i ::= a) (fun _ : state => True)
______________________________________(2/2)
forall P : Assertion,
hoare_proof P (WHILE b DO c END) (fun _ : state => True)

===== Definition of the hint database HDBhoare =====

Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: none
Cut: Ø
For any goal ->   (*external*) intros; apply I(level 10, id 0)
For hoare_triple ->   apply hoare_asgn(level 0, id 0)
                      apply hoare_skip(level 0, id 0)
                      apply hoare_while(level 1, id 0)
                      apply hoare_if(level 2, id 0)
                      eapply hoare_seq(level 3, id 0)
                      eapply hoare_consequence(level 5, id 0)
For True ->   exact I(level 0, id 0)
For hoare_proof ->   apply H_Asgn(level 0, id 0) apply H_Skip(level 0, id 0)
                     apply H_While(level 1, id 0) apply H_If(level 2, id 0)
                     eapply H_Consequence_pre(level 3, id 0)
                     eapply H_Seq(level 3, id 0)
                     eapply H_Consequence(level 5, id 0)

===== What I don't understand =====

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?

Thanks & best regards,

Michael

P.S.:

I am using Coq 8.4pl4