Confusing performance issues with induction

Stream: lean4

[Jad Ghalayini]

So I have two inductions; this one

theorem Term.stlc_wknth_false {t: Term} {Γ: Sparsity} {n: Nat}
: (t.wknth n).stlc (Γ.wknth n false) = t.stlc Γ
:= by {
  revert Γ n;
  induction t with
  | var v =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [stlc_var]
    simp only [Sparsity.stlc, Sparsity.wknth_ix_false, Sparsity.wknth_dep]
  | _ =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [Wk.lift_wknth_merge]
    repeat rw [Wk.liftn_wknth_merge]
    repeat rw [<-wknth_def]
    try (rename TermKind _ => k; cases k);
    try (rename AnnotSort => s; cases s);
    all_goals try rfl;
    all_goals (
      simp only [stlc]
      simp only [Sparsity.wknth_merge]
      simp only [*]
      repeat rw [Term.stlc_ty_wknth]
      try rfl
    )
}

theorem Term.stlc_wknth_true {t: Term} {Γ: Sparsity} {n: Nat}
: (t.wknth n).stlc (Γ.wknth n true) = (t.stlc Γ).wknth (Γ.ix n)
:= by {
  revert Γ n;
  induction t with
  | var v =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [stlc_var]
    simp only [Sparsity.stlc]
    split
    . have H: Γ.dep v = true := by
        rw [<-Sparsity.wknth_dep]
        assumption
      rw [Sparsity.wknth_ix_true' H]
      rw [if_pos H]
      simp only [Stlc.wknth, Stlc.wk, Wk.wknth_var]
    . rw [if_neg]
      rfl
      simp only [Sparsity.wknth_dep] at *
      assumption
  | _ =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [Wk.lift_wknth_merge]
    repeat rw [Wk.liftn_wknth_merge]
    repeat rw [<-wknth_def]
    try (rename TermKind _ => k; cases k);
    try (rename AnnotSort => s; cases s);
    all_goals try rfl;
    all_goals (
      simp only [stlc]
      simp only [Sparsity.wknth_merge]
      simp only [*]
      repeat rw [Term.stlc_ty_wknth]
      try rfl
    )
}

and directly under it in the same file, this one

theorem Term.stlc_wknth_false {t: Term} {Γ: Sparsity} {n: Nat}
: (t.wknth n).stlc (Γ.wknth n false) = t.stlc Γ
:= by {
  revert Γ n;
  induction t with
  | var v =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [stlc_var]
    simp only [Sparsity.stlc, Sparsity.wknth_ix_false, Sparsity.wknth_dep]
  | _ =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [Wk.lift_wknth_merge]
    repeat rw [Wk.liftn_wknth_merge]
    repeat rw [<-wknth_def]
    try (rename TermKind _ => k; cases k);
    try (rename AnnotSort => s; cases s);
    all_goals try rfl;
    all_goals (
      simp only [stlc]
      simp only [Sparsity.wknth_merge]
      simp only [*]
      repeat rw [Term.stlc_ty_wknth]
      try rfl
    )
}

theorem Term.stlc_wknth_true {t: Term} {Γ: Sparsity} {n: Nat}
: (t.wknth n).stlc (Γ.wknth n true) = (t.stlc Γ).wknth (Γ.ix n)
:= by {
  revert Γ n;
  induction t with
  | var v =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [stlc_var]
    simp only [Sparsity.stlc]
    split
    . have H: Γ.dep v = true := by
        rw [<-Sparsity.wknth_dep]
        assumption
      rw [Sparsity.wknth_ix_true' H]
      rw [if_pos H]
      simp only [Stlc.wknth, Stlc.wk, Wk.wknth_var]
    . rw [if_neg]
      rfl
      simp only [Sparsity.wknth_dep] at *
      assumption
  | _ =>
    intro Γ n;
    simp only [wknth, wk]
    repeat rw [Wk.lift_wknth_merge]
    repeat rw [Wk.liftn_wknth_merge]
    repeat rw [<-wknth_def]
    try (rename TermKind _ => k; cases k);
    try (rename AnnotSort => s; cases s);
    all_goals try rfl;
    all_goals (
      simp only [stlc]
      simp only [Sparsity.wknth_merge]
      simp only [*]
      repeat rw [Term.stlc_ty_wknth]
      try rfl
    )
}

In context: the wildcard tactics at the bottom of both induction are not only basically exactly the same, but produce almost exactly the same intermediate rewrites as far as I can tell. Yet the bottom induction completes in a fraction of a second, whereas the top one takes almost a minute on an i9 and eats up a whole 16 gigabytes of RAM. Any idea what gives, or how I could go about reducing this to a small test case? I had a few other similar inductions which were giving me grief...

[Jad Ghalayini]

Extra context: the top induction requires set_option maxHeartbeats 1000000 to even typecheck at all. No other nonstandard options are set anywhere

[Alex Keizer]

Could you provide a #mwe? What are Term and Sparsity here?

[Jad Ghalayini]

Alex Keizer said:

Could you provide a #mwe? What are Term and Sparsity here?

I'm probably gonna try and minimize it later this week. Term is a small enum representing basically the STLC + products, say about 10 variants, while Sparsity is just an alias for List Bool.

[Leonardo de Moura]

@Jad Ghalayini Thanks! A #mwe would be very useful for us.