## Stream: Coq users

### Topic: proving invariance of a function under reordering lists

#### Sam van G (Feb 19 2022 at 08:00):

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.

#### Paolo Giarrusso (Feb 19 2022 at 09:22):

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

#### Paolo Giarrusso (Feb 19 2022 at 09:23):

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

#### Paolo Giarrusso (Feb 19 2022 at 09:27):

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.

#### Paolo Giarrusso (Feb 19 2022 at 09:29):

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

#### Paolo Giarrusso (Feb 19 2022 at 09:33):

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

#### Sam van G (Feb 19 2022 at 10:46):

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!

#### Paolo Giarrusso (Feb 19 2022 at 13:59):

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

#### Paolo Giarrusso (Feb 19 2022 at 14:15):

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?

#### Alexander Gryzlov (Feb 19 2022 at 18:22):

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.

#### Pierre Castéran (Feb 19 2022 at 19:41):

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

#### Paolo Giarrusso (Feb 19 2022 at 22:32):

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

#### Alexander Gryzlov (Feb 19 2022 at 23:15):

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

#### Alexander Gryzlov (Feb 19 2022 at 23:27):

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.

#### Sam van G (Feb 20 2022 at 10:17):

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: Sep 26 2023 at 12:02 UTC