Proof Reconstruction

Proof reconstruction module: Lean 4 proof steps for optimization and rewriting rules used in Blaster.

Support the development efforts with the following acceptance criteria:

- Proof Reconstruction of the optimization step complete for basic types Nat, String, Int, etc. The optimization and rewriting steps have corresponding Lean 4 proof reconstruction steps.
- Progress on Proof Reconstruction of the optimization step for complex terms as lambda lifting, different reductions, etc.
- Tests used to test the implemented optimization steps produce valid Lean 4 proofs
- A selection of representative examples that are proved with Blaster in only-optimize mode have full proof reconstruction

Support the development efforts to produce:

- Proof reconstruction module is delivered in the lean-blaster repository
- A new major version is released integrating the optimization step proof reconstruction

The present scope is based on the existing infrastructure for implementing Proof Reconstruction. Optimization rules can push proof steps onto a proof stack, and the tactic replays that stack to close the goal. Nat is fully covered today and all Nat optimization tests pass with real reconstructed proofs. The remaining work is to extend this coverage to the other types and to the more complex reductions.