algebra.why 4.17 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 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 6 ``````theory 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} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 16 ``````theory 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} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 26 ``````theory AC `````` 27 `````` `````` 28 29 `````` clone export Assoc clone Comm with type t = t, function op = op `````` Andrei Paskevich committed Jun 29, 2011 30 `````` meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) `````` 31 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 32 33 ``````end `````` 34 ``````(** {2 Monoids} *) `````` MARCHE Claude committed Apr 20, 2012 35 `````` `````` 36 ``````theory Monoid `````` MARCHE Claude committed Oct 19, 2010 37 `````` `````` 38 `````` clone export 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 `````` `````` 47 ``````theory CommutativeMonoid `````` Jean-Christophe Filliâtre committed Mar 23, 2010 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 `````` 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 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 72 ``````theory CommutativeGroup `````` 73 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 74 `````` clone export Group `````` Andrei Paskevich committed Jun 29, 2011 75 76 `````` clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) `````` 77 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 78 79 ``````end `````` MARCHE Claude committed Apr 20, 2012 80 81 ``````(** {2 Rings} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 82 ``````theory 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 90 `````` clone CommutativeGroup with type t = t, `````` Jean-Christophe Filliatre committed Feb 06, 2012 91 `````` constant unit = zero, `````` Andrei Paskevich committed Jun 29, 2011 92 93 `````` function op = (+), function inv = (-_) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 94 `````` `````` Andrei Paskevich committed Jun 29, 2011 95 `````` clone Assoc with type t = t, function op = (*) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 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 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 99 `````` `````` Andrei Paskevich committed Jun 29, 2011 100 `````` function (-) (x y : t) : t = x + -y `````` 101 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 102 103 ``````end `````` MARCHE Claude committed Apr 20, 2012 104 105 ``````(** {2 Commutative Rings} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 106 ``````theory CommutativeRing `````` 107 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 108 `````` clone export Ring `````` Andrei Paskevich committed Jun 29, 2011 109 110 `````` clone Comm with type t = t, function op = (*) meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*) `````` 111 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 112 113 ``````end `````` MARCHE Claude committed Apr 20, 2012 114 115 ``````(** {2 Commutative Rings with Unit} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 116 ``````theory UnitaryCommutativeRing `````` 117 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 118 `````` clone export CommutativeRing `````` Jean-Christophe Filliatre committed Feb 06, 2012 119 `````` constant one : t `````` Jean-Christophe Filliâtre committed Mar 23, 2010 120 `````` axiom Unitary : forall x:t. one * x = x `````` 121 `````` axiom NonTrivialRing : zero <> one `````` 122 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 123 124 ``````end `````` MARCHE Claude committed Apr 20, 2012 125 126 ``````(** {2 Ordered Commutative Rings} *) `````` Andrei Paskevich committed Oct 26, 2010 127 ``````theory OrderedUnitaryCommutativeRing `````` 128 `````` `````` Andrei Paskevich committed Oct 26, 2010 129 `````` clone export UnitaryCommutativeRing `````` Andrei Paskevich committed Jun 29, 2011 130 131 132 `````` predicate (<=) t t predicate (>=) (x y : t) = y <= x clone export relations.TotalOrder with type t = t, predicate rel = (<=) `````` Andrei Paskevich committed Oct 26, 2010 133 `````` `````` Andrei Paskevich committed Dec 14, 2011 134 135 `````` axiom ZeroLessOne : zero <= one `````` Jean-Christophe Filliatre committed Jun 21, 2011 136 `````` axiom CompatOrderAdd : `````` Jean-Christophe Filliatre committed May 09, 2011 137 `````` forall x y z : t. x <= y -> x + z <= y + z `````` Jean-Christophe Filliatre committed Jun 21, 2011 138 `````` axiom CompatOrderMult : `````` Jean-Christophe Filliatre committed May 09, 2011 139 `````` forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` 140 `````` `````` Andrei Paskevich committed Oct 26, 2010 141 142 ``````end `````` MARCHE Claude committed Apr 20, 2012 143 144 ``````(** {2 Field theory} *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 145 ``````theory Field `````` 146 `````` `````` MARCHE Claude committed Oct 19, 2010 147 `````` clone export UnitaryCommutativeRing `````` Andrei Paskevich committed Jun 29, 2011 148 `````` function inv t : t `````` Andrei Paskevich committed Jun 21, 2010 149 `````` axiom Inverse : forall x:t. x <> zero -> x * inv x = one `````` Andrei Paskevich committed Jun 29, 2011 150 `````` function (/) (x y : t) : t = x * inv y `````` MARCHE Claude committed Jul 01, 2011 151 `````` `````` MARCHE Claude committed May 18, 2012 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 committed Jul 01, 2011 161 `````` lemma assoc_mul_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 162 163 164 `````` (* todo: discard the hypothesis ? *) z <> zero -> (x*y)/z = x*(y/z) `````` MARCHE Claude committed Jul 01, 2011 165 `````` lemma assoc_div_mul: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 166 167 168 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> (x/y)/z = x/(y*z) `````` MARCHE Claude committed Jul 01, 2011 169 `````` lemma assoc_div_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 170 171 172 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 173 ``````end `````` Andrei Paskevich committed Oct 26, 2010 174 `````` `````` MARCHE Claude committed Apr 20, 2012 175 176 ``````(** {2 Ordered Fields} *) `````` Andrei Paskevich committed Oct 26, 2010 177 ``````theory OrderedField `````` 178 `````` `````` Andrei Paskevich committed Oct 26, 2010 179 180 `````` clone export Field `````` Andrei Paskevich committed Jun 29, 2011 181 182 183 `````` predicate (<=) t t predicate (>=) (x y : t) = y <= x clone export relations.TotalOrder with type t = t, predicate rel = (<=) `````` Andrei Paskevich committed Oct 26, 2010 184 `````` `````` Andrei Paskevich committed Dec 14, 2011 185 186 `````` axiom ZeroLessOne : zero <= one `````` Andrei Paskevich committed Oct 26, 2010 187 `````` axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z `````` Andrei Paskevich committed Jun 29, 2011 188 189 `````` axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` 190 `````` `````` Andrei Paskevich committed Oct 26, 2010 191 ``````end `````` Jean-Christophe Filliatre committed Apr 08, 2011 192 `````` `````` MARCHE Claude committed Apr 20, 2012 193 194 ``````(*** to be discussed: should we add the following lemmas, and where `````` Jean-Christophe committed Jun 16, 2011 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 *)``````