## Stream: Coq users

### Topic: How to reuse code / modularize

#### 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

#### 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

#### Paolo Giarrusso (Jan 21 2023 at 18:08):

of course, I assume that has reasons

#### 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?

#### 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

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

#### 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

#### 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:

• your proofs seem to proceed by "functional induction"/"functional inversion" — informally, induction on the execution graph of 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).
• extracting the ~-rules from the bubblesort skeleton might be helpful (see compare_ sd_no_obj above) to reason about them separately
• it seems that preservation lemmas could be proven by showing each rewrite step preserves those properties, then lifting over the transitive closure; rewrite steps can be represented as an inductive type, which is often easier to reason about in a proof assistant, thanks also to tactics like inversion. 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".

#### Patrick Nicodemus (Jan 24 2023 at 16:06):

Thank you!

Last updated: Oct 04 2023 at 23:01 UTC