Odd rewrites when dealing with Int32

Stream: new members

[ZDHKLV]

Hi,

I'm a complete Lean beginner with a bit of Isabelle background.
Here is a minimal example of my situation :

inductive Expr where
  | Num : Int32 → Expr
  | Plus : Expr → Expr → Expr

open Expr

def opt : Expr → Expr
  | Plus (Num 0) e => opt e
  | Plus e (Num 0) => opt e
  | Plus e₁ e₂ => Plus (opt e₁) (opt e₂)
  | other => other

theorem l : ∀ e, opt (Plus (Num 0) e) = opt e := by
  intro e
  rw [opt]

I'm trying to prove a very basic arithmetic simplification.
Whenever my numbers (from Expr.Num) are of type Nat, the rw [opt] in my proof works exactly as I expect it to do and it solves the goal. However, when the type is Int32, it creates 3 subgoals which I do not understand.

Subgoal 1 : (opt (Num 0)).Plus (opt e) = opt e
For me, it makes no sense as it seems to apply the 3rd rule "opt (Plus e1 e2) = Plus (opt e1) (opt e2)" when it should apply the first rule "opt (Plus (Num 0) e) = opt e"

Subgoal 2 : Num 0 = Num { toUInt32 := { toBitVec := 0#32 } } → False
Subgoal 3 : e = Num { toUInt32 := { toBitVec := 0#32 } } → False

I understand nothing about the last two subgoals. I know that Int32 is defined way differently from Nat, but I don't know how and I assume I shouldn't have to know (?).
What I am wondering is why can't I do this single rewrite when "it looks obvious". I would have expected to finish my goal with this single rw [opt].

Thank you very much for reading this.

[Markus Himmel]

Thank you for reporting this. This is indeed very unfortunate. As you guessed, rw decides that it should apply the third rule and asks you to prove that the first two rules are not applicable, but of course this is impossible since the first rule is in fact applicable. In this specific case, you can use erw instead of rw, which is basically a version of rw that will try harder to apply the first rule for opt and it succeeds on your goal. It is completely reasonable to expect normal rw to succeed here. I will create a Lean issue for this problem.

[ZDHKLV]

Thank you very much for your response. While erw works for this minimal version, unfortunately I hit a timeout in my real one (where the opt function contains many more cases). If this is indeed the case that the issue isn't from a bad comprehension from me then I am perfectly fine with it and I'll try to work with the Int type instead (which works at intended just like Nat). Thank you again.