feat(puddle): add denotational validity

[math-fehr]

This change adds Pattern.PreservesSemantics, a proposition that asserts that a puddle pattern is semantically valid. With this, we can prove (in a separate PR) that once the pattern is compiled, it satisfies LocalRewritePattern.PreservesSemantics.

This change also creates simpPuddleSemantics, a simplification tactic to remove all the PreservesSemantics definitions, so the only has a clean goal to prove.

[tobiasgrosser]

CI failure:

 trace: .> LEAN_PATH=/home/runner/work/veir/veir/.lake/packages/Coinductive/.lake/build/lib/lean:/home/runner/work/veir/veir/lean-ctrees/.lake/build/lib/lean:/home/runner/work/veir/veir/ExArray/.lake/build/lib/lean:/home/runner/work/veir/veir/.lake/build/lib/lean /home/runner/.elan/toolchains/leanprover--lean4---v4.33.0/bin/lean --tstack=400000 /home/runner/work/veir/veir/UnitTest/Puddle.lean -o /home/runner/work/veir/veir/.lake/build/lib/lean/UnitTest/Puddle.olean -i /home/runner/work/veir/veir/.lake/build/lib/lean/UnitTest/Puddle.ilean -c /home/runner/work/veir/veir/.lake/build/ir/UnitTest/Puddle.c --setup /home/runner/work/veir/veir/.lake/build/ir/UnitTest/Puddle.setup.json --json
    error: UnitTest/Puddle.lean:36:23: Function expected at
      RuntimeValue.Conforms.integerType
    but this term has type
      RuntimeValue.Conforms ?m.68 ⟨Attribute.integerType ?m.69, ?m.70⟩ ↔
        ∃ val, ?m.68 = RuntimeValue.int (IntegerType.bitwidth ?m.69) val
    
    Note: Expected a function because this term is being applied to the argument
      hx
    error: UnitTest/Puddle.lean:36:11: Tactic `rcases` failed: `x✝ : ?m.72` is not an inductive datatype
    error: Lean exited with code 1
    Some required targets logged failures:
    - UnitTest.Puddle

... i guess this is still WIP - I wait until this is marked ready-for-review ..

[math-fehr]

Yes, I am fixing the tactic a bit (not the final version of the tactic, but at least something that works) before marking this ready. I shouldn't have requested review on a draft PR though.
Anything besides the tactic is fixed though

[math-fehr]

Should be good now

[math-fehr]

@tobiasgrosser gentle ping on this, it should be ready for review now

[tobiasgrosser]

Nice. We should probably organize a code-walk? But good to go for now.

[ineol]

Really cool! only minor naming comments