The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I often use :

Hint Rewrite
  orb_false_r                    (** b || false -> b *)
  orb_false_l                    (** false || b -> b *)
  orb_true_r                     (** b || true  -> true *)
  orb_true_l                     (** true || b  -> true  *)
  andb_false_r                   (** b && false -> false *)
  andb_false_l                   (** false && b -> false *)
  andb_true_r                    (** b && true  -> b *)
  andb_true_l                    (** true && b  -> b  *)
  negb_orb                       (** negb (b || c) -> negb b && negb c *)
  negb_andb                      (** negb (b && c) -> negb b || negb c *)
  negb_involutive                (** negb( (negb b) -> b *)
  : bool_simpl.

Hint Rewrite <- andb_lazy_alt : bool_simpl. (** a &&& b -> a && b *)
Hint Rewrite <- orb_lazy_alt : bool_simpl.  (** a ||| b -> a || b *)

Ltac bool_simpl := autorewrite with bool_simpl in *.

which you can adapt to autorewriting in an hypothesis.


then, in your case, you can use "discriminate" to conclude.

With best regards,
thomas



On Thu, Oct 7, 2010 at 11:54 AM,  
<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
>
>
>