blob: 55ef7abe405572b8b7767e37f6f99954f6f4fe22 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
Set Primitive Projections.
Require Import ZArith ssreflect.
Module Test3.
Set Primitive Projections.
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.
|
