Rewrite under binder

Stream: lean4

[Wojciech Nawrocki]

A possibly dumb question, is the following supposed to fail?

opaque foo (m : Nat) : Nat

example (h : ∀ n, foo 10 = foo n) (h' : foo 10 = 11) : false := by
  rw [h'] at h -- good
  sorry

opaque bar (m n : Nat) : Nat

example (h : ∀ m n, bar 10 n = bar m n) (h' : ∀ n, bar 10 n = 11) : false := by
  /- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
    bar 10 ?n
  h : ∀ (m n : Nat), bar 10 n = bar m n
  h' : ∀ (n : Nat), bar 10 n = 11
  ⊢ false = true -/
  rw [h'] at h
  sorry

[Sebastian Ullrich]

I think so. It's not that rw can't rewrite under binders as sometimes stated, but that it cannot rewrite bound variables, or terms involving them.

[Wojciech Nawrocki]

Okay, is simp only or something else the preferred alternative?

[Sebastian Ullrich]

Yeah, simp only is the next closest one I'd say

[Sebastian Ullrich]

Try proving both examples using ▸ if you want to understand rw's troubles :)

[Wojciech Nawrocki]

Right, I guess kabstract is not sufficient and we must first intro the binders which rw does not do (?). Thanks!

[Kyle Miller]

rw doesn't know about funext, which would give you the power to indiscriminately rewrite under the binders. simp knows about it though.

[Wojciech Nawrocki]

That's fair, although this particular example does not need funext:

opaque bar (m n : Nat) : Nat

theorem barThm (h : ∀ m n, bar 10 n = bar m n) (h' : ∀ n, bar 10 n = 11) : ∀ m n, 11 = bar m n :=
  fun m n => h' n ▸ h m n

/- 'GF256.barThm' does not depend on any axioms -/
#print axioms barThm

[Sebastian Ullrich]

▸ may have been a red herring as it's rewriting the goal, not the hypothesis. You'd need a have to simulate rw.

[Wojciech Nawrocki]

Is that a relevant difference? We can also just write

theorem barThm (h : ∀ m n, bar 10 n = bar m n) (h' : ∀ n, bar 10 n = 11)
    : ∀ m n, 11 = bar m n := by
  have := fun m n => h' n ▸ h m n
  clear h
  exact this

[Sebastian Ullrich]

That is, the corresponding tactic proof is

  intro m n
  rw [← h' n]
  exact h m n

[Sebastian Ullrich]

And the doomed term corresponding to rw [h'] at h would be

  have h : ∀ m n, 11 = bar m n := h' _ ▸ h

type mismatch
  h
has type
  ∀ (m n : Nat), bar 10 n = bar m n : Prop
but is expected to have type
  ∀ (m n : Nat), bar 10 (?m.338 h h') = bar m n : Prop

As you can see, the missing hole is not allowed to refer to the bound n