## Stream: new members

### Topic: reduce bool variable

#### Alex Kassil (Oct 11 2019 at 05:49):

If I have this:

variable b : bool
#reduce b && tt
#reduce b && ff
#reduce ff && b
#reduce tt && b


I get back

b && tt
b && ff
ff
tt && b


my question is why does b && ff not reduce to ff and why does tt && b not reduce to b? Thanks!

#### Floris van Doorn (Oct 11 2019 at 05:56):

The reason is that band (the name for &&) was defined as follows:

def band : bool → bool → bool
| ff _  := ff
| tt ff := ff
| tt tt := tt


If we would have defined it as follows

def my_band : bool → bool → bool
| ff _ := ff
| tt b := b
variable b : bool
#reduce my_band b tt
#reduce my_band b ff
#reduce my_band ff b
#reduce my_band tt b


then, as you can see tt && b would reduce to b.

I don't think that there is a way to define && so that both ff && b and b && ff will reduce to ff: it will have to decide which side it will evaluate first.

#### Kevin Buzzard (Oct 11 2019 at 07:32):

No doubt you can apply a theorem in the library to get from tt && b to tt, but #reduce doesn't do that.

Last updated: May 14 2021 at 03:27 UTC