Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Call to Rewrite tactic from OCaml in a coq plugin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Call to Rewrite tactic from OCaml in a coq plugin


Chronological Thread 
  • From: "Андрей Козырев" <kozyrev.andreiii2016 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Call to Rewrite tactic from OCaml in a coq plugin
  • Date: Tue, 10 Jan 2023 15:40:48 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kozyrev.andreiii2016 AT gmail.com; spf=Pass smtp.mailfrom=kozyrev.andreiii2016 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f49.google.com
  • Ironport-data: A9a23:2ImoXK5gdLyILkN3hZAgnQxRtODDchMFZxGqfqrLsTDasY5as4F+v jdMXG2Bb//bYjamct91Pd/gp0gPscDWzYVkSARlpXgxZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOC6UYYoAwgpLSd8UiAtlBl/rOAwh49skLCRDhiE0 T/Ii5S31GSNhnglbAr414rZ8Ek05K2r4GtD1rADTakjUGH2xyF94K03fvnZw0vQGuF8AuO8T uDf+7C1lkuxE8AFV7tJOp6iGqE7aua60Tqm0hK6aID+6vR2nRHe545gXBYqhei7vB3S9zx54 I0lWZVd0m7FNIWU8AgWe0Ew/y2TocSqUVIISJSymZX78qHIT5fj6+tHEFMEAZYjwaFMGHxK+ PsVciooYSnW0opawJrjIgVtrsEqLc2uMYFG/388nHfWCvEpRZ2FSKLPjTNa9G1o14YeQLCEP ppfNWsHgBfoO3WjPn8UD4Avhuq2wHD5fydVqVOU//JuvUDcyQVw1P7mN9+9ltmiGZkLwR3J+ TquE2LROgs4MNiv9B+/2EnzqKzPuXjnW64QPejtnhJtqATLmjZ75ActfVC8uLyyjlO0c8lOL lQdvCsot6k7skKxJuQRRDW9qX+A+xMeAp9eT7x85waKxa7ZpQ2eAwDoUwKtdvQ4ndMkdwAx7 WTOpMr0ATFoveePbH2ko+L8QSyJBQAZKmoLZCkhRAQD4sX+rIxbsv4pZoYzeEJSpo2lcQwc0 wxmvwBl2OpO1Z9jO7GTuAGY02j19/AlWyZsvl2PNl9J+D+Vc2JMWmBFwV3S7PIFIYTAC1fd7 T4LnM+R6O1IBpaI/MBsfAnvNODwjxpmGGeE6bKKI3XH32rzk5JEVd4NiAyS3G8zbq45lcbBO Sc/Qz956p5JJ2eNZqRqeY+3AMlC5fG+So+/BqGMNIEUOsIZmOq7EMdGNR74M4fFwBhErE3DE crznTuEVydEVPs4nFJauc9NjOZ3rszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4FX+PTk0s3eLSnPkH/rNBORXhXciBTLc6s96R/KLXYSiI4QzFJNhMk6el+E2CTt/8FyLmgE 7DUchMw9WcTclWedV7SNy06Neq3NXu9xFpiVRER0Z+T8yBLSe6SAG03LvPbpJF2r7Qx/u0+V PQfZcSLD9JGTzmNqXxXboDwoMYmPF6njB6HdXjtKjUuXY9SdyqQ8P/dfyzr6HYvCAizvpAAu LGO7F7QbqcCYAVAN/zoTsyT4Wm/hlUno9IqbXD0eoFSXG7O7LlVLzfAi65rAsMUdjTG6Dio9 yeXJhY6o+PyjZc/24TLj/rcrqOCMeh3LmxFFUb1sJe0Mij7+DK44IliCeynQxHUZFnWyo6DO 9pH7qjbG+IVuXp3qKxAKqZP4YNiwsrwtplY4x9BHn6WX2+0C7hlHGaK7fNPuoJJ2LVdnwm8A WCLxfV3JpSLP9HDAncKBQ94cNmG6+4YqgPS4dsxPk/+wi19p5iDcEdKOiizmD5vF6R0PKwl0 NUelpYvsSLnsSUTM/GCkixw3EaPJCZZU6wY67crMLWygQ8vklx/cZjQDxHt2662avJODBgOA iSVj6/8lbhj1hL8U34sJ0Psg8tZp7oz4S5v8nFTBm60iuLkh+A21iJ/6T4YbBpY5TQZ3vNRO lpEDVxUJ6KP9QhGnMJoBmSlGSxdNh+gp2j0x0UDzmHCfXL1VGaXdGwZEsSO9XA/7GhzUGV6/ raZ6WC9ShfsXpj78RUTUH5fic7IbIJO5CjdvsG4DuK5H5UeShj0sJ+EPGYnhUPuPpIsuRfhu +JvwtdVVYT6Eiwh+4sAFIiQ0OUreiCufWBtb6low/IUIDv6Zjq35DmpLnKxcONrI9jh0xexK +5qF/J1eyWO7gS8hRFFOvdUOJ5xpuAj2/QacLCyJWImjaqWngA0jL3urBrBlE0ZaPQwt/ZlM Y7AVSOwIkrJj1tupmL9hs1lOG25XNo6WDPBzN2FqNsuKZZSn9xvIGcT06S1tUq7KAFI3QyZl yKdar70z95N85VNnYztIP8aBwyLNs7CDrWU0QGssuZhacHEHtfOujg09HjmHVVyFpkAV+tnk Y+itIbM43rEm7ItQkbllIKkBYAQwemPBM9sLdPQAFxBuCmzSOvAwkAkxTijCJprlNh92JGWd zGgYpHtSe9PCsZv+nJFTgN/TTMPALvTRYX9r3qfq/+sNEAs4TbfJon6yU6zPHBpTQ5WCZjQE QSuhu2P4Opfp4FyBBMpIfFqLpt7AV37U5sdaNzDmmiEP1asn2+9lOPupTg45RHPL0u0IsLwz JbGZxr5LRqM4fCCiJkTtoFppRQYAUpsmeR6LApX59dyjCv8F2Ica/gUNZIdEJxPjyjuz9fCa SrQaHc5QzDINdienc4QPPy4NuteOgAPBjs9Djkg/kfRZiXvQY3cUf1u8SBv53owcTzmpA1ix Rfy5VWoViVdALkwLQrQ2hB/qehiz/LegHkP/CgRVuTsVg0GD+xiOGNJRWJwuO+uLy0JvErOL GkxA2tDRSlXjKI3/dlIIxZoJf3SgN8jI/jEo8tCLBYzdrh3FNF99cA=
  • Ironport-hdrordr: A9a23:9f5VcqoEVJArg9PDB56FzgMaV5oDeYIsimQD101hICG9Ffbo8/ xG/c5rsCMc7Qx6ZJhOo6H5BEDtewK+yXcK2/hpAV7SZniAhILAFugLhuvfKlXbehEWndQts5 uIHZIOc+EYzmIXsS852mSF+5JM+qjkzEllv4jjJg9WPHtXgmhbgTtENg==
  • Ironport-phdr: A9a23:wwochhMM89jPuuPKAJgl6naKBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6gr3QWCBdyTwskHotSVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5Z3ebx9MiTajbr9+M Ai6phjNu8cLhodvNqk+xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3Q rJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6 bpgRRn1gykFKjE56nnahMxsg6xUrx2vuh9xzYDKbo+SL/d+YrrdfdYGSWpBQspcVSpMCZ68Y YsVCOoBOP5Vo4fhqlsOtRq+HRejBfvywTFNgX/3xbU70/w/Hgzb0gArAtUDsHfTrNT0NKYSS /66zLfSwTrZafNZxC3955bJchAgoPGAQ658fdfQxEQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmW OmyhGEptxt/rSKzxscwlIbJnIQVx0jY+ChnwYs4J921RUF7b9CkDJZcqi+UOpZ4TM88XW1lp Ds2x6AGt5O1ciYEx4grygPRZfGDcoWF7BztWfqSLDp7gn9uZbGxhw6q/ES+1uHxUtO43VVKo yZfjNXAq3MA2wbc58WDUvdx4Fqt1SiV2wzN9u1IPFo4mKXUJpI73LI9mZ4evELeFSHsgkr2l rWZdkA89+io9evnZrLmq4eZN4BuiwH+Nr0ildK9AeglKwQOUWeW9OCm2L3s+k35R7pKjvkon aXDrJ/aIsEbqra4Aw9TzIkj9w6yAym63Nkch3UKL1JIdAiZg4T0OFzCOv/1APOnj1Spijhrx vTGPrP7ApXKK3jOiLThfbF86k9c0go8085f64hOBbEHPf3zQFH+tN3ZDh84LQC43/vrBdRm2 4MRXGKAGK6ZMKfIvVCU4eIvJvGAZIkOtznlMfgq++bujWMlmV8aZaSlwIMbaGqkEfR+P0WZf X3sj88dHmcNpwoyVfDliFmfUTFIfHuyRKI95jQjCI28F4vDR4atgKaA3CihBJFWaHpGWRiwF iLjcJzBUPMRYgqTJNVgm3oKT+uPUYgkgFuHtObixlMvDe09EzUVn9irgNty9fzJmA90/Dp4F cmc0mDXFzgqtmwNTj4ymqt4pBoumR+4zaFkjqkARpRo7PRTX1JiXXa95+lzCtSpHxnEYs/MU 1G+BNOvHTA2SNs1hd4IeUd0Xdu43VjYxyT/JbgTmvSQAYAstLrG1i3yINRs0XvYkqAng0MrQ 8pObzX/2IZw8gHSA8jClEDK372ye/Ek1TXWvHyG0XLIuUhZVABqVqCQXncNd1Hbs5Lw4E/YQ r6vCO5/a1VpxsuLK68MYdrs3h1dXPm2HtPYbiqqnnuoQxaFwrTZdI3xZ2AUxznQEmABmgEXu HuEbE0wWnbnrGXZAzhjU1noZisA6MFYr3W2Bg8xxgCONAh60qatvwUSnbqaQu8S2bQNvGEgr S91FRCzxYCeDd3IvAdncKhGBLF1qF5ayWLUsRB8NZ28PuhjgFAZaQF+o0Lp0V1+FIxBlcEgq H5iwhB1LOqU11ZIdjXQ2p6VWPWfKW7g7Qqidejf3F3E3deX+/1XsaoQpFDqvQXvHU0nsj1m3 9RTz3qA98DSFgNBNPC5Gk0z9hV8u/Tbenxnv9KShSAqa/Dk9GOTiLdLTKM/xx2tfslSKvaBH Q72SIgBAtS2bfctgx6vZw4FO+Zb8Og1Odmnfr2Iwv3OXq4okTS4gGBA+I043FiL8n82Senaz owI3beR2AedWjb9jQ35657floVNZDVUFW26g3uBZsYZduhpcIAHBH37ac6w1MRkioCrUnhU7 lOiBlJcgJb3URWXZl35mwZX0A5ExB7v0Tv9xDtynTYzq6OZ1yGb2OXuei0MPWtTTXVjh1PhS WStp+gTR1PgLw0glR/+oF3/27Aev6NnaW/aXUZPeSHyaWBkSKq58LSYMYZD75YhsCMfV+rZA xjSSbnvsgEXzWXqGWdEyTE6dmvy48vRkBlziWbbJ3F25HbUYsB/wx7D6ceUH6YAmGpbAnMh2 X+LVxC1JLzLtZ2Mmo3Gs/yiWm7pTZBVfSTxjMuBuCa9+Wx2EEi6lvG3lMfgFFty2iv62t92E CTQ+UykM8+7iuLgaLIhIhg7YT20o9B3EYx/jIYq0ZQZ2HxBw46Q4WJCimDrd9NSxaP5anMJA z8N2d/cpgb/iygBZjqEwZz0UnKFz45vfd6/NykV3TAs9c1UTq6S4KZJnCp0+ALh8yreZPF8m nEWzv5kuxt4y6kZ/REgyCmQGOVYHk5KLDbhiVKB6dykoaRWZTz3KOaY2093nNTnB7aH6FI5O j6xatIpGil+6d96OVTH3Sjo643qT9LXaMoaqhyelxqTx/gQMp86keAGwDZ2IW+o92Nw0PY11 FY9uPPy9JjCMWhm+7i1RwJVJiGgLd1G4Snj1O5fhprEhN3pR8Q5XG9XA92wCqj0WDMK6aa5a 0DUS2Z68ynDX+KYRF76ig8urmqTQc71cSjPfj9Bi40lHkHVJVQD0l5KGm9mz9hpTkbyg5a5O EZhumJOvBih9l0Vm7gub16mAgK97E+pcmtmF8TZdUALqFkEvwCMb4Sf9r4hRnkIuMT+80rdb DTcPV0ADHlVCBXbXBa6b+XovZ+YtLHGY4j2Z/rWPefU8b0YB6rOnMj/lNMhpmnEN93TbCM7U btmigwaDCo/Q4OAyn0OU3BFzXuTKZTA9VHnoGsv6ZnulZajEBTm4Y/FY1dLGfNo/R3+waKKN urLwT18NS4dzZQUg3nB1LkY2lcWzSBobTikV7oa52bLS+rLl6lbAgR+CWs7PdZU7686wghGO NLKwtLz2Llii/cpClBDHVX/k8CtbMYOLimzLlTCTEqMMb2HI3XMzaSVKeukTqZMiexPqxCqk TOSEkumMzba0je1BlagNuZDiCzdNxtb+cm8fhtrFWn/XYfmZxm8Y7oVxXU9xbw5gG+PNHZJa 2AtNRMQ6OfJvWUE06YaeSQJ9HduIOialjzM6uDZLs1Tqv53GmFvkPoc5n0myrxT5SUCRfpvm SKUoMQ9xjPu2uSJ1DdjVwJD7zhRg4fe90ZlK7TD+4cGUHDI5h8M7GTKU01Uj9RgA9zr/atXz 5Kc8cC7YCcH6N/S8cYGUoLML9mbNXM6LRfzMDvdDQ9AQDzycG+D1gpSl/ad8nDTpZ8/4MuJ+ tJGWvpQU1o7EekfA0JuEYkZIZt5aTgjlKaSkM8C4XfWRPz5S8BTv5SBXfWXU62HwNexiLBFY 14Fw+q9I9hCcIL83ENmZx9xm4GYQyI4svhCpyRgakk/p0AfqRBD
  • Ironport-sdr: 63bd78f2_rBPT9PxZk0maBS6qsf5PJ232KU/7F8E4PheKxkNoeCIlfc+ s3QjoE4Pi7Lp1ooy3f0iyyKiJxMXCG5nGaMTppw==

Hi everyone,

I am writing a COQ plugin with a custom tactic in OCaml using coq-api 8.16. I
need to modify the current goal of the proof by a call to rewrite tactic. I
am struggling to do that. I have a name of the theorem I want to apply and
the direction I want to apply it at.

I’ve seen an «apply» tactic in «Tactics.New» module, but it takes a
«Econstr.constr» as an input, meaning I would need to extract the
implementation of the theorem myself. Moreover, «apply» will not be that
useful in my case.

I’ve also checked the Rewrite (previously Ltac_plugin.Rewrite) module, but I
am struggling to find how to use its functions appropriately.

Does anyone have ideas? Thank you in advance.

Regards,
Andrei

  • [Coq-Club] Call to Rewrite tactic from OCaml in a coq plugin, Андрей Козырев, 01/10/2023

Archive powered by MHonArc 2.6.19+.

Top of Page