Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Problem with last version of CoqHammer

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with last version of CoqHammer


Chronological Thread 
  • From: "dapoignyrichard AT yahoo.fr" <dapoignyrichard AT yahoo.fr>
  • To: Coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Problem with last version of CoqHammer
  • Date: Tue, 6 Sep 2022 22:51:23 +0000 (UTC)
  • Authentication-results: mail3-smtp-sop.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 sonic308-18.consmr.mail.ir2.yahoo.com
  • Ironport-data: A9a23:LiEOOqvZ2qstYFVr96GRYqxJnefnVMlYMUV32f8akzHdYApBsoF/q tZmKWjTOKzeYTCnLtx3bNiy/R4Ou5LQzYBlTVNsqSk9FHgVgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+5yHZgf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnYyRFR8bb4zDoslHaUV7FGIiEaxZ4oaSdBBTseTLp6HHW2DrxfRlVxlmeNRIvO1wB3pL7 7odITEJKBGZ3aSnybK8Ta9ngcFLwMvDY9xZ4Cowi2iGXbB/Hc6rr6bivbe02B88j9hJHPnYd tAYYjpmdhjochRPPVBRBohWcOKA3CKnKG0B9A39SawfyEPryRRSwpXWDfnKPd2SG4IMhGClq TeTl4j+KkpAaIXDk2btHmiXruTIhGbwXJ8YPKap8+ZjxlyV3G0aThMMPWZXutGijUi/UIkHe wlNqmwlqq4p8VbtS9D8W1u5uiTCrxccXN0WGOo/gO2Q9kbKyxa4WnA2Hx9OUvF8jpMVQn92+ l6Wheq8UFSDr4apYX6a876Vqxa7Ni4UMXIOaEc4oe0tvIeLTGYb0UynczpzLEKmpoCuQmqvk 1hmuAB72e9O3JZjO7CTpwivvt66mnTeZi8Yjuk9dk645Ad4YuZJjKSEsQKzARpoCIuYSEKds WJspiRzxPsJC5CGz3TdBbxdWrqu4e2AKnvZiF9rWZg7rXK88n6kesZb5zQWyKZV3iQsJmCBj Kz741k5CHpv0J2CMPYfj2WZVp1C8EQYPY65Ps04l/IXCnSLSCeJ/Tt1eWmb1H33nU4nnMkXY MnFK5r8XC5AWfs8kVJaotvxN5d1l0jSIkuNFfjGI+iPiNJymVbOEuhUajNikMhls/zsTPrpH yZ3bJHWkkkFDIUSkwHG+I4UKhlCMHtzHp3stc1ce/XLJgtjGX0sB5fsLUAJJORYc1Buvr6Qp BmVAxcGoHKm3CGvAVjUNhhLNey3Nb4h9y5TFXJ3Zj6AhSNzCbtDGY9FKPPbi5F8pLI9pRO1J tFZE/i97gNnE2yapW9MNcam8uSPtn2D3GqzAsZsWxBnF7YIeuAD0oaMktLH+HZcAyypm9E5p rH8hArXTYBTFRVrDMHRLvy1lgvjsX8YkeN0fk3JPtgDJB61r9A2c3T83q0tPsUBCRTf3T/Gh QyYNhEV+LvWqIgv/diV2K2J9t/7E+Z3EkdAMXPc6LK6aXvT8ma5kd1RWeaPenbTTjqsqqmlY OxUydD6MeEGzAoR6tUkT+4zwPtntdX1prJcwgB1J1nxbgymWuF6P32L/chTrakRlLVXjg27B xCU8d5ANLTVZc7oHQJDJAchaejfh/gYliOJsqYuJ0P773QvrP/eAQNZOB+XjTYbKbJ0NMUk2 71nqccW7Av5gR0va47UgidR/mWKD3oBT6R458lGWNKx0lImmgNYfJjRKi7q+5XQOdhBN08dJ DXL1qfPgrJrwFXPLigoHn/X0OsB3pkD5EJQwFkZKwjbk9bJnKRojgZW9zU8FVwFi0wXlel0P HNuLQtwLKSKuTZy3o5SVmCrHEdKAxjAoh79zF4AlWv4SUi0VzOcdDFlZLzVpE1JoXhBejV7/ a2DzDm3XDvvevb31HRgVENgrcvlUtEspBbJn9qqHpjeEpQ3CdY/bnRCuYbVR9rb7cINaInvv u5s/e0rMf2+bH5WqKo9EIyAk7EZSRTCJXYYB+Bo/KQOW2rbfVleHNRIx1+ZIqtwyz7iqCdUy PCC4upeXhS502CAtFj3wIYSdqRskqdBCMUqI9vWyK1vj1dbhitgsJXXsCbk7IPurxOCju5lQ r7sm/m+/qB8SJead6IhbCWJB4ZgXeQ5WQ==
  • Ironport-hdrordr: A9a23:/op2/6GlLvQ2RnO+pLqEO8eALOsnbusQ8zAX/mp2TgFYddHdss yokukbvCWE8Qr5OUtQ/exoXZPqfZqyz/BICOUqXItKPzOW3VdATrsSjrcKqgeIc0LDH6xmpM BdmsNFeb/N5DZB7foSmDPIdeoI8Z281oeJr6Py7VdICTtLRYYI1W1EIzfeKEtwRAMDIbVRLv ahDp4unVedRUg=
  • Ironport-phdr: A9a23:MFN6NBE1utLnbGwvL/rxu51Gf3lGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmTDNSQsqkMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9WiDe5Zb5+I wi6oAvMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM3/mHZhNJzgqxGrx2uuxJ/zYnPbY6PKPZxZbjScMkGSWdDWMtaSixPApm7b 4sKF+cNM/tXoJPlp1sJrBu+Cg+sBeP1yj9JmnD23bc10/48Hgzd3A0vBdIOsHPTrNnvOqcSS +65x7TPwDredfxWwTD96InHchAnofCMR7NwftbRyUY1DQPKk06dqIz/MDOV0eQNtHKX7+R6V e+2jWMstg5+rCS1yMg2lonJmpwaykrC9ShhwIs7KsO1RUp/bNOmH5VcqT+XOo92TM4gXW1lp jg3x6AGt5O1YCQH1ZQqygDbZvGEc4aF5h3uWeaSLDp5mX5od7SyjAux/0i40uDxVMu53ExUo idLkdTArG0B2h7Q58SdV/dw8Uas1DCS3A7J8O5EO1o7la/DJp4h3LEwkp0TvFzYHi/xnkX2j bOZe0s49uWr8ujrf7brqoWAOI9zjAH+KaEumtalDeQ9KAcOXmyb9f691L3540H1WrVLgec2k qnet5DWP9gUpqm8AwNN04Yj7QiwDyu+3dkan3QLNkxJdRyEgoTzJl3DIvP1Ae2ij1mjkTpn3 /XGMafgApXJIHjDirDhfbNl5kFB0gUz1ddf55NbCrEHIPPzQE7xu8DYDhAjKQy73v3qCdVn2 YMeXmKPBbWVMK3IsVOQ4OIgOPGDZJUJtzblN/gl+/nugGcklVMFZ6mmwYMXaGykHvRhO0iWf X3sgs4YHWgWugo+UfflhUaZUT9TYnayR7gz6is6CIKgF4fDR5qijKaP3CehTdVqYTVtDUnJG nP1fc3QUPAVLSmWP8VJkzoeVLHnRZV3hj+0swqvgbZuNu3V9SsJr5Po1NFv68XCnBE18np6F Y7Vh22EV2Z1kWUZXT493KllrWRsw1eE1u52maoLRpRo+/pVX1JiZtbnxOtgBoWqMuqgVtKAS VL9B86jHSl0VdUphdkHf0d6HdymyBHFxSujRbEPxPSQHJJh1KXa0jDqItpljW7c3fwthkEhQ 8RJJHenja527QT7FofJlELfmbz5Pb8E0nv1/XyYhXGLoFkeVQdxVavfWnVKakLOqtX24FLYT rSuAK4rGhpIycmFbKVQOZXylVsTYvDlNZzFZn6p3We9ARHd3rSXcI/jYHkQxg3GD04FmFtLr TPfZU41ASG6pniYCTVvERTueRmq4OB+r3T9RUgxp+2TR2tm0bf9uhschPjHDugWwqpBoyA57 TN9AFe62dvSTduGvQtoOqtGM5s75x9c2GTVuhYYXNToJr1+hlMYbwV8vl//nxRxBIJalME2r XQshANsIKOc2VlFenuWx5f1crHQL2Dz+lioZcu0khnS2c6R+6gJ+e45oFXqpg2BB0Mi9HIh3 cMUm3qQ65PWDRYDBIrrWxVSlVAyrLXbby8hooLMgCIzd/Pv4nmbhIJvXbd7mXPCN59FPaiJF RH/CZgfDsmqc6kxnkSxKwkDJKZU/bI1OMWvc72H3rSqNaBuhmHD7ywP7YZj30aL7yc5RPTP2 sNPz/iA2QqIUSbmjVyhu9r7sZFNZTYVWGSlg3uBZsYZduhpcIAHBH37acG+3tJ/iJj8QX9T9 Fe5C3sX0c+uflycdRauuG8YnVRSqnuhlyyiyjVymDx8tauT0hvFxOH6fQYGMGpGLIV7pW/lO pP8z9UTXUzzKhMsiAPg/kHiga5SuKV4KWDXB0ZOZSn/aW94AOO8sb+LYsgH751N020fXO2kZ lGVTK/nohAa2jnvN3pXxDc8MT+w8pn0hB11jmuBIW078yWfI5ogg06AtJqFGaAZ1yFjJmEwk TTNA1mgI9Sltc6ZkZvOqKH2Vm6sUIFSbTi+yIqBsCWh4mg5ZH/31/u3m9DhDU07yXqkiJ8wD nWO9UmsJNC3ifffU6ovZERjCV7i5tAvH4h/ltB1n5QMwT0BgY3T+3MbkGD1ONEd2KTkbXNLS yRYprydqAXjxkBnKWqEgozjUXDIiMdof967bWUHwCM278lQBI+F5bxDmm17uBDryGCZKeg4h TobxfY0vTQWivkOuQUr3z+cCbAbB0VwLCXskBPO4cr0/8A1LC6/NLO30kR5h9WoCrqP9xpdV HjOcZAnBSZs7897PQGEwDjp54rjYtWVccMLu0jejULbl+YMYsFU9LJClW99NGn6p3Fg1+Mrk Ukkw8ShpIbeY31x5vCoCx5fMXv+YMZb4i3337dXnsGRmYaiAt02EzEPFvMEVNqOFzQf/bTiP geKS3gnr2uDXKHYBUmZ4VtnqHTGF9aqMWuWLT8X14cqQh7VP0FZjA0OOVdy1pckCgCnwtDge 0Zl93gQ4FD/sB5F1uNvMVH2TG7eoA6ibjp8RoKYKVJa6QRL5kGdNsL7jKo7ByZD4piotxCAM ESAYAJJBjpRCgndVxboOb+14MOG9uGZAqy/NaGIcLyOrusYXPCNhPfNmsNn8zuKKsSTLyxiA vk8iQJIWXF0Hdicmi1aFHNRzXmdKZfE9FHlpnMky6L3uO7mUw/u+4aVXr5bMNE0vguznb/GL OmIwiBwNTdf0JoIg37O0rkWmlAI2EQMP3GgF6oNsSnVQefegKhSWlQXYjt0NcRO/rg91QlEI 8Lzm9r10bk+gOR/WDInHRTx39qkY8AHOTT3LFTcGEOCL6iLPxXQxMf2avjkGfgJ3KNfsBurv CzdFkbiOnKCjWOvRhmvNuYKhyaedk872sn1YlNmDm7tS8jjYxuwPYpsjDE49rYzg2vDKW8WN TUUm6Zlv7SQ6iQejO8tQwSpD1J+Ku+FkH3Bv6yBetAdtv1wBz4ykutb5DI70eET/ShEQ/szk yzX/IYGS76Og+CPzT0hXgAc8152
  • Ironport-sdr: NQVzRn5vLK62KoO0AYhY5HqLPc8aT6TRV9m1N0pi76fOEf3rzTzzThuatVE/j4ae1wDpk1QX7f 6YMI8pQ4AUfWNYkXX0JcsxcplAq+Gl4suC/k8SmlVpxPhj6TDYTk9G8hsdGcCpC/rEEE2CUUhY 9uMrVvbwbFNlVjDKCxwvMUU/k3uDrIDuPJzG2fZbnBW6/N9bl68eIFS3ReyNk7x6sx8P7NImFr ag7VdKG35Fgro3ps14jnkS3JzKla0DFCm+AtfjHl+8UWzycI+WQVnO9wuZsdIe5wZMb8ZnwLay 4DF1YjGsEJUNwjAwc5LmbeQF

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





Archive powered by MHonArc 2.6.19+.

Top of Page