Stream: Coq users

Topic: proving invariance of a function under reordering lists


view this post on Zulip 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.

view this post on Zulip 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”.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 19 2022 at 09:29):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 :-).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 19 2022 at 22:32):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC