weird interaction between `mod_cases` and `induction`

Stream: mathlib4

[David Renshaw]

This looks to me like an elaboration bug in the mod_cases tactic.

import Mathlib.Tactic.ModCases

theorem foo (n : ℕ) (z : ℤ) : n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
     mod_cases z % 3
     · sorry
     · sorry
     · sorry

/-
type mismatch
  sorryAx ?m.55
has type
  ?m.55 : Sort ?u.54
but is expected to have type
   Nat.succ _uniq.37 = Nat.succ _uniq.37 : Prop
-/

[Heather Macbeth]

@David Renshaw Thanks for discovering this! :upside_down: I'd like to record it, could you open an issue for it?

[David Renshaw]

https://github.com/leanprover-community/mathlib4/issues/1851

[David Renshaw]

Adding a withMainContext fixes this. PR incoming.

[David Renshaw]

https://github.com/leanprover-community/mathlib4/pull/1865

[David Renshaw]

It's somewhat surprising to me that the main goal and the local context are independent pieces of implicit state.

[David Renshaw]

I think I had kind of assumed that if the main goal is set to something, then the local context must be set to match it.

[Jannis Limperg]

Nope. The whole withContext situation is by far the biggest footgun in the API.

[Mario Carneiro]

David Renshaw said:

I think I had kind of assumed that if the main goal is set to something, then the local context must be set to match it.

This wouldn't really work, since "the main goal" is not really a piece of state, the list of goals is the state and these can be "accidentally" solved by doing other things

[Mario Carneiro]

getMainGoal calculates the first unassigned metavariable on the spot

[David Renshaw]

yeah, having mvarId.assign possibly change the local context seems like it would maybe be bad

[Mario Carneiro]

One way to make it slightly less footgunny would be to have TacticM not extend MetaM at all but require you to "enter" a particular metavariable's context to run things