The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear,

Thanks for your reply but neither solution does not fit. Hypotheses in my
context are propositional expressions over arithmetic expressions.
For example (simplified):

H : a <> b \/ c = d /\ e > a \/ ...

From such hypotheses I require only an arithmetic expressions of the form
X = Y (I need them for rewriting).

Your first solution does not fit to me because I do not know whether the
same hypothesis contain expressions X = Y and X <> Y.

The second solution does not fit to me because if I put "foo" instead of
all occurences of a = b then I can have foo and ~foo in the same
hypothesis.

Thanx again,

Marko Malikovic

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


-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------