decide regression

Stream: lean4

[Kevin Buzzard]

The following came up on the Discord. In Lean 3 this is just a second or two:

import data.nat.basic

example : ∀ a < 9, ∀ b < 9, ∀ c < 9,  a^2 + b^2 + c^2 ≠ 7 := dec_trivial

Copying the relevant instances over to core Lean 4 we get

@[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

instance decidableBallLT :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, P, _ => isTrue fun n h => by cases h
| (n+1), P, H => by
  cases decidableBallLT n fun k h => P k (Nat.le_succ_of_le h) with
  | isFalse h => refine isFalse (mt ?_ h)
                 intro hn k h
                 apply hn
  | isTrue h => refine Decidable.byCases (p := (P n n.lt_succ_self)) (fun p ↦ ?_) (fun p ↦ ?_)
                · exact
                    isTrue fun k h' =>
                      (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) fun e =>
                        match k, e, h' with
                        | _, rfl, _ => p
                · exact isFalse (mt (fun hn => hn _ _) p)

theorem test : ∀ a, a < 9 → ∀ b, b < 9 → ∀ c, c < 9 → a ^ 2 + b ^ 2 + c ^ 2 ≠ 7 := by decide

which pauses for a good few seconds and then times out. This came up in the context of discussing how to prove various bounds for Waring's problem (the number of powers you need to express every number as a sum of powers). Increasing timeout just makes the pause longer -- I've never seen this succeed in Lean 4.

[Henrik Böving]

This seems to be an issue with the kernel reduction engine to me, if you run with native_decide it finishes instantly.

[Kevin Buzzard]

Bhavik says that this fixes it but I'm just off to bed so can't check

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)

[Bhavik Mehta]

Yes, this restores decide to be just as fast as in Lean 3 - the key difference is the first match, which was previously a by cases

[Bhavik Mehta]

In particular,

instance decidableBallLT :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, P, _ => isTrue sorry
| (n+1), P, H =>
  match decidableBallLT n fun k h => P k (Nat.le_succ_of_le h) with
  | isFalse h => by refine isFalse sorry
  | isTrue h => by
                refine Decidable.byCases (p := (P n n.lt_succ_self)) (fun p ↦ ?_) (fun p ↦ ?_)
                · exact isTrue sorry
                · exact isFalse sorry

makes it fast, and

instance decidableBallLT :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, P, _ => isTrue sorry
| (n+1), P, H => by
  cases decidableBallLT n fun k h => P k (Nat.le_succ_of_le h) with
  | isFalse h => refine isFalse sorry
  | isTrue h => refine Decidable.byCases (p := (P n n.lt_succ_self)) (fun p ↦ ?_) (fun p ↦ ?_)
                · exact isTrue sorry
                · exact isFalse sorry

makes it slow

[Bhavik Mehta]

Note this is one of many regressions I've observed with decide - there are a good number of things that dec_trivial can do in Lean 3, but decide times out on in Lean 4, and my understanding is that the kernel reduction engine is very similar in both.

[Scott Morrison]

Thanks for the nice minimisation. I've recorded this at lean4#2552.

[Kevin Buzzard]

Thanks! Credit to @Eric Rodriguez too who did the minimisation

[Eric Rodriguez]

#7232 works around this, in Mathlib. I'm curious if it also fixes some mysterious slowdowns with Finset that were reported elsewhere.

[Eric Rodriguez]

OK, so a third one:

instance decidableBallLT :
  ∀ (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Decidable (P n h)], Decidable (∀ n h, P n h)
| 0, P, _ => isTrue sorry
| (n+1), P, H => by
  cases decidableBallLT n fun k h => P k (Nat.le_succ_of_le h) with
  | isFalse h => refine isFalse sorry
  | isTrue h => exact if (P n n.lt_succ_self) then isTrue sorry else isFalse sorry

is in between the two, but certainly slower than the match version. This may be relevant for other instances; for example, I was trying to debug https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.20insertion.20slowdown, and in that case key instances that are used such as docs#forall_prop_decidable use if.

[Eric Rodriguez]

There's a second issue, in that there is duplicated instances. Mathlib provides docs#List.decidableBex, docs#List.decidableBall, but Std provides (and these are currently unpatched) docs#List.decidableBEx, docs#List.decidableBAll. These are equal, so one of these (likely mathlib's) should be removed.

[Scott Morrison]

@Eric Rodriguez, your fix in #7232 goes beyond what is currently reported in lean4#2552.

lean4#2552 only demonstrates a problem with use cases.

However your 2nd and 3rd changes #7232 seems to be fixing a problem with merely using if! Is that really the case? If so, we either need a second issue for the lean4 issue tracker, or lean4#2552 updated to explain that you can't even safely use if!

[Scott Morrison]

Also, the second change in #7232 in Mathlib/Init/Data/List/Instances.lean should have a link to the issue, so it can be cleaned up later.

[Eric Rodriguez]

hmm, I seem to remember having done this for some reason but rewriting the instance with ite seems just as performant:

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 =>
  have := decidableBallLT n (P · <| Nat.le_succ_of_le ·)
  if h : (∀ (n_1 : Nat) (h : n_1 < n), P n_1 <| Nat.le_succ_of_le h)
    then have := H n Nat.le.refl
    if p : P n Nat.le.refl then isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p) else isFalse (p <| · _ _)
    else isFalse (h fun _ _ => · _ _)

this version is actually mildly faster than the match version in mathlib... (on the big example I put, it takes 179K heartbeats instead of 186K)

[Eric Rodriguez]

I will keep an eye out for the issue again but I dug through some stuff and couldn't find me talking about it. Good reason to start keeping a log of all experiments I do...

[Eric Rodriguez]

this very explicit version is faster again (174K), but I don't think it'd be worth writing this to such a ridiculous extent:

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 =>
  @dite (Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)) _ (decidableBallLT n (P · <| Nat.le_succ_of_le ·)) (fun h ↦ @dite (Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)) _ (H n Nat.le.refl) (fun p ↦ isTrue fun _ h' => (Nat.le_of_lt_succ h').lt_or_eq_dec.elim (h _) (· ▸ p)) (fun p ↦ isFalse (p <| · _ _))) (fun h ↦ isFalse (h fun _ _ => · _ _))

[Scott Morrison]

Just noting that Leo has just closed lean4#2552 via lean4#2730. If anyone has related problems still occurring, please let us know!

[Kevin Buzzard]

This is great news!