Simp not collapsing simultaneous matching

Stream: general

[l1mey]

Consider this simple inductive type with the function iN.addNsw containing a simultaneous match on the inputs checking for poison. If either aren't poison, it calls iN.addNswBV which the implementation of isn't important here.

The theorem poison_left passes easily by simp, but poison_right doesn't pass by simp. I know this is due to how Lean represents simultaneous matching, but how can I circumvent it while keeping matching (or use if statements)?

Defining a simp lemma for poison_right not be the right way to go, as there are around 20 instructions each with their own variants.

Below is a MWE:

/--
LLVM-style integers with poison value.
-/
inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

export iN (poison bitvec)

protected def iN.addNswBV {n : Nat} (a b : BitVec n) : iN n :=
  if BitVec.saddOverflow a b then
    poison
  else
    bitvec (a + b)

protected def iN.addNsw {n} : iN n → iN n → iN n
  | poison, _ => poison
  | _, poison => poison
  | bitvec a, bitvec b => iN.addNswBV a b

theorem poison_left {n} {x : iN n}
    : iN.addNsw poison x = (poison : iN n) := by

  unfold iN.addNsw
  simp

theorem poison_right {n} {x : iN n}
    : iN.addNsw x poison = (poison : iN n) := by

  unfold iN.addNsw
  simp
  /-
  n : Nat
  x : iN n
  ⊢ (match x, poison with
    | poison, x => poison
    | x, poison => poison
    | bitvec a, bitvec b => iN.addNswBV a b) =
    poison
  -/
  sorry

[Jakub Nowak]

In match x, poison there are two possible cases poison, x or x, poison and simp generally can't do case by case analysis like that.

This works:

theorem poison_right {n} {x : iN n}
    : iN.addNsw x poison = (poison : iN n) := by

  unfold iN.addNsw
  cases x <;> simp

After cases x there are two goals and simp can solve each one individually, because there's only one possible branch of the match.

[l1mey]

Could I use an if statment instead? I just don't know how to extract out a case without a match.

[Jakub Nowak]

Usually you wouldn't use if or match in tactic mode. cases is similar to match. cases x creates two subgoals. In one subgoal x is replaced with bitvec a, in the second subgoals it's replaced with poison.

Not sure if you know <;> syntax, maybe this would be simper to understand:

theorem poison_right {n} {x : iN n}
    : iN.addNsw x poison = (poison : iN n) := by

  unfold iN.addNsw
  unfold iN.addNsw
  cases x

  · simp
  · simp

You can put cursor right after cases x and inspect both subgoals it created.