stdlib/algebra.mlw

   1
   2 (** {1 Basic Algebra Theories} *)
   3
   4 (** {2 Associativity} *)
   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 end
  13
  14 (** {2 Commutativity} *)
  15
  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 end
  23
  24 (** {2 Associativity and Commutativity} *)
  25
  26 module AC
  27
  28   clone export Assoc with axiom Assoc
  29   clone export Comm with type t = t, function op = op, axiom Comm
  30   meta AC function op
  31
  32 end
  33
  34 (** {2 Monoids} *)
  35
  36 module Monoid
  37
  38   clone export Assoc with axiom Assoc
  39   constant unit : t
  40   axiom Unit_def_l : forall x:t. op unit x = x
  41   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   clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
  50   clone export Comm with type t = t, function op = op, axiom Comm
  51   meta AC function op
  52
  53 end
  54
  55 (** {2 Groups} *)
  56
  57 module Group
  58
  59   clone export Monoid with axiom Assoc, axiom Unit_def_l, axiom Unit_def_r
  60   function inv t : t
  61   axiom Inv_def_l : forall x:t. op (inv x) x = unit
  62   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 end
  69
  70 (** {2 Commutative Groups} *)
  71
  72 module CommutativeGroup
  73
  74   clone export Group with axiom .
  75   clone export Comm with type t = t, function op = op, axiom Comm
  76   meta AC function op
  77
  78 end
  79
  80 (** {2 Rings} *)
  81
  82 module Ring
  83
  84   type t
  85   constant zero : t
  86   function (+) t t : t
  87   function (-_) t : t
  88   function (*) t t : t
  89
  90   clone export CommutativeGroup with type t = t,
  91                                 constant unit = zero,
  92                                 function op = (+),
  93                                 function inv = (-_),
  94                                 axiom .
  95
  96   clone Assoc as MulAssoc with type t = t, function op = (*), axiom Assoc
  97
  98   axiom Mul_distr_l : forall x y z : t. x * (y + z) = x * y + x * z
  99   axiom Mul_distr_r : forall x y z : t. (y + z) * x = y * x + z * x
 100
 101 end
 102
 103 (** {2 Commutative Rings} *)
 104
 105 module CommutativeRing
 106
 107   clone export Ring with axiom .
 108   clone Comm as MulComm with type t = t, function op = (*), axiom Comm
 109   meta AC function (*)
 110
 111 end
 112
 113 (** {2 Commutative Rings with Unit} *)
 114
 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 end
 123
 124 (** {2 Ordered Commutative Rings} *)
 125
 126 module OrderedUnitaryCommutativeRing
 127
 128   clone export UnitaryCommutativeRing with axiom .
 129
 130   predicate (<=) t t
 131
 132   clone export relations.TotalOrder with
 133     type t = t, predicate rel = (<=), axiom .
 134
 135   axiom ZeroLessOne : zero <= one
 136
 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   meta "remove_unused:dependency" axiom CompatOrderMult, function (*)
 143
 144 end
 145
 146 (** {2 Field theory} *)
 147
 148 module Field
 149
 150   clone export UnitaryCommutativeRing with axiom .
 151
 152   function inv t : t
 153
 154   axiom Inverse : forall x:t. x <> zero -> x * inv x = one
 155
 156   function (-) (x y : t) : t = x + -y
 157   function (/) (x y : t) : t = x * inv y
 158
 159   lemma add_div :
 160     forall x y z : t. z <> zero -> (x+y)/z = x/z + y/z
 161   meta "remove_unused:dependency" lemma add_div, function (/)
 162
 163   lemma sub_div :
 164     forall x y z : t. z <> zero -> (x-y)/z = x/z - y/z
 165   meta "remove_unused:dependency" lemma sub_div, function (/)
 166
 167   lemma neg_div :
 168     forall x y : t. y <> zero -> (-x)/y = -(x/y)
 169   meta "remove_unused:dependency" lemma neg_div, function (/)
 170
 171   lemma assoc_mul_div: forall x y z:t.
 172     (* todo: discard the hypothesis ? *)
 173      z <> zero -> (x*y)/z = x*(y/z)
 174   meta "remove_unused:dependency" lemma assoc_mul_div, function (/)
 175
 176   lemma assoc_div_mul: forall x y z:t.
 177     (* todo: discard the hypothesis ? *)
 178      y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)
 179   meta "remove_unused:dependency" lemma assoc_div_mul, function (/)
 180
 181   lemma assoc_div_div: forall x y z:t.
 182     (* todo: discard the hypothesis ? *)
 183      y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y
 184   meta "remove_unused:dependency" lemma assoc_div_div, function (/)
 185
 186 end
 187
 188 (** {2 Ordered Fields} *)
 189
 190 module OrderedField
 191
 192   clone export Field with axiom .
 193
 194   predicate (<=) t t
 195
 196   clone export relations.TotalOrder with
 197     type t = t, predicate rel = (<=), axiom .
 198
 199   axiom ZeroLessOne : zero <= one
 200
 201   axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
 202
 203   axiom CompatOrderMult :
 204     forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
 205
 206 end
 207
 208 (***
 209  to be discussed: should we add the following lemmas, and where
 210
 211   lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
 212   lemma InvSquare : forall x : t. x * x = (-x) * (-x)
 213   lemma ZeroMult : forall x : t. x * zero = zero = zero * x
 214   lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
 215   lemma SquareNonNeg : forall x : t. zero <= x * x
 216 *)