feat: Rewrites from GlobalIsel

[osmanyasar05]

This PR introduces some of the rewrites from GlobalISel that we had in Lean-MLIR as well.

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: fb71c72	Previous: b8265aa	Ratio
add-fold-worklist/create	1873000 ns (± 29838)	2434000 ns (± 160814)	0.77
add-fold-worklist/rewrite	3551000 ns (± 96676)	3947500 ns (± 56105)	0.90
add-fold-worklist-local/create	1930000 ns (± 47268)	2386000 ns (± 117421)	0.81
add-fold-worklist-local/rewrite	3141000 ns (± 151597)	3322500 ns (± 19159)	0.95
add-zero-worklist/create	1914000 ns (± 68902)	2406000 ns (± 109136)	0.80
add-zero-worklist/rewrite	2432000 ns (± 13180)	2501000 ns (± 29385)	0.97
add-zero-reuse-worklist/create	1597000 ns (± 47363)	2069000 ns (± 69158)	0.77
add-zero-reuse-worklist/rewrite	2019000 ns (± 57297)	2093000 ns (± 17355)	0.96
mul-two-worklist/create	1908000 ns (± 77200)	2233000 ns (± 45758)	0.85
mul-two-worklist/rewrite	5229000 ns (± 228273)	5578000 ns (± 83143)	0.94
add-fold-forwards/create	1916000 ns (± 39096)	2254000 ns (± 34802)	0.85
add-fold-forwards/rewrite	2829000 ns (± 47527)	2977000 ns (± 15110)	0.95
add-zero-forwards/create	1861000 ns (± 29399)	2289000 ns (± 70319)	0.81
add-zero-forwards/rewrite	1802000 ns (± 52457)	1951000 ns (± 10968)	0.92
add-zero-reuse-forwards/create	1581000 ns (± 19386)	1916000 ns (± 120621)	0.83
add-zero-reuse-forwards/rewrite	1450000 ns (± 30328)	1551000 ns (± 35552)	0.93
mul-two-forwards/create	1899000 ns (± 107765)	2356000 ns (± 73814)	0.81
mul-two-forwards/rewrite	3299500 ns (± 122026)	3575000 ns (± 63979)	0.92
add-zero-reuse-first/create	1581000 ns (± 45658)	1906500 ns (± 78414)	0.83
add-zero-reuse-first/rewrite	10500 ns (± 2537)	8000 ns (± 2040)	1.31
add-zero-lots-of-reuse-first/create	1571000 ns (± 53223)	1819000 ns (± 82223)	0.86
add-zero-lots-of-reuse-first/rewrite	838000 ns (± 52379)	783000 ns (± 27096)	1.07

This comment was automatically generated by workflow using github-action-benchmark.

[luisacicolini]

lgtm, thanks!

[luisacicolini]

sorry, I got confused. could we have a proof for these rewrites? Like the ones in Proofs.lean.