coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kazuhiko Sakaguchi <pi8027 AT gmail.com>
- To: coq-club AT inria.fr, ssreflect <ssreflect AT msr-inria.inria.fr>
- Cc: Pierre.Roux AT onera.fr
- Subject: [Coq-Club] [ANN] Algebra Tactics 1.1.1 released
- Date: Thu, 13 Apr 2023 15:12:30 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pi8027 AT gmail.com; spf=Pass smtp.mailfrom=pi8027 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
- Ironport-data: A9a23:P8/PPKOuWHV0U7nvrR1vk8FynXyQoLVcMsEvi/4bfWQNrUog0jdRy GIdXzjTbP2JZmqje9kiadm180tUvJaEzNVnGXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQ7NNwJcaDpOsPrf8Ug35pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXDTUvG0dxJNXgYEtVJq+9NIW9t3 NEHfWVlghCr34pawZq+Q+how8kvdYzlYN1ZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JgeW6qAD yYaQWIHgBDoexwfYg1IIJ07leaswHL4dlW0rXrI/vBpuDiIkmSd1pDBL/XOcNLbGv9og3mhr GXm/G3iXRUVYYn3JT2tqyrw3IcjhxjTU4ULUba86/RCm0yW3mVVCRsMVFL9r+PRt6Klc9dWK khR9yZ36KZuqgqkSd7yWxD+q3mB1vIBZzZOO+gE2Cuf443t2ii2XjlVRwRhZv8PmdBjEFTGy WS1t9/uADVutpicRnSc6qqYoFuO1c49fT5qicgsHVtt3jXznG0gpkmQEYs7QcZZmvWwSG6gm WnbxMQrr+xL1ZZj6kmtwbzQb9uRSnXhSwc04kDaUjvg4F8nIoGiYIOs5B7Q6vMowGelorup7 Clsdyu2trhm4XSxeMqlHr5l8FaBuantDdEkqQQzd6TNDhz0k5JZQahe4StlOGBiOdsedDnib Sf74F0BvcQJYCHwPf8rMupd7vjGK4CwRLwJsdiEPrJzjmRZKWdrAQk0NBXOhzC3+KTSuf1jY szznTmQ4YYyUPw7llJats8S1rgkwi1W+I8gbcGT8vhT6pLHPCT9Ye5dbjOmN7llhIvZ/li92 4sAb6OilU8DOMWgOXK/2dBIfTg3wY0TX8+eRzp/Lb7dfGKL2QgJV5fs/F/WU9Y/x/gOyr6Qo CrVt40x4AOXuEAr4D6iMhhLAI4Dl74mxZ7iFX13ZQSbyDI4bJyx7awSUZIycPN1vKZg1PN4B b1NMcmJHv0FGHyN9iU/fKvNitVoVC2qogaSYAujQjw0JKB7SyLzp9TLQwrI9Qs1NBSRi/cQm bOb+z3+fYsiXCVnVcbfV+KuxQi+vF8bg+NDYHHLKdhyJmTpqYhjFDPtvMAOM+UzGE3lx2ac3 VzHBx03mPT8+d4p0djWhJKrq5WiPPt+E3F7QUjaz+eSHgvL8lWzxbRvVL6zQgncc2fv6oCOV P5wzcygAMYYnV1PjZVwI4xrwY06+dHrgb1QlSZgI1nmcHWpDelGDkSd/MwSqJBI+KBViTG2V m2L5NNeH7eDY+HhMVwJITsafvax7u4VlhbS/MYKDh3DvgEvx4W+UGJWIxWoow5eJuEsMIoan MEQiPRP4Am70hcXItKKix5PzFu1L1sCbfQDloobC4rVmAYU2gl8QZjDOBTXvrCLSftxa3cPH BHFpZDspbpmwmj6T0ESDlnIhOpUuoQPsktFzXgEPFW4peDGjf4WgjxU/SgGcQBO6hBhzehIG 3NKMndtLv6k5AZYh8lkXkGtFTpeBRafxFfD9lsRmEDdTGiqTmboLlBhHcqo42Yi7Dt6UhVA2 bOX2kLJcGzPR97g+Dk2VWpOie3RffYo+iLswMmYTtm4Rb8kaj/bs4qSTGsvqT68JOguhUfC9 NJYzMwpZYLVbScv8rAGUa+E3rEtSTeBFmxIYddl2IgrRWj8WjWD6QKiGnCLWPFmBqL1qBejK slUOMhweQy013+OohAlFKc8GeJIs8Bz1uUSWIHABDAgg+OEoytLoaDg0HH0pFUWTuVElec/L YLsdAy+LFGAuEsMpUjzqJhrB2npR/gFewz2486t+sorCZ8okb9hYGMy4JSOrlSXNwpVpUuUt Tzcep6MnvBDyJttraToAK5sFwW5EvKtdeWqoSSYkcVCUsPLCujK7zgqk1jAOx9HG4ceQPFlv O2pnOOv+XjarZEadnv8maiRM4VovuKMBPF2NODzJ1lkxRqyYtfmuUY/yjrpOK53n8N4zej5Y hmzd++bV8MfAvVZz11rMxluKQ4XUfnLX/2xtBGGjqq+DzYG2lb6N/Khz3jiaF9begIuO5HTD gzVue6k1utHrbZjVQM1OPV7P6BWeFPTe7MqV9nUhwmqCmOFhlCjuLy7myR5uHuPQjOBHd3h6 J3IegnmeV7g8OvUxdVeqMppsgdREH95hvIqc1kA/8JtzQq3F3MCMf9XJKBu5ku4ScAu/MqQi PDxgGoe5eHVWD1FdVDx7I2mUFvBQOMJPdj9K3oi+Eb8h+Jawm+fKOMJy8uiyy4elvjfICWPJ tQX+3m2NR+0qn2sbfhG/eS12I+L2duDrk/lOinBfwjaDBMXALFM33tkdOaIueorDOmV/Hj2y aMJqayoja11pYMd0SqtRpKNJCwkgQ==
- Ironport-hdrordr: A9a23:WnyFFKqO7Zcjd5KAS5My024aV5oSeYIsimQD101hICG9vPbo8P xG+85rrCMc6QxhPk3I/OrrBEDuewK+yXcY2+ks1NSZPTUO2lHYTr2KhLGKq1bd8kbFh4tgPM lbAsxD4R7LYWSST/yW3OB1KbkdKRC8npyVuQ==
- Ironport-phdr: A9a23:wQNmzBblUQVJ6n5cSizJPCL/LTF42oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gKPB9WLoKwcw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpV O5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxtIiTanf79/L xa7oQrQu8UKnIBvNrs/xhzVr3RHfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQ LJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4 btnRAPuhSwaMTMy7WPZhdFqjK9Drx2vpxJxzY3Jbo+LKvdxYqzTcMgGRWpYRMtdSzBNDp++Y oYJEuEPPfxYr474p1YWqBWxHwitBP7vyj9JhX/22rAx3fk7HgHFxgMgEM8Ov2jUrNX0KawfV vi1zKjLwDnfcf9b2yzw6IfNch87oPGMWah8ftbWyUkqDg7IiEibpoP5MT2PzOsNr3Sb4PR6V eKpk2MppR18rzuhyMkil4TEm58Zxk3Z+ShkxIs4JNK1RU1nbdCkEJVcqT+WOYt4T80sXWxlu SI3xL0EtJOnciYHyZAqyhjCYPKEa4iF+gzvWPqVLDtih39oeKiziwiu/UWj0OHxWci53VBXp SRfiNbMrGoC1xnL58iHVPR9+kCh1C6K1w/J6+FEJVk4mrTGJJI827IwmJUevEXZEi/5n0X2i 6CWdkE69eSy9+vnZbDmqoedN49ylA7+LrwjltKjDek8KAQDXGiW9f6i2LH//kD1WrpHg/wun qncqp/aJMAbpqCjAw9S14Yu8w6/Dzal3dgEg3UKLklIeB2Cj4fzOlHOJOr0Auu4g1SpiDtrw evJMaX7AprRNnjDjKvhfbFl5kJB0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m2 4MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8Zw2Ce mDhjNMMGntC6hElVuHkjFCJTRZWfGz3XqQm5zh9CYS8DI6FSJr705Kb2yLuPZREe2BHCVfEK n7rfoqZUPcNIHaKI585yGMsWr2oSotn3har4lypg4F7J/bZr3VL/ano08J4srW7fXAa8DV1C 5/YyGSRVyRvmXtOQTYq3ad5qEg7y1GZ0KE+jeYLXcdL6aZvVQE3fYXZ0/Q8E8r7DxrALo/TF 36pR9ynBXc6Sddii8QWbRNFEs65xgvGwzLsBrYUk7KRA5lh6qOMhyKuD8l4wnfCkqImigpuW dNBYEuhgKM37A3PH8jJnkGewr6tbrgZ1TXR+X2ryGOPuARVXFc1X/mbG38YYUTSoJLy4Uaqo 6aGL7MhP0MBzMeDLvAPcdj1lRBdQ++lPt3CYmW3kmP2BBCSx7rKYpC4M2MalD7QDkQJiWVxt T6PKBQ+CyG9omnfEC0mFFThZFnp+PV/r3XzR1E9zgWDZUlsn7Sv/RtdifuZQvIVlrUK3UVp4 y11TA7ngPrZDtOBo0xqe6AdKdIx7VFb1H7I4hRnN8/oJKRji1gCNgVv6hm2hlMnV8MayZhs8 C15qWg6YbiV215AaT6CiJX5O7mMb3L34AjqcKnOnFfXzNeR/K4LrvU+sVTq+g+zRS9Auz1q1 cdY13yE69DEFg0XBNjpUxZvrUdSqLTTYy177ITRny4JU+H8onrZ1tQlCfFwgA6hL48Fb4uLE QbzF4sRAM3ke6Q63lOuaBwDJuVb8qU5atine/Wx06muJO98nTiigAyr+ahF21mXv2p5Q+/Mh NMexu2AmxCAT3H6hUugtcb+ncZFYysTFyyx03qsCIlUb6x0NYEFbAXma9W2lo0k2LbiXndZ8 BioAFZO1MKyeBWUZkDwxkUKjRVR8SHhw3PoiWAq2zgy5rKSxinP3/jveH9lciZQSW9ugE2ta Ym4gtYGXVS5Og0glR+r/0H/lOBQoKVyKXWWQF8dJXCnaTE/FPHo5vzePZ0qittgqyhcXeWib ErPT7f8p0BfyCb/By5Fwyh9cTi2u5L/lhg8iWSHLX81omCKHKM4jRrZ+tHYQuZcmzQcQywtw yHWVgDmYPGm+NyVk9HIteX0BAfDHtVDNDLmy4+Nrn7x/Ww6WUfgt/+2k9zjVwM91GWon8kvX iLOohHmZ4Dt3KnvKuNrcH5jA1rk4tZ7EIVzwe5SzNkAnGIXjZKP8T8bgH/+ZJ9FjLnmYiNHF nYbhsTY6w//1Ah/I2KVksjnA26FzJIEBZHyY3tKiHlgqZkbUOHOsOMCxWwv/hK5tV6DP6Q7x GxGj6JwsDhCxLhY8As1knfDXPZLRRMeZWq00E7QirL25KRPODTxL/7qiBs4zYjnVPbY+kldQ CqrJc1kRHM2t5QldgqLiS2765m4KoaMK4tJ61vM1U+H1rYwStp5l+JW13M/aSSk4iJjm6hjy kY3lZCi4NredD4rpfPlREYebnqsOYsS4m2/1/4P2JbLmdn1TtM5XWxUOfmgBfOwTGBI7Kqha lbISWxm7C/cQOuXHBfDuh0/8TSVSMHtbCvRfD5AnJ10TR2ZbiSzmSgyWzM31t48HwGun4n6d VthoysW/hj+owdNzeRhM1/+VH3erUGmcGV8Tp/XNxdQ4gxYgiWdecWD8uJ+GT1Z9Zy9vUSML GKcfQFBEWAOXASNGVniOrCk4dSI/fKfA6KyKP7HYLPGruI7Nb/A3ZW0zo5v5CqBLO2KN3hmS vA3gw9NAS4/FMPelDECDScQkmOFbsKWogu95jwirs2796eOOkqn7o+OBr1OdNR3rkru0OHTa qjK3HY/dWgLs/FEjWXFw7UewlMI3iRndj32VK8FqTaIV6XI3KleEx8cbSp3cspO9aM1mAdXa qu5wpv40KB1ivktBhJLT1vkz4uxZJxSeT6VO1bOBULNP7ODb26uoYm/ceanRLtcgf8B/QW3o iqeGlT/My6rkjDoU1WiPbgJgn3FehNZv465f1BmDm2pH7eEIlWrddRwizMx27g9gHjHYHUdP TZLeERItrSM7Clcj52X+kRE53thaOSIwmOXs7eeJZERvv9mRC9zkrACiJzf47RQ5SBAAvdyn XmKxjaBi16jm+iLjDFgVUgXwgs=
- Ironport-sdr: 6437ffcb_++RBrsCk31iXsJWkKuHjdTsginSXtkfgSe5wMxNobO+wgjh +4gMF1Glm38rVDbzi2XT5lNy/asiUR+QJSmq+Dw==
Dear Mathematical Components users,
We are pleased to announce the release of Algebra Tactics 1.1.1.
In addition to the already provided `ring` and `field` tactics, this
release gives access to the `lra`, `nra` and `psatz` tactics from the
Micromega plugin shipped with Coq. For the moment, the new tactics are
*considered experimental features and subject to change*.
The new release is available in the OPAM package
`coq-mathcomp-algebra-tactics.1.1.1` compatible with Coq 8.16 and 8.17
and MathComp 1.15 and 1.16. A Nix package is also available.
The new tactics work for any abstract `realDomainType`
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.
Example any_realDomain (F : realDomainType) (x y : F) :
x + 2 * y <= 3 -> 2 * x + y <= 3 -> x + y <= 2.
Proof. lra. Qed.
Print Assumptions any_realDomain. (* Closed under the global context *)
```
or any `realFieldType` with divisions
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.
Example any_field (F : realFieldType) (x y : F) :
x / 2 + y <= 3 -> x + y / 2 <= 3 -> x + y <= 4.
Proof. lra. Qed.
```
They also handle any concrete instance of the above (like the rational
numbers for instance)
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum rat lra.
Local Open Scope ring_scope.
Example rat (x y : rat) :
x + 2 * y <= 3 -> 2 * x + y <= 3 -> x + y <= 2.
Proof. lra. Qed.
```
The `nra` (non-linear real arithmetic) tactic is an extension of the
`lra` tactic that handles some non-linear goals
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.
Example non_linear (F : realDomainType) (x y : F) : - x * x >= 0 -> x * y = 0.
Proof. nra. Qed.
```
One can also use the `psatz` tactic, provided the CSDP solver is installed.
Just like the `ring` and `field` tactics, `lra`, `nra` and `psatz`
handle any ring morphism, either abstract
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum lra.
Local Open Scope ring_scope.
Example abstract_rmorphism (R : realDomainType) (f : {rmorphism R -> R})
(x y : R) : f y >= 0 -> f x + 2 * f (y + 1) <= f (3 * y + x) + 2.
Proof. lra. Qed.
```
or concrete (`ratr` is the injection from `rat` to any ring)
```
From mathcomp Require Import ssreflect ssrfun ssrbool ssralg ssrnum rat lra.
Local Open Scope ring_scope.
Example ratr (R : realFieldType) (x y : rat) :
ratr y >= 0 :> R -> ratr x + 2 * ratr (y + 1) <= ratr (3 * y + x) + 2 :> R.
Proof. lra. Qed.
```
We would like to thank Frédéric Besson and Enrico Tassi for their help
respectively with Micromega and Coq-Elpi.
Kazuhiko and Pierre
- [Coq-Club] [ANN] Algebra Tactics 1.1.1 released, Kazuhiko Sakaguchi, 04/13/2023
Archive powered by MHonArc 2.6.19+.