algebra.mlw 4.35 KB
Newer Older
1

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

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

6
module Assoc
7

8
  type t
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
module Comm
17

18
  type t
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
module AC
27

28 29
  clone export Assoc with axiom Assoc
  clone export Comm with type t = t, function op = op, axiom Comm
30
  meta AC function op
31

32 33
end

34
(** {2 Monoids} *)
35

36
module Monoid
37

38
  clone export Assoc with axiom 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
42

43
end
44

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

47
module CommutativeMonoid
48

49 50
  clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
  clone export Comm with type t = t, function op = op, axiom Comm
51
  meta AC function op
52 53 54 55 56

end

(** {2 Groups} *)

57
module Group
58

59
  clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
60 61 62
  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
module CommutativeGroup
73

74 75
  clone export Group with axiom .
  clone export Comm with type t = t, function op = op, axiom Comm
76
  meta AC function op
77

78 79
end

80 81
(** {2 Rings} *)

82
module Ring
83

84
  type t
85
  constant zero : t
86 87 88
  function (+) t t : t
  function (-_) t : t
  function (*) t t : t
89

90 91 92
  clone export CommutativeGroup with type t = t,
                                constant unit = zero,
                                function op = (+),
93 94
                                function inv = (-_),
                                axiom .
95

96
  clone Assoc as MulAssoc with type t = t, function op = (*), axiom Assoc
97

98 99
  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
100 101 102

end

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

105
module CommutativeRing
106

107 108
  clone export Ring with axiom .
  clone Comm as MulComm with type t = t, function op = (*), axiom Comm
109
  meta AC function (*)
110

111 112
end

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

115
module UnitaryCommutativeRing
116

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

122 123
end

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

126
module OrderedUnitaryCommutativeRing
127

128
  clone export UnitaryCommutativeRing with axiom .
129

130
  predicate (<=) t t
131

132 133
  clone export relations.TotalOrder with
    type t = t, predicate rel = (<=), axiom .
134

135 136
  axiom ZeroLessOne : zero <= one

137
  axiom CompatOrderAdd  :
138
    forall x y z : t. x <= y -> x + z <= y + z
139

140
  axiom CompatOrderMult :
141
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
142

143 144
end

145 146
(** {2 Field theory} *)

147
module Field
148

149
  clone export UnitaryCommutativeRing with axiom .
150

151
  function inv t : t
152

153
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
154 155

  function (-) (x y : t) : t = x + -y
156
  function (/) (x y : t) : t = x * inv y
MARCHE Claude's avatar
MARCHE Claude committed
157

158 159 160 161 162 163 164 165 166
  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)

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

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

175
  lemma assoc_div_div: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
176 177 178
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y

179
end
180

181 182
(** {2 Ordered Fields} *)

183
module OrderedField
184

185
  clone export Field with axiom .
186

187
  predicate (<=) t t
188

189 190
  clone export relations.TotalOrder with
    type t = t, predicate rel = (<=), axiom .
191

192 193
  axiom ZeroLessOne : zero <= one

194
  axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
195

196 197
  axiom CompatOrderMult :
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
198

199
end
200

201 202
(***
 to be discussed: should we add the following lemmas, and where
Jean-Christophe's avatar
Jean-Christophe committed
203 204 205 206 207 208 209

  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
*)