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!
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!