Define boole?

[semorrison]

Per discussions at

• https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Is.20this.20thing.20useful/near/169601079
• feat(data/list/sort): ordered_insert lemmas #1437 (comment) and
• feat(algebra/big_operators): simp lemmas #1471 (comment)

I would want such a definition to be reducible or even an abbreviation, to avoid compelling people to use it:

abbreviation boole {A : Type u} [has_zero A] [has_one A] (b : bool) : A := if b then 1 else 0

example {P : Prop} [decidable P] : ℕ := boole P

It's not super important, but has come up several times recently so I thought I'd record it here.

[semorrison]

If anyone implements this, it might be worth grepping for if.*then 1 else 0 and ite.* 1 0 and seeing if any occurrences are clearer when using boole instead.

[jcommelin]

Would it make sense to even stack a dirichlet delta on top of this?

[fpvandoorn]

The name for this in math (or maybe only physics?) is the Kronecker Delta function, right?

[jcommelin]

Oops... my bad

[rwbarton]

This is also the Iverson bracket, though I definitely don't suggest using that notation!
I'm not sure I understand the proposed name boole, though I also don't have another name in mind.

[digama0]

I think Boole gets the credit for considering propositions as a ring with 0 and 1, but I forget exactly where I've heard this name before. Mathematica?

[semorrison]

There are a lot of Unicode square brackets out there, if we want something like the Iverson bracket. (My suggestion for the name in creating the issue was solely following Mario's suggestion on zulip.)

…

On Thu, Sep 26, 2019, 9:57 AM Mario Carneiro ***@***.***> wrote: I think Boole gets the credit for considering propositions as a ring with 0 and 1, but I forget exactly where I've heard this name before. Mathematica? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#1472?email_source=notifications&email_token=AADUWBEIT5GLN3656OHBHXLQLP3GRA5CNFSM4IZFQSLKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD7TZIMY#issuecomment-535270451>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADUWBA5N3UMDUOVP7WYEJTQLP3GRANCNFSM4IZFQSLA> .

[digama0]

I definitely recommend against using the Iverson bracket notation. Besides the fact that brackets are way overloaded already, this is not even common notation in math. I think that {\bf 1}_P (x) is a more common way to notate this, but I would suggest using no notation for it and just using the named function.

[avigad]

The function x -> if P x then 1 else 0 is often called the "indicator function" for P. Would it help to define indicator P and then take this particular one to be indicator (eq x)?

[rwbarton]

Oh yes, I also meant to suggest a name based on "characteristic function" or "indicator function", though "characteristic" is too overloaded I think.

[urkud]

I'm not sure what will be better:

• Should it take s : set α, α → Prop or α → bool as an argument?
• Should it use ℕ as the codomain or should it take the codomain as an argument?
• If it takes to codomain as an argument, should it be an explicit argument?

BTW, do we have statements like (∀ x, decidable (x ∈ s)) → (∀ x, decidable (x ∈ t)) → ∀ x, decidable (x ∈ (s ∪ t)) and similarly for other operations?

[rwbarton]

Related: integrals over subsets #1875.

[urkud]

We have indicator in data/indicator_function #1875. Should we close this issue?

[jalex-stark]

We have indicator in data/indicator_function #1875. Should we close this issue?

I suppose there's still the task of propagating the use of indicator out to places where ite is currently used.

[urkud]

@jalex-stark I don't think that it makes sense to have a tracking issue without a list of places where ite should be replaced with indicator. Feel free to open a new issue with an itemized list of such places (or just replace ite with indicator here and there).