Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: setoid_ring_module.v Sprache: Coq

Original von: Coq^©

Require Import Setoid Ring Ring_theory.

Module abs_ring.

Parameters (Coef:Set)(c0 c1 : Coef)
(cadd cmul csub: Coef -> Coef -> Coef)
(copp : Coef -> Coef)
(ceq : Coef -> Coef -> Prop)
(ceq_sym : forall x y, ceq x y -> ceq y x)
(ceq_trans : forall x y z, ceq x y -> ceq y z -> ceq x z)
(ceq_refl : forall x, ceq x x).

Add Relation Coef ceq
  reflexivity proved by ceq_refl symmetry proved by ceq_sym
  transitivity proved by ceq_trans
  as ceq_relation.

Add Morphism cadd with signature ceq ==> ceq ==> ceq as cadd_Morphism.
Admitted.

Add Morphism cmul with signature ceq ==> ceq ==> ceq as cmul_Morphism.
Admitted.

Add Morphism copp with signature ceq ==> ceq as copp_Morphism.
Admitted.

Definition cRth : ring_theory c0 c1 cadd cmul csub copp ceq.
Admitted.

Add Ring CoefRing : cRth.

End abs_ring.
Import abs_ring.

Theorem check_setoid_ring_modules :
  forall a b, ceq (cadd a b) (cadd b a).
intros.
ring.
Qed.

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.