Mathe-Klassen: Beweisen Sie, dass MUNIT ihre eigene Negation ist

Question

ich mit der Mathe-Klassen-Bibliothek spielen gerade begonnen haben um und ich würde möchte folgende Lemma beweisen:

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

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

Ich hatte geplant, zu beweisen dies etwa so:

1. hinzufügen MUNIT auf der rechten Seite mit right_identity: Munit = - Munit & Munit
2. verwenden left_inverse auf der rechten Seite: Munit = Munit
3. Verwenden Sie reflexivity.

aber wenn ich versuche, rewrite <- right_inverse anzuwenden, erhalte ich die folgende Fehlermeldung:

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" 

Warum sucht Coq für eine Equiv (MonUnit M) anstatt nur einem Equiv M oder MonUnit M, die in der Umwelt sind? Ist es möglich, diesen Beweis zu vervollständigen? Wenn das so ist, wie?

Answer 1

Munit ist eine Instanz der parametrierten MonUnit Typklasse. Das bedeutet, Munit ist im Wesentlichen ein Datensatz (mit genau einem Feld - mon_unit), aber ich denke, Sie möchten Ihre Aussage über das Einheitselement vom Typ M haben, da es nicht viel Sinn macht, einen Datensatz in der Regel zu negieren.

Ich glaube, es ist möglich, im Prinzip zu Coq Munit zu machen auspacken und das Richtige tun, aber warum Kampf, wenn wir nur das Lemma neu formulieren:

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

Dann geht alles so wie du beschrieben hast :

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