De Morgan Laws for booleans

Stream: mathlib4

[Henrik Böving]

I think I might have discovered a bug related to precedence of boolean operators. When using:

@[simp]
theorem not_and : ∀ a b : Bool, !(a && b) = (!a || !b) := by decide
#align bool.bnot_band Bool.not_and

@[simp]
theorem not_or : ∀ a b : Bool, !(a || b) = (!a && !b) := by decide
#align bool.bnot_bor Bool.not_or

from Mathlib.Data.Bool.Basic (docs4#Bool.not_and and docs4#Bool.not_or) These theorems give me the statement:

⊢ ∀ (a b : Bool), (!decide ((a && b) = (!a || !b))) = true

But I don't think this is what we want these statements to mean right? It would be better if they were actual equalities to rewrite over. If they are written as:

theorem not_and : ∀ a b : Bool, (!(a && b)) = (!a || !b) := by decide

instead I get the desired equality:

⊢ ∀ (a b : Bool), (!(a && b)) = (!a || !b)

Is this a bug? if yes how do we fix this? Changing precedence of ! in lean? Adding the extra pair of parentehsis? If no, how can I get the equational rewriting behaviour that I want from the current theorem?

[Yury G. Kudryashov]

Thanks for catching this bug! If you want a quick fix, then you should add extra parentheses in Mathlib. If you can wait longer, then you should fix it in the core. Here is the current definition:

@[inherit_doc] notation:max "!" b:40 => not b

[Yury G. Kudryashov]

I don't know for sure how notation works an why it "eats" the equality sign.

[Yaël Dillies]

40 looks very low precedence for such an operator. I would have expected at least 200. In comparison, docs#has_compl.compl has priority 1025.

[Yaël Dillies]

You could check what the precedence is in Lean 3.

[Yury G. Kudryashov]

BTW,

postfix:999 "ᶜ" => compl

sometimes eats too much on the left.

[Reid Barton]

1024 is the priority of function application IIRC.

[Reid Barton]

So 999 is not high enough.

[Reid Barton]

I can't say I remember ever seeing a precedence in the range [100, 900].

[Reid Barton]

e.g. ^ has pretty high precedence, and it's 80.

[Reid Barton]

Probably the precedence of boolean NOT should be higher than the precedence of boolean AND, right?

[Reid Barton]

Mathlib 3 has prefix `!`:90 := bnot

[Yury G. Kudryashov]

Probably, we should add some tests for precedence of operations like a * b + c = (a * b) + c := rfl etc.

[Reid Barton]

Oh I see--boolean NOT is indeed higher than boolean AND, it's = that messes it up.

[Reid Barton]

I think the way we got away with this in Lean 3 is by basically never using ! or &&

[Reid Barton]

There's a tension between "I want to write equations about the results of boolean operations" and "I want to combine the truth values of equations using boolean operations". In Lean 3, we never really did the second one with bool.

[Reid Barton]

So all the boolean operations have much higher priority than =, and it works fine.

[Floris van Doorn]

Reid Barton said:

There's a tension between "I want to write equations about the results of boolean operations" and "I want to combine the truth values of equations using boolean operations". In Lean 3, we never really did the second one with bool.

In Lean 4, for the second one we can use ==.