coq 中有限映射的相等性（使用 map2 定义）

Question

假设我想在 Coq 中定义一种单项式。这些将是从一些有序变量集到 nat 的有限映射，例如，x²y³ 由将 x 发送到 2、y 发送到 3 的映射表示，而其他所有内容都获得默认值零。

基本定义似乎并不难：

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.

此时，我想证明以下内容：

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

我可以看到如何使用引理 Equal_mapsto_iff 证明这两个映射是 Equal，但我真的想说我的类型确实代表单项式并且乘法是真正可交换的（并且映射是 @ 987654325@)。

我对 Coq 还是很陌生：尝试证明这是合理的事情吗？

另外，我意识到这可能取决于有限映射的实现：如果 FMapList 是错误的选择，而另一个实现使这更容易，请指出这一点！

Answer 1

我可以看到如何使用引理 Equal_mapsto_iff 证明这两个映射相等，但我真的想说我的类型确实代表单项式，并且乘法是真正可交换的（并且映射是 eq）。

我对 Coq 还是很陌生：尝试证明这是合理的事情吗？

另外，我意识到这可能取决于有限地图的实现：如果 FMapList 是错误的选择，而另一个实现使这更容易，请指出我！

确实，您走在正确的轨道上。您使用的集合类型不具有两个具有相同元素的集合在 Coq 中定义相等的属性。由于这样的集合被实现为二叉树，你可能有Node(A, Node(B,C)) <> Node(Node(A,B),C)。

特别是，由于几个问题，在 Coq 中拥有一个好的“集合类型”是一项极具挑战性的任务，请参阅 anwser How to define set in coq without defining set as a list of elements 以获得更多讨论。

做正确的代数确实需要很多复杂的基础设施，@ErikMD 的指针是正确的，你应该看看 math-comp 和相关论文以了解最新技术。当然，继续尝试！

Answer 2

关于 Coq 中单项式和多元多项式的形式化，您可以考虑使用 multinomials 库。它在 OPAM 上可用：

$ opam install coq-mathcomp-multinomials

它自然地证明了与您的 mon_times_comm 引理相似的结果：

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.

请注意，多项式库是基于与SSReflect extension of the Coq proof language 密切相关的MathComp 库构建的。

最后，请注意，该库非常方便开发涉及多项式多项式的 Coq 证明，但不能直接使用这些 Coq 数据类型 (Eval vm_compute in ...) 进行计算。如果您也对这方面感兴趣，您可能还想看看CoqEAL 库（尤其是它依赖于FMaps 的multipoly.v 理论）。