Equality of finite maps in coq (defined using map2)

Question

Suppose I want to define a type of Monomials in Coq. These would be finite maps from some ordered set of variables to nat where, say, x²y³ is represented by the map that sends x to 2, y to 3 and where everything else gets the default value, zero.

The basic definitions don't seem so hard:

Require Import
  Coq.FSets.FMapFacts
  Coq.FSets.FMapList
  Coq.Structures.OrderedType.

Module Monomial (K : OrderedType).
  Module M := FMapList.Make(K).

  Module P := WProperties_fun K M.
  Module F := P.F.

  Definition Var : Type := M.key.
  Definition Monomial : Type := M.t nat.

  Definition mon_one : Monomial := M.empty _.

  Definition add_at (a : option nat) (b : option nat) : option nat :=
    match a, b with
      | Some aa, Some bb => Some (aa + bb)
      | Some aa, None => Some aa
      | None, Some bb => Some bb
      | None, None => None
    end.

  Definition mon_times (M : Monomial) (M' : Monomial) : Monomial :=
    M.map2 add_at M M'.

End Monomial.

At this point, I'd like to prove something like:

Lemma mon_times_comm : forall M M', mon_times M M' = mon_times M' M.

I can see how to prove that the two maps are Equal using the lemma Equal_mapsto_iff, but I'd really like to say that my type really represents monomials and that multiplication is genuinely commutative (and the maps are eq).

I'm pretty new to Coq: is this a reasonable thing to try to prove?

Also, I realise that this might depend on the finite map implementation: if FMapList was the wrong choice and another implementation makes this easier, please point me at that!

Answer 1

I can see how to prove that the two maps are Equal using the lemma Equal_mapsto_iff, but I'd really like to say that my type really represents monomials and that multiplication is genuinely commutative (and the maps are eq).

I'm pretty new to Coq: is this a reasonable thing to try to prove?

Also, I realise that this might depend on the finite map implementation: if FMapList was the wrong choice and another implementation makes this easier, please point me at that!

Indeed, you are on the right track. The set type you are using doesn't have the property that two sets with the same elements are definitionally equal in Coq. As such sets are implemented as binary trees you may have Node(A, Node(B,C)) <> Node(Node(A,B),C).

In particular, having a good "set type" is an extremely challenging task in Coq due to several issues, see the anwser How to define set in coq without defining set as a list of elements for a bit more of discussion.

Doing proper algebra does indeed require a lot of complex infrastructure, @ErikMD's pointer is the right one, you should have a look at math-comp and related papers to get an understanding on the state of the art. Of course, keep experimenting!

Answer 2

Regarding the formalization of monomials and multivariate polynomials in Coq, you could consider using the multinomials library. It is available on OPAM:

$ opam install coq-mathcomp-multinomials

and it naturally proves a similar result to your mon_times_comm lemma:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import choice finfun tuple fintype ssralg bigop.
From SsrMultinomials Require Import freeg mpoly.

Lemma test1 (n : nat) (m1 m2 : 'X_{1..n}) : (m1 + m2 = m2 + m1)%MM.
Proof.
move=> *.
by rewrite addmC.
Qed.

Lemma test2 (n : nat) (R : comRingType) (p q : {mpoly R[n]}) :
  (p * q = q * p)%R.
Proof.
move=> *.
by rewrite mpoly_mulC.
Qed.

Note that the multinomials library is built upon the MathComp library that is strongly related to the SSReflect extension of the Coq proof language.

Finally, note that this library is very convenient to develop Coq proofs involving multinomial polynomials, but doesn't directly allow computing with these Coq datatypes (Eval vm_compute in ...). If you are also interested in that aspect, you may also want to take a look at the CoqEAL library (and in particular its multipoly.v theory that relies on FMaps).