reduce bool variable

Stream: new members

[Alex Kassil]

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]

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]

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