simp[LE.le] crashes Lean server

Stream: mathlib4

[Arnav Sabharwal]

Upon applying the simp[LE.le] tactic, the Lean server crashes and an uncaught exception is raised. What could possibly cause this issue? If further context is needed, I'd be happy to provide it! Thanks!

[Wen Yang]

We always need the #mwe to reproduce the problem.

[Arnav Sabharwal]

Sure, let me know if it must be minimized further. The trouble-making section is the last-example.

/-!
# Inductive type variant of `Fin`

`Fin` is defined as a subtype of `Nat`. This file defines an equivalent type, `PFin2`, which is
defined inductively, and is universe polymorphic. This is useful for its induction principle and
different definitional equalities.


## Main declarations

* `PFin2 n`: Inductive and universe polymorphic type variant of `Fin n`. `fz` corresponds to `0` and
  `fs n` corresponds to `succ n`.
* `Fin2 n`: shorthand for `PFin2.{0} n`, i.e., it lives in `Type`
* `toNat`, `optOfNat`, `ofNat'`: Conversions to and from `Nat`. `ofNat' m` takes a proof that
  `m < n` through the class `is_lt`.
* `add k`: Takes `i : PFin2 n` to `i + k : PFin2 (n + k)`.
* `left`: Embeds `PFin2 n` into `PFin2 (n + k)`.
* `insertPerm a`: Permutation of `PFin2 n` which cycles `0, ..., a - 1` and leaves `a, ..., n - 1`
  unchanged.
* `remapLeft f`: Function `PFin2 (m + k) → PFin2 (n + k)` by applying `f : PFin2 m → PFin2 n` to
  `0, ..., m - 1` and sending `m + i` to `n + i`.
-/


open Nat

universe u



/-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
inductive PFin2 : Nat → Type u
  | /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
  fz {n} : PFin2 (succ n)
  | /-- `n` as a member of `fin (succ n)` -/
  fs {n} : PFin2 n → PFin2 (succ n)
  deriving DecidableEq

namespace PFin2

/-- Define a dependent function on `PFin2 (succ n)` by giving its value at
zero (`H1`) and by giving a dependent function on the rest (`H2`). -/
-- @[elab_as_eliminator]
protected def cases' {n} {C : PFin2 (succ n) → Sort u} (H1 : C fz) (H2 : ∀ n, C (fs n)) : ∀ i : PFin2 (succ n), C i
  | fz => H1
  | fs n => H2 n

/-- Ex falso. The dependent eliminator for the empty `PFin2 0` type. -/
def elim0 {C : PFin2 0 → Sort u} : ∀ i : PFin2 0, C i :=
  by intro i; cases i

/-- Converts a `PFin2` into a natural. -/
def toNat : ∀ {n}, PFin2 n → Nat
  | _, @fz _ => 0
  | _, @fs _ i => succ (toNat i)

/-
  ## LT / LE
-/
instance instOrd (n : Nat) : Ord (PFin2 n) where
  compare := (compare ·.toNat ·.toNat)

instance instLT {n : Nat} : LT (PFin2 n) := ⟨(Nat.lt ·.toNat ·.toNat)⟩
instance instLE {n : Nat} : LE (PFin2 n) := ⟨(Nat.le ·.toNat ·.toNat)⟩

instance decidable_lt (n : Nat) : DecidableRel (@LT.lt (PFin2 n) instLT) := fun a b =>
    let d : Decidable (a.toNat < b.toNat) := by infer_instance
    match d with
    | isTrue h  => isTrue  $ by assumption
    | isFalse h => isFalse $ by intro a_lt_b; apply h a_lt_b

instance decidable_le {n : Nat} : DecidableRel (@LE.le (PFin2 n) instLE) := fun a b =>
    let d : Decidable (a.toNat ≤ b.toNat) := by infer_instance
    match d with
    | isTrue h  => isTrue  $ by assumption
    | isFalse h => isFalse $ by intro a_le_b; apply h a_le_b

example (n : ℕ) (a : PFin2 n) (b : PFin2 n) :
a < b ↔ a ≤ b ∧ ¬(b ≤ a) :=
by
simp[LT.lt]

[Wen Yang]

Don't forget to add import Mathlib at the beginning of your example. I can reproduce your problem now. However, I don't know why simp [LT.lt] raises error.

[Johan Commelin]

Since LT on Nat is implemented using recursion, you are generating very deeply nested match expression by calling that simp, until Lean bails out.

Here is the "standard" way to solve it:

theorem lt_def {n : Nat} (a b : PFin2 n) : a < b ↔ a.toNat < b.toNat := Iff.rfl
theorem le_def {n : Nat} (a b : PFin2 n) : a ≤ b ↔ a.toNat ≤ b.toNat := Iff.rfl

example (n : Nat) (a : PFin2 n) (b : PFin2 n) :
    a < b ↔ a ≤ b ∧ ¬(b ≤ a) := by
  rw [lt_def, le_def, le_def, Nat.lt_iff_le_not_le]

[Kim Morrison]

We would like to have more helpful behaviour in these cases, so if you have the energy to make a no-imports-at-all #mwe demonstrating this, and issue would be welcome.

[Junyan Xu]

The code does work in the web editor without imports.

[Arnav Sabharwal]

Scott Morrison said:

We would like to have more helpful behaviour in these cases, so if you have the energy to make a no-imports-at-all #mwe demonstrating this, and issue would be welcome.

Sure! However, I'm a bit confused by what you mean by "no-imports-at-all". Could you please clarify? Thanks!

[Ruben Van de Velde]

There should be no import statements in the file; it should stand entirely in its own

[Arnav Sabharwal]

Junyan Xu said:

The code does work in the web editor without imports.

That's very interesting, the following no-imports version fails for me in the web-editor:

open Nat

/-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
inductive PFin2 : Nat → Type u
  | /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
  fz {n} : PFin2 (succ n)
  | /-- `n` as a member of `fin (succ n)` -/
  fs {n} : PFin2 n → PFin2 (succ n)
  deriving DecidableEq

namespace PFin2

/-- Converts a `PFin2` into a natural. -/
def toNat : ∀ {n}, PFin2 n → Nat
  | _, @fz _ => 0
  | _, @fs _ i => succ (toNat i)

instance instLT {n : Nat} : LT (PFin2 n) := ⟨(Nat.lt ·.toNat ·.toNat)⟩
instance instLE {n : Nat} : LE (PFin2 n) := ⟨(Nat.le ·.toNat ·.toNat)⟩

-- Uncommenting causes session to crash
-- example (n : Nat) (a : PFin2 n) (b : PFin2 n) :
-- a < b ↔ a ≤ b ∧ ¬(b ≤ a) :=
-- by
-- simp[LE.le];

end PFin2

Could you kindly share what you did differently that caused it to work with LE.le without imports? Thanks!