The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

[auto] works by syntactic matching of head symbols, and the conclusion 
and [H] don't start with the same head symbol.  You should be able to 
use a [Hint Extern] to get the effect you want, though.

On 06/11/2012 10:35 AM, 
bartdevylder AT gmail.com
 wrote:
> I am puzzled why the auto tactic does not solve a subgoal which only involves
> applying "apply" twice with a Hypothesis from the current context. I didn't
> find a solution/explanation in the documentation or mailing lists.
>
> Concretely, this is the state I'm stuck in:
>
> 2 subgoals
> s : state
> v : volumeName
> H : uniqueLocation s
> H0 : consistent1 s
> v1 : volumeName
> v2 : volumeName
> H1 : v1<>  v2
> ______________________________________(1/2)
> match s v1 with
> | volstate n1 p1 _ _ =>
>      match s v2 with
>      | volstate n2 p2 _ _ =>  n1<>  n2 \/ p1<>  p2
>      end
> end
>