lean4
lean4 copied to clipboard
leanprover
Make `Decidable` a subtype of `Bool`
This resolves the diamond between Decidable and BEq, which is starting to cause lots of headaches in mathlib.
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.
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.
Here are the benchmark results for commit 6cdf707193b1dc637570ae141fd0eabf944cc5fc. There were significant changes against commit 345aa6f835aa6ab1c31180281b18e3b80b7d173a:
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 σ)
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.
@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.
