Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?


Chronological Thread 
  • From: Jim Fehrle <jim.fehrle AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Is it save to use (Proof Mode "Ltac2") in big projects?
  • Date: Fri, 26 Jul 2024 23:33:53 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f48.google.com
  • Ironport-data: A9a23:E2YkQ6u96kzSbO2rILXIyG88TOfnVM9aMUV32f8akzHdYApBsoF/q tZmKWCHPqyNMTPzKNh+a4i3oEoCv8OBx4VqGlRuq3xnQy8UgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTrSCYEidfCc8IA85kxVvhuUltYBhhNm9Emult Mj7yyHlEAbNNwVcbCRMuspvlDs15K6u4GxC4ARlDRx2lAa2e0c9XMp3yZ6ZdCOQrrl8RoaSW +vFxbelyWLVlz9F5gSNz94X2mVTKlLjFVDmZkh+A8BOsTAezsAG6ZvXAdJHAathZ5plqPgqo DlFncTYpQ7EpcQgksxFO/VTO3kW0aGrZNYriJVw2CCe5xSuTpfi/xlhJHMTYdwG9MFzOEpt5 P0CARodQlO7xMvjldpXSsE07igiBMziPYdat305iD+FXbApRpfMR6iM7thdtNsyrpoWTLCOO oxDMWopMESojx5nYj/7DLo8neLuiHT/aTlVgF2QrKszpWPUyWSd1ZC8a4KLIYLTFK25mG6bn lDj4lbIUyoxNdHDkAjGqnmmouLAyHaTtIU6T+DhrqE73jV/3Fc7AxoPEFC/vPORkV+7Q9sZK koO+yNoo7JayaCwZtz0Xhn9rXLd+xBAC5xfFOo17AzLwa3Ri+qEOoQaZgxkNI04uugyfBcJx 16Ttvn5KX9X85TAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJQwc1 Qxmu8TXuln+pcsC1qH+8Fyexjzw9t7GSQk64giRVWWghu+YWGJHT931gbQ4xa8fRGp8crVnl CZY8yR5xL5SZaxhbATXHI0w8EiBvp5pygH0j191BIUG/D+w4XOldo04yGghfh0xaZ5eImCwM Ba7VeZtCHl7bCvCgUhfM9LZNijW5fGxfTgYfqmIMIoeP8ErHON51HgwOBbPgAgBb3TAYYlkZ M7DLpfyZZrrIatgyzWySq8c17Rtrh3SNkuCLa0XOy+PiOLEDFbMEeltGALXMogRsvnYyC2Lq I03H5XRm31ivBjWOHa/HXg7dgBUcxDWxPne96RqSwJ0ClY+SDt+V6SJnuNJlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQik7Mu29boU1tn8hIy0nMHCh3nVpM87l774Se9FzNfMr/fBqh6w8B fQUWdSyMtIWQBT++hMZccbcqq5mf0+Vng6gBXeuTwU+WJ9CfDb33OHYUDHhzhRTMRrvh/AC+ +Wh8ij5Xas8Qx9TCZeKSfC3kHK0k3svuMNzeErqJNNsVl3m29VoIXapj9scAcIFGTPczBS0i ieUBhY5o7HWgokXqdPmu4GNn72LIcBfQHVIPjD8xqmkEAXn5Uyf+J9kfMfUWCHCRUX21b6HZ +4I/8rjMfYCoklGg7B8H5lv06g6wdnl/J1e8ShJA1TJaEaNGJp7A3zbw/RKiLJB9oVZtSSyR EiL3NtQYpeNGcH9FW8uNBgXVfuC2d4Uiwvtw6wMemui3xBO/Z2DTUl2FDuPgnYELLJKbaUU8 d14s8sSswGCmh4mN+idtR9t9kOOE2chVps2vZRLEa7pjQsWkmt5W6L+MROvwp+zaIRrCHIIc xu0n6vJgopOynXSK0QTEWf/5ssDpJAsli0T8no8CQWooOfVvt42wxxbzhovRCt30Bhs8rx+K 0prBWJPNISM+DZiu+ZbVUv1HzNtKQGr+HWt714FimeDQ1KabTHPJjdlOMKm3kMQw0RDdBd1o ZCaz2fEV27xXcfThyEdZ29sm8bBf/dQqDLQvd+BHtuUOaU6bR7OoL6cVUBRpzTJWcoO1VD6/ 8909+NOWIjHHC83oZxjLbKF1L4VGSu2FEYbTd5PpKo2THzhIhes0j2zKme0SMNHB9rO1WSaU 8VOBMZ+Zy6S5Ra0jAIwJPAzeudvvfsT+tA9VKvhJjcGv5uhvzNZis/s2RaktlA7YedFsJgbE ZzQRQKgA2bLpHpzmk3xludmFFe8Q+E5YFzb4Ljo3sQPT4kOocN9Q3EUi7GUhUiYACFj3hCTv T7AWZPo8vxf+dxssrboQ4p+BFSSCNLsVe633hi5nPZQYPjub8rflQMnhWP2HgZRPIlLAtR+q quQgYSmwGLEo7cEfGTLkLaRF6RyxJuTXcgGFunVPXVljS+5d8u02CQ6+ke8Mo1vrNxGw9uOH i+UVZOVTsEEfPt431hXWjh6PzdGLJqvdYbmhye2j8rUOygnyQadce+Wry74X19UZgojGsPbG ATrn92M+9oBjoBHJCFcNsFcG5UifWPSA/o3RebQ6wudIHKj2G6Zm73YkhEl1zHHJ1+EHOv+4 rPHXhLOTwuzio6Z0OBmt5FOgTNPAEZfmeUQemcvy+xygR2+D08EKr05GrcCAZd2jCfz9c/ZY BfgUWgcMhj+DA90KUjE3NfeXwmhX71Efp+zIzEy5EqbZhunHI7KUvMr6i5k5GwwYTf5iv2uL dYF4HDrIxyt2ddTSP0O4uCgy/JSrh8AKqnkJWim+yAzP/ofPVnO/HloHQ4IWCCeVs+RxAPEI m86QW0CS0a+IaI0/QCMZFYNcCz1fhu2p9nrUctL6NnasoSfiuZHzZUT/snth6YbYp1iyKEmH BvKqqjk34xS8nMWsKot/dkuhMeYzB5N8teSdMfeeOHZo018BqnL8S/PcerjgfzOIDJiLm4=
  • Ironport-hdrordr: A9a23:PTHQQahdkGCrfQny9xpgS8FH0nBQXuMji2hC6mlwRA09TyX4rb HWoB1/73XJYVkqKRQdcLy7Scu9qDbnhP1ICOoqXItKPjOW3FdARbsKheDfKn/bexEWndQtsp uIHZIObuEYzmIXsS852mSF+hobr+VvOZrHudvj
  • Ironport-phdr: A9a23:20c9MRAOq70VfuX29fcBUyQU2kkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua41ygGXFtyDuroE07OQ7/qxHzRYoN6oizMrTt9lb1w/tY0uhQsuAcqIWwXQDcXBSGgEJ vlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+I A+5oAjfqsUam4pvJ6c+xhfUvndFf/ldyWd0KV6OhRrx6dm88Zp5/yhMp/4t8tNLXLnncag/U bFXAzMqPnwv6sHsqRfNUxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt7 6FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY6nc YABE/QOMvpZr4nlplsBsx2+BRW3BOjyzjNEn2L60bEm3+gkFwzNwQ4uEM8UsHnMo9r1OqUdX +C7wqfL0DvNce9Z1Czn54TUaB0su+2AUa5yfMfX1EIhFxnFjlKVqYH9Oz2V1+ENuHWb4eV+V eKvkWonpB9sqTWoxMcsi4zJipgbyl/a9SV52oI1KsOjRU50ZN6rCppQtyWAO4RqRcMiRnhlt SAnwbIJpZC1ZjIFyIg7xxHBcfyHdZCF7xD9WeuRIDp1i3xrdbGiixu28kWuyvHxWtWp3VtWo SdIltbCu24M2hHR5MaKVvRw80Si1DiB1w3e5O9JLV0qmafdNpUvzLkwlp8JvkTCGC/7gET2j KmMdkUl4Oek8ernYq/gq5SBNIF0khnzProylsG7G+g1MQgDU3KF9eig17Dv50L0TbZMg/Yrj KTZtI3aJd8HpqGnGQ9bz4cj6hehADq+zNgVm2QMIkhfdxKdlYfpPknDIPDmAve7hFShiDJry OrHPr3lG5nCMGXMnKr4cbZz5ENRyxA/zd9Y55JTBbEBJOz8VlXtu9zfCx81Kw20w+D5B9Vhz o4SR36DD6uDPK7RsVKE/PwjL/WPaYMPtzvwKOAp5/v0gn84nV8dc7Op3ZwSaH2gHPRmIkCZb WDigtgfEWcKpA4+Q/LxhV2NVD5cfXeyX6Ym6j4nD4KmCJ/PRoa2j7OZxie0AoVWZnxaClCLC Xrkap2IW+0QZyKKPs9hjjsEWKC9RI8mzBGirRP1y756LuXP4SAYrpLi1N1t5+LJjx0y9Dp0D 96c026XVW10kHkIFHcK2/VUplU14VOe2+AsiPtBUNdX+vlhUwEgNJeawfYsWP7oXQeUXNaMA HirQs+iDHllTNM0hdEDY1x5Fv2tixnC22yhBLpDxO/DP4A97q+Jhyu5HM160XuTkfB51zHOI +NKPGyi3etk8hTLQpXOiwOfnrqrcqIV2GjM8n2CxCyAphIQSxZ+BIPCW31XfU7KtZLh/EqXT b6rT7oqMhFFxOaNL6JLbpviilAVDOz7NoHmanmq03y1GQ7Ow7qNaITwfGBI3iTYTkYJkxoX8 F6JMAE/AmGqpGeNRCd2GwfJZEXhufJ7tGv9TkIwyFSSaFZ90rOu5hMPrfmVSvdW075d/Sl9+ 3N7G1Gy29+QAN2Fz+Z4VINbZ951oFJO1GaC8hd4IoTlNKd6wFgXbwVwuUrqkRRxEIRJ18Yw/ jssy0JpJKSU3UkkFXvQ1I3sOrDRNmj5/Qy+I6/Q1FbE1d+K+6AJoP0molTntQutGwIs6XJim 9VS1nKd4N3NAm9wGdrzU0Nx+RV6vbXXSiY47oLQk3ZrNOj8szPP3c4oGPpw0gypLJ9UNKKJE hO3EtVPXZD/brx33QLxPlRYbLM3luZ8Jc6tevqY1bT+Oe9hmGnjlmFb+MVm1VrK8SNgS+nO1 pJDwveC3wLBWS2v6TXp+s3xh41AYikfW2Slzi2xToxQY+t8cIYRDWqGLMi+x9E4jJnoES09l hbrFxYd1cmldADHJV782Ete2EQNpXGPli6xzjgymDYs5Pn6vmSG06HpcxwJPXROTW9pgAL3I IS6uNsdWVChcwkjkBbNCV/S/6FAv+w/KmDSRRwNZC3qNyR5VbP2sLOeYslJ4ZdusCNNUe36b 0rIArL6phIb1WvkEQ48jHg5djTstJj5hRh3oG2YJXd36nHefIl8yAze69rVWfNKlmBeFW8o1 H+NXgj6Y4nh9M7cj5rZt+GiS2+tM/8bOTLmy4+Nrmrz5GFnBwG+g+Hmn9TmFQYg1iqon9JuV CjOsFP9etyxj/X8Yb8hJBE4QgOsuK8YUslkn4A9hY8dwy0fj5SRpj8clHvrdM5cweT4ZWYMQ jgCx5jU5hLk0QttNCHspcqxW3ODz89mf9T/bHkR33d37cFPTqmZ7KZAkAN6p1O5qUTaZv03z VJ/gbM+rWUXhe0Eol9nzCSYRL4fHVNcMATjkh2J65a1q6AdNwPNOfCgkUF5m96mFrSLpApRD W34dpkVFih19sxjMVjI3S67+sT+ddLXd95WqgyMnkKKkb1OMJxo3Klv52IvKSfnsHYi0eJ+k RF+wcTwot2cM2s0tKOhXkwDa3usNptVoG2yy/4ZxJre3pjzTMs9XG9QB92xE6ruSHVL5JGFf 06PCGFu9CndQOKFW1fZsAA89zrOC8z5aS/RfiVIi4U6AkHafhQXgRhIDmpg2MdlUFn7noq5N x4pg1JZrl/g9kkTlqQxbUS5CiGH4172IjYsFMrGdEoQt14doReTaYvEt6pyB30Kp8L66lXcd irDIVwPVD9sOATMBki/bOP2tJ+Qrq7BXLr4d7yXPv2PsbAMDa7Wg8//lNI3pXDUcZzednh6U 69hgxQFBysoXZ+D3W1IEn1y9WqFecefoF3UFjRfiMe5/byrXQvu4dDKEL5OKZB0/Ajwh66fN umWjSI/KDBC15pKy2WagL4YlEUfjS1jbVzPWfwJqDLNQaTMm6RWEw9TaiV9M9FN5r492Q8FM NDSi9f83Lp1xvAvDFINWVvkk8CvLcsERgP1fEvAH1qOPa+aKCfjxsj2ZeaxReQVgrkE8RK3v jmfHgnoOTHC3zjlWhazMP1d2SGWOBsN3eP1Oh1pCGXlUJfnckjhaI4x3WBwm+VkwC+aZgt+e XBmfkhAr6Od93Zdi/R7QCla62Z9aPKDg2Cf5vXZLZAftb1qBD51nqRU+idfqfMd4SdaSfhyg CaXoMRppgTskOiKjDRqUABKpx5EgYuKuQNpPqCTpfwiET7UuQkA62mdEUFAv9x+FtjmoLxd0 PDKnaP3bTpOqpfaoZtaCM/TJ8aKdnEmNFC6fVycRBtARjmtO2bFgkVbm/zH7XyZoK8xrZ30k YYPQLtWPLTUPvYTC0AgEdBbZZkrDnUrlrmUiMNO7n27/kG5rCBysZXOV/bUCvLqem7xZVZsa B4BwLe+JoMWZNST5g==
  • Ironport-sdr: 66a494de_Gf3ynpAM/62890BjwTULRpBfIAPoOpOfAlXNIjDvuj/Nuqz Ftq+VpijQKWFopwxPVv29mg2SS9wg1pdqEua7NQ==

Use "ltac1:(pose proof a b c)" to access that tactic from Ltac2.  The set of tactics and their syntax differs slightly  in Ltac2.  The doc gives the Ltac1 info.

Jim


On Fri, Jul 26, 2024, 10:39 PM Iaroslav Baranov <kciray8 AT gmail.com> wrote:
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:
  1. 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.
  2. 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

kciray8 AT gmail.com




Archive powered by MHonArc 2.6.19+.

Top of Page