simp at h has no effect but changes subsequent tactics?

Stream: lean4

[Jeremy Salwen]

Hello, I am unsure if this is a bug or behavior I am unaware of.

In the middle of my proof, I noticed behavior where I have the following hypothesis and goal:

n: ℕ
head: Char
tail: List Char
h: ¬head = Char.ofNat 45
⊢ (if head = Char.ofNat 45 then -↑(toNatX tail) else ↑(toNatX (head :: tail))) = ↑n

simp [h] refuses to simplify the if statement. However, if I first do simp at h and then simp [h] it works fine, despite the fact that simp at h makes no visible difference to h or any other part of the proof state.

I tried creating a MWE, but it doesn't exhibit the same behavior:

def toNatX (_s: (List Char)): Nat := 0

lemma wtf (n: ℕ) (head: Char) (tail: List Char) (h: ¬head = Char.ofNat 45): (if head = Char.ofNat 45 then -↑(toNatX tail) else ↑(toNatX (head :: tail))) = ↑n := by
  simp [h]

Instead it does what I expected, which is simp [h] just working.

[Sebastian Ullrich]

Do you see a change from at h with set_option pp.all true?

[Jeremy Salwen]

Yes, It changed from

h₃: Not (@Eq.{1} Char head (Char.ofNat 45))

to

h₃: Not (@Eq.{1} Char head (Char.ofNat (@OfNat.ofNat.{0} Nat 45 (instOfNatNat 45))))

[Kevin Buzzard]

and what does the goal term head = Char.ofNat 45 look like? Maybe you just answered your own question?

[Jeremy Salwen]

⊢ @Eq.{1} Int
  (@ite.{1} Int (@Eq.{1} Char head (Char.ofNat (@OfNat.ofNat.{0} Nat 45 (instOfNatNat 45))))
    (instDecidableEqChar head (Char.ofNat 45))
    (@Neg.neg.{0} Int Int.instNegInt
      (@Nat.cast.{0} Int (@NonAssocRing.toNatCast.{0} Int (@Ring.toNonAssocRing.{0} Int Int.instRingInt))
        (String.toNatΔ tail)))
    (@Nat.cast.{0} Int (@NonAssocRing.toNatCast.{0} Int (@Ring.toNonAssocRing.{0} Int Int.instRingInt))
      (String.toNatΔ (@List.cons.{0} Char head tail))))
  (Int.ofNat n)

[Jeremy Salwen]

I don't understand what any of this means. I thought ¬head = Char.ofNat 45 meant ¬head = Char.ofNat 45 :sob:

[Jeremy Salwen]

Does this mean I need to defensively simplify my hypotheses regularly? I probably wouldn't have noticed this behavior if the hypothesis or goal were slightly more complicated.

[Andrés Goens]

set_option pp.all true is just turning off pretty printing of the syntax, so what you're seeing there is just the full spelled out names of the functions that build that. For example the = in head = Char.ofNat 45 is just the pretty version of @Eq.{1} Int head (Char.ofNat 45), there's a type Eq which has an (implicit) parameter which is the type, that has one constructor, which is what is used to define equality, and the rest of what's happening there is similarly showing you everything that's under the hood

[Mario Carneiro]

More precisely, what this indicates is that the original h was ¬head = Char.ofNat (nat_lit 45) where nat_lit 45 is a "raw nat literal", and simp turned it into ¬head = Char.ofNat 45 using a properly marked up nat literal which also happens to match the expression in the if statement of the goal

[Mario Carneiro]

so the question is: how did you come to obtain a hypothesis containing a raw nat literal?

[Jeremy Salwen]

I did have h₃: ¬head = '-' := to generate h₃, so maybe the literal '-'?

[Mario Carneiro]

I see, that makes sense. I take it that you didn't write Char.ofNat 45 in the if statement either, you just simped it and it ended up like that

[Mario Carneiro]

In other words, the issue is that '-' is not in simp-normal form

[Mario Carneiro]

I think the best fix here is to make '-' expand to Char.ofNat 45 instead of Char.ofNat (nat_lit 45). Regular number literals like 45 are automatically marked up so character literals should be as well

[Jeremy Salwen]

Are there other scenarios I should be on the lookout for differences that are hidden by the pretty printer?

[Mario Carneiro]

For your specific issue though the quick fix is to just simp the hypothesis as well, just as if it was written in some inconvenient way that needed simping

[Mario Carneiro]

This is a bug, I don't think you necessarily need to be on guard against similar things

[Jeremy Salwen]

Ok thanks, should I file it on github?

[Mario Carneiro]

but you should be generally aware that the pretty printer does not show all information by default, and sometimes the behavior of a tactic depends on things that aren't visible

[Mario Carneiro]

besides using pp.all, another method that isn't quite so much of a fire-hose is to use the goal view to click on expressions and see how they are constructed

[Kevin Buzzard]

rw works up to syntactic equality, and simp uses rw, so the syntactic change made all the difference here.