The Coq mailing list

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

On 12/24/2011 01:04 AM, Marko Malikoviæ wrote:
> can somebody explain me how can I match equality in context without
> involving negation of inequality.
> For example, here I am interested only for terms ?a = ?b without ?a<>  ?b:
>
> match goal with
>      | id : context [?a = ?b] |- _ =>  ...
> ...
> end
>
> Namely, ?a<>  ?b is interpreted as ~ ?a = ?b. Because it include ?a<>  ?b
> in result of matching.
>    

That's an interesting puzzle!  You could definitely first match [?a = 
?b] and then perform a second match which _fails_ iff [a <> b] is also 
matched.  Whether this is sufficient depends on your context.

You might also try using a named [context] pattern, which should let you 
reconstitute the context with some other term plugged into the hole 
where [a = b] was.  If you pick a sufficiently rare term (let's call it 
[foo] here), you can then search for [~foo] in the result, which means 
[a = b] occurred inside a [not].