Using simprocs to simplify `bif` with constructors

Stream: general

[l1mey]

Take this inductive type:

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

I have expressions of the form:

bif a.slt 0#n = false then bitvec 1#1 else bitvec 0#1
-- or in general:
bif _ then bitvec _ else bitvec _

I would like to move the bitvec constructor outside, so I can eventually bubble up all constructors to the root. Like bitvec bif _ then _ else _. This would be pretty fragile to do with normal simp lemmas as i want it to be general on all ifs, I'm guessing simprocs are the way to do it?

This is what I have so far:

simproc ↓ bifBitvec (cond _ (bitvec _) (bitvec _)) := fun e => do
  let_expr cond v lhs rhs := e | return .continue
  unless ← matchesInstance lhs (mkConst ``bitvec) do return .continue
  unless ← matchesInstance rhs (mkConst ``bitvec) do return .continue

  let some va ← getBitVecValue? (lhs.getArg! 0) | return .continue
  let some vb ← getBitVecValue? (rhs.getArg! 0) | return .continue

  -- va : (n : Nat) × BitVec n
  -- vb : (n : Nat) × BitVec n

  -- ?

[Aaron Liu]

are you looking for the reverse direction of docs#Bool.apply_cond

[l1mey]

Yes, that seems like it. However I want this to be part of a wider proof automation pipeline, I would like to apply it to bubble up constructors over many different expressions, and bif is not the only one.

[Aaron Liu]

what are the other ones

[Eric Wieser]

docs#apply_ite

[Eric Wieser]

You could imagine one for general matches too

[Eric Wieser]

I think this has been discussed before

[l1mey]

Aaron Liu said:

what are the other ones

At the moment just HAnd, which is defined as:

protected def iN.poisonWrapper {n} {k} (g : BitVec n → BitVec n → iN k) : iN n → iN n → iN k
  | poison, _ => poison
  | _, poison => poison
  | bitvec a, bitvec b => g a b

/--
LangRef: https://llvm.org/docs/LangRef.html#and-instruction
-/
protected def iN.and {n} : iN n → iN n → iN n :=
  iN.poisonWrapper (· &&& ·)

instance {n} : HAnd (iN n) (iN n) (iN n) where
  hAnd := iN.and

The bubbling up should basically work for every instruction that uses iN.poisonWrapper in its body. Which is why I would want it to be extensible.

[l1mey]

I already have some automation for decomposing iN.poisonWrapper which leaves me with many ifs and ands. But in general it should work for any boolean expression.

[Aaron Liu]

write a lemma about iN.poisonWrapper

[l1mey]

I already have a collection of lemmas, but these don't try to match the arbitrary expressions unless g is carefully simplified in a way such that it is an actual function application:

image.png

[l1mey]

Is there a way to match expressions that don't force me to ensure that the expression is a function? For example, nested expressions inside the condition where g is don't simplify at all.