match reduction is slow

[kbuzzard]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Another instance where decide is surprisingly slow and native_decide is quick.

Context

Zulip discussion here.

Steps to Reproduce

The following code creates two defeq lists parts and parts2 and then loops through them; for some reason the parts loop is very slow with decide, but quick with native_decide.

section decidability_instances

variable {α : Type} {p : α → Prop} [DecidablePred p]

instance decidableBex : ∀ (l : List α), Decidable (∃ x, x ∈ l → p x)
  | []    => isFalse sorry
  | x::xs =>
    match ‹DecidablePred p› x with
    | isTrue h₁ => isTrue sorry
    | isFalse h₁ => match decidableBex xs with
      | isTrue h₂  => isTrue <| by sorry
      | isFalse h₂ => isFalse <| by sorry

instance decidableBall (l : List α) : Decidable (∀ x, x ∈ l → p x) :=
  match (inferInstance : Decidable <| ∃ x, x ∈ l → ¬ p x) with
  | isFalse h => isTrue $ fun x hx => match ‹DecidablePred p› x with
    | isTrue h' => h'
    | isFalse h' => False.elim $ h sorry
  | isTrue h => isFalse <| sorry

end decidability_instances

@[inline] protected def List.insert {α : Type} [DecidableEq α] (a : α) (l : List α) : List α :=
  if a ∈ l then l else a :: l

def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0, 1, 1]) <|
  List.insert ([1, 0, 0, 1]) <| List.insert ([1, 1, 1, 0]) <| List.insert ([1, 0, 0, 0]) <|
  List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] []

def parts2 : List (List Nat) :=
  [[1, 1, 0, 0], [0, 0, 1, 1], [1, 0, 0, 1], [1, 1, 1, 0], [1, 0, 0, 0], [1, 2, 3, 4], [5, 6, 7, 8]]

-- quick
example : parts = parts2 := rfl

-- quick
example : ∀ (x) (_ : x ∈ parts2) (y) (_ : y ∈ parts2), x ++ y ∉ parts2 := by decide

-- quick
example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by native_decide

-- slow
set_option maxHeartbeats 600000 in -- needed
example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by decide

Expected behavior: Hoped behaviour: the last by decide is quick.

Actual behavior: The last example needs a heartbeats bump.

Versions

4.1.0-rc1 and earlier versions.

Impact

People doing additive combinatorics like Bhavik Mehta run into things like this when formalising research level mathematics. Additive combinatorics is a very successful topic for Lean; both Bhavik and Yael Dillies have nearly finished formalising big new papers that came out within the last year and were featured in Quanta. Both of them are still working in Lean 3, because dec_trivial solves the goal quickly in Lean 3. Note that in the actual applications there are finsets not lists, and insert is the usual constructor for finsets. It is important to get these people upgrading to Lean 4, which is why I took the time to minimise the issue.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

Preliminary hypothesis: insufficient caching during matcher reduction leads to exponential behavior. This would explain why kernel reduction is much faster, which does not have a matcher special case.