Can `simp` introduce variables?

Stream: general

[l1mey]

I have these definitions of a structure:

/--
LLVM-style integers with poison value.
-/
structure iN (bits : Nat) : Type where
  protected bitvec : BitVec bits
  protected poison : Bool

  protected poison_inv : poison → bitvec = 0

def poison {n : Nat} : iN n := ⟨0, true, by simp⟩
def bitvec {n : Nat} (value : BitVec n) : iN n := ⟨value, false, by simp⟩

To create a value of poison, use the poison function, and the bitvec a with a : BitVec n to instantiate a bitvector. In general you shouldn't construct iN directly. I would like to create a normal form for when some x : iN n is either poison or a bitvec.

@[simp, grind]
theorem poison_norm {n} (x : iN n) {h : x.poison = true}
    : x = poison := by

  obtain ⟨x_bitvec, is_poison, poison_inv⟩ := x
  have h' : x_bitvec = 0 := poison_inv h

  subst h'
  subst h
  rfl

@[simp, grind]
theorem bitvec_norm {n} (x : iN n) {_h : ¬x.poison = true}
    : ∃ (a : BitVec n), x.bitvec = bitvec a := by

  unfold bitvec
  simp

The poison_norm turns all x : iN n that have x.poison into the actual poison definition. However, for the bitvec_norm, i would have to introduce variables. What would be the best way to allow simp to introduce these variables? I have used an exists here, but simp wouldn't instantiate it. Would a simproc work for this?

[Yan Yablonovskiy 🇺🇦]

Perhaps you mean :

@[simp, grind]
theorem bitvec_norm {n} (x : iN n) {_h : ¬x.poison = true}
    : ∃ (a : BitVec n), x.bitvec = (bitvec a).1 := by

  unfold bitvec
  simp

If I fill in your simp with sorry, I get a type error for the statements definition. And such questions may get better traction in the `new members' chat channel :slight_smile: .

[Eric Wieser]

Have you considered using Option (BitVec bits) instead?