Definitional equality woes in metaprogramming (reification)

Stream: general

[l1mey]

(See mwe below) I am building a tactic that manipulates expressions in a reified intermediate representations similar to bv_decide. It operates on iN n, which is similar to a BitVec n:

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

How it would generally work is the following:

(reify) Expr -> IR, returns a proof that IR.eval = expr
(denote) IR -> Expr, returns a proof that IR.eval = expr

given opt : IR -> IR and lhs:

  ir  = reify lhs     (IR.eval ir = lhs)
  ir' = opt ir        (IR.eval ir ~> IR.eval ir')   (use opt.wf)
  rhs = denote ir'    (IR.eval ir' = rhs)

chain the proofs to end up with lhs ~> rhs

I'm having issues creating my reify function. It currently accepts expressions of the form

fun {n} ... {m} (x : iN n) ... (z : iN m) : iN n => ...

and builds up two assignments

structure PackediN where
  {n : Nat}
  x : iN n
deriving BEq

abbrev Assignment := Lean.RArray PackediN
abbrev WidthAssignment := Lean.RArray Nat

such that if fun {n} (x : iN n) => x, it should assign

let ξ : WidthAssignment := (RArray.leaf n)
let σ : Assignment := RArray.leaf { n := ξ.get 0, x := x }
let ir : IR 0 := IR.var 0

and return a value ⟨IR.var 0, x_expr, pure none⟩ : ReifiedIR 0 where

structure ReifiedIR (idx : Nat) where
  irExpr : IR idx
  originalExpr : Expr

  /- proof that IR.eval irExpr = originalExpr, or by rfl if none  -/
  proof : M (Option Expr)

Evaluating the ir given the two assignments assigns semantics to it. When reifying, similar to bv_decide, it assumes that the evaluation of the IR.var is definitionally equal to x. However, this is not the case, as you can see:

def eval (ξ : WidthAssignment) (σ : Assignment) : IR idx → iN (ξ.get idx)
  | var id =>
    let pack := σ.get id
    /- h is always true, this if is for totality -/
    if h : pack.n = (ξ.get idx) then
      h ▸ pack.x
    else
      pack.truncate (ξ.get idx)

  | const_poison => poison

theorem defeq {n} (x : iN n)
    : IR.eval (RArray.leaf n) (RArray.leaf { n := (RArray.leaf n).get 0, x := x }) (IR.var 0 : IR 0) = x := by

  rfl
  /-
  Tactic `rfl` failed: The left-hand side
    IR.eval (RArray.leaf n) (RArray.leaf { n := (RArray.leaf n).get 0, x := x }) (IR.var 0)
  is not definitionally equal to the right-hand side
    x
  -/
  simp [IR.eval] -- this works!

Taking a look at the proofs that bv_decide creates, the difference between my tactic and bv_decide is shown. Since I want my tactic to work on rewriting quantified bitvectors in the IR, not just bitvectors with a fixed width, I need to introduce two different assignments. One set of assignments for the variables, and one set of assignments for the bitwidths.

theorem t8 (p : BitVec 8)
  : Std.Tactic.BVDecide.BVExpr.eval (Lean.RArray.leaf { w := 8, bv := p })
    (Std.Tactic.BVDecide.BVExpr.var 0) = p := by

  rfl

/- when you introduce a quantifier, it fails to be definitionally equal! -/
theorem tn {n} (p : BitVec n)
  : Std.Tactic.BVDecide.BVExpr.eval (Lean.RArray.leaf { w := n, bv := p })
    (Std.Tactic.BVDecide.BVExpr.var 0) = p := by

  rfl -- fails!

Creating a general theorem to prove this works as well, as you can see inlining the ξ : WidthAssignment makes this theorem type nice as ξ.get 0 = n holds as a definitional equality:

theorem reflect_var_eval_var {idx id} (x : iN n) (σ : Assignment)
    (hb : (σ.get id).n = n)
    (h : hb ▸ (σ.get id).x = x)
    : IR.eval (RArray.leaf n) σ (IR.var id : IR idx) = x := by

  simp [IR.eval, hb, h]

Furthermore, hb and h are definitional equalities as well when you inline σ in the "evals at atoms assignments" part of reify.

I guess the question I am asking is that how would I formulate this in a nice way in my tactic given that they're not definitionally equal? Or, maybe they are definitionally equal and I am formulating it wrongly?

An mwe is attached: mwe.lean, it doesn't depend on anything but Lean and Qq. I'm quite new to metaprogramming tactics in this style, so some guidance would be greatly appreciated!

[l1mey]

Maybe someone might be able to answer why the theorem defeq isn't provable by just definitional equality, is it because of the variables on the type?

theorem defeq {n} (x : iN n)
    : IR.eval (RArray.leaf n) (RArray.leaf { n := (RArray.leaf n).get 0, x := x }) (IR.var 0 : IR 0) = x := by

  rfl
  /-
  Tactic `rfl` failed: The left-hand side
    IR.eval (RArray.leaf n) (RArray.leaf { n := (RArray.leaf n).get 0, x := x }) (IR.var 0)
  is not definitionally equal to the right-hand side
    x
  -/

[Aaron Liu]

it's because you have a if h : pack.n = (ξ.get idx)

[Aaron Liu]

the way docs#Nat.decEq reduces this will only definitionally reduce to true when both sides are definitionally the same numeral (not a variable)

[l1mey]

I understand. I guess instead of definitional equality it would just suffice to create a simp context and do the equivalent of simp [IR.eval] to prove the goal. I'll add in caching as well like bv_decide.

Last question, what is the interaction with definitional equality and decidable equality? I thought definitional equality does reduction based on the definition, I didn't know it called out to decidable instances.

[l1mey]

Ah, nevermind. dite requires a decidable h.

[Aaron Liu]

I see above the if statement

    /- h is always true, this if is for totality -/
    if h : pack.n = (ξ.get idx) then

so maybe if you pass in a proof instead of making the function total, then you can still get definitional equality?

[l1mey]

The issue is I can't do such a thing, because the IR.eval function is meant to work for things that aren't .var as well. In the mwe and code snippets, I include cases for .const_poison with the rest of the cases omitted. It wouldn't work in general.