algebra.mlw 4.35 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Apr 20, 2012 2 3 4 ``````(** {1 Basic Algebra Theories} *) (** {2 Associativity} *) `````` MARCHE Claude committed Apr 19, 2012 5 `````` `````` Andrei Paskevich committed Dec 22, 2017 6 ``````module Assoc `````` 7 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 8 `````` type t `````` Andrei Paskevich committed Jun 29, 2011 9 `````` function op t t : t `````` Andrei Paskevich committed Jun 21, 2010 10 `````` axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z) `````` 11 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 12 13 ``````end `````` MARCHE Claude committed Apr 20, 2012 14 15 ``````(** {2 Commutativity} *) `````` Andrei Paskevich committed Dec 22, 2017 16 ``````module Comm `````` 17 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 18 `````` type t `````` Andrei Paskevich committed Jun 29, 2011 19 `````` function op t t : t `````` Andrei Paskevich committed Jun 21, 2010 20 `````` axiom Comm : forall x y : t. op x y = op y x `````` 21 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 22 23 ``````end `````` MARCHE Claude committed Apr 20, 2012 24 25 ``````(** {2 Associativity and Commutativity} *) `````` Andrei Paskevich committed Dec 22, 2017 26 ``````module AC `````` 27 `````` `````` Andrei Paskevich committed Jun 14, 2018 28 29 `````` clone export Assoc with axiom Assoc clone export Comm with type t = t, function op = op, axiom Comm `````` Andrei Paskevich committed Aug 20, 2015 30 `````` meta AC function op `````` 31 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 32 33 ``````end `````` 34 ``````(** {2 Monoids} *) `````` MARCHE Claude committed Apr 20, 2012 35 `````` `````` Andrei Paskevich committed Dec 22, 2017 36 ``````module Monoid `````` MARCHE Claude committed Oct 19, 2010 37 `````` `````` Andrei Paskevich committed Jun 14, 2018 38 `````` clone export Assoc with axiom Assoc `````` Jean-Christophe Filliatre committed Feb 06, 2012 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 committed Oct 19, 2010 42 `````` `````` 43 ``````end `````` MARCHE Claude committed Oct 19, 2010 44 `````` `````` 45 ``````(** {2 Commutative Monoids} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 46 `````` `````` Andrei Paskevich committed Dec 22, 2017 47 ``````module CommutativeMonoid `````` Jean-Christophe Filliâtre committed Mar 23, 2010 48 `````` `````` Andrei Paskevich committed Jun 14, 2018 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 `````` Andrei Paskevich committed Aug 20, 2015 51 `````` meta AC function op `````` 52 53 54 55 56 `````` end (** {2 Groups} *) `````` Andrei Paskevich committed Dec 22, 2017 57 ``````module Group `````` 58 `````` `````` Andrei Paskevich committed Jun 14, 2018 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 `````` MARCHE Claude committed Sep 04, 2011 63 `````` `````` MARCHE Claude committed Apr 20, 2012 64 ``````(*** `````` MARCHE Claude committed Sep 04, 2011 65 `````` lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y `````` MARCHE Claude committed Sep 05, 2011 66 ``````*) `````` MARCHE Claude committed Sep 04, 2011 67 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 68 69 ``````end `````` 70 ``````(** {2 Commutative Groups} *) `````` MARCHE Claude committed Apr 20, 2012 71 `````` `````` Andrei Paskevich committed Dec 22, 2017 72 ``````module CommutativeGroup `````` 73 `````` `````` Andrei Paskevich committed Jun 14, 2018 74 75 `````` clone export Group with axiom . clone export Comm with type t = t, function op = op, axiom Comm `````` Andrei Paskevich committed Aug 20, 2015 76 `````` meta AC function op `````` 77 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 78 79 ``````end `````` MARCHE Claude committed Apr 20, 2012 80 81 ``````(** {2 Rings} *) `````` Andrei Paskevich committed Dec 22, 2017 82 ``````module Ring `````` 83 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 84 `````` type t `````` Jean-Christophe Filliatre committed Feb 06, 2012 85 `````` constant zero : t `````` Andrei Paskevich committed Jun 29, 2011 86 87 88 `````` function (+) t t : t function (-_) t : t function (*) t t : t `````` Jean-Christophe Filliâtre committed Mar 23, 2010 89 `````` `````` Andrei Paskevich committed Aug 20, 2015 90 91 92 `````` clone export CommutativeGroup with type t = t, constant unit = zero, function op = (+), `````` Andrei Paskevich committed Jun 14, 2018 93 94 `````` function inv = (-_), axiom . `````` Jean-Christophe Filliâtre committed Mar 23, 2010 95 `````` `````` Andrei Paskevich committed Jun 14, 2018 96 `````` clone Assoc as MulAssoc with type t = t, function op = (*), axiom Assoc `````` Jean-Christophe Filliâtre committed Mar 23, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 100 101 102 `````` end `````` MARCHE Claude committed Apr 20, 2012 103 104 ``````(** {2 Commutative Rings} *) `````` Andrei Paskevich committed Dec 22, 2017 105 ``````module CommutativeRing `````` 106 `````` `````` Andrei Paskevich committed Jun 14, 2018 107 108 `````` clone export Ring with axiom . clone Comm as MulComm with type t = t, function op = (*), axiom Comm `````` Andrei Paskevich committed Aug 20, 2015 109 `````` meta AC function (*) `````` 110 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 111 112 ``````end `````` MARCHE Claude committed Apr 20, 2012 113 114 ``````(** {2 Commutative Rings with Unit} *) `````` Andrei Paskevich committed Dec 22, 2017 115 ``````module UnitaryCommutativeRing `````` 116 `````` `````` Andrei Paskevich committed Jun 14, 2018 117 `````` clone export CommutativeRing with axiom . `````` Jean-Christophe Filliatre committed Feb 06, 2012 118 `````` constant one : t `````` Jean-Christophe Filliâtre committed Mar 23, 2010 119 `````` axiom Unitary : forall x:t. one * x = x `````` Andrei Paskevich committed Oct 25, 2010 120 `````` axiom NonTrivialRing : zero <> one `````` 121 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 122 123 ``````end `````` MARCHE Claude committed Apr 20, 2012 124 125 ``````(** {2 Ordered Commutative Rings} *) `````` Andrei Paskevich committed Dec 22, 2017 126 ``````module OrderedUnitaryCommutativeRing `````` 127 `````` `````` Andrei Paskevich committed Jun 14, 2018 128 `````` clone export UnitaryCommutativeRing with axiom . `````` Andrei Paskevich committed Aug 20, 2015 129 `````` `````` Andrei Paskevich committed Jun 29, 2011 130 `````` predicate (<=) t t `````` Andrei Paskevich committed Aug 20, 2015 131 `````` `````` Andrei Paskevich committed Jun 14, 2018 132 133 `````` clone export relations.TotalOrder with type t = t, predicate rel = (<=), axiom . `````` Andrei Paskevich committed Oct 26, 2010 134 `````` `````` Andrei Paskevich committed Dec 14, 2011 135 136 `````` axiom ZeroLessOne : zero <= one `````` Jean-Christophe Filliatre committed Jun 21, 2011 137 `````` axiom CompatOrderAdd : `````` Jean-Christophe Filliatre committed May 09, 2011 138 `````` forall x y z : t. x <= y -> x + z <= y + z `````` Andrei Paskevich committed Aug 20, 2015 139 `````` `````` Jean-Christophe Filliatre committed Jun 21, 2011 140 `````` axiom CompatOrderMult : `````` Jean-Christophe Filliatre committed May 09, 2011 141 `````` forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` 142 `````` `````` Andrei Paskevich committed Oct 26, 2010 143 144 ``````end `````` MARCHE Claude committed Apr 20, 2012 145 146 ``````(** {2 Field theory} *) `````` Andrei Paskevich committed Dec 22, 2017 147 ``````module Field `````` 148 `````` `````` Andrei Paskevich committed Jun 14, 2018 149 `````` clone export UnitaryCommutativeRing with axiom . `````` Andrei Paskevich committed Aug 20, 2015 150 `````` `````` Andrei Paskevich committed Jun 29, 2011 151 `````` function inv t : t `````` Andrei Paskevich committed Aug 20, 2015 152 `````` `````` Andrei Paskevich committed Jun 21, 2010 153 `````` axiom Inverse : forall x:t. x <> zero -> x * inv x = one `````` Andrei Paskevich committed Aug 20, 2015 154 155 `````` function (-) (x y : t) : t = x + -y `````` Andrei Paskevich committed Jun 29, 2011 156 `````` function (/) (x y : t) : t = x * inv y `````` MARCHE Claude committed Jul 01, 2011 157 `````` `````` MARCHE Claude committed May 18, 2012 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) `````` MARCHE Claude committed Jul 01, 2011 167 `````` lemma assoc_mul_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 168 169 170 `````` (* todo: discard the hypothesis ? *) z <> zero -> (x*y)/z = x*(y/z) `````` MARCHE Claude committed Jul 01, 2011 171 `````` lemma assoc_div_mul: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 172 173 174 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> (x/y)/z = x/(y*z) `````` MARCHE Claude committed Jul 01, 2011 175 `````` lemma assoc_div_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 176 177 178 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 179 ``````end `````` Andrei Paskevich committed Oct 26, 2010 180 `````` `````` MARCHE Claude committed Apr 20, 2012 181 182 ``````(** {2 Ordered Fields} *) `````` Andrei Paskevich committed Dec 22, 2017 183 ``````module OrderedField `````` 184 `````` `````` Andrei Paskevich committed Jun 14, 2018 185 `````` clone export Field with axiom . `````` Andrei Paskevich committed Oct 26, 2010 186 `````` `````` Andrei Paskevich committed Jun 29, 2011 187 `````` predicate (<=) t t `````` Andrei Paskevich committed Aug 20, 2015 188 `````` `````` Andrei Paskevich committed Jun 14, 2018 189 190 `````` clone export relations.TotalOrder with type t = t, predicate rel = (<=), axiom . `````` Andrei Paskevich committed Oct 26, 2010 191 `````` `````` Andrei Paskevich committed Dec 14, 2011 192 193 `````` axiom ZeroLessOne : zero <= one `````` Andrei Paskevich committed Oct 26, 2010 194 `````` axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z `````` Andrei Paskevich committed Aug 20, 2015 195 `````` `````` Andrei Paskevich committed Jun 29, 2011 196 197 `````` axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` 198 `````` `````` Andrei Paskevich committed Oct 26, 2010 199 ``````end `````` Jean-Christophe Filliatre committed Apr 08, 2011 200 `````` `````` MARCHE Claude committed Apr 20, 2012 201 202 ``````(*** to be discussed: should we add the following lemmas, and where `````` Jean-Christophe committed Jun 16, 2011 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 *)``````