The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Thomas,


 In coq's doc, there is a mention "The tactic must be loaded by Require 
Import Ring. The ring structures must be declared with the Add Ring 
command (see below). The ring of booleans is predefined"

 I couldn't find exactly this definition in the library. I assume that 
using ring and ring_simplify
on boolean expressions can be more efficient than autorewrite, and we 
should have
the possibility of solving equations that involve associativity and 
commutativity, but we may
lose properties of negb ?

Pierre



Le 07/10/2010 13:41, Thomas Braibant a écrit :
> 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
> >
> >
> >
> >