Make Decidable a subtype of Bool
#2038
Conversation
| -/ | ||
| return false | ||
| /- | ||
| TODO: remove this hack after we refactor `Decidable` as suggested by Gabriel. |
There was a problem hiding this comment.
this TODO can now be removed, right? Or is the return false still a hack?
There was a problem hiding this comment.
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.
|
This PR is blocked by what I can only assume to be a miscompilation. Running stage1 immediately segfaults in the Diffing the IR code is hard because we generate lots of |
|
Regarding the explosion of join points (which perhaps is triggering the bug), I think the old compiler is very reliant on @[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 |
Without this change, we would not inline anything inside let x_42 := casesOn x_3 fun .. => ... here ...
|
Rebasing onto #2060 seemed to fix the compilation errors. !bench |
|
!bench |
|
Here are the benchmark results for commit 6cdf707. 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 σ) |
|
Just a ping in eager anticipation of progress on this PR! |
|
Something that might be a less invasive change is this: 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 |
|
@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 hsays "'unreachable' code was reached". UPD: I see that the assertion in |
|
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 |
|
This PR is subsumed by #8309, which uses the approach suggested by Kyle and Joachim with the new compiler. |
This resolves the diamond between
DecidableandBEq, which is starting to cause lots of headaches in mathlib.