coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Iaroslav Baranov <kciray8 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?
- Date: Sat, 27 Jul 2024 08:38:15 +0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kciray8 AT gmail.com; spf=Pass smtp.mailfrom=kciray8 AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f175.google.com
- Ironport-data: A9a23:KM25861ZNPjdZjRNVvbD5Ux1kn2cJEfYwER7XKvMYLTBsI5bpzJUy GoZCG3UOq7YMWb1L90nYYXl9kgBsZPWyt8yTwJo3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3Zhn9ilaYDkpOs/jf8Ew14qyp0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW1fGnvxwIV45BpwV86FcDlhFz uNCcy9YO3hvh8ruqF66Yuxlh8BmPdayeY1G5SwmwjbeAvIrB5vERs0m5/cChGZ21p0IRKyOI ZNGNFKDbzyYC/FLElQcCYg3jbeAiXz2cjkeo1WQzUYyyzmIlFIoj+e3WDbTUtuof8JZvVzCm mv92G33LE8bMuO+1hPQpxpAgceUwHqjB9NMfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGqKEz8Am6UYC4UUTn/TiLuRkTX9cWGOo/gO2Q9kbKyyqzW2EaYyFOU80rvYgdSgUh7 UDTxMy8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0ts4mLTGYb3kKnczpzLJNZmOEZDt0Z/ txnhC03hrFWnNFSkqviog2BjDWrqZzECAUy4207v15JDCspNeZJhKTxtjA3CMqsyq7HFTFtW 1BawKCjABgmV83lqcB0aLxl8EuVz/iEKibAplVkAoMs8T+gk1b6ItoKuGomfhw2a5ZdEdMMX KM1kVMBjHO0FCv6BZKbn6roWqzGMIC5SYq1Bq2NNLKinLAoKlLfo34GibGsM5DFyxV1yf5uZ /93gO6jCnEVDakvzTy9AY8gPUwDl0gDKZfobcmjlXyPiOLADFbMEOttGAXUMogRsvjfyC2Lq IY3Cid/408AOAEISnKHr9B7wJFjBSRTOK0aXOQOKL/ZflE2Rzl+YxITqJt4E7FYc21uvr+g1 hmAtoVwkTITXFWecV/QOENwIqjiR4h+pn8dNCkhdwTgkXs6bIrlqO9Ve5IrdPN1vKZu3Nxlf ckjIs+gO/VoTiiY2jI/aZKmkpduWi72ji2zPg2kQgMFQbheeyLz9OXZIzTfrBs1MnLvtO8Vg aGR6QfAcJ9SGyVgFJn3bdys/XOQvF8cuuR4YGXQKPIOek+2qIlOAA7yh88RPMsjB0jixDyb9 gDOGjYeh7DHjLEU+enzp5KvjtmWAconOWFFDUz30K2QCRDK2kaCnapRT/eufx3GcWH/pZWZe uReys/jPM09nFplt5R2F5Bpx/kc4+TDiqB7zAN2OmfidHWuV61dJ0eZ0fl1tqFiwqFTvS20U Bmt/vhYIbC4B9P3ImUOJQYKbvWx6t9Mo2P8tc8KGUTd4DN72JGlUk8IZhmFt3F7HYtPaYggx b8shd4S5wmBkSEVC9ehjB1P1mGyP3cFArQGtJYbPdfRsTAV6Gp+OL7SNiynx6u0SYRoElIrK Tqqlqb9l+xi5k7dQUESS1nJ/8Rg3Korhj4b7WU/N2yom8XEjMAZxBd+0yo6ZSULwwRl09BcA HlKNUp0L5qg5z1D3ZVPTU2wKQNsXzuip0r7kQoPnkLkUnjyB3DsLXI8C8mJ7ks242JRRRkF3 bC6mULOcyfmQ9H15QQ2AXVakv3EScdg0DHClOSMPdW3L7NjbRXL2qaRNHc18T35CsYPtWj7j OhN/tcoT5bkNCQV8pYJO6PD2Zs+EBm7dXF/G9d/96Y0HEbZSjG4+R6KD2uTIsptBfj7wXWUO vxUBPBkdkqBjX6VjzUhG6QzDad+n6cp6Po8a7rbHzM6nIXFnAV5kqD713bYv3AqceVMgMxmC 4L2dhC+KEKyq0ZQuVfwqJhjBjLlT/gCPBbxzcKkwtUvTpgjitxhQWs287mzvkiWDjdZwgKpj FvDSpLSnsNfytVKvorzE698KR2+BvHtWc+prg2ikdR8QuneEMXJtjFP81nuABtLDOFAR/V2i rW/n9rl12zVvLsNcj74mrvQM4Jr9MmNTO5sHcavF0ZjnAyGQ97K3xQY3nKRcLhlrYt43da2Y Cedc+6yRM4xd/YG40MNcAlYMRIWK5qvX5favSnn8si9UEkM4zLIPPaM1CHMf2pEUgQqJpenK Av/m8j21+BitI4WWSM1XaB3MaRZfm3md7AtLeDqlD+iCWKtvFOOl53imTck6hDJEnO0K9n70 72UWinBcAmOh4+QwOF7q4BSujglPER5i8Q0fWMf/IdSoBK+B2gkM+8cEMsnDrd5ry/M76z7N Qr9NDYaNSbAXDp6KES2pJypWwqEHeUBN+voPjFjrQvedy6yA5jGG7d7sDtp53BtYDb40eW7M pck92btOgSqiIRcLQrJCidXXc88rh8b+p4Jxaw5u8n7AhJbEKpTkXI4Q1cLWivAHMXA0k7MI ADZgIyCrF6TESbM/QRIIha52y31eBvgyjwpaWGEx9O3V0Cz0rhb0POmUw3s+uRrUSnJTYLig Vv4QmKM5yad3Xl7VW7FfT42qfccNM9n1fRW4EMuqcP+Uk1wBqka0xs+oBcy
- Ironport-hdrordr: A9a23:fZqDKKPRpAE9bsBcTsyjsMiBIKoaSvp037BL7TEXdfUxSKalfq +V7ZcmPHPP6Ar5O0tApTnjAtjjfZq0z/ccirX5Vo3SOTUO1lHYSL2KLrGP/9QjIUDDHyJmup uIupIRNOHN
- Ironport-phdr: A9a23:m0PB1RxREAMebzLXCzI2wFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xSZu6sm3QCBHd2Cra4e2qyO6+GocFdDyKjCmUhBSqAEbwUCh8QSkl5oK+++Imq/EsTXaTcnF t9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5/I gm6oR/Qu8QXjodvLqQ8wQbNrndUZuha32xlKUyXkhrm+su84Jtv+DlMtvw88MJNTar1c6MkQ LJCCzgoL34779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9 LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWMtaSi5PDZ6mb 4YXAOUPPehWoYrgqVUQsRSzHhOjCP/1xzJSmnP6wa833uI8Gg/GxgwgGNcOvWzXotrvLqcSV vu1zK3SwjXdcvhbxC3y6JLSfRAnpvGMQ697fM3SyUYzFgPFlE+fqIzmMj6O2eQNtnKU7+tkV e61l2EnrARxryGpy8wxhYbHmpgbxUrY9SVl3ok1P9u4RVZ6bNOmFJZcqSGUO5Z0T80tTG9mt zo3xL0YtZO/fCYH1YoqywLdZvGJfYWF4BztWuaMLTp7hHxoe6+yiwix/EWkzOD3S8e60FFPr iVfk9nMsGgA1x3V6sidS/ty5F2t2TiV1w3V9+pKIlg0mLLFJ5I9xrM8jJkevETZEiPrhkn7j 7Waelgm9+Wo7ensf6vrppuBN49vlgHxLL4ulNG+AeU5LAcDR3SX9OKh37P550L5Wq9Fjvgun 6nZrp/aIcMbq7a8AwBP04Yj7w+zDjeo0dgFhHUHIk9JdRCHgoTzNFHOJ/f4Dfi7g1uyijtk2 /fGPrj5DpXMKHjMjqvhcK5j50JAzAc/19NS6pJOBr0cPv7+WVX9uMHaAxI5KwC0xvzoCNR51 oMQQ2KPBaqZPbvRsVCU5+IvOfODZY8WtTvmJPgl4uThjX49mVMHYaap2p4XZGi+Hvt9O0qZe 2bjgs8dEWcWuQozVPHmhEWYUTFPf3ayQ7485jYjBY26CofDX5mhj6CF3CemBZJbfXtGC1CJE XfwbYqIQfYMaCSIIs9giDMIT7ahS5VynS2p4QT90v9sKvfe0iwer5PqktZvtMPJkhRn1DVuC N+Z2n/FZWhul2UPWXdi36t+u0Vsmn+M1KF5h7pTEtkFtKABaRszKZOJl78yMNv1QA+UJr9hK X6jS9SiWnQqS84phsQJewB7EsmjiRbK22yrBaUUnvqFHs986brSil72Ics10HPazO85lVBzQ cBOL2S31oZw8gHSA8jClEDK372ye/Ek1TXWvHyG0XLIuUhZVABqVqCQXnsefELH/fz240rDS /mlDrF0ehBZx5ukLa1HIsbskU0ARPrnP4HGZHmtnm6rGRuS7raFbY6vanpEmSuEVxVCnAcU8 nKLcwM5A09Nukr4CzpjXRLqakLoqqxlrW+jC1Qz10eMZlFg0Ly8/lgUg+adQrUdxOBMviBps DhyEFunurCeQ9OduwpserldatIh8R9G02zerQl0Ip2nKehrmFcfdw19u06m2Q9wD81Mls0jr XViywQXS+rQ01hAbTqJjbj/P7TWLi/5+xXuI6/a11fC0cqHr78V4adwoFHisQe1U0s6pi8/g p8Fjj3FvMWMVVVPAveTGg4t+hN3pq/XeHw47oLQjjh3NLWs9yTFw5QvDfckzRCpe5FeNrmFH Un8CZ5/ZYDmJeo0llyudh9BMvpV8ft+PMinbfKXiIakOe9hmHStimENs+UfmgqcsjFxTOLFx cNPwPqZxAKWBx/ziV6gtob8noUONnkCW2G4zybjHotYYKZ/KJ0KBWmZKMqy3txihpTpVha07 XabDkgdkI+scBuWNBnm2BFIkF8QuTqhkDe5yDp9l3coqLCe1WrA2baqeB0CM29NDG5s6DWka Yu/jsoTTRiAYA0glR/j7kH/j6RWv6VwKWDPTFwAJXCnaTE/FPLq5vzbPJMH4YhgqShNVeWgf V2WL9y16wAX1S/uBSoWxTw2cS2rpoSsmhV7jGyHK3Mg5HHdeMx22VLe/ImGHa8XjmdAHXMoz 2CIWwvZXZHh59ifmpbdv/rrUmugUsYWaiz31cabszP942R2ABq5lvT1m9v9EAF83zWosrsiH SjOshv4ZZHmkqqgNucyNEpjBUX1+ppSFYR3k492j5YVkyt/5N3d7T8cnGH/PM8Ok6H1bWAEV G4jzNvc4Qyj00pmZCHB18fyUXOTxdFkbt+xbzYN2y4z2MtNDb+d8L1OmSYmxzjw5RKUe/V2m S0RjOc/8HNPyf9coxIjl2/OSqBXB0RTOjbg0giF/8zr5rsCf36hKN3SnAJ/hYzzV+zE+1AEH iylJdF6WnUspsRnbACSjDupsdqiIYeIK4pU70zckg+c3bYLbstpzLxSw3IgYzqY3zVtyvZn3 0Iwm8vm7c7XcyM1u/jhSh9Aam+qPYVKpne03PwYxoHPj8iuBskzRWlNBcG1C6ruSHVL65GFf 06PCGFu8y/LX+OAQknPrh8h9SuHEoj3ZSjIfz9AnIkkHF/FYxUByAEMAGdgxs9/Rl3snZaxN h8+v290hBawqwMQmLgxaV+iAiGG9V3uMnBtGdCeNEYEtFgcoR2OYIrFtKQrWHgJtouoqAjHQ oCCTyJPC2xBGkmNBlS4e6Kr+cGF6O+AQOy3M/rJZ7yK7+1YTfaBg5y1gMNg+H6XO8ODM2MHb bVz01dfXX1/B8XSmikeAy0RmSXXaseHpRC6siRpp8G7+f7vVUrh/4yKQ7dVNNxu/Vixj8Lhf 6aIgz1lLD9Dyp4W7XrBybxazUFLzi83KGTrHrMHuirACqnXn+4fDhIWbT9yKNod76842VooW 4aTgdf027hky/8tXg0dBBqxx4fwP5xMej7gZzalTA6ROb+LJCPG2ZTyaKK4EvhLiflM8ga3o XCdGlPiOTKKk3/oUQquOKdClnL+XlQWtYejfxJqEWWmQsjhb0jxM9R2lzQnkZU7g3rLMSgXN j02ICYv5vWAqDhVhPlyATkL9n1+MeyNgDqU9cHdI5cS9Op0W2F6zr0Hpns9zLRR4WdPQ/k/y 06w5pZ+5lqhlOeI0D9uVhFD/y1KiIy8tkJnIazF95NEVB4sGToC6GyRD1IBoN43UrUHWohVw 9nL0bPscXJMqo2Ju8QbAMfQJYSMN39zaXIB9xbbCQIESXigMmSN3iRg
- Ironport-sdr: 66a487d1_RvDg/U2IYbqPAuV8fZpLN1X87Bz0WXh9oDklrk8sEyae3CM UhdX73gucNYQ6g3+/9mORgmii78BilQrGpW2JCQ==
Hi!
I decided that I want to use more automation for my Coq project, so I added From Ltac2 Require Import Ltac2 and I encountered a few problems:
- There is no "pose proof a b c." tactic in Ltac2 (even though it is clearly specified in the docs), which is very convenient to me. I tried "assert" but it is not an equivalent (it requires round brackets which is not convenient) and also makes you either specify the H name explicitly or add unneeded body to the hypothesis. I tried to wrap ltac1 pose proof in ltac2, it worked but with a limitation (it requires round brackets again), and it seems like a cheat anyway.
- I also had to add the tick character (') when I use refine refine '(_: ¬ (∃ y. P y)-> ⊥ ).
Ltac2 pp_tac (x: constr) := (ltac1:(x |-pose proof (x))) (Ltac1.of_constr(x)).
Ltac2 Notation "pp" p(constr) := pp_tac p.
...
pp (imp_in a b c).
If I continue using Ltac2, how many such incompatibilities will I encounter?
Can you list me the potential issues if you encountered them in the past?
Does it worth to push on and continue using Proof Mode "Ltac2"? Or maybe it is better to use Classic mode and call Ltac2 tactics from a wrapper when I need them?
Best regards,
-- Iaroslav Baranov
- [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?, Iaroslav Baranov, 07/27/2024
- Re: [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?, Jim Fehrle, 07/27/2024
Archive powered by MHonArc 2.6.19+.