feat: Decidable as subtype of Bool

[Rob23oba]

This PR changes the definition of Decidable p to a structure containing a Bool and a proof of either p or ¬p (basically the approach proposed by @kmill in #2038). Due to bugs in the old compiler, this was previously not possible; however, now that the new compiler is enabled, this works perfectly fine.
Using Bool in the definition of Decidable has several advantages, in particular

• There are many more definitional equalities, e.g.

  variable (a b : Bool)
  
  #check (rfl : decide (a = true) = a)
  #check (rfl : decide (a = false) = !a)
  #check (rfl : decide (a = true ∧ b = true) = a && b)
  #check (rfl : decide (a = true ∨ b = true) = a || b)
  #check (rfl : decide (¬a) = !a)
  #check (rfl : decide (a = true ↔ b = true) = (a == b))

• The decide tactic no longer needs to carry proofs with it, improving performance for well-written Decidable instances.
• LawfulBEq and DecidableEq are now compatible: When using the DecidableEq instance provided by LawfulBEq, decide (a = b) is definitionally equivalent to a == b.
• Decidable no longer needs special casing in the compiler.

In order to take full advantage from these changes, it is recommended to use the decidable_of_bool and decidable_of_iff functions to construct Decidable instances.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 579d0ad15db8062933ecc0833562c875216cc9d7 --onto 2b4f372317f214e92988a79fc765586fbfb64e97. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-13 10:04:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ff85acedb91537b383b744fcf4639a3a663df90f --onto 29cc75531a5a0e8626fa5e96371e7ceb98877782. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-14 12:42:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 106708ee78ef174fb69c34c76a08b1321a85f6ca --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-08 12:29:16)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e7c8baaef5daac6e94bb4e18c2c49d3810ad55a2 --onto db499e96aac8ad654c8ed5ab40c4e6885d38c9a1. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-21 09:34:17)
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-07-10 22:07:54) View Log
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-07-11 05:50:15) View Log
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-07-11 05:53:25) View Log
• ❌ Mathlib branch lean-pr-testing-8309 built against this PR, but testing failed. (2025-07-11 06:35:46) View Log
• ❌ Mathlib branch lean-pr-testing-8309 built against this PR, but testing failed. (2025-07-11 07:16:37) View Log
• ✅ Mathlib branch lean-pr-testing-8309 has successfully built against this PR. (2025-07-11 07:52:53) View Log
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-07-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-13 11:08:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20873d5d7293d18d3f2aeda35388a23ea7f406a7 --onto d869c38e7bee7d484040b758837be76f55db9498. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-17 00:44:23)
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-09-17 16:23:21) View Log
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase be2c2bcf9b9b27dc223e9141d6ba9c0204f68397 --onto efbbb0b230ce95653d25b59c83fd24a51a8bf363. (2025-10-25 19:41:18)
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-10-25 19:53:49) View Log
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-10-25 20:39:56) View Log
• ❌ Mathlib branch lean-pr-testing-8309 built against this PR, but testing failed. (2025-10-25 20:55:28) View Log
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2025-10-25 21:08:04) View Log
• ✅ Mathlib branch lean-pr-testing-8309 has successfully built against this PR. (2025-10-25 22:10:56) View Log

[hargoniX]

The general approach and the changes you did inside of the compiler seem reasonable to me. I do not feel confident enough in all of the elaborator to sign off on the change my own so I would prefer someone else to take a look at that as well.

One thing I was wondering though: You're redefining lots of Decidable instances though I would assume (or at least hope) that one can simply keep the old code around without type checking issues? What's the motivation for the change here?

[Rob23oba]

Well, the idea is to make boolean functions and Decidable instances more compatible and more performant with the new system. For example, we wrap most Decidable instances directly in a constructor application as to reduce the projection decide quicker and use boolean functions to provide compatibility with them (e.g. making decide (a = true ∧ b = true) = a && b or Nat.beq m n = (m == n) true by defeq). One important part about this is that due to directly using a constructor with a boolean function, we don't need to carry proofs around while reducing. I haven't done this with all of them yet but I'll maybe do it with some of the other ones in the future.

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 23d879d against be2c2bc are in! @hargoniX

Major changes (8)

• Init.Prelude async//instructions changed by +3.0% (🟥).
• ilean roundtrip//instructions changed by +2.2% (🟥).
• iterators (elab)//instructions changed by -2.8% (✅).
• parser//instructions changed by -2.2% (✅).
• phashmap.lean//instructions changed by +2.5% (🟥).
• rbmap_1//instructions changed by +19.3% (🟥).
• reduceMatch//instructions changed by +2.7% (🟥).
• stdlib//instructions changed by +0.4% (🟥).

Minor changes (18)

