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.

[ghost]

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
• 💥 Mathlib branch lean-pr-testing-8309 build failed against this PR. (2026-02-02 20:03:04) View Log

[Rob23oba]

!radar

[leanprover-radar]

Benchmark results for 507f2a8 against 58a8cd7 are in. There are significant results. @Rob23oba

• ✅ build//instructions: -146.4G (-1.25%)

Large changes (11✅, 3🟥)

• ✅ build/module/Init.Data.Nat.ToString//instructions: -21.2G (-74.15%)
• ✅ build/module/Std.Data.HashMap.RawLemmas//instructions: -11.1G (-9.93%)
• ✅ build/module/Std.Http.Data.Headers.Name//instructions: -7.0G (-36.21%)
• ✅ compiled/ilean_roundtrip//instructions: -325.5M (-1.45%)
• 🟥 compiled/parser//instructions: +334.9M (+0.97%)
• 🟥 compiled/phashmap//instructions: +72.8M (+0.84%)
• 🟥 elab/cbv_decide//instructions: +3.3G (+10.94%)
• ✅ elab/cbv_divisors//instructions: -2.7G (-5.75%)
• ✅ elab/cbv_merge_sort//instructions: -2.3G (-14.60%)
• ✅ elab/cbv_merge_sort//task-clock: -188ms (-14.00%)
• ✅ elab/cbv_merge_sort//wall-clock: -186ms (-13.93%)
• ✅ elab/whnfMatcherImplicitTransparencyCaching//instructions: -2.7G (-9.83%)
• ✅ elab/whnfMatcherImplicitTransparencyCaching//wall-clock: -120ms (-10.66%)
• ✅ lake/inundation/config/elab//instructions: -109.4M (-3.69%)

Medium changes (36✅, 6🟥)

• ✅ build/module/Init.Data.String.Basic//instructions: -4.6G (-16.13%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Vector.Lemmas//instructions: -2.1G (-4.84%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.Build.Facets//instructions: -1.4G (-15.14%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.App//instructions: -1.0G (-2.60%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.StructInst//instructions: -1.1G (-3.45%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: -1.9G (-9.26%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Elab.Tactic.Omega.Frontend//instructions: -1.3G (-5.14%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Sym.DSimp.EvalGround//instructions: -1.1G (-5.56%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Sym.Simp.EvalGround//instructions: -1.3G (-5.24%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.BVDecide.Normalize.Simproc//instructions: -1.5G (-5.97%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.FunInd//instructions: -1.1G (-2.71%)
• ✅ build/module/Lean.Meta.Tactic.Grind.AC.Eq//instructions: -1.6G (-5.76%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr//instructions: -3.2G (-8.13%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize//instructions: -1.4G (-14.20%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr//instructions: -2.0G (-8.03%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Cutsat.Search//instructions: -3.0G (-12.32%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Arith.Linear.Search//instructions: -1.5G (-8.89%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Core//instructions: -1.1G (-8.37%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: -1.2G (-3.35%) (reduced significance based on absolute threshold)
• ✅ build/module/Lean.Meta.Tactic.Grind.Internalize//instructions: -1.2G (-6.73%) (reduced significance based on absolute threshold)
• and 21 more
• and 1 hidden

Small changes (418✅, 198🟥)

• 🟥 build/module/Init.Classical//instructions: +16.6M (+1.54%)
• 🟥 build/module/Init.Control.Lawful.Instances//instructions: +25.9M (+0.38%)
• 🟥 build/module/Init.Control.Lawful.MonadAttach//instructions: +4.4M (+0.88%)
• 🟥 build/module/Init.Control.Lawful.MonadLift.Instances//instructions: +6.5M (+0.56%)
• 🟥 build/module/Init.Control.Lawful.MonadLift//instructions: +5.1M (+1.04%)
• 🟥 build/module/Init.Core//instructions: +171.0M (+1.73%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Array.Attach//instructions: +26.5M (+0.25%)
• ✅ build/module/Init.Data.Array.BinSearch//instructions: -21.2M (-0.33%)
• ✅ build/module/Init.Data.Array.Bootstrap//instructions: -93.6M (-3.84%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Lemmas//instructions: -629.8M (-1.15%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Lex.Basic//instructions: -134.5M (-9.03%) (reduced significance based on absolute threshold)
• 🟥 build/module/Init.Data.Array.Range//instructions: +14.6M (+0.36%)
• 🟥 build/module/Init.Data.Array.Sort//instructions: +5.0M (+0.95%)
• 🟥 build/module/Init.Data.Array.Zip//instructions: +19.2M (+0.41%)
• 🟥 build/module/Init.Data.Array//instructions: +4.8M (+0.87%)
• ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -448.9M (-0.84%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.BitVec.Bootstrap//instructions: -11.1M (-0.40%)
• 🟥 build/module/Init.Data.BitVec.Decidable//instructions: +12.1M (+1.57%)
• ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -983.4M (-0.81%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Bool//instructions: -168.9M (-3.86%) (reduced significance based on absolute threshold)
• and 596 more