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，但我真的很想说我的类型确实表示单项式并且乘法是真正可交换的（地图是 eq）。

我是 Coq 的新手：尝试证明这是一件合理的事情吗？

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

Answer 1

关于 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.

请注意，多项式库基于 MathComp library that is strongly related to the SSReflect extension of the Coq proof language。

最后，请注意，此库非常方便开发涉及多项式多项式的 Coq 证明，但不允许直接使用这些 Coq 数据类型进行计算 (Eval vm_compute in ...)。如果你也对这方面感兴趣，你可能还想看看依赖FMaps的CoqEAL library (and in particular its multipoly.v理论。

Answer 2

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!

确实，您的方向是对的。您使用的集合类型没有属性两个具有相同元素的集合在 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 和相关论文以了解最先进的技术。当然，继续尝试！

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

Equality of finite maps in coq (defined using map2)

proof

coq