Simple expression IR with rewriting

Stream: general

[l1mey]

What is the easiest way to create a simple expression treelike based IR, that I would be able to apply rewrites to, prove equivalence between two different expressions by unwrapping the actual semantics of the instructions, and prove confluence of rewriting?

I tried before to create an SSA based IR with what lean-mlir are doing, but I don't need effects, looping control flow or cyclic dataflow. Everything is going to be just simple expressions, and deduplicating expressions at the end.

Here is an example of what I would want:

theorem con1 : (.add (.var X) (.var Y)).semantics = (.add (.var Y) (.var X)).semantics := by
  funext x y
  ...

I'm guessing the alternative to this would be to write the IR and compiler in a separate language, and have the compiler generate proof certificates that can be checked in Lean.