proving invariance of a function under reordering lists · Coq users

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

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

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

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?

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

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, mis 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):

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.

Stream: Coq users

Topic: proving invariance of a function under reordering lists

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