3 ms·
This is a common criticism of tactic based proofs, but the style that's being adopted more and more involves heavy use of proof automation which allows fairly m
by p0llard 6y ago
This is a common criticism of tactic based proofs, but the style that's being adopted more and more involves heavy use of proof automation which allows fairly major changes to be made without breaking the proof script.
- zozbot234 6y agoFrom this POV, proof automation just enables bigger proof steps. Of course, sometimes the inputs to the "automation" are enough to disambiguate the logical step on their own (e.g. whenever a lemma is proved in a single "auto" step, though this is far from a novel approach!) but declarative proofs are nonetheless a more consistent solution to this issue.