algebra.why 3.24 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 2 3 `````` theory Assoc type t `````` Andrei Paskevich committed Jun 29, 2011 4 `````` function op t t : t `````` Andrei Paskevich committed Jun 21, 2010 5 `````` axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 6 7 8 9 ``````end theory Comm type t `````` Andrei Paskevich committed Jun 29, 2011 10 `````` function op t t : t `````` Andrei Paskevich committed Jun 21, 2010 11 `````` axiom Comm : forall x y : t. op x y = op y x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 12 13 14 15 ``````end theory AC type t `````` Andrei Paskevich committed Jun 29, 2011 16 17 18 19 `````` function op t t : t clone Assoc with type t = t, function op = op clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 20 21 22 23 ``````end theory Group type t `````` MARCHE Claude committed Oct 19, 2010 24 `````` `````` Andrei Paskevich committed Jun 29, 2011 25 `````` function unit : t `````` MARCHE Claude committed Oct 19, 2010 26 `````` `````` Andrei Paskevich committed Jun 29, 2011 27 28 `````` function op t t : t function inv t : t `````` MARCHE Claude committed Oct 19, 2010 29 `````` `````` Andrei Paskevich committed Jun 21, 2010 30 `````` axiom Unit_def : forall x:t. op x unit = x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 31 `````` `````` Andrei Paskevich committed Jun 29, 2011 32 `````` clone Assoc with type t = t, function op = op `````` Jean-Christophe Filliâtre committed Mar 23, 2010 33 `````` `````` Andrei Paskevich committed Jun 21, 2010 34 `````` axiom Inv_def : forall x:t. op x (inv x) = unit `````` MARCHE Claude committed Sep 04, 2011 35 36 37 `````` lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 38 39 40 41 ``````end theory CommutativeGroup clone export Group `````` Andrei Paskevich committed Jun 29, 2011 42 43 `````` clone Comm with type t = t, function op = op meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 44 45 46 47 ``````end theory Ring type t `````` Andrei Paskevich committed Jun 29, 2011 48 49 50 51 `````` function zero : t function (+) t t : t function (-_) t : t function (*) t t : t `````` Jean-Christophe Filliâtre committed Mar 23, 2010 52 53 `````` clone CommutativeGroup with type t = t, `````` Andrei Paskevich committed Jun 29, 2011 54 55 56 `````` function unit = zero, function op = (+), function inv = (-_) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 57 `````` `````` Andrei Paskevich committed Jun 29, 2011 58 `````` clone Assoc with type t = t, function op = (*) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 59 `````` `````` Andrei Paskevich committed Jun 21, 2010 60 `````` axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z `````` Jean-Christophe Filliâtre committed Mar 23, 2010 61 `````` `````` Andrei Paskevich committed Jun 29, 2011 62 `````` function (-) (x y : t) : t = x + -y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 63 64 65 66 ``````end theory CommutativeRing clone export Ring `````` Andrei Paskevich committed Jun 29, 2011 67 68 `````` clone Comm with type t = t, function op = (*) meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 69 70 71 72 ``````end theory UnitaryCommutativeRing clone export CommutativeRing `````` Andrei Paskevich committed Jun 29, 2011 73 `````` function one : t `````` Jean-Christophe Filliâtre committed Mar 23, 2010 74 `````` axiom Unitary : forall x:t. one * x = x `````` 75 `````` axiom NonTrivialRing : zero <> one `````` Jean-Christophe Filliâtre committed Mar 23, 2010 76 77 ``````end `````` Andrei Paskevich committed Oct 26, 2010 78 79 ``````theory OrderedUnitaryCommutativeRing clone export UnitaryCommutativeRing `````` Andrei Paskevich committed Jun 29, 2011 80 81 82 `````` 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 83 `````` `````` Jean-Christophe Filliâtre committed Jun 21, 2011 84 `````` axiom CompatOrderAdd : `````` Jean-Christophe Filliâtre committed May 09, 2011 85 `````` forall x y z : t. x <= y -> x + z <= y + z `````` Jean-Christophe Filliâtre committed Jun 21, 2011 86 `````` axiom CompatOrderMult : `````` Jean-Christophe Filliâtre committed May 09, 2011 87 `````` forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` Andrei Paskevich committed Oct 26, 2010 88 89 ``````end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 90 ``````theory Field `````` MARCHE Claude committed Oct 19, 2010 91 `````` clone export UnitaryCommutativeRing `````` Andrei Paskevich committed Jun 29, 2011 92 `````` function inv t : t `````` Andrei Paskevich committed Jun 21, 2010 93 `````` axiom Inverse : forall x:t. x <> zero -> x * inv x = one `````` Andrei Paskevich committed Jun 29, 2011 94 `````` function (/) (x y : t) : t = x * inv y `````` MARCHE Claude committed Jul 01, 2011 95 `````` `````` MARCHE Claude committed Jul 01, 2011 96 `````` lemma assoc_mul_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 97 98 99 `````` (* todo: discard the hypothesis ? *) z <> zero -> (x*y)/z = x*(y/z) `````` MARCHE Claude committed Jul 01, 2011 100 `````` lemma assoc_div_mul: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 101 102 103 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> (x/y)/z = x/(y*z) `````` MARCHE Claude committed Jul 01, 2011 104 `````` lemma assoc_div_div: forall x y z:t. `````` MARCHE Claude committed Jul 01, 2011 105 106 107 `````` (* todo: discard the hypothesis ? *) y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 108 ``````end `````` Andrei Paskevich committed Oct 26, 2010 109 110 111 112 `````` theory OrderedField clone export Field `````` Andrei Paskevich committed Jun 29, 2011 113 114 115 `````` 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 116 117 `````` axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z `````` Andrei Paskevich committed Jun 29, 2011 118 119 `````` axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z `````` Andrei Paskevich committed Oct 26, 2010 120 ``````end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 121 `````` `````` Jean-Christophe committed Jun 16, 2011 122 123 124 125 126 127 128 129 130 131 ``````(* to be discussed: should we add the following lemmas, and where 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 lemma ZeroLessOne : zero <= one *) ``````