Stream: Coq users

Topic: How to reuse code / modularize


view this post on Zulip Patrick Nicodemus (Jan 21 2023 at 17:39):

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

view this post on Zulip Paolo Giarrusso (Jan 21 2023 at 18:05):

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

view this post on Zulip Paolo Giarrusso (Jan 21 2023 at 18:08):

of course, I assume that has reasons

view this post on Zulip Paolo Giarrusso (Jan 21 2023 at 18:18):

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?

view this post on Zulip Paolo Giarrusso (Jan 21 2023 at 18:18):

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

view this post on Zulip Patrick Nicodemus (Jan 21 2023 at 19:46):

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 AA and an equivalence relation \sim on seqAseq A which respects list concatenation. the relation \sim is generated by a handful of simple rules concerning sequences of length 2\leq 2. I have a total linear order << on AA and I am trying to prove that every sequence in seqAseq A is \sim-equivalent to a <<-ordered sequence by repeatedly rewriting according to the laws which generate \sim, oriented in a certain order

view this post on Zulip Patrick Nicodemus (Jan 21 2023 at 19:47):

I call it a "sorting algorithm" because it very much resembles a bubblesort, it's structurally quite similar

view this post on Zulip Paolo Giarrusso (Jan 23 2023 at 07:18):

coming back to this... Here's a few ideas, sorted from more shallow to a bit less shallow:

view this post on Zulip Patrick Nicodemus (Jan 24 2023 at 16:06):

Thank you!


Last updated: Oct 04 2023 at 23:01 UTC