Zulip Chat Archive

Stream: new members

Topic: reduce bool variable

view this post on Zulip 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
tt && b

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

view this post on Zulip 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.

view this post on Zulip 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