Hi! I've now twice run into the following "design" problem with a proof assistant, and the question is a bit hard to Google.

*Short version:* how to rewrite terms in an abelian monoid in Coq, if the terms are given as lists?

*More detailed version:* I have a type `A`

and a function `m : A -> A -> nat`

. From this, I define a function `f : list A -> nat`

by folding `m`

, so `f([]) := 0`

and `f(a :: as) := m a f(as)`

. It is straightforward to prove for my examples that `m`

is commutative, i.e., `m a b = m b a`

for all a, b of type A. Using this fact, I want to prove that f is invariant under re-orderings of the list. More precisely, I want to show that if `as`

and `bs`

are two lists of A's that have the same element count, i.e., `count_occ a as = count_occ a bs`

for all a of type A, then `f as = f bs`

.

*Simple instance to see why it's true:* take A to be nat, and m to be +, then f is the sum function on lists, and the sum of any list only depends on the occurrence count of the list.

*My thoughts so far:* I think I can prove this by showing first that if two lists have the same occurrence count, then one can be obtained from the other by a sequence of swaps of pairs of elements, and then doing an induction on the number of required swaps? But I wonder if there is a way to use an existing library for this? `m`

equips `A`

with an abelian monoid structure. I found the abelian monoid type class, but I'm not sure how to use it to prove what I want.

The proof you sketch with occurrence counts and counting swaps does not feel ideal for Coq. Coq’s stdlib defines an inductive type of proofs that a list is a permutation of another list, and structural induction on such proofs will remember “why”.

Using counts means destroying the “why”, but in a formalized proof you’d have to reconstruct it.

Concretely, https://gitlab.mpi-sws.org/iris/stdpp/-/blob/ebfb79dd8b7d0a1b2d317037cb13969adfa9306c/theories/list.v#L4424 has a general proof that foldr f respects permutations under suitable “commutativity” of f (not exactly commutativity), and that theorem should specialize to what you want, else offer an idea.

And that proof starts indeed by structural induction on proofs of permutations.

But you probably shouldn’t use stdpp if you’re working with abelian monoids; most people recommend math-comp for mathematicians.

Thanks for the link! I'll try to take inspiration from that code.

I also found an implementation of multi-sets somewhere, which is another way of stating the same idea: if two lists have the same underlying multi-set then their "sum" under any abelian monoid operation is equal. Maybe this sounds familiar to somebody?

Here, "abelian monoids" was just my mathematical way of phrasing the fact that I have an associative & commutative operation, not much deep math going on (yet). But if anyone reading this has an idea how to import the fact I'm looking for from math-comp that would of course also be interesting!

If you're not aiming for advanced maths, maybe stdpp is for you, dunno :-). There was discussion of recommendations in the other thread anyway :-).

Depending on your background, Software Foundations might be helpful to learn more about structural induction, also in practice.

Finally, as unsolicited advice: I forgot to say that your proof strategy is probably common in "mainstream mathematics". But I think that's because mainstream mathematics seems to use induction on naturals almost exclusively. I suspect that structural induction might be a 20th century innovation?

Sam van G said:

More detailed version:I have a type`A`

and a function`m : A -> A -> nat`

. From this, I define a function`f : list A -> nat`

by folding`m`

, so`f([]) := 0`

and`f(a :: as) := m a f(as)`

. It is straightforward to prove for my examples that`m`

is commutative, i.e.,`m a b = m b a`

for all a, b of type A. Using this fact, I want to prove that f is invariant under re-orderings of the list. More precisely, I want to show that if`as`

and`bs`

are two lists of A's that have the same element count, i.e.,`count_occ a as = count_occ a bs`

for all a of type A, then`f as = f bs`

.

I don't get how `f`

is defined here, looks like `m`

should have the type `nat -> nat -> nat`

from the constraints.

You may have to assume `m: nat->nat->nat`

is associative too.

For instance, if I define `m x y := S x * S y`

, `m`

is clearly commutative, but `f (2::3::1::nil) = 39`

and `f (3::2::1::nil)= 40`

.

With commutativity and associativity of `m`

, you can prove your lemma with Stdlib's `Permutation`

.

```
Goal forall l l', Permutation l l' -> f l = f l'.
induction 1.
(* 4 simple cases , the third one applies associativity of m *)
Qed.
```

I should have mentioned that stdpp also uses the stdlib's `Permutation`

.

If I understand the whole thing correctly, using mathcomp you'd express your monoid as a pair of `Monoid.law`

+ `Monoid.com_law`

canonical instances, encode your function `f`

using the "big operator" notation instead of a manual fold, and then what you want is just the following lemma: https://math-comp.github.io/htmldoc/mathcomp.ssreflect.bigop.html#perm_big

In general, plugging in mathcomp for the purpose of simplifying a few reordering proofs is probably an overkill, but if you have to consistently reason about such fold-style functions and their interactions with algebraic structures then mathcomp and specifically the bigop machinery might be worth looking into.

Thanks @Alexander Gryzlov, I also came to the conclusion yesterday after I asked the question that "bigop" looks like the right tool for this in general! But I have not yet learned how to use math-comp and this notation in particular, so for now I'm probably going to stick with a more *ad hoc* proof, although all this is motivating me to learn how to use math-comp at some point...

And indeed, @Pierre Castéran, associativity of the operation is needed too, I forgot to mention that in my first message. I'll have a look at `Permutation`

too.

Thanks for all the help.

Last updated: Jun 24 2024 at 01:01 UTC