coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "dapoignyrichard AT yahoo.fr" <dapoignyrichard AT yahoo.fr>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Problem with last version of CoqHammer
- Date: Wed, 7 Sep 2022 11:54:37 +0000 (UTC)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dapoignyrichard AT yahoo.fr; spf=Pass smtp.mailfrom=dapoignyrichard AT yahoo.fr; spf=None smtp.helo=postmaster AT sonic311-30.consmr.mail.ir2.yahoo.com
- Ironport-data: A9a23:c6lrYa5Vv3VbwPJYcJwSsgxRtKTBchMFZxGqfqrLsTDasY5as4F+v jNKWWzTOPzZYGT0LY9ybYm3pBkBvcPWnNFjHVc/+X9hZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2eaEvfDjW1nX4 YKq/JWFULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 O0dsYWbYyZ4B4LjxO1GQwBECmZ3FpQTrdcrIVDn2SCS51bBdXrnmKw3SRpue4Yf/P1yGydL/ P0cbjEXNFaSjuKxx/SwTewEasYLc5atZthP/Cg/k3eAU6xOrZPrG80m4fdU1S83h89IDOzfb MoQczZHfR3AZBoJNE1/5JcWwb733SGuKmIwRFS9/fF0yFHiywZKiJfIIOfbfd+QRPtlpxPNz o7B1z+jXkhGboD3JSC+2nmrn6rEmT7xcJkDEaWxsP9smlyagGIJYCD6TnOgpv+4gRXnApcEc wof/Sw1qLJ08UWqSp/8RUf+sXeEuRlaUN1VewEn1O2T4pKE5x+yLElVdxFuNNV9pNYqXHsj/ WbcyrsFGgdTmLGSTHuc8JKdojWzJTUZIAc+icksElVtDz7L/99bs/7fcjpwOPPu1YaqSVkc1 xjP8nJj1u17Ydsjjf3TwLzRv967jrnkJuLfzinKVGak6GuVj6aJP9bABbTzyftBKp2FQ0Ppg ZTps9OZ6uEFVsjU0XfVBu4KGqqs/bCAOTzYx191Rd8w/jSq/DioeoU4DNBCyKVBYp5sldzBO hW7VeZtCHl7YSbCgUhfPt7ZNijS5fK8fekJr9iNBja0XrB/dRWc4AZlblOK0mbmnSAEyP9hY 8vLIJ72XSlBVMyLKQZaoc9DgNfHIQhglQvuqWzTlnxLLJLFPyHEE9/pznPSMb9RAFy4TPX9q IwDbpfQl32zocXvaynQ9sdbMFNCNnUhG5H9ptcfcu+GIxZrFAkc5wz5ntscl3het/0NzI/gp ynjMmcBkQaXrSCZdW2iNy87AJuxB8oXhSxgZkQEYw33s0XPlK70sM/zgbNsIOF7nAGipNYoJ 8Q4lzKoWaQTFWSao2xCBXQ/xaQ7HCmWacu1F3LNSFACk1RIHmQlI/foIVni8jcgFC2yuZdsq rGszFOJUJMDQAMkAtyPMKCjyFa4vH48nuNuXhuUeYAMIBm0qIU6eTbsivIXIt0XLUmRzDWt0 QvLUwwTovPAotNo/dSQ3fKEoo6lHvFQBE1fG2WHv7+6OTOKrHuqwYhHFuiSJGiPWGTx8aSkR ONU0/CsbKZeww4W69JxSu85w7g/6t3jo65h4j5lRHibPU62Dr5AI2Wd2ZUdvKN6wLIE6xC9X ViC+4UHNLiEZJHlHVoWKFZ3Z+iPz6pLyCLV6/U+exyjoXQvurGAV15XJV+JgS1ZarpvasU0y Ocmv4gd7Anm0kgmNdOPjyZ18WWQLyNRC/l/68tCWIK72BA2zlxiYIDHDnCk7ZyKbeJKOBZ4L zKRgp3EmLkBlFHJdGA+FCSW0OcB144CvgtGkA0LK1iTwYWXnfgx3RYKqG1yFVwTxRJByOdpf G1iNkkzJL/UuSZhhM9EGWurHlgZVhGe/0XwzXoPlXHYEBjwCjSQdjVlNLbf5l0d/kJdYiNfo +OVxWPjZjDgI5P80y40bkh6pqGxVtd27ADDxJuqEsnt80PWutY5bnJCpFbkqicLxesqg0vGr rIzpaMrMevwMigLprd9DoCb0fIRUkrCNWVCRvYn96QMdY0ZlPdexhDWQ31duOsUTxAJzaN8I 91nJsVIERqkvMpLhi5OHrYCeteYg9ZwjOfvudrXyaouorKfqT0vvoi4Gu0SQoM0a40GrPvR4 b89u95P/qJ8SJeUd6LwQBF4B1eF
- Ironport-hdrordr: A9a23:d1jz5q4r2pLHstVbbQPXwN3XdLJyesId70hD6qkDc31om62j/P xG88536faZskdyZJhko6HkBEDiex/hHPxOi7X5VI3KNDUO+lHYT72KhrGN/9SPIU3DH6Jmup tdTw==
- Ironport-phdr: A9a23:daPqrBaPe7xj37fyiBiCieP/LTEj2oqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1gSPBt2DoK4Yw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PdbglSijexfa9+I Bq5oAjeq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ 7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4 qF2QxHqlSgHLSY0/m/XhMJuj6xUohyhqQFwzIHIZ4+YL+Bxcr/GctwBX2dNQsRcWipcCY28d YsPCO8BMP5Wo4bgvVQOtRy+BQijBOPpyj5InH720rE60+s7CwHJwRctHtIUv3TUq9X1M70eU e6vzKXG0D7OaO5Z1i3l6IjPcxAhrveMXLJqccrQ1UYvFxnKjk+NpoH+PzKazOQNs2+c7+Z6W +KvkXcqpgdsqTeg2skikJPGhp4Jyl/a7yV5xp44KN2kREN/fNKpFJpduSGaOYZ5Tc0uX2Flt SU1x7AGu5O2fCwHxIojyhLDdfGKb4iF7xDnWeuRPTp2i29pdbG7ihu07EOuxOr8Vsyu31ZLq CpIitbMtnER1xzT98iIUeFx8Vum2TaK0Q3Y9+JKIVgsmKfZKZMt2KA8m5QQvEjZAyP7mkT7g LWLekgl5OSl7fnsbK/8qZ+GLYB0jxnzMqQwlcy7BuQ1KhMOX2+d+eS9yLLu81D1TKhTgvA4j qXVqozVJcMdpq6iBg9VyJwv6xOlADen1NQUh3gHLEhbdB6dj4nmIVHOIPf/Dfuln1uslzJry +jHPr3nHJrNMmDOnbXjcLpn9UJRxgk+wcpC659WC7wNOu//V07vuNDACx82KQ20w+LpCNVn0 YMeXHqCDbKDP6PKtl+I5+0vI++MZY8PuTbyN/gl6OT0jXAkglIcfbOm3ZsQaHC/BPhmLV+Zb WLqgtgaCWgKpBYxTPT2iF2eVj5ef2u+U7om5j4nEIKmEZvDRoe1jbOd2ye7B4RaaXxCClCRC njlbJ6EWvcJaCKKOMBtiD0EVb67S48gzx6irgH6y6A0ZtbTr2cTsoum39xo7cXSkwsz/Hp6F Y7Vh2qKViR/mn4Cbz4wxqF250JnnASty6991rZUHMRU5vxPQx07Pp7V1eBSGtnyXQWHcM3DA AKqS82hAD43X8gwyN8HeUpVCtyiiReF0TD8UOxdrKCCGJFhqvGU5HP2Pcsokx4utYEkhlgiG I5UMHG+w7R4/E7VDpLIlEOQk+Crc74d1WjD7jTL1nKA6WdfVgM4SqDZRTYHfEKDod3h4ULNS a60CL8nOxFN4d+LKqxNLNPz3h1dXPm2AN3FeCqqnnuoQxOBx7eCdo3vLmkUxCLcB04ViQEY/ X+cOSAvDyempCTQFm8mDkrhNmXr9+Q2s3anVgk0wgWNOlVmzKaw8wUJiOa0UPQV37lf4X5k8 G0yF1G7xNfMTd+Jpg4nfb8GJ8I04FBAk2nesmSRJ7SGKKZvzh4begVz5Qb10glvT59Hmo4sp W8rywx7LeSZ1klAfnWWx8K4PLqfMWT08B21DsyekljDzNab/LsO4/Ukuh3iug+uDE8r73Rg1 ZFczXKd4pzACAdaX4j2Vw478B1zpreSZSdYhcuc2XR0Nqi7tC7Y2tkpDfEp4gepf9BYdq2eV UfzH8AcG8myObkygVH6C3BMdOtW9aMyI4anb67Zh+jxZ7YmxW34yz0ZutMYsArE7Sd3R+/W0 oxQxviZ2lHCTDLglBK7tcuxn4lYZDYUF275yC7+BYcXaLchGORDQWqoPcCzwc1zwpD3XHsNv lKqH1QH18m4YxuZb1Xn0SVB3EQQpjqpg2Hrql482yFstaeZ0CHUlq7ufQIAO2FNVXNjhlflO 4ScntkaW0/uYRJjx37HrQ7qgqNcoqp4NWzaR0xFKjP3I29VWay1rrOeYsRL5fvEqA1vWf+nK RCfQ7/5+V4B1j/7WnFZz3Y9fi2rvZPwm1p7jnicJTB9tiiRdcZ1zBbZrNvSIJwZljYPXC55h j/GHFm3P9Cz8f2FnpfEtaawTSqtW4ZSfi/i0Y6b/HTkozcxUVvmwK71w4O9WQEhtE2zn8FnT yDJsArxbsHw2qK2PPgmNkhkCVng6tZrT4R3k48+npYVih14zt2e+XsKl3u2MM0Ohv24NiFdA 2dUnZiMvlK2vS8rZmiEzI/4SHiHl85oZt3gJ3gTxjp49cdBTqGd8L1DmyJx5Fu+twPYJ/Znz VJ/gbMj7mAXh+YRtU8j1CKYV/oeFFFfPCPqhg6J5NC3tql/dW+vdr/22lA0zrXDRPmS5xpRX nr0YMJoESZo6cRwNkPW0Xbz45voUMjZbdUU8BOO2USl7aAdONc6kfwEgjBiMGT2sCg+yuI1u hdp2ImzoImNL2g+tLL8GBNTMSf5It8C4jy4x7gLhd6Yhsr8e/cpUiVORpbjSuikVS4fpeiyf RjbCyUy8z+DBaCNDAaf70AgpHXKW4i3LSOGLXkeypNkSQXVc0VbhEp8sCwSuJk/G0jqwcXgd B08/TUN/hvirRAKzOt0Nh75W2OZpQGyaz5yRoLNZBxRphpP4UvYK6n8pqp6Aj1Y85u9rQeMN n3TZgJGCnsMU1CFAFarN6en5N3J+eyVTuSkKP6GbbKLoO1YH/CGoPDnmpNh5CqJP96TM2NKF Po920EYBCk8QJyfkDIJUCkN0SfEbsrdpQ3mvDx+rse4tv/sXUOKh8PHCrdfN8lu5wHjgaqHM L3YjyJ4JDBEk5IUkCCXjuJEjBhL1H8oLmf3QtFi/WbXQandm7FaFUseYiJ3bo5T6r4kmxNKM ojdg8/00bhxirg0DU1EXBrvgJLMB4RCLmejOVfAHEvOOq6BIGiBz8jvZqKzT6xKje5Uvge8k SeSE0jkeDqZ3WqMNVjnIaRXgSeXMQYL8pm6aQpoAHP/QcjOcRq9MdQs1GRzmuVyjXTMLmsGd z11ckcLr6fKqzJRgvJ4XWdG6zA2SIvM0zbc5O7eJJEMtPJtCSkhjONW7kMxzL5N5T1FTvh48 MM3hs9no1ah1OeVmGIPuPtmsTFNhYnQ5BwnYv2f/Z5GQnPeuhcE7GHWCg5Q4cpsCtro/atXz 4qX/EocACZL89XTu8UGVZG8FQ==
- Ironport-sdr: HA0YtZA5DyqY2kX4ax81k7WM3A1Qhp2BiEJnYff5jyE9EUgnEk/usJOrwqh7bqcnYi2VkVFQlj HpgEqjXQlqDV+99KldI64RUuB1gv1fRxFOL7h0DZ6lccY+RLKUBcc40ObH96Q5eAQ0xgDgGyZX Z8JIPfB4JxBEzJTwkGMuNYcc2xE+5LQKUNiUkr2jya0yZyk23y/zMncptWO5qie+Avp6ZfUHCP 5bkWGiHTm3jMElfTLrvsNz9Xf2Rd91AU3JN+0Z61FlHG6SKgxV/aTNlY9Vi+ZXro3pXf8qJ0vw dz2wPgsUbxHtcYQX1DVF1DWd
Thanks Theo for the answer. I have checked multiple lemmas and effectively the problem occurs only with "srun eauto use".
However, if in all lemmas i substitute "srun eauto use" with "sauto use", then it works perfectly.
Le mercredi 7 septembre 2022 à 13:27:32 UTC+2, Théo Zimmermann <theo AT irif.fr> a écrit :
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
>
>
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+.