Make Decidable a subtype of Bool

[gebner]

This resolves the diamond between Decidable and BEq, which is starting to cause lots of headaches in mathlib.

[digama0]

this TODO can now be removed, right? Or is the return false still a hack?

[gebner]

From what I understand, the return false here is about instances that have more than one exit point, i.e., if c then { a := 42 } else { a := 1 }. We still allow that and I didn't remove class inductive either.

[gebner]

This PR is blocked by what I can only assume to be a miscompilation. Running stage1 immediately segfaults in the Syntax.identComponents function where we call lean_inc on a freed object that was allocated in splitNameLit.

Diffing the IR code is hard because we generate lots of block y := ..; case x of false-> jmp block 0; true -> jmp block 1 instead of a direct case distinction.

[Kha]

Regarding the explosion of join points (which perhaps is triggering the bug), I think the old compiler is very reliant on ite being a direct recursor application . At the LCNF level we expand macro_inline but no matchers. Unfortunately

@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
  h.decide.casesOn
    (fun h => e (nomatch h.2 ·))
    (fun h => t (h.1 (.refl _)))
    h.decide_iff

@[macro_inline] def ite {α : Sort u} (c : Prop) [Decidable c] (t e : α) : α :=
  dite c (fun _ => t) (fun _ => e)

doesn't really help because the overapplication of Bool.casesOn seems to trigger a similar join point mess.

[gebner]

Rebasing onto #2060 seemed to fix the compilation errors.

!bench

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6cdf707.
There were significant changes against commit 345aa6f:

  Benchmark          Metric         Change
  ===================================================
- binarytrees        task-clock       3.9%   (10.5 σ)
- stdlib             instructions     2.1% (1236.2 σ)
- stdlib             maxrss           1.4%  (140.2 σ)
- stdlib             task-clock       1.5%   (19.4 σ)
- stdlib             wall-clock       1.3%   (67.3 σ)
- stdlib size        bytes .olean     2.2%
- workspaceSymbols   maxrss           1.4%   (15.2 σ)
+ workspaceSymbols   task-clock      -4.0%  (-20.8 σ)
+ workspaceSymbols   wall-clock      -4.0%  (-20.8 σ)

[fgdorais]

Just a ping in eager anticipation of progress on this PR!

[kmill]

Something that might be a less invasive change is this:

class Decidable (p : Prop) where
  /-- The truth value of the proposition `p` as a `Bool`.
  If `true` then `p` is true, and if `false` then `p` is false. -/
  decide : Bool
  /-- `decide p` evaluates to the Boolean `true` if and only if `p` is a true proposition.  -/
  cond_decide : cond decide p (Not p)

/-- Prove that `p` is decidable by supplying a proof of `p` -/
@[match_pattern] def Decidable.isTrue {p : Prop} (h : p) : Decidable p where
  decide := true
  cond_decide := h

/-- Prove that `p` is decidable by supplying a proof of `¬p` -/
@[match_pattern] def Decidable.isFalse {p : Prop} (h : Not p) : Decidable p where
  decide := false
  cond_decide := h

In my limited testing, you don't need to touch pre-existing match patterns, which would be great if that meant downstream projects don't need to be updated.

However, this does need a modification to erase_irrelevant.cpp and perhaps other parts of the compiler, since properties of Decidable are hard-coded into it, and changing Decidable out from under it causes assertion violations.

[urkud]

@kmill I tried your definition on current version of Lean4, then

@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
  match h with
  | .isTrue h => t h
  | .isFalse h => e h

says "'unreachable' code was reached". UPD: I see that the assertion in decidable_to_bool_cases fails, I'll fix it tonight after day job.

[nomeata]

I am also getting interested in the change, in the form that Kyle and I came up with: It seem it would allow me to first write a decision procedure using normal booleans, and then do the proof separately, and finally when using decide, the kernel will quickly start reducing the plain boolean function, which is (maybe) more efficient than carrying the extra type parameter around all the time.

[zwarich]

This PR is subsumed by #8309, which uses the approach suggested by Kyle and Joachim with the new compiler.