The Coq mailing list

[Bart De Vylder <bartdevylder AT gmail.com>]

On Mon, Jun 11, 2012 at 4:38 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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

Thanks for your answer, but it seems I can't get it to work. 

If I use Hint Extern to match against the goal somehow, I don't see how i can refer to 'some' hypothesis in the context.

I read in the docs that Hint Extern can also be used to match against a hypothesis in the context, but I can't find an example of the syntax to use.

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
 

-- 
Bart De Vylder

+32(0)496/558065

bartdevylder AT gmail.com