I'm reading two things at the same time<p>99 Variations on a Proof
<a href="https://press.princeton.edu/books/hardcover/9780691158839/99-variations-on-a-proof" rel="nofollow">https://press.princeton.edu/books/hardcover/9780691158839/99...</a><p>and the newly published paper<p>Draft, Sketch, and Prove: Guiding Formal Theorem Provers With Informal Proofs
<a href="https://arxiv.org/pdf/2210.12283.pdf" rel="nofollow">https://arxiv.org/pdf/2210.12283.pdf</a><p>As you all know De Morgan's Laws provide great simplification of terms
to canonical forms. Application of these laws improved circuit design forever.<p>My question: Can "Irrelevance Laws" be developed in proofs so one style
of proof can be mechanically converted to another style? If so, can a system
like LEAN convert the library to canonical forms?<p>Canonical forms of proof, if they exist, and if they have the proper form,
would make it possible to develop "proof compilers" that could generate
code from (constructive) proofs. (See Ording 28, p65, of special interest).<p>Is there any reason to believe canonical forms exist? I know that judgment
towers can be expanded in various ways. Perhaps there is a mechanical
theory to put (some of) the LEAN library in "canonical form".<p>Beside the book, is there any known collection of proof transformation?