change _ at h fails

Stream: lean4

[Sven Manthe]

This feels like a bug, but I have no understanding of what is going on in the following MWE:

def g (_ : Nat) : Nat := 0
theorem iff (a : Nat) :
  0 = g 0 ↔ 0 = a := by sorry
theorem test
  (T : Unit)
  (h : 0 = g 0)
  (ih : T = T) --removing this parameter makes change succeed below
  : 0 = g 0 := by
  --change _ at h --adding this line makes change succeed below
  rw [iff] at h
  change _ at h --fails with type mismatch

[Floris van Doorn]

Thanks for the minimization! The precise error is

type mismatch
  this
has type
  ?m.158 : Sort ?u.157
but is expected to have type
  0 = ?m.129 : Prop

[Sven Manthe]

Even swapping the order of the parameters h and ih makes the error go away (which also explains why the first change helps)

[Daniel Weber]

def g (_ : Nat) : Nat := 0
theorem iff (a : Nat) :
  0 = g 0 ↔ 0 = a := by sorry

theorem test
  (T : Unit)
  (h : 0 = g 0)
  (ih : T = T) --removing this parameter makes change succeed below
  : 0 = g 0 := by
  --change _ at h --adding this line makes change succeed below
  rw [iff ?p] at h
  change 0 = ?p at h --fails with type mismatch

Gives

synthetic hole has already been defined with an incompatible local context

which might be relevant?

[Daniel Weber]

theorem test
    (T : Unit) (ih : T = T) (h : 0 = g 0)
    : 0 = g 0 := by
  let n : Nat := ?p
  rw [iff ?p] at h

gives

T: Unit
ih: T = T
h✝: 0 = g 0
h: 0 = ?p
n: Nat := ?p
⊢ 0 = g 0

while

theorem test
    (T : Unit) (h : 0 = g 0) (ih : T = T)
    : 0 = g 0 := by
  let n : Nat := ?p
  rw [iff ?p] at h

gives

T: Unit
h✝: 0 = g 0
h: 0 = ?p
ih: T = T
n: Nat := ?m.142 ih
⊢ 0 = g 0

[Jovan Gerbscheid]

The problem is that rewriting a local variable replaces later free variables with different free variables of the same name. So the ih after the rewrite is different from the ih before the rewrite. So metavariables before and after the rewrite depend on different ih, so they are not compatible.

import Lean

open Lean Elab

elab "log_local_contexts" : tactic => do
  let mctx ← getMCtx
  let log decls := decls.toArray.filterMap (Option.map (fun decl => (Expr.fvar decl.fvarId, decl.fvarId.name)))
  logInfo m!"local context of ?a: {log (← (mctx.userNames.find! `a).getDecl).lctx.decls}"
  Tactic.withMainContext do
  logInfo m!"local context of ?b: {log (← (mctx.userNames.find! `b).getDecl).lctx.decls}"

theorem test
  (h : True)
  (s : String) -- removing this makes `exact rfl` succeed
  : True := by
  let a : Nat := ?a
  rw [Eq.refl True] at h -- removing this makes `exact rfl` succeed
  let b : Nat := ?b
  /-
  local context of ?a: [(test, _uniq.1176), (h, _uniq.1177), (s, _uniq.1178)]
  -/
  /-
  local context of ?b: [(test, _uniq.1176), (h✝, _uniq.1177), (h, _uniq.1199), (s, _uniq.1202), (a, _uniq.1203)]
  -/
  log_local_contexts
  have : a = b := by
   exact rfl -- error

[Jovan Gerbscheid]

Here's another example that fails for the same reason when there is an extra variable in the local context:

example (h : 0 = 2) (s : String) : False := by
  /-
  tactic 'rewrite' failed, did not find instance of the pattern in the target expression
    ?m.84 - ?m.85

  h✝: 0 = 2
  h: ?m.67 - ?m.67 = 2
  s: String
  ⊢ False
  -/
  rw [← Nat.sub_self, ← Nat.sub_eq] at h

[Sven Manthe]

https://github.com/leanprover/lean4/issues/4885