Proofs by rfl simp better?

Stream: lean4

[Siddharth Bhat]

I have a situation that I'm currently MWEing, but I thought to ask about the general scenario in case someone has insights.
The TL;DR is that two proofs of the same equality behave differently under simp: The proof of equality by rfl succeeds in simping. The proof that is more complex (ie, not rfl) does not simp, with the generic error simp made no progress. Also, rw fails in this context with "motive is not type correct", so we really do need simp to exploit the equality.

I'm wondering if it is expected behaviour that rfl proofs simp better than non-rfl proofs, in dependently typed contexts?

lemma ConcreteOrMVar.instantiate_mvar_zero'_by_rfl :
    (ConcreteOrMVar.mvar (φ := 1) ⟨0, by simp⟩).instantiate (Subtype.mk [w] (by simp)) = w := by
  rfl

lemma ConcreteOrMVar.instantiate_mvar_zero'_by_norfl :
    (ConcreteOrMVar.mvar (φ := 1) ⟨0, by simp⟩).instantiate (Subtype.mk [w] (by simp)) = w := by
  simp [instantiate, Vector.head]

/- This one does not have the 'snoc' leftover. -/
set_option pp.proofs.withType true in
theorem ok : src 1  ⊑ tgt 1  := by
  ...
  -- simp only [ConcreteOrMVar.instantiate_mvar_zero'_rfl] -- succeeds
  simp only [ConcreteOrMVar.instantiate_mvar_zero'_norfl] -- fails

[Ruben Van de Velde]

Probably yes. These also apply with dsimp

[Siddharth Bhat]

Right. Can one characterise which simp actions do not work in the non-rfl case? I'm trying to build a mental model of how much I can expect from non-rfl equalities in a heavily dependent typed context.

[Andrés Goens]

curious about how the two terms differ, it sounds like some of the peskier congr's could be added in the second case that are just 'regular' Eq in the first? (just a hunch)

[Andrés Goens]

(I know that simp sometimes adds some congr lemmas that are especially annoying to deal with later when there's dependent types involved)

[Floris van Doorn]

Lemmas proved with rfl can be used to rewrite even when you have dependent types.
Here is a simple example that shows some differences:

import Mathlib.Data.Fin.Basic

def n := 2
lemma not_with_rfl : n = 2 := by simp [n]
lemma with_rfl : n = 2 := rfl

example : ∀ x : Fin n, x.1 = 2 := by
  -- simp [not_with_rfl] -- fails
  -- simp [with_rfl] -- works
  intro x
  -- simp [not_with_rfl] at x -- creates new copy of `x` that doesn't occur in the goal
  simp [with_rfl] at x -- changes the type of `x`

dsimp can be used to use simp only with rfl-lemmas

[Tobias Grosser]

Thank you @Floris van Doorn. Out of interest, do you happen to know why simp would introduce a new copy of x. I am curious about the typical development flow in which this simplified copy of x is used.

[Kyle Miller]

It's because x is used in the goal, and simp copies hypotheses in the situation where the new type isn't defeq to the old one.

[Kyle Miller]

It's sort of for the same reason that simp [not_with_rfl] fails before doing intro, due to the dependence.

[Tobias Grosser]

Right. I am just curious why simp does then rewrite types at all in the hypothesis, if the hypothesis that is used remains unsimplified. Assuming I apply simp [not_with_rfl], how am I then supposed to start using the new x, e.g., in the example above? If it is not possible to use the new x in the goal, would it then not make more sense for simp to just not do anything rather than introducing a hypothesis that cannot be effectively used?

[Kyle Miller]

I don't have any immediate examples, but I've had a number of cases where this behavior was helpful (though of course it's not always helpful!). Potentially, though, it would lead to clearer proofs if you had to explicitly do have x' := x; simp ... at x'

[Tobias Grosser]

@Kyle Miller @Floris van Doorn, I just found an interesting example where I feel the proof should be trivial, but it somehow is not:

def test_ok {A : BitVec 0} : BitVec.toNat A = 0 := by
  simp only [of_length_zero, toNat_ofNat, pow_zero, Nat.zero_mod]

def test_broken {A : BitVec w} (h : w = 0) : BitVec.toNat A = 0 := by
  simp [h] at A
  -- w : ℕ
  -- A✝ : BitVec w
  -- h : w = 0
  -- A : BitVec 0
  -- BitVec.toNat A✝ = 0
  simp [of_length_zero] -- does not apply as A was replaced with A✝

[Sebastian Ullrich]

It would be type-incorrect to place the new A in the goal's conclusion. You'll need to apply the equality to the entire goal at once using subst h

[Tobias Grosser]

Lovely! That works.