{"shas":[["56d194e1c99c297a7c7e46db771d490e4b2209d6","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Almost all theory regarding order revised. We now have abstract interfaces that uniquely specify the order on the naturals, integers and rationals. We also specify default implementations of these abstract interfaces.\n\nMore specifically:\n* New notion of a semiring order introduced.\n* A lot of theory about (semi)ring orders formalized.\n* Proven that a total (semi)ring order uniquely specifies the ordinary order on the naturals and integers.\n* Moved Theory about nat_distance, int_abs, order on the naturals to a separate file.\n* Introduced the Grothendieck ring (a ring constructed from semiring pairs). This was first implicitly contained in natpair_integers.\n* The positive cone of a semiring is again a semiring. This was first this was implicitly contained in positive_integers_naturals.\n* Nice notations for the nonnegative, positive and negative cone.\n* Concrete orders for nearly all implementations implemented and a moreover a default order for the naturals, integers and rationals.\n\nAlso:\n* Params for nearly all operations are set to hopefully gain some speedups.\n* More consistent naming and various ugly proves cleaned up\n\nThis has the following advantages:\n* If we define an alternative order on the naturals, integers or rationals (for example from the standard library) it follows automatically that it coincides with any other order.\n* Our theorems about order also apply to orders from the standard library.\n* So... hopefully a much smoother integration with CoRN in which solely the orders from the standard library are used.\n* We can refer to order properties of the naturals, integers, rationals, with a common name. Also, beforehand we rarely proved any results about the order on the rationals, now we get all properties of ordered (semi)rings for free.\n* If we define a ring order (todo) on the dyadics we get all these results for free as well.\n\nTodo:\n* Fix the dyadics (which are now broken) and define an order on it.\n* Prove that a total ring order uniquely specifies the order on the rationals.\n* Prove that the default order on the rationals is total","Robbert Krebbers"],["29c2586d41a7fed5b647076c929132348ad141c1","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Dyadics fixed and more results about the order on the rationals.","Robbert Krebbers"],["2c3466329f870388c34648a6294f427ba3a2a496","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Some new results on < and some renaming.","Robbert Krebbers"],["f096de1427b2f56f0cc68f889c8a941fd8d7fb92","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","More renaming","Robbert Krebbers"],["73f64ac0903744c81c1f1497e1dfda4b64f03c5d","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","More results on < and *.","Robbert Krebbers"],["765360e440319003fbccca3e4732279d8f486180","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Make compile with r13781\n\nNOTE: Coq is unable to derive some implicit arguments in interfaces.sequences and theory.sequences. I have now explicitly specified them, but have no clue why that's needed in the first place.","Robbert Krebbers"],["d4857d1cfd3c677ac6234da21e5378e20078c221","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Results about order and dec_mult_inv","Robbert Krebbers"],["ddbb3bfee3dd188659189289fdd4086120e3edf0","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","More on dec_mult_inv and order","Robbert Krebbers"],["01c6aecc4117a55c612db8e10149c488ab46aa27","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Removed type classes for minus and division. They turned out to be too cumbersome for the advantages they would ever give.","Robbert Krebbers"],["21577f59bae2ee891e096f0f71024d374b8841ef","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Fixed the dyadics again. Also I have specified some duplicate instances to gain some speed ups.","Robbert Krebbers"],["3656c8b2cf70c9a297c0b2a3e5ef515e8642d825","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","bool_decide","Robbert Krebbers"],["01786043614268a8863f846d4fd3a2c93ff88567","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Notion of StrictlyOrderPreservingBack","Robbert Krebbers"],["11a1fbf65901e378e21374ba98283d4665400934","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Type classes and theory for IntPow and Abs. CutMinus defined on the total order.","Robbert Krebbers"],["2274ab3d9b7d312bed0e51972bbfecbefe083dc3","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Haskell style notations for multiplication. More consistent use of canonical names.","Robbert Krebbers"],["ef386858e61c6246ee09ba1161d9e1646fc728ef","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Removed StrictlyOrderPreservingBack again, it turned out to be superfluous","Robbert Krebbers"],["3630223f6788eb502be44daa2f6260ee230e2d36","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Removed Group_Morphism and Ring_Morphism. Monoid_Morphism and SemiRing_Morphism already preserve -, so these notions are obsolete.","Robbert Krebbers"],["687ff1d6ffcb1db7464dd13adf1797992e652d78","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","The default order on the rationals is total","Robbert Krebbers"],["e7b9998f678a49ab1f66e5046e2aa20aff30aa64","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Using int_pow we can define DtoQ_alt nicely. As a result, it is much easier to prove that DtoQ is a ring morphism.\n\nAlso, now it only takes 3:30 min to compile dyadics.v!","Robbert Krebbers"],["e7d7afcdd987d1264c918a4e9b2e9fc08e106d98","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","Code style of dyadics.v improved. Order on the dyadics.","Robbert Krebbers"],["017a056dcb16f3d6ecb8ba01572a6c1586d42d0c","1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@robbertkrebbers.nl","NatPow, Abs and decidable equality on the dyadics.","Robbert Krebbers"]],"repo":"0x01/math-classes","actor":"0x01","ref":"refs/heads/master","size":142,"head":"2a7583d39dea342d75e93d5475a587deaf7ee9fc","actor_gravatar":"9a2601268a5194646e6c7532947764db","push_id":30503027}