I often have difficulty turning a long verbose simple proof into a simpler shorter one that relies on a few basic reusable building blocks, does anybody have suggestions to help with this?
The other day I wrote two proofs https://github.com/patrick-nicodemus/category-theory/blob/simplex/Instance/Simplex/CanonicalFactorization.v,
sort_no_obj'_preserves_well_formed and
sort_no_obj'_preserves_cod, which are very elementary throughout, I think there should be a way to make them more compact
in this example, first, can sort_no_obj
be made into a reusable generic sorting algorithm? It seems not, because it sometimes modifies elements by +/-1 — so even the name "sorting algorithm" is surprising
of course, I assume that has reasons
but my first strategy to extract reusable blocks from proofs is to extract reusable blocks from definitions if possible. Can some helpers be extracted from the algorithm? Would it make sense to extract something like a "compare and transform elements" function compare_ sd_no_obj : sd_no_obj -> sd_no_obj -> seq sd_no_obj
, which would sort the two keys or return the empty sequence if they're equal?
Otherwise, I count ~10 matches in sort_no_obj'
, so I'd expect at least ~10 direct matches in direct proofs about it — maybe you can prove "helper properties" directly, and your top-level statements need not unfold sort_no_obj'
and could have simpler proofs, but you're right that it's probably hard
Paolo Giarrusso said:
in this example, first, can
sort_no_obj
be made into a reusable generic sorting algorithm? It seems not, because it sometimes modifies elements by +/-1 — so even the name "sorting algorithm" is surprising
yeah hahaha I see why that's confusing. I am not sure what the right level of generality is here, but as a first attempt to describe a more general setting in which this works,
I have a set and an equivalence relation on which respects list concatenation. the relation is generated by a handful of simple rules concerning sequences of length . I have a total linear order on and I am trying to prove that every sequence in is -equivalent to a -ordered sequence by repeatedly rewriting according to the laws which generate , oriented in a certain order
I call it a "sorting algorithm" because it very much resembles a bubblesort, it's structurally quite similar
coming back to this... Here's a few ideas, sorted from more shallow to a bit less shallow:
sort_no_obj'
. If you use this a lot on a function, tools like Function
and Equations
have specific tactics that can be more expressive. However, that won't change the substance of the proof, just shorten the scripts (sometimes, significantly).compare_ sd_no_obj
above) to reason about them separatelyinversion
. This is a standard technique for syntactic/combinatorial proofs, that appears in term rewriting systems, with applications in programming languages and logic. It should be easy to prove that your function produces a valid rewrite sequence. Proving this produces a normal form doesn't become immediate, but it might follow similarly to bubblesort — especially if you can find a "termination metric".Thank you!
Last updated: Oct 13 2024 at 01:02 UTC