coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] “Running” Proofview.tactic to see if it would succeed

From: RanDair Scott Porter <randair AT uw.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] “Running” Proofview.tactic to see if it would succeed
Date: Fri, 7 Aug 2020 07:41:17 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=randair AT uw.edu; spf=Pass smtp.mailfrom=randair AT uw.edu; spf=None smtp.helo=postmaster AT mxout22.s.uw.edu
Ironport-phdr: 9a23:6AoUNhaAYOBLiRoQM89LTsH/LSx+4OfEezUN459isYplN5qZoMWybnLW6fgltlLVR4KTs6sC17OI9fC6EjNdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsrgjdqMYajIliJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UrhKvqRJ83oDafp2aOeFkca/BZ94XX3ZNUtpTWiFHH4iyb5EPD+0EPetAs4fyvV0OoxWkCgmtHuPk1yJGiWPx3a0mz+QqDBvI3As6H9ISrnvUtsj+OaAIUe+vyqnH0C/Mb/JM2Trm9YjJfAotru+RUrJtaMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+duWv6jhmo5pwxvoDWixsghh43Gi48Wzl3I6Th0zZo1K9CkSkN2fcKpHpVOuiyHOIZ6X8cvTW92tCsmyrALpIC2cS4Xw5ok3x7Sc+GLf5aL7x75UOucIS10iGxqdb6hnRq+71asxvPkWsWqzFpHqjBJn9rMu3wXyRDf98uKRuF880ql3zuEyhrd5fteIU8ukKrWM54hzaA0lpoUqUnDGyD3mELrjK+KaEko5PKk6//9brX7qJ6QLZF7hRzjMqg2m8y/B/o3MhQWUmSG5+ix16fv8En5TblQkPE7nbfVvIrEKcgFuKK1GwpV3Zwi6xa7ATemytMYnXwfIVJfYh2HiZXmNEvPIPDiFvq/nlqtnC11yP/bI73tGo/NIWTbkLf9YbZ97FZRxxY0zdBG/p5bFrUBIO/oVULqr9zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6KO6VIYQRpTzVKv4/5veog2Vqt0UaePyT1J07YXGiVs9tJFmFKULrmMsMCy9epAM4QOXrknWfTnhea2vkDPF03S0yFI/zVdSLfYuqmrHUhH7mTK0TXXhPDxW3KVmtd4iAXK5cOieCJdJ9yGZCTv68VMks2Qz87FammYoiFfLd/2gjjbymzMJ8t7/Oilc/+SEmV53MgVHIdHl9myYzfxFz2al+pUJnzVLTg7VnxfFUCI4K6g==

Hi all,

I’m writing a plugin that suggests a sequence of tactics to copy-and-paste into my proof.

I would prefer not to generate tactics that fail. My idea is to first build the Proofview representation of these tactics, and then to silently “execute them” on a goal/environment. If it fails, my plugin is to consider different tactics. Is this possible?

Thanks!

RanDair

[Coq-Club] “Running” Proofview.tactic to see if it would succeed, RanDair Scott Porter, 08/07/2020