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

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:

- 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".

Thank you!

Last updated: Oct 04 2023 at 23:01 UTC