Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reduction of Decidable instances very slow when using cases tactic. #2552

Closed
kim-em opened this issue Sep 17, 2023 · 3 comments
Closed

Reduction of Decidable instances very slow when using cases tactic. #2552

kim-em opened this issue Sep 17, 2023 · 3 comments
Labels
RFC Request for comments

Comments

@kim-em
Copy link
Collaborator

kim-em commented Sep 17, 2023

It is easy to write Decidable instances which use cases internally, which are then unusable in the kernel.

  • Can we change this behaviour to make such instances usable?
  • If not, how can we help users avoid this?

This issue, or something quite close to it, has come up multiple times now.

Example below provided by @kbuzzard and @bmehta on zulip:

@[inline] def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
  decidable_of_decidable_of_iff h

theorem LE.le.lt_or_eq_dec {a b : Nat} (hab : a ≤ b) : a < b ∨ a = b :=
by cases hab
   · exact .inr rfl
   · refine .inl ?_ ; refine Nat.succ_le_succ ?_ ; assumption

section succeeds_using_match

local instance decidableBallLT :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, _, _ => isTrue fun _ => (by cases ·)
| (n+1), P, H =>
  match decidableBallLT n (P · <| Nat.le_succ_of_le ·) with
  | isFalse h => isFalse (h fun _ _ => · _ _)
  | isTrue h =>
    match H n Nat.le.refl with
    | isFalse p => isFalse (p <| · _ _)
    | isTrue p => isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)

-- succeeds quickly
example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide

end succeeds_using_match

section fails_with_timeout

-- we change `match decidableBallLT` to `by cases decidableBallLT' ... exact`: 
local instance decidableBallLT' :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, _, _ => isTrue fun _ => (by cases ·)
| (n+1), P, H => by
  cases decidableBallLT' n (P · <| Nat.le_succ_of_le ·) with
  | isFalse h => exact isFalse (h fun _ _ => · _ _)
  | isTrue h =>
    exact match H n Nat.le.refl with
    | isFalse p => isFalse (p <| · _ _)
    | isTrue p => isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)

-- still fast:
example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by native_decide

