The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

Le 07/10/2010 11:54, 
filou AT labri.fr
 a écrit :
> I was wondering if there exists a tactic to simplify boolean
> expressions in hypotheses, such as in a goal of the form
>
> H: a && false && b = true
> -------------------------
> False
>
> I've tried "contradict H;ring" but it seems that ring doesn't deal with
> inequalities.

Indeed, ring deals only with equalities. In your case, you can do 
"ring_simplify in H" that will turn H into "false = true", which can 
then be solved by "discriminate".

Note that the boolean ring is declared in terms of andb and xorb. You 
should be able to express all boolean expressions in terms of these.


Cheers,

--
Stéphane