simp vs rw with match witness

Stream: lean4

[Chris Bailey]

Is there an option to get simp [(h0 : e = e')] to rewrite a match statement that has a witness (as inmatch h : e with)? It seems that rw works, but inquiring minds would like to know about simp. Mwe:

def i_isSome (elems : Array A) (i : Nat) : Bool :=
  match h : elems[i]? with
  | none => false
  | some _ => true

-- succeeds using `rw [h]`
example (elems : Array Char) (i : Nat) (h : elems[i]? = some 'a') : i_isSome elems i = true := by
  simp only [i_isSome]
  rw [h]

-- fails with `simp [h]`
example (elems : Array Char) (i : Nat) (h : elems[i]? = some 'a') : i_isSome elems i = true := by
  simp only [i_isSome]
  simp [h]
  /-
  ⊢ (match h : elems[i]? with
  | none => false
  | some val => true) =
  true
  -/

[Gabriel Ebner]

That's because the automatically generated congruence lemmas are too weak. If you set set_option pp.match false, then you'll see that the match is implemented as a function. And the types of the match arms depend on the Array Char argument, therefore if you want to rewrite there you need to modify the arguments as well so that the match still type checks.

[Gabriel Ebner]

Here's a toy repro:

opaque f (x : Nat) (k : x = 0 → Nat) : Nat
example : f (0 + x) k = f x fun h => k (by simp_all) := by simp

[Gabriel Ebner]

To rewrite 0 + x to x we need to change the (proof in the) second argument. But simp doesn't know how to do that.

[Chris Bailey]

Thanks for the explanation and example. I looked at the pp.all true output but wasn't sure whether there was a magic simp flag or anything.