• Init.Data.BitVec.Lemmas//instructions changed by -0.7% (✅).
• big_deceq//instructions changed by +1.2% (🟥).
• big_deceq_rec//instructions changed by +1.3% (🟥).
• bv_decide_mod//instructions changed by -0.9% (✅).
• bv_decide_mul//instructions changed by -0.9% (✅).
• bv_decide_realworld//instructions changed by -0.8% (✅).
• grind_bitvec2.lean//instructions changed by -0.7% (✅).
• hashmap.lean//instructions changed by +1.9% (🟥).
• identifier auto-completion//instructions changed by +2.0% (🟥).
• import Lean//instructions changed by +1.0% (🟥).
• iterators (interpreted)//instructions changed by +1.9% (🟥).
• lake build no-op//instructions changed by +0.9% (🟥).
• language server startup//instructions changed by +0.6% (🟥).
• rbmap//instructions changed by -1.6% (✅).
• riscv-ast.lean//instructions changed by +1.3% (🟥).
• treemap.lean//instructions changed by +0.7% (🟥).
• workspaceSymbols with new ranges//instructions changed by +0.6% (🟥).
• workspaceSymbols//instructions changed by +1.9% (🟥).

[nomeata]

I wouldn't call this a chore. It’s at least a refactor, if not a perf or feat actually. It certainly warrants being shown in the release notes.

[Rob23oba]

Yeah, you're right, I also thought about that

[linesthatinterlace]

I am not a maintainer or anything - so my voice has the least weight here compared to anyone else - but I do want to say I like these changes and find them very sensible in principle, and have some comments.

One question: you mention that due to these changes, decidable_of_bool and decidable_of_iff are recommended to construct decidability instances. But obviously this isn't how many elementary decidability instances are constructed in the prelude and often that is where users will look! In practice it seems we are often even in the very early files retaining the definition of Decidable using match statements, and I just wonder: this doesn't seem to chime with the recommendation you make and I do worry it would be confusing to users. Could you introduce these constructors earlier and be stricter about their use? To be clear I think it absolutely makes sense to have isTrue and isFalse as match patterns and eliminate using them - it means that if nothing else we solve a lot of compatibility issues - but I think bluntly your recommendations above will not be followed unless you more clearly demonstrate their use.

I also wonder about this Bool.Reflects predicate that you define: I like it and it seems like it gives good definitional equality, but you mention it is equivalent to b \iff p and I haven't yet found that theorem in what you have. It seems to me that surely that would affect your definition of decidable_of_bool, which is essentially the same as your new definition of Decidable except for this difference. Yet you construct decidable_of_bool using a match statement - even though by all rights this one, at least, should be constructable using the constructor directly.

[Rob23oba]

Well, the main point of the Bool.Reflects predicate is that I want that Decidable.intro true h / Decidable.intro false h typechecks for h : p / h : ¬p under reducible transparency. As such, it currently has no API except its definitional equalities. I haven't quite decided yet on whether we want users to interact with Bool.Reflects directly but since it is part of the definition of Decidable, people will most likely naturally stumble upon it and I see how it could be weird then to see that Bool.Reflects doesn't have any API.
Regarding how you're meant to construct Decidable instances: What I mean by that sentence is that if you use decidable_of_iff and decidable_of_bool, you'll get the definitional equality advantages of the new definition, which you won't get if you instead use match with isTrue and isFalse. The question of whether Decidable.intro is fine is I guess the question of whether we want to consider it and Bool.Reflects part of the public API -- I haven't quite decided yet but it might be a good idea; but we can also do this later. For Decidable instances that use matches: I intend to reduce the amount of them later but at first it's simpler to reduce the amount of changes since there's also all kinds of bootstrapping weirdness involved.
Also, if you meant match statements as the second parameter of Decidable.intro: There's not really any problem with that, in fact I'm not sure if there's really a better way to do this; it's just a proof parameter and we have proof irrelevance so it doesn't really matter.

[linesthatinterlace]

My gut feeling is that one should only define something if one intends to create API for it. You could replace decide.Reflects p with cond decide p (Not p) and I think it would still have all the properties you want for it. Or even bif decide then p else Not p, if we have that notation at that point though that feels somewhat like over-egging it. Conversely you could proceed with introducing Reflects - which I actually quite like - but then I feel you want at minimum b.Reflects p \iff (b = true \iff p) as a theorem somewhere.

I see the point about proof irrelevancy making the match statements not matter though and bootstrapping can be a pain.

My instinct is that Decidable.intro isn't needed and should probably be private... but this is because I think decidable_of_iff is Just Better for actually constructing an instance.

[Rob23oba]

You could replace decide.Reflects p with cond decide p (Not p) and I think it would still have all the properties you want for it.

You're right, that's what I originally had. However, cond doesn't reduce under reducible transparency and Decidable.isTrue is an abbreviation, so when you unfold it you'd end up with a term that doesn't typecheck under reducible transparency (under the cond definition), so you'd end up with defeq abuse (It probably wouldn't matter but better be safe). Also, Decidable.intro can't be private since we need to expose Decidable.isTrue and Decidable.isFalse for match patterns and exposed definitions can't refer to private declarations.

[linesthatinterlace]

Right, yes I see. If they weren't abbreviations that would not be an issue, is that right?