unfold triggers infinite loop

Stream: lean4

[Alex Keizer]

In the following MWE, uncommenting the unfold seems to trigger an infinite loop, burning 100% of my CPU without being caught by maxHeartBeats.

inductive Ty
  | nat

def Ctxt : Type :=
  List Ty


def Ctxt.Var (Γ : Ctxt) (t : Ty) : Type :=
  { i : Nat // Γ.get? i = some t }


def matchVar {t : Ty} : {Δ : Ctxt} → Δ.Var t → Option Bool
  | _::Δ, ⟨w+1, h⟩ => -- w† = Var.toSnoc w
      let w : Ctxt.Var Δ t := ⟨w, by simp_all[List.get?]⟩
      matchVar w
  | _, _ =>
      none


example {Δ : Ctxt } {w : Δ.Var t} :
  matchVar w = none
    := by
        -- uncommenting the `unfold` triggers an infinite loop of sorts,
        -- consuming 100% CPU without being caught by `maxHeartbeats` timeout
        -- unfold matchVar
        sorry

Running under gdb, we find that we are in:

#6203 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6204 0x00007fc263bda95d in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6205 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6206 0x00007fc263bda95d in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6207 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6208 0x00007fc263bda95d in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6209 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6210 0x00007fc263bda95d in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6211 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6212 0x00007fc263bda95d in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop () from /home/grosser/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/../lib/lean/libleanshared.so
#6213 0x00007fc263bd9f24 in l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___lambda__2 ()

Which seems to correspond to:

  proveSubgoalLoop (mvarId : MVarId) : MetaM Unit := do
    trace[Meta.Match.matchEqs] "proveSubgoalLoop\n{mvarId}"
    match (← injectionAny mvarId) with
    | InjectionAnyResult.solved => return ()
    | InjectionAnyResult.failed =>
      let mvarId' ← substVars mvarId
      if mvarId' == mvarId then
        if (← mvarId.contradictionCore {}) then
          return ()
        throwError "failed to generate splitter for match auxiliary declaration '{matchDeclName}', unsolved subgoal:\n{MessageData.ofGoal mvarId}"
      else
        proveSubgoalLoop mvarId'
    | InjectionAnyResult.subgoal mvarId => proveSubgoalLoop mvarId

  proveSubgoal (mvarId : MVarId) : MetaM Unit := do
    trace[Meta.Match.matchEqs] "subgoal {mkMVar mvarId}, {repr (← mvarId.getDecl).kind}, {← mvarId.isAssigned}\n{MessageData.ofGoal mvarId}"
    let (_, mvarId) ← mvarId.intros
    let mvarId ← mvarId.tryClearMany (alts.map (·.fvarId!))
    proveSubgoalLoop mvarId

My original code threw a failed to generate splitter for match auxiliary declaration error, instead of the infinite looping behaviour; this code suggests that the two problems are related.

Does anybody have any idea of what triggered this, and how to circumvent it?

[Alex Keizer]

Aha, explicitly spelling out the second case seems to work!

inductive Ty
  | nat

def Ctxt : Type :=
  List Ty


def Ctxt.Var (Γ : Ctxt) (t : Ty) : Type :=
  { i : Nat // Γ.get? i = some t }


def matchVar {t : Ty} : {Δ : Ctxt} → Δ.Var t → Option Bool
  | _::Δ, ⟨w+1, h⟩ => -- w† = Var.toSnoc w
      let w : Ctxt.Var Δ t := ⟨w, by simp_all[List.get?]⟩
      matchVar w
  | _, ⟨0, _⟩ =>
      none


example {Δ : Ctxt } {w : Δ.Var t} :
  matchVar w = none
    := by
        unfold matchVar -- Yay, it works
        sorry

[Alex Keizer]

This insight did not help to solve the original error I was seeing, here is another attempt at an MWE. This one depends on Mathlib and does showcase the exact error I'm having trouble with.

import Mathlib.Data.Erased

inductive Ty
  | nat

def Ctxt : Type :=
  Erased <| List Ty

noncomputable def Ctxt.snoc (Γ : Ctxt) (t : Ty) : Ctxt :=
  Erased.mk <| t :: Γ.out

def Ctxt.Var (Γ : Ctxt) (t : Ty) : Type :=
  { i : Nat // Γ.out.get? i = some t }

inductive CtxtProp : Ctxt → Type
  | nil : CtxtProp (Erased.mk [])
  | snoc : CtxtProp Δ → CtxtProp (Δ.snoc t)


noncomputable def matchVar {t : Ty} {Δ : Ctxt} : CtxtProp Δ → Δ.Var t → Option Bool
  | .snoc d, ⟨w+1, h⟩ => -- w† = Var.toSnoc w
      let w : Ctxt.Var _ t := ⟨w, by simp_all[List.get?, Ctxt.snoc]⟩
      matchVar d w
  -- Neither spelling out all cases, nor having a single fallback case work
  | .snoc _, ⟨0, _⟩ | .nil, ⟨0, _⟩ | .nil, ⟨_+1, h⟩ => none
  -- | _, _ => none


example {Δ : Ctxt} (d : CtxtProp Δ) {w : Δ.Var t} :
  matchVar d w = none
    := by
        unfold matchVar /- throws error:
          failed to generate splitter for match auxiliary declaration 'matchVar.match_1', unsolved subgoal:
            case x
            t: Ty
            motive: (Δ : Ctxt) → CtxtProp Δ → Ctxt.Var Δ t → Sort u_1
            h_1: (Γ : Ctxt) →
              (t_2 : Ty) →
                (d : CtxtProp Γ) →
                  (w : ℕ) →
                    (h : List.get? (Erased.out (Ctxt.snoc Γ t_2)) (w + 1) = some t) →
                      motive (Ctxt.snoc Γ t_2) (CtxtProp.snoc d) { val := Nat.succ w, property := h }
            h_2: (Γ : Ctxt) →
              (t_2 : Ty) →
                (a : CtxtProp Γ) →
                  (property : List.get? (Erased.out (Ctxt.snoc Γ t_2)) 0 = some t) →
                    (∀ (Γ_1 : Ctxt) (t_1 : Ty) (d : CtxtProp Γ_1) (w : ℕ)
                        (h : List.get? (Erased.out (Ctxt.snoc Γ_1 t_1)) (w + 1) = some t),
                        ((fun b => t_2 :: Erased.out Γ = b) = fun b => t_1 :: Erased.out Γ_1 = b) →
                          HEq (_ : ∃ a, (fun b => a = b) = fun b => t_2 :: Erased.out Γ = b)
                              (_ : ∃ a, (fun b => a = b) = fun b => t_1 :: Erased.out Γ_1 = b) →
                            HEq (CtxtProp.snoc a) (CtxtProp.snoc d) →
                              HEq { val := 0, property := property } { val := Nat.succ w, property := h } → False) →
                      motive (Ctxt.snoc Γ t_2) (CtxtProp.snoc a) { val := 0, property := property }
            h_3: (property : List.get? (Erased.out (Erased.mk [])) 0 = some t) →
              motive (Erased.mk []) CtxtProp.nil { val := 0, property := property }
            h_4: (n : ℕ) →
              (h : List.get? (Erased.out (Erased.mk [])) (n + 1) = some t) →
                motive (Erased.mk []) CtxtProp.nil { val := Nat.succ n, property := h }
            Δ✝: Ctxt
            t✝: Ty
            a✝: CtxtProp Δ✝
            x✝²: Ctxt.Var (Ctxt.snoc Δ✝ t✝) t
            val✝: ℕ
            property✝¹: List.get? (Erased.out (Ctxt.snoc Δ✝ t✝)) val✝ = some t
            property✝: List.get? (Erased.out (Ctxt.snoc Δ✝ t✝)) Nat.zero = some t
            Γ: Ctxt
            t_1: Ty
            d: CtxtProp Γ
            w: ℕ
            h: List.get? (Erased.out (Ctxt.snoc Γ t_1)) (w + 1) = some t
            fst_eq: (fun b => t✝ :: Erased.out Δ✝ = b) = fun b => t_1 :: Erased.out Γ = b
            snd_eq: HEq (_ : ∃ a, (fun b => a = b) = fun b => t✝ :: Erased.out Δ✝ = b)
              (_ : ∃ a, (fun b => a = b) = fun b => t_1 :: Erased.out Γ = b)
            x_1: HEq (CtxtProp.snoc a✝) (CtxtProp.snoc d)
            x_2: HEq { val := 0, property := property✝ } { val := Nat.succ w, property := h }
            x✝¹: CtxtProp (Ctxt.snoc Δ✝ t✝)
            x✝: Ctxt.Var (Ctxt.snoc Δ✝ t✝) t
            ⊢ False
        -/
        sorry

[Alex Keizer]

Tracing with trace.Meta.Match.matchEqs tells us Lean is repeatedly trying to apply injective to the fst_eq hypothesis of that goal, which fails because it's not an injective type.

Is there some attribute I can use to add a custom injectivity theorem for the injective tactic to use?