数学课:证明Munit是它自己的否定

Question

我刚刚开始玩数学课库，我想证明以下引理：

Require Import
    MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.interfaces.canonical_names. 

Lemma Munit_is_its_own_negation `{Module R M} : Munit = - Munit.

我本来打算证明这一点的：

1. 使用right_identity：Munit = - Munit & Munit将Munit添加到右侧
2. 右侧使用left_inverse：Munit = Munit
3. 使用reflexivity。

但是，当我尝试应用rewrite <- right_inverse时，会出现以下错误：

Error:
Unable to satisfy the following constraints:
In environment:
R : Type
M : Type
Re : Equiv R
Rplus : Plus R
Rmult : Mult R
Rzero : Zero R
Rone : One R
Rnegate : Negate R
Me : Equiv M
Mop : SgOp M
Munit : MonUnit M
Mnegate : Negate M
sm : ScalarMult R M
H : Module R M

?A : "Type"

?B : "Type"

?H : "Equiv (MonUnit M)"

?op : "?A → ?B → MonUnit M"

?inv : "?A → ?B"

?RightInverse : "RightInverse ?op ?inv Munit"

为什么Coq要寻找Equiv (MonUnit M)而不是环境中的Equiv M或MonUnit M？有可能完成这个证明吗？如果是这样的话，是怎么做的？

Answer 1

Munit是参数化MonUnit类型集的一个实例。这意味着Munit本质上是一条记录(只有一个字段-- mon_unit)，但是我认为您希望有关于M类型的单元元素的声明，因为通常否定记录没有多大意义。

我认为，原则上可以让Coq解压缩Munit并做正确的事情，但如果我们能够重新描述这个引理，为什么还要挣扎呢？

Lemma mon_unit_is_its_own_negation `{Module R M} :
  mon_unit = - mon_unit.

然后一切都如你所描述的那样：

Proof.
  rewrite <- (right_identity (- mon_unit)).
  now rewrite left_inverse.
Qed.