algebra.why 4.17 KB
Newer Older
1

2 3 4
(** {1 Basic Algebra Theories} *)

(** {2 Associativity} *)
MARCHE Claude's avatar
MARCHE Claude committed
5

6
theory Assoc
7

8
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
9
  function op t t : t
10
  axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)
11

12 13
end

14 15
(** {2 Commutativity} *)

16
theory Comm
17

18
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
19
  function op t t : t
20
  axiom Comm : forall x y : t. op x y = op y x
21

22 23
end

24 25
(** {2 Associativity and Commutativity} *)

26
theory AC
27

28 29
  clone export Assoc
  clone Comm with type t = t, function op = op
Andrei Paskevich's avatar
Andrei Paskevich committed
30
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
31

32 33
end

34
(** {2 Monoids} *)
35

36
theory Monoid
MARCHE Claude's avatar
MARCHE Claude committed
37

38
  clone export Assoc
39
  constant unit : t
40 41
  axiom Unit_def_l : forall x:t. op unit x = x
  axiom Unit_def_r : forall x:t. op x unit = x
MARCHE Claude's avatar
MARCHE Claude committed
42

43
end
MARCHE Claude's avatar
MARCHE Claude committed
44

45
(** {2 Commutative Monoids} *)
46

47
theory CommutativeMonoid
48

49 50 51 52 53 54 55 56 57 58 59 60 61 62
  clone export Monoid
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)

end

(** {2 Groups} *)

theory Group

  clone export Monoid
  function inv t : t
  axiom Inv_def_l : forall x:t. op (inv x) x = unit
  axiom Inv_def_r : forall x:t. op x (inv x) = unit
63

64
(***
65
  lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y
66
*)
67

68 69
end

70
(** {2 Commutative Groups} *)
71

72
theory CommutativeGroup
73

74
  clone export Group
Andrei Paskevich's avatar
Andrei Paskevich committed
75 76
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
77

78 79
end

80 81
(** {2 Rings} *)

82
theory Ring
83

84
  type t
85
  constant zero : t
Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88
  function (+) t t : t
  function (-_) t : t
  function (*) t t : t
89 90

  clone CommutativeGroup with type t = t,
91
                              constant unit = zero,
Andrei Paskevich's avatar
Andrei Paskevich committed
92 93
                              function op = (+),
                              function inv = (-_)
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95
  clone Assoc with type t = t, function op = (*)
96

97 98
  axiom Mul_distr_l : forall x y z : t. x * (y + z) = x * y + x * z
  axiom Mul_distr_r : forall x y z : t. (y + z) * x = y * x + z * x
99

Andrei Paskevich's avatar
Andrei Paskevich committed
100
  function (-) (x y : t) : t = x + -y
101

102 103
end

104 105
(** {2 Commutative Rings} *)

106
theory CommutativeRing
107

108
  clone export Ring
Andrei Paskevich's avatar
Andrei Paskevich committed
109 110
  clone Comm with type t = t, function op = (*)
  meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*)
111

112 113
end

114 115
(** {2 Commutative Rings with Unit} *)

116
theory UnitaryCommutativeRing
117

118
  clone export CommutativeRing
119
  constant one : t
120
  axiom Unitary : forall x:t. one * x = x
121
  axiom NonTrivialRing : zero <> one
122

123 124
end

125 126
(** {2 Ordered Commutative Rings} *)

127
theory OrderedUnitaryCommutativeRing
128

129
  clone export UnitaryCommutativeRing
Andrei Paskevich's avatar
Andrei Paskevich committed
130 131 132
  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134 135
  axiom ZeroLessOne : zero <= one

136
  axiom CompatOrderAdd  :
137
    forall x y z : t. x <= y -> x + z <= y + z
138
  axiom CompatOrderMult :
139
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
140

141 142
end

143 144
(** {2 Field theory} *)

145
theory Field
146

MARCHE Claude's avatar
MARCHE Claude committed
147
  clone export UnitaryCommutativeRing
Andrei Paskevich's avatar
Andrei Paskevich committed
148
  function inv t : t
149
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
Andrei Paskevich's avatar
Andrei Paskevich committed
150
  function (/) (x y : t) : t = x * inv y
MARCHE Claude's avatar
MARCHE Claude committed
151

152 153 154 155 156 157 158 159 160
  lemma add_div :
    forall x y z : t. z <> zero -> (x+y)/z = x/z + y/z

  lemma sub_div :
    forall x y z : t. z <> zero -> (x-y)/z = x/z - y/z

  lemma neg_div :
    forall x y : t. y <> zero -> (-x)/y = -(x/y)

MARCHE Claude's avatar
MARCHE Claude committed
161
  lemma assoc_mul_div: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
162 163 164
    (* todo: discard the hypothesis ? *)
     z <> zero -> (x*y)/z = x*(y/z)

MARCHE Claude's avatar
MARCHE Claude committed
165
  lemma assoc_div_mul: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
166 167 168
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)

MARCHE Claude's avatar
MARCHE Claude committed
169
  lemma assoc_div_div: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
170 171 172
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y

173
end
174

175 176
(** {2 Ordered Fields} *)

177
theory OrderedField
178

179 180
  clone export Field

Andrei Paskevich's avatar
Andrei Paskevich committed
181 182 183
  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)
184

Andrei Paskevich's avatar
Andrei Paskevich committed
185 186
  axiom ZeroLessOne : zero <= one

187
  axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
Andrei Paskevich's avatar
Andrei Paskevich committed
188 189
  axiom CompatOrderMult :
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
190

191
end
192

193 194
(***
 to be discussed: should we add the following lemmas, and where
Jean-Christophe's avatar
Jean-Christophe committed
195 196 197 198 199 200 201

  lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
  lemma InvSquare : forall x : t. x * x = (-x) * (-x)
  lemma ZeroMult : forall x : t. x * zero = zero = zero * x
  lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
  lemma SquareNonNeg : forall x : t. zero <= x * x
*)