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
|
Require Import ssreflect ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Axiom finGroupType : Type.
Axiom group : finGroupType -> Type.
Axiom abelian : forall gT : finGroupType, group gT -> Prop.
Arguments abelian {_} _.
Axiom carrier : finGroupType -> Type.
Coercion carrier : finGroupType >-> Sortclass.
Axiom mem : forall gT : finGroupType, gT -> group gT -> Prop.
Arguments mem {_} _ _.
Axiom mul : forall gT : finGroupType, gT -> gT -> gT.
Arguments mul {_} _ _.
Definition centralised gT (G : group gT) (x : gT) := forall y, mul x y = mul y x.
Arguments centralised {gT} _.
Axiom b : bool.
Axiom centsP : forall (gT : finGroupType) (A B : group gT),
reflect (forall a, mem a A -> centralised B a) b.
Arguments centsP {_ _ _}.
Lemma commute_abelian (gT : finGroupType) (G : group gT)
(G_abelian : abelian G) (g g' : gT) (gG : mem g G) (g'G : mem g' G) :
mul g g' = mul g' g.
Proof.
Fail rewrite (centsP _). (* fails but without an anomaly *)
Abort.
|
