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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
Require Export Crypto.Util.FixCoqMistakes.
Require Export Crypto.Util.Decidable.
Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.
Require Coq.setoid_ring.Field_theory.
Require Crypto.Tactics.Algebra_syntax.Nsatz.
Require Coq.Numbers.Natural.Peano.NPeano.
Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
Section Algebra.
Context {T:Type} {eq:T->T->Prop}.
Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
Section SingleOperation.
Context {op:T->T->T}.
Class is_associative := { associative : forall x y z, op x (op y z) = op (op x y) z }.
Context {id:T}.
Class is_left_identity := { left_identity : forall x, op id x = x }.
Class is_right_identity := { right_identity : forall x, op x id = x }.
Class monoid :=
{
monoid_is_associative : is_associative;
monoid_is_left_identity : is_left_identity;
monoid_is_right_identity : is_right_identity;
monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op;
monoid_Equivalence : Equivalence eq
}.
Global Existing Instance monoid_is_associative.
Global Existing Instance monoid_is_left_identity.
Global Existing Instance monoid_is_right_identity.
Global Existing Instance monoid_Equivalence.
Global Existing Instance monoid_op_Proper.
Context {inv:T->T}.
Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }.
Class is_right_inverse := { right_inverse : forall x, op x (inv x) = id }.
Class group :=
{
group_monoid : monoid;
group_is_left_inverse : is_left_inverse;
group_is_right_inverse : is_right_inverse;
group_inv_Proper: Proper (respectful eq eq) inv
}.
Global Existing Instance group_monoid.
Global Existing Instance group_is_left_inverse.
Global Existing Instance group_is_right_inverse.
Global Existing Instance group_inv_Proper.
Class is_commutative := { commutative : forall x y, op x y = op y x }.
Record abelian_group :=
{
abelian_group_group : group;
abelian_group_is_commutative : is_commutative
}.
Existing Class abelian_group.
Global Existing Instance abelian_group_group.
Global Existing Instance abelian_group_is_commutative.
End SingleOperation.
Section AddMul.
Context {zero one:T}. Local Notation "0" := zero. Local Notation "1" := one.
Context {opp:T->T}. Local Notation "- x" := (opp x).
Context {add:T->T->T} {sub:T->T->T} {mul:T->T->T}.
Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
Class is_left_distributive := { left_distributive : forall a b c, a * (b + c) = a * b + a * c }.
Class is_right_distributive := { right_distributive : forall a b c, (b + c) * a = b * a + c * a }.
Class ring :=
{
ring_abelian_group_add : abelian_group (op:=add) (id:=zero) (inv:=opp);
ring_monoid_mul : monoid (op:=mul) (id:=one);
ring_is_left_distributive : is_left_distributive;
ring_is_right_distributive : is_right_distributive;
ring_sub_definition : forall x y, x - y = x + opp y;
ring_mul_Proper : Proper (respectful eq (respectful eq eq)) mul;
ring_sub_Proper : Proper(respectful eq (respectful eq eq)) sub
}.
Global Existing Instance ring_abelian_group_add.
Global Existing Instance ring_monoid_mul.
Global Existing Instance ring_is_left_distributive.
Global Existing Instance ring_is_right_distributive.
Global Existing Instance ring_mul_Proper.
Global Existing Instance ring_sub_Proper.
Class commutative_ring :=
{
commutative_ring_ring : ring;
commutative_ring_is_commutative : is_commutative (op:=mul)
}.
Global Existing Instance commutative_ring_ring.
Global Existing Instance commutative_ring_is_commutative.
Class is_zero_product_zero_factor :=
{ zero_product_zero_factor : forall x y, x*y = 0 -> x = 0 \/ y = 0 }.
Class is_zero_neq_one := { zero_neq_one : zero <> one }.
Class integral_domain :=
{
integral_domain_commutative_ring : commutative_ring;
integral_domain_is_zero_product_zero_factor : is_zero_product_zero_factor;
integral_domain_is_zero_neq_one : is_zero_neq_one
}.
Global Existing Instance integral_domain_commutative_ring.
Global Existing Instance integral_domain_is_zero_product_zero_factor.
Global Existing Instance integral_domain_is_zero_neq_one.
Context {inv:T->T} {div:T->T->T}.
Class is_left_multiplicative_inverse := { left_multiplicative_inverse : forall x, x<>0 -> (inv x) * x = 1 }.
Class field :=
{
field_commutative_ring : commutative_ring;
field_is_left_multiplicative_inverse : is_left_multiplicative_inverse;
field_is_zero_neq_one : is_zero_neq_one;
field_div_definition : forall x y , div x y = x * inv y;
field_inv_Proper : Proper (respectful eq eq) inv;
field_div_Proper : Proper (respectful eq (respectful eq eq)) div
}.
Global Existing Instance field_commutative_ring.
Global Existing Instance field_is_left_multiplicative_inverse.
Global Existing Instance field_is_zero_neq_one.
Global Existing Instance field_inv_Proper.
Global Existing Instance field_div_Proper.
End AddMul.
Definition char_ge {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero).
Existing Class char_ge.
End Algebra.
Section ZeroNeqOne.
Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}.
Lemma one_neq_zero : not (eq one zero).
Proof.
intro HH; symmetry in HH. auto using zero_neq_one.
Qed.
End ZeroNeqOne.
|