-- fails with (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached
example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide

end fails_with_timeout
@kim-em kim-em added the RFC Request for comments label Sep 17, 2023
@b-mehta
Copy link
Contributor

b-mehta commented Sep 18, 2023 •
edited
Loading

Perhaps it's sensible to have a (maybe mathlib-only) linter which warns the user if they are using certain tactics to build data - I suspect similar instances of this have been caused by mathport porting lean 3 cases.

Also, adding credit for @ericrbg who helped with the minimisation a lot.

@digama0
Copy link
Collaborator

digama0 commented Sep 18, 2023 •
edited
Loading

It is strange to me that this would be slow in the first place. Do we have an explanation for the performance issue here? cases elaborates to a use of the casesOn function, which should compute just fine in the kernel (in a decide proof).

@ericrbg ericrbg mentioned this issue Sep 18, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this issue Sep 18, 2023
@ericrbg
fix: use match with Decidable. (#7232)
5f9ca85 
This works around leanprover/lean4#2552 - fix found by @b-mehta. I changed the `Nat` instance where the issue was found, and some `List` instances in hope it fixes mysterious slowdowns with `Finset` decidability. Any more instances changed would probably be good.
@Kha
Copy link
Member

Kha commented Sep 19, 2023

With #2559:

scratch.lean:52:81: error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
[Elab.command] [0.187339s] example : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide
  [Elab.step] [0.150821s] decide
    [Elab.step] [0.150808s] decide
      [Elab.step] [0.150796s] decide
        [Meta.whnf] [0.148372s] 💥 Decidable.casesOn (decidableBallLT' 9 fun a a_1 => ∀ (b : Nat), b < 9 → ∀ (c : Nat), c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7) [...]
          [Meta.whnf] [0.148358s] 💥 Decidable.rec (fun h => (fun x => false) h) (fun h => (fun x => true) h) [...]
            [Meta.whnf] [0.148238s] 💥 Decidable.casesOn (motive := fun t => [...]
              [Meta.whnf] [0.148233s] 💥 Decidable.rec (motive := fun t => [...]
                [Meta.whnf] [0.148185s] 💥 Decidable.casesOn (motive := fun t => [...]
                  [Meta.whnf] [0.148181s] 💥 Decidable.rec (motive := fun t => [...]
                    [Meta.whnf] [0.148135s] 💥 Decidable.casesOn (motive := fun t => [...]
                      [Meta.whnf] [0.148131s] 💥 Decidable.rec (motive := fun t => [...]
                        [Meta.whnf] [0.148090s] 💥 Decidable.casesOn (motive := fun t => [...]
                          [Meta.whnf] [0.148086s] 💥 Decidable.rec (motive := fun t => [...]
                            [Meta.whnf] [0.148046s] 💥 Decidable.casesOn (motive := fun t => [...]
                              [Meta.whnf] [0.148042s] 💥 Decidable.rec (motive := fun t => [...]
                                [Meta.whnf] [0.148001s] 💥 Decidable.casesOn (motive := fun t => [...]
                                  [Meta.whnf] [0.147997s] 💥 Decidable.rec (motive := fun t => [...]
                                    [Meta.whnf] [0.147954s] 💥 Decidable.casesOn (motive := fun t => [...]
                                      [Meta.whnf] [0.147950s] 💥 Decidable.rec (motive := fun t => [...]
                                        [Meta.whnf] [0.147910s] 💥 Decidable.casesOn (motive := fun t => [...]
                                          [Meta.whnf] [0.147906s] 💥 Decidable.rec (motive := fun t => [...]
                                            [Meta.whnf] [0.147866s] 💥 Decidable.casesOn (motive := fun t => [...]
                                              [Meta.whnf] [0.147862s] 💥 Decidable.rec (motive := fun t => [...]
                                                [Meta.whnf] [0.147829s] 💥 (fun p motive isFalse isTrue h => isTrue h) [...]
                                                  [Meta.whnf] [0.147827s] 💥 (fun h => [...]
                                                    [Meta.whnf] [0.147825s] 💥 (fun h h_1 => [...]
                                                      [Meta.whnf] [0.147823s] 💥 _ ▸ [...]
                                                        [Meta.whnf] [0.147801s] 💥 _ ▸ [...]
                                                          [Meta.whnf] [0.147467s] 💥 (fun {α} a motive refl => refl) (isTrue _) [...]
                                                            [Meta.whnf] [0.147465s] 💥 match [...]
                                                              [Meta.whnf] [0.147420s] 💥 (fun n P motive x h_1 h_2 => Decidable.casesOn x (fun h => h_1 h) fun h => h_2 h) 0 [...]
                                                                [Meta.whnf] [0.147417s] 💥 Decidable.casesOn [...]
                                                                  [Meta.whnf] [0.147411s] 💥 Decidable.rec (fun h => (fun h => h_1 h) h) (fun h => (fun h => h_2 h) h) [...]
                                                                    [Meta.whnf] [0.147324s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                      [Meta.whnf] [0.147320s] 💥 Decidable.rec (motive := fun t => [...]
                                                                        [Meta.whnf] [0.147275s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                          [Meta.whnf] [0.147271s] 💥 Decidable.rec (motive := fun t => [...]
                                                                            [Meta.whnf] [0.147230s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                              [Meta.whnf] [0.147226s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                [Meta.whnf] [0.147187s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                  [Meta.whnf] [0.147183s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                    [Meta.whnf] [0.147144s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                      [Meta.whnf] [0.147140s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                        [Meta.whnf] [0.147101s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                          [Meta.whnf] [0.147097s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                            [Meta.whnf] [0.147058s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                              [Meta.whnf] [0.147054s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                [Meta.whnf] [0.147014s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                  [Meta.whnf] [0.147011s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                    [Meta.whnf] [0.146969s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                      [Meta.whnf] [0.146965s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                        [Meta.whnf] [0.146931s] 💥 (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                          [Meta.whnf] [0.146929s] 💥 (fun h => [...]
                                                                                                            [Meta.whnf] [0.146928s] 💥 (fun h h_3 => [...]
                                                                                                              [Meta.whnf] [0.146926s] 💥 _ ▸ [...]
                                                                                                                [Meta.whnf] [0.146921s] 💥 _ ▸ [...]
                                                                                                                  [Meta.whnf] [0.146604s] 💥 (fun {α} a motive refl => refl) (isTrue _) [...]
                                                                                                                    [Meta.whnf] [0.146602s] 💥 match [...]
                                                                                                                      [Meta.whnf] [0.146588s] 💥 (fun n P motive x h_1 h_2 => Decidable.casesOn x (fun h => h_1 h) fun h => h_2 h) 0 [...]
                                                                                                                        [Meta.whnf] [0.146585s] 💥 Decidable.casesOn [...]
                                                                                                                          [Meta.whnf] [0.146580s] 💥 Decidable.rec (fun h => (fun h => h_1 h) h) (fun h => (fun h => h_2 h) h) [...]
                                                                                                                            [Meta.whnf] [0.146494s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                              [Meta.whnf] [0.146490s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                                                [Meta.whnf] [0.146448s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                                  [Meta.whnf] [0.146444s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                                                    [Meta.whnf] [0.109100s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                      [Meta.whnf] [0.109095s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                        [Meta.whnf] [0.053888s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                          [Meta.whnf] [0.053884s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                            [Meta.whnf] [0.026602s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                              [Meta.whnf] [0.026598s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                [Meta.whnf] [0.012938s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                  [Meta.whnf] [0.012931s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                [Meta.whnf] [0.013614s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                  [Meta.whnf] [0.013613s] ✅ (fun h => [...]
                                                                                                                                                    [Meta.whnf] [0.013611s] ✅ (fun h h_3 => [...]
                                                                                                                                                      [Meta.whnf] [0.013609s] ✅ _ ▸ [...]
                                                                                                                                                        [Meta.whnf] [0.013603s] ✅ _ ▸ [...]
                                                                                                                                                          [Meta.isDefEq] [0.012996s] ✅ isTrue _ = [...] =?= isTrue _ = isTrue _
                                                                                                                                                            [Meta.isDefEq] [0.012979s] ✅ decidableBallLT' 4 fun x x_1 => [...] =?= isTrue _
                                                                                                                                                              [Meta.isDefEq] [0.012924s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                [Meta.whnf] [0.012766s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                  [Meta.whnf] [0.012760s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                            [Meta.whnf] [0.027237s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                              [Meta.whnf] [0.027235s] ✅ (fun h => [...]
                                                                                                                                                [Meta.whnf] [0.027234s] ✅ (fun h h_3 => [...]
                                                                                                                                                  [Meta.whnf] [0.027231s] ✅ _ ▸ [...]
                                                                                                                                                    [Meta.whnf] [0.027225s] ✅ _ ▸ [...]
                                                                                                                                                      [Meta.isDefEq] [0.026619s] ✅ isTrue _ = [...] =?= isTrue _ = isTrue _
                                                                                                                                                        [Meta.isDefEq] [0.026602s] ✅ decidableBallLT' 5 fun x x_1 => (fun x x_2 => (fun x x_3 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _) x _ =?= isTrue _
                                                                                                                                                          [Meta.isDefEq] [0.026547s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                            [Meta.whnf] [0.026390s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                              [Meta.whnf] [0.026385s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.012739s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                  [Meta.whnf] [0.012733s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.013599s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                                  [Meta.whnf] [0.013597s] ✅ (fun h => [...]
                                                                                                                                                                    [Meta.whnf] [0.013596s] ✅ (fun h h_3 => [...]
                                                                                                                                                                      [Meta.whnf] [0.013594s] ✅ _ ▸ [...]
                                                                                                                                                                        [Meta.whnf] [0.013588s] ✅ _ ▸ [...]
                                                                                                                                                                          [Meta.isDefEq] [0.012983s] ✅ isTrue _ = [...] =?= isTrue _ = isTrue _
                                                                                                                                                                            [Meta.isDefEq] [0.012961s] ✅ decidableBallLT' 4 fun x x_1 => (fun x x_2 => (fun x x_3 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _) x _ =?= isTrue _
                                                                                                                                                                              [Meta.isDefEq] [0.012907s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                                [Meta.whnf] [0.012753s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                  [Meta.whnf] [0.012746s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                        [Meta.whnf] [0.055160s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                          [Meta.whnf] [0.055158s] ✅ (fun h => [...]
                                                                                                                                            [Meta.whnf] [0.055157s] ✅ (fun h h_3 => [...]
                                                                                                                                              [Meta.whnf] [0.055154s] ✅ _ ▸ [...]
                                                                                                                                                [Meta.whnf] [0.055148s] ✅ _ ▸ [...]
                                                                                                                                                  [Meta.isDefEq] [0.054532s] ✅ isTrue _ = decidableBallLT' 6 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _ = isTrue _
                                                                                                                                                    [Meta.isDefEq] [0.054516s] ✅ decidableBallLT' 6 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _
                                                                                                                                                      [Meta.isDefEq] [0.054460s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                        [Meta.whnf] [0.054303s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                          [Meta.whnf] [0.054298s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                            [Meta.whnf] [0.026292s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                              [Meta.whnf] [0.026288s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.012794s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                  [Meta.whnf] [0.012788s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.013449s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                                  [Meta.whnf] [0.013448s] ✅ (fun h => [...]
                                                                                                                                                                    [Meta.whnf] [0.013446s] ✅ (fun h h_3 => [...]
                                                                                                                                                                      [Meta.whnf] [0.013444s] ✅ _ ▸ [...]
                                                                                                                                                                        [Meta.whnf] [0.013438s] ✅ _ ▸ [...]
                                                                                                                                                                          [Meta.isDefEq] [0.012849s] ✅ isTrue _ = [...] =?= isTrue _ = isTrue _
                                                                                                                                                                            [Meta.isDefEq] [0.012833s] ✅ decidableBallLT' 4 fun x x_1 => (fun x x_2 => (fun x x_3 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _) x _ =?= isTrue _
                                                                                                                                                                              [Meta.isDefEq] [0.012778s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                                [Meta.whnf] [0.012624s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                  [Meta.whnf] [0.012618s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                            [Meta.whnf] [0.027958s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                              [Meta.whnf] [0.027956s] ✅ (fun h => [...]
                                                                                                                                                                [Meta.whnf] [0.027955s] ✅ (fun h h_3 => [...]
                                                                                                                                                                  [Meta.whnf] [0.027952s] ✅ _ ▸ [...]
                                                                                                                                                                    [Meta.whnf] [0.027946s] ✅ _ ▸ [...]
                                                                                                                                                                      [Meta.isDefEq] [0.027357s] ✅ isTrue _ = decidableBallLT' 5 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _ = isTrue _
                                                                                                                                                                        [Meta.isDefEq] [0.027341s] ✅ decidableBallLT' 5 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _
                                                                                                                                                                          [Meta.isDefEq] [0.027285s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                            [Meta.whnf] [0.027134s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                              [Meta.whnf] [0.027129s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                                [Meta.whnf] [0.012755s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                  [Meta.whnf] [0.012749s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                                [Meta.whnf] [0.014326s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                                                  [Meta.whnf] [0.014324s] ✅ (fun h => [...]
                                                                                                                                                                                    [Meta.whnf] [0.014323s] ✅ (fun h h_3 => [...]
                                                                                                                                                                                      [Meta.whnf] [0.014320s] ✅ _ ▸ [...]
                                                                                                                                                                                        [Meta.whnf] [0.014314s] ✅ _ ▸ [...]
                                                                                                                                                                                          [Meta.isDefEq] [0.013718s] ✅ isTrue _ = decidableBallLT' 4 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _ = isTrue _
                                                                                                                                                                                            [Meta.isDefEq] [0.013702s] ✅ decidableBallLT' 4 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _
                                                                                                                                                                                              [Meta.isDefEq] [0.013646s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                                                [Meta.whnf] [0.013495s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                                  [Meta.whnf] [0.013489s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                    [Meta.whnf] [0.037216s] 💥 (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                      [Meta.whnf] [0.037214s] 💥 (fun h => [...]
                                                                                                                                        [Meta.whnf] [0.037213s] 💥 (fun h h_3 => [...]
                                                                                                                                          [Meta.whnf] [0.037210s] 💥 _ ▸ [...]
                                                                                                                                            [Meta.whnf] [0.037205s] 💥 _ ▸ [...]
                                                                                                                                              [Meta.isDefEq] [0.037167s] 💥 isTrue _ = decidableBallLT' 7 fun x x_1 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _ =?= isTrue _ = isTrue _
                                                                                                                                                [Meta.isDefEq] [0.037154s] 💥 decidableBallLT' 7 fun x x_1 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _ =?= isTrue _
                                                                                                                                                  [Meta.isDefEq] [0.037098s] 💥 Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                    [Meta.whnf] [0.037092s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                      [Meta.whnf] [0.037087s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                                                                        [Meta.whnf] [0.037041s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                          [Meta.whnf] [0.037037s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                                                                            [Meta.whnf] [0.026255s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                              [Meta.whnf] [0.026251s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.012711s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                  [Meta.whnf] [0.012705s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                                [Meta.whnf] [0.013497s] ✅ (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                                  [Meta.whnf] [0.013495s] ✅ (fun h => [...]
                                                                                                                                                                    [Meta.whnf] [0.013494s] ✅ (fun h h_3 => [...]
                                                                                                                                                                      [Meta.whnf] [0.013491s] ✅ _ ▸ [...]
                                                                                                                                                                        [Meta.whnf] [0.013485s] ✅ _ ▸ [...]
                                                                                                                                                                          [Meta.isDefEq] [0.012897s] ✅ isTrue _ = [...] =?= isTrue _ = isTrue _
                                                                                                                                                                            [Meta.isDefEq] [0.012881s] ✅ decidableBallLT' 4 fun x x_1 => (fun x x_2 => (fun x x_3 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _) x _ =?= isTrue _
                                                                                                                                                                              [Meta.isDefEq] [0.012826s] ✅ Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                                [Meta.whnf] [0.012672s] ✅ Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                  [Meta.whnf] [0.012665s] ✅ Decidable.rec (motive := fun t => [...]
                                                                                                                                                            [Meta.whnf] [0.010737s] 💥 (fun p motive isFalse isTrue h => isTrue h) [...]
                                                                                                                                                              [Meta.whnf] [0.010735s] 💥 (fun h => [...]
                                                                                                                                                                [Meta.whnf] [0.010734s] 💥 (fun h h_3 => [...]
                                                                                                                                                                  [Meta.whnf] [0.010731s] 💥 _ ▸ [...]
                                                                                                                                                                    [Meta.whnf] [0.010726s] 💥 _ ▸ [...]
                                                                                                                                                                      [Meta.isDefEq] [0.010700s] 💥 isTrue _ = decidableBallLT' 5 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _ = isTrue _
                                                                                                                                                                        [Meta.isDefEq] [0.010683s] 💥 decidableBallLT' 5 fun x x_1 => (fun x x_2 => (fun c a => 0 ^ 2 + 0 ^ 2 + c ^ 2 ≠ 7) x _) x _ =?= isTrue _
                                                                                                                                                                          [Meta.isDefEq] [0.010628s] 💥 Decidable.casesOn (motive := fun t => [...] =?= isTrue _
                                                                                                                                                                            [Meta.whnf] [0.010622s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                              [Meta.whnf] [0.010617s] 💥 Decidable.rec (motive := fun t => [...]
                                                                                                                                                                                [Meta.whnf] [0.010573s] 💥 Decidable.casesOn (motive := fun t => [...]
                                                                                                                                                                                  [Meta.whnf] [0.010567s] 💥 Decidable.rec (motive := fun t => [...]

The terms further down don't look very nice:

[Meta.whnf] [0.144874s] 💥 Decidable.casesOn (motive := fun t =>
                                              (decidableBallLT' 1 fun x x_1 =>
                                                    (fun x x_2 =>
                                                        (fun x x_3 =>
                                                            (fun x x_4 =>
                                                                (fun x x_5 =>
                                                                    (fun x x_6 =>
                                                                        (fun x x_7 =>
                                                                            (fun x x_8 =>
                                                                                (fun a a_1 =>
                                                                                    ∀ (b : Nat),
                                                                                      b < 9 →
                                                                                        ∀ (c : Nat),
                                                                                          c < 9 →
                                                                                            a ^ 2 + b ^ 2 + c ^ 2 ≠ 7)
                                                                                  x _)
                                                                              x _)
                                                                          x _)
                                                                      x _)
                                                                  x _)
                                                              x _)
                                                          x _)
                                                      x _) =
                                                  t → ...

@Kha Kha changed the title Kernel reduction of Decidable instances very slow when using cases tactic. Reduction of Decidable instances very slow when using cases tactic. Sep 19, 2023
kodyvajjha pushed a commit to leanprover-community/mathlib4 that referenced this issue Sep 22, 2023
@ericrbg @kodyvajjha
fix: use match with Decidable. (#7232)
f5e3b7d 
This works around leanprover/lean4#2552 - fix found by @b-mehta. I changed the `Nat` instance where the issue was found, and some `List` instances in hope it fixes mysterious slowdowns with `Finset` decidability. Any more instances changed would probably be good.
@collares collares mentioned this issue Sep 23, 2023
Closed
leodemoura added a commit that referenced this issue Oct 21, 2023
@leodemoura
perf: closes #2552
90ea192
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
RFC Request for comments
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@Kha @kim-em @digama0 @b-mehta