The Coq mailing list

[Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>]

filou AT labri.fr
 wrote:
> Hi all,
>
> 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.
>
> Thanks,
> Vincent

There is something wrong with your environment.

===

Require Import Bool Ring.

Goal forall a b, a && false && b = true -> True.

intros.
ring_simplify in H.

=============

works

--
Laurent