coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo AT irif.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with last version of CoqHammer
- Date: Wed, 7 Sep 2022 13:27:05 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
- Ironport-data: A9a23:aMHmkq9ecqu0vL1I+lpgDrUDqXiTJUtcMsCJ2f8bNWPcYEJGY0x3m mQbWmiCOP+DMWSmf4p1bou3pEMD68CGzoNqGgBprH9EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9i6mJUqYLhWVnV6 Iut+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Zx txG6LywRzUTIazOpc1BckFyAXBQFPgTkFPHCSDXXc27zErcdH/h3bNzCkAoeJUR4OdsXidA7 5T0KhhUP0zF3b/qhuziDLA31qzPL+GzVG8bkm1gwDbxDOwnT9bNWc0m4PcFhWhq2J4RR54yY eI9ZyZ3ZxnCbCREEX5IVrkih+2Fi1nGJmgwRFW9/PZmsjeDk2SdyoPFO93MP9eOWM99hVedv muA/mLjAxhcOsb39Nae2nGrnOjLkD29RYQTCvig/+RrmwLVyHZ75AAquUWTr/Cy126+VeBlN E0WxwNyjPAY5h2FZ4yoN/Gnm0KsshkZUttWNuQ17gCR16bZizqk6ng4oi1pNIx275VsLdA+/ gXVx4y0bdB6mOfNERqgGqGoQSSaFxJ9wYUqXSYeTBBtDzLL/9xr106nojpLu0ixg5j5FHTe2 TmMpyVWulnysSLp//vrlbwkq2v8znQscuLTzl6HNo5Cxl8iDLNJn6TytTDmAQx8BIiYVEKdm 3MPhtKT6usDZbnUynLXHLVcROv3vK/dWNE5vbKJN8d+n9hK0yD/Fb28HBkkdBcB3jssJW+5P hWM42u9GrcCZib0BUOIX25BI512nPm/RYuNugH8dNdIa4R8bme6ENJGOyatM5TWuBF0y8kXY M/FGe71VCZyIfk5kFKeGrlMuZd1nXpW7T2IGvjGI+GPiuf2TGSLUo0MLFbmRrl/tMtoVi2Or 40AXyZLoj0DONDDjt7/qt5PcgBXdSBkbX00wuQOHtO+zsNdMDlJI5fsLXkJIuSJRoxZybXF+ G+TQEhdxAatjHHLM1rYa2piZvXhR88n/348OCUtO3eu2mQiONr0tfpFJ8duLLR3pvZ+yfNUT uUef5nSCPp4TDmaqS8WaoPwrdA/eRny3VCOMiOpbSIRZZllQwCVqNbochGwpigUDyTxu9Fn+ ++s0QbSQJwiQQV+DZ+KM6vylQPt5CkQwbsgUVHJL99ffFTX3LJrcyGh3OUqJ8wsKAnYwmfI3 QihBxpF9/LGpJU48YWUiK2J89WpHu95EhYIFmXX9+zsZyrd5G2nzJEGTeCJY3XFXXn14/rka /8Ml6PwN/gOnVBrtYtgEu8zlPhuuYCx/+dXnlZ+AXHGT1W3Ebc+cHOI6sl4qfEfzLFuvwbrC FmE/cNXOOjXNZq9QkIRPgcscs+KyeoQxmvJ9f0wLUimtjV7+qGLDRdbMxWW0nYPL7xvN4co3 6E8vs8IrhS2kBsxbZCIlHkMpWiLK3UBVYQht40bWdey0Fp1kQ8aOZGMWDXr5JyvaslXNhd4K DGjhJ3d2+ZWyH3EfidhDnPKx+dc2MoD4UgY0F8YKl2VsdPZnftrjgZJ+DE6Qwk9Is+rCA6v1 ryH9nGZJJliOx9rg9JEW22yXRxHBQPc4kXrykBW0mPDJ6VtuqohM0VlUdthPmhAm46fQtSf1 LCCyWijXyyCkATZwH4pQUA8wxD8ZYUZy+AB8fxL2+yEBZg0JzT/6kNriazktDO/af4MaIb7S SWGMQq+hWAX9cLdnkHjN7Sn6A==
- Ironport-hdrordr: A9a23:H8oO2qCWMC4+Il3lHekF55DYdb4zR+YMi2TDsHoBNiC9E/bo6/ xG+c536faaskdpZJhNo6HnBEDEewK6yXcX2/h1AV7BZnichILAFugLhuGMrVzd8m/Fh4pgPM xbAtJD4bPLfCVHZAXBgDWQIpIPxNGG9eSPnufRz3BkSEVPZ7t75wl0Tia3e3cGPDWuyaBJd6 Z1aad81kSdUEVSSsS/G3UfU+Wrnay7qHsuW29lO/f50mWzpALt6/rxEhqd1hcaFx9J3rsm93 Hdn2XCl9WemsD+yVvX1m3W55RS3OHqzMBObfb8+fQ9G3HuzgyoZoBoW7jHhi08vf20gWxa4u Xxnw==
- Ironport-phdr: A9a23:C2sSZxMNKtYNuxPgwEIl6nY7BhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r1weRFt6Lo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJbQhEmCaxbbx8I Ri1sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85 Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb 4UBAekcM+hGs4bzqEADrQenBQS2GO/j1iNEi33w0KYn0+ohCwbG3Ak4EtwQsHTTttL1O78RX uC0yanIyCvMb+lT2Tjn7ojIdA0qrPaQXbJwb8XRzlIiFwLfjlWRp4zpJT2V1v4UvmWd8uFvW v6hhXQ9pAFtvjig2N0sio/Ri48JyV3J6zt1zZs1K9GlVEJ1Yd6qHYZMuiyaNIZ4Td0uTmVst Ss01rELuZG1cDYKxZkl2xLSd/OKfouG7x/+SeqcJypzinxieLK6nRmy8E6gx/XzVsm1zFZKr jdFncLWun8R0BzT786KQeZ+8Ee5wTuDygTe5+5eLUwqlafWJIQtz78tmpYJrEjOECz7lF3og KOKckgo4Oul5uT9brn4uJOQKZV4hhz8P6kqnMG0HP42PRIUX2eB/OSxzL3j8lP9QLVNlvA2k a7ZsIrdJcQfuKG5HRVZ0psl6xa+ETeqycwYkmMdLFJEYxKKjZLlO1/UIPzgDPe/hUqjkCtzy vzbOrDsDY/BImbDnbruZ7pw6lNQxBAuwd1R5J9YErQBL+jyWk/1utzYFBg5Mwmszub7CNVyy IQeVHmOAq+DMaPSv0WE5uw1I+WUYo8aoy7yK+I56P72kX85hVgdcLG00ZcPcnC3AuxmI1mFY XrrmtoODWAKvhMnQOP2jF2CTCVcam2pX6M84zE7EJipAZ3CRoCrmryB3T20EodYZmBcWRiwF iLDcJzMcPMRYmrGKch41zcASLKJSok71BjouhWsmJR9Ke+Bxi2ZsqXR1d1w6vfWnBc0vWhoD 8ma+2CXTm8ykHleFGx+57x2vUEokgTL6qN/mfENUIULv5uhMy8/PJ/YlalhDszqHxjGdZGPQ UqnRdOvBXcwSMgwypkAeRU1AM2s2zbE2SfiGLoJj/qTHpVh7qLR2FDwPcdzjXjch+E6l1dze sJULiW9g7JnsQ3aBorHiUKcwrqqeKM03TTM+iGN1znGp1lWBSh3V6iNRnUDfg3WoND+s1vFV KOrAK87PxFpysmYLa9HdJv0i1RYAe/qItXFPCS/gQ9cHD6uwbWBJMrvcmQZhmDGDVQc1hoU9 jCAPBQ/ASGopyTfCiZvHBTheRGk9+42s369QkIuqmPCJ0R8y7q4/AIUjv2AWrsS2LwDoiIot zRzGh60wdvXD9OKowcpcr9bZJsx51JO1GSRsAIYXNToM6BvgXYfaQV5+U30ll12BohGjck2v SYy1gMhYamc0V5Ha3aZxcWpa+GRcDSuuk72LfeNigK7sp7e4KoE5fUmpk+2uQioEhBn6HB7y 5xP1HDa4JzWDQ0UWJa3U0At9hE8qauJB0t1r47Sy3BoNrG59zHY3Nd8TvclxxGIfs1ePuWKD kWhW91fHMWoJOEwzhK1bh8DFOFI9aByMdnsJJ7kkOa7ee1nmjyhl2FO5otwh1mN+yRLQenNx 58Zwvuc02NrTh/EhUy6+oDykIFAP3QJG3anjDLjD8hXb7FzeoACDSGvJde2z5NwncylV3ld/ V+lT1QIva3hMQaSYlvV3BdR2wIZuzSrlDC5wDp9jzwy5vPOgGqUnrikKkNBYzUbDGB5xU/hO 421k8wXUACzYg4lmQHkgCSyj6lXqaJjLnXCFEJBfiz4NWZnAeO7sruPZdIK6Yt96HQLFr7hP RbEE/ik+EtJtkGrV3FTzz06aTyw75DwnhggzXmYMG42tn3SP8d52RbY4tXYA/9XxDsPAidi2 ly1ThCxOcek+dKMmtLNqOe7Aii9VpBUWSjxzI3GujHxtiV6RAaymfy+gIitDQg31gf6zdhkE yvS5kWZAMGjx+GxNuRpeVNtDVn35p9hG41wpYA3gYkZxXkQgpjGtWpCi2r4Ns9XnL7vdHdYD yBe2MbbuUK2vS8rZmLM3Y/yUW+Rh9dsd8XvKH1DwToztohPGO/D5bhA10OZu3KeqgTcKbh4l zYZk7417WICxvsOs0wrxzmcBbYbGQ9ZOzbtnlKG9YL2qqIff2upfbWqsSg21dm8ELGPpB1dU 3fla98jGyF39MB2LFPL1jX69IjlfNDaad9buAeTll/MiO1cKZR5kfRv52IvIWXmoXgs0PI2l zRt2ou9uIWZbXhr/bz8GhdCNyaqIc0Ju3nsgatYgseKztWvE5FmSVBpFNPjSfOlFi5XtOyyb lfSVmdh9jHFQPyGRl/MjSUu52jCGJ2qKXyNcXwQzNE4AQKYOFQamgcfGjMzgp8+EAmugs3na kZwoD4LtTua4lNBzPxlMx7nXyLRvgCtP30oSJWYBBtM7w8E6V2fYqn8pqpjWjpV+JGstlnHM muAewFBFn0EQGSHAErkOrSwo8TG8vbdHuOkLuCRJ7uU4787Nb/A1dek1Y1o+CyJP8OEMyx5D vE17UFEWGhwB8XTnzhno8M/ljjMYYiVvkXlksWWhsO46vPvVRyp+I2OFf5KOM9u4E/wj73Rb 4Z4YQ54MzdWkJ0Wlyeg9Q==
- Ironport-sdr: eJ5URay6LBsVlw4KYZXcSxqufTsQo2Msv/zcknADTeAk2vWg4ayjSadEKz7HzR+WLfIty0hKoQ 82sI1mcYsOqWIJ3/ziIS2rzs4eDE8ZVIoI424HeKMw74gFAwagkAHPGOMlETtHYaZ+AW+jrmMf HqmXSVY8tYBQU4XVn/+H9Oc4A1V6Mj8GJh2pATec8sXrbkTDE5jpcXrFpYq97uTqfeETevJWuG oq1f70jEgy8sVizRY8LnVcju81gyHr7NKW0Pc1K6tXYVmsCwcPXre49srRwVvB39aJnlt00kDL VumkGuHeBg8V0quJryDFb/ap
Hi,
I'm not very knowledgeable about CoqHammer, so I'm not fully sure
whether this will help but:
- srun eauto use: indeed gives a syntax error whatever the version of
Coq (I've just tested this with Coq 8.12-8.15 and an appropriate
CoqHammer for each of these versions).
- However, sauto use: does exist. I haven't been able to test your
particular example since you didn't give specific instructions to
reproduce it, but I suggest that you try that instead.
- It also looks like the problem you encountered was already reported
but with no response so far:
https://github.com/lukaszcz/coqhammer/issues/144. Maybe we should ping
the maintainer.
Cheers,
Théo
Le mer. 7 sept. 2022 à 07:54, dapoignyrichard AT yahoo.fr
<dapoignyrichard AT yahoo.fr> a écrit :
>
> Dear all,
> I have installed the latest of Coq (8.15.2) together with CoqHammer and
> additional provers.
> Some lemmas are proved but when i reach the following:
>
> Lemma set_eq_equiv : forall s s':N, incl s s' /\ incl s' s <-> set_eq s s'.
> Proof.
> hammer.
> I get a positive answer:
> CVC4 (nbayes-32) succeeded
> - dependencies: Mereology_on_Onto_sets_v3.DST_signature.incl_set_eq,
> Mereology_on_Onto_sets_v3.DST_signature.set_eq_incl
> Reconstructing the proof...
> Tactic srun eauto succeeded.
> Replace the hammer tactic with:
> srun eauto use: incl_set_eq, set_eq_incl.
> but when I replace hammer with the above code i get the following error:
> Syntax error: [ltac_use_default] expected after [tactic] (in
> [tactic_command]).
> (the colon symbol is colored in red)
> If any one has an idea?
> Thanks in advance.
> Richard
>
>
- [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Théo Zimmermann, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Łukasz Czajka, 09/07/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, dapoignyrichard AT yahoo.fr, 09/08/2022
- Re: [Coq-Club] Problem with last version of CoqHammer, Théo Zimmermann, 09/07/2022
Archive powered by MHonArc 2.6.19+.