spelling Bool-valued operations

Stream: mathlib4

[Sky Wilshaw]

I have some lemmas I'm trying to port like:

theorem countp_cons_of_neg {a : α} (l) (pa : ¬p a) : countp p (a :: l) = countp p l

I'm a bit concerned about the spelling of the ¬p a hypothesis. countp now takes a Bool-valued function not a Prop-valued one, so should the spelling be something like pa : p a == false?

[Yaël Dillies]

Bool-valued arguments are a pain. We should consider having a mathlib version of countp that still uses Prop.

[Yaël Dillies]

After the port we can decide which one to keep.

[Sky Wilshaw]

One slightly irritating thing is that !(p a) = (p a == false) isn't true by reflexivity.

[Mario Carneiro]

I think using ¬p a is the most likely to fit with downstream uses, and we should have simp lemmas and such which rewrite b = false to ¬(b = true) so that you can use logical operators as much as possible

[Sky Wilshaw]

Should count (= countp (· == a)) lemmas be spelled in terms of DecidableEq or LawfulBEq?

[Sky Wilshaw]

Since DecidableEq gives an automatic LawfulBEq instance, I think it would be more flexible to just require a LawfulBEq.

[Sky Wilshaw]

I'm also wondering if we should use the bif spellings for bool-valued if statements or not.

[Sky Wilshaw]

e.g.

theorem countp_cons (a : α) (l) : countp p (a :: l) = countp p l + if p a then 1 else 0

[Sky Wilshaw]

Also, any of these could be used:

• if a == b then ...
• if a = b then ...
• bif a == b then ...

[Reid Barton]

I tried changing some such lemmas to use bif because it seemed sensible, but it made later parts of the file more awkward

[Mario Carneiro]

I think we should use if where we used to use if and bif where we used to use cond, at least for the short to mid term. I think this will lead to the least amount of bool-related pain. Maybe if we get better lemmas and/or tactics we can use bif more, but for now I would stick to using it only in definitions for programming purposes (and even then it might not be necessary depending on how good the compiler is)