Unexpected Editor Crash

Stream: lean4

[Kaiyu Yang]

Hi,

My Lean editor crashes when running the following code:

import Mathlib.Tactic

variable {α : Type u} {a b : Nat}

-- A sequence of α with index in [a, b]
-- Empty sequence if b < a
def Sequence (α : Type u) (a b : Nat) :=
  { arr : Array α // arr.size = max 0 (b - a + 1) }


def Sequence.get (s : Sequence α a b) (i : Nat) (h : a ≤ i ∧ i ≤ b) : α :=
  s.1.get ⟨i - a, by
    simp [s.2]
    match h with
    | ⟨h₁, h₂⟩ =>
      have hab : a ≤ b := by linarith
      have : i - a ≤ b - a := by simp [*]
      linarith
  ⟩


instance : GetElem (Sequence α a b) ℕ α (fun _ i => a ≤ i ∧ i ≤ b) where
  getElem := fun s i h => s.get i h

def s : Sequence ℕ 2 4 := ⟨#[1, 2, 3], rfl⟩
#eval s[5]

However, after removing variable {α : Type u} {a b : Nat}, the code can run with the expected result below:
image.png

I'm wondering if variable {α : Type u} {a b : Nat} makes any difference here. Thanks!

[Kaiyu Yang]

The issue can be reproduced on https://live.lean-lang.org/

[Kim Morrison]

It looks like this example might be easy to remove Mathlib from (which is pretty much a pre-requisite for getting bugs diagnosed / fixed). Does the same behaviour show after replacing the Mathlib tactics by sorry (and replacing ℕ with Nat)?

[Kaiyu Yang]

Removing mathlib doesn't help. Below is a MWE:

def Sequence (α : Type u) (a b : Nat) :=
  { arr : Array α // arr.size = max 0 (b - a + 1) }


def Sequence.get (s : Sequence α a b) (i : Nat) (h : a ≤ i ∧ i ≤ b) : α :=
  s.1.get ⟨i - a, by sorry⟩


instance : GetElem (Sequence α a b) Nat α (fun _ i => a ≤ i ∧ i ≤ b) where
  getElem := fun s i h => s.get i h

def s : Sequence Nat 2 4 := ⟨#[1, 2, 3], rfl⟩
#eval s[5]

Now it crashes w/ or w/o variable {α : Type u} {a b : Nat}.

[Kim Morrison]

That's great -- I wasn't expecting that removing mathlib would help, rather that now this makes a great issue to report on the lean4 repo. :-)

[Mauricio Collares]

Is this lean4#2252 (i.e., lean4#1697)?

[Kim Morrison]

Seems likely!