Tactic to match and dispel cases

Stream: general

[l1mey]

Consider this inductive type:

inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

A repeated proof technique is to match on all the iN n inputs, and immediately clear the cases where it is poison, before actually proving the useful section. The proof ends up looking like this:

theorem addNsw_refine {n} (x y : iN n)
  : x +nsw y ~> x + y := by

  cases x
  case bitvec a =>
    cases y
    case bitvec b =>

      simp [iN_unwrap_inst]
      if h : a.saddOverflow b then
        simp [h]
      else
        simp [h]

    case poison => simp [iN_unwrap_inst]
  case poison => simp [iN_unwrap_inst]

theorem addNsw_assoc_if_same_sign {n} {hn : Bits n} (x y z : iN n)
    (h :
      (x ≥ₛ 0) &&& (y ≥ₛ 0) &&& (z ≥ₛ 0) ~> 1 ∨
      (x <ₛ 0) &&& (y <ₛ 0) &&& (z <ₛ 0) ~> 1)

    : (x +nsw y) +nsw z <~> x +nsw (y +nsw z) := by

  cases x
  case bitvec a =>
    cases y
    case bitvec b =>
      cases z
      case bitvec c =>
        simp [iN_unwrap_inst] at *

        have h' : a.msb = b.msb ∧ b.msb = c.msb := by
          bv_decide

        rw [BitVec.saddOverflow_assoc_monotone a b c h']
        rw [BitVec.add_assoc a b c]
        exact hn

      case poison => simp [iN_unwrap_inst]
    case poison => simp [iN_unwrap_inst]
  case poison => simp [iN_unwrap_inst]

In both cases, there is a repeated cases x; case bitvec a => for every single argument in the function. My question, is there a nice way to represent this without making the cases explicit?

It would be nice for it to look like poison_unroll x y z => a b c, maybe metaprogramming could help?

[l1mey]

image.png

I have tried using match, and it does bind a etc, but it keeps around x y z : iN n as you can see in the commented goal and doesn't actually perform substitutions of of them into the hypotheses and goal.

[l1mey]

I've tried this macro (MWE below), but getting multiple errors:

import Lean

open Lean Elab Tactic Meta

syntax (name := poisonUnroll) "poison_unroll " ident+ " => " ident+ : tactic

macro_rules
| `(tactic| poison_unroll $xs:ident* => $ys:ident*) => do
  if ¬xs.size == ys.size then
    Macro.throwError s!"poison_unroll: got {xs.size} variables but {ys.size} names"
  let rec go (i : Nat) : MacroM Syntax := do
    if h : i < xs.size then
      let xi := xs[i]'h
      let yi := ys[i]!
      let inner ← go (i+1)
      `(tactic|
        cases $xi <;>
          first
            | case bitvec $yi => $inner
            | case poison     => simp [iN_unwrap_inst])
    else
      `(tactic| skip)
  go 0

image.png

How could I remedy this?

[l1mey]

Okay, so this macro worked and type checks:

macro_rules
| `(tactic| poison_unroll $xs:ident* => $ys:ident*) => do
  if ¬xs.size == ys.size then
    Macro.throwError s!"poison_unroll: got {xs.size} variables but {ys.size} names"
  let rec go (i : Nat) : MacroM (TSyntax `tactic) := do
    if h : i < xs.size then
      let xi := xs[i]'h
      let yi := ys[i]!
      let inner ← go (i+1)
      `(tactic|
          cases $xi:ident with
          | bitvec $yi => $inner:tactic
          | poison => simp [iN_unwrap_inst])
    else
      `(tactic| skip)
  go 0

But is seeming to not work with tactics:

image.png

It isn't able to bring the goal down like in this example:

image.png

[l1mey]

Solved. The macro

macro_rules
| `(tactic| poison_unroll $xs:ident* => $ys:ident*) =>
  `(tactic|
    ($[cases $xs:ident with
      | bitvec $ys:ident => ?_
      | poison => simp [iN_unwrap_inst]];*))

worked.