математические классы: Докажите, что 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. Добавить MUNIT в правую сторону, используя right_identity: 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 typeclass. Это означает, что 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.