feat: proof reconstruction for rewrite rules (proofStack)#108

Draft

felipeperet wants to merge 15 commits into

input-output-hk:mainfrom

felipeperet:feat/proof-reconstruction-rewrite

Commits on Mar 20, 2026

implement proof stack for Nat rewrite rules
felipeperet
committed

Commits on Mar 27, 2026

Commits on Apr 1, 2026

emit precise proof steps for reorder operations, remove ac_rfl fallback and add testOptimize support for proof reconstruction
felipeperet
committed
Merge branch 'main' into feat/proof-reconstruction-rewrite
felipeperet
authored
proof reconstruction for propositional equality goals with forall binders
felipeperet
committed

Commits on Apr 2, 2026

exact proofStep and proof reconstruction for LE, LT, Not False, and Bool.not
felipeperet
committed

Commits on Apr 3, 2026

proof reconstruction for eliminated forall binders and Nat.succ normalization
felipeperet
committed

Commits on Apr 7, 2026

proof reconstruction for eq_self, Nat.pred, and P = True goals
felipeperet
committed

Commits on Apr 10, 2026

Commits on Apr 20, 2026

infrastructure for optimizeRecFun
felipeperet
committed

Commits on Apr 21, 2026

proof reconstruction for recursive function equivalence
felipeperet
committed

Commits on Apr 22, 2026

proof reconstruction for recursive function equivalence via local proof stacks
felipeperet
committed