Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_1302.v Sprache: Coq

Original von: Coq^©

Set Primitive Projections.
Require Import ZArith ssreflect.

Module Test1.

Structure semigroup := SemiGroup {
  sg_car :> Type;
  sg_op : sg_car -> sg_car -> sg_car;
}.

Structure monoid := Monoid {
  monoid_car :> Type;
  monoid_op : monoid_car -> monoid_car -> monoid_car;
  monoid_unit : monoid_car;
}.

Coercion monoid_sg (X : monoid) : semigroup :=
  SemiGroup (monoid_car X) (monoid_op X).
Canonical Structure monoid_sg.

Parameter X : monoid.
Parameter x y : X.

Check (sg_op _ x y).

End Test1.

Module Test2.

Structure semigroup := SemiGroup {
  sg_car :> Type;
  sg_op : sg_car -> sg_car -> sg_car;
}.

Structure monoid := Monoid {
  monoid_car :> Type;
  monoid_op : monoid_car -> monoid_car -> monoid_car;
  monoid_unit : monoid_car;
  monoid_left_id x : monoid_op monoid_unit x = x;
}.

Coercion monoid_sg (X : monoid) : semigroup :=
  SemiGroup (monoid_car X) (monoid_op X).
Canonical Structure monoid_sg.

Canonical Structure nat_sg := SemiGroup nat plus.
Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n.

Lemma foo (x : nat) : 0 + x = x.
Proof.
apply monoid_left_id.
Qed.

End Test2.

Module Test3.

Structure semigroup := SemiGroup {
  sg_car :> Type;
  sg_op : sg_car -> sg_car -> sg_car;
}.

Structure group := Something {
  group_car :> Type;
  group_op : group_car -> group_car -> group_car;
  group_neg : group_car -> group_car;
  group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y)
}.

Coercion group_sg (X : group) : semigroup :=
  SemiGroup (group_car X) (group_op X).
Canonical Structure group_sg.

Axiom group_neg_op : forall (X : group) (x y : X),
  group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y).

Canonical Structure Z_sg := SemiGroup Z Z.add .
Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr.

Lemma foo (x y : Z) :
  sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) =
  group_neg Z_group (sg_op Z_sg x y).
Proof.
  rewrite -group_neg_op.
  reflexivity.
Qed.

End Test3.

¤ Dauer der Verarbeitung: 0.60 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.