coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Tactic for Automatic Forward Reasoning
- Date: Wed, 17 Apr 2019 02:04:31 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=s8mawutt AT stud.uni-saarland.de; spf=None smtp.mailfrom=s8mawutt AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
- Autocrypt: addr=s8mawutt AT stud.uni-saarland.de; prefer-encrypt=mutual; keydata= mQINBFWVkZsBEADmp2Mq5XZcOg38F91SMR5uF8cqC7LaODrnF+xh3TNKgbK301sPwcSKA4gr +TKV73e4VQoWihiWaYfPJYHsudXrp644dqYvWuxNWlkh4S2HIOmcopuTEd063TL5hRvhkg0V ZOMq000ucKo0yBsUux7+TdZdDAX3WP1whF7jY8OTe5xnEO3yv4xydAZhbT/gMO/IW6BVE2xO eElXEwC8Tnssar8cM0wZcnxgKXq4dhjDO6sSkeaf81a6FPlpy+VuCIHFYoFIAquX6T6V+Zbi UXJyDSUSUVVmechLA8vXmiRgOTyVMdTejXQb5niLGjb/Upvy9uSlO7eR0aSkCs3vqeXIppmS PDTKVwPso/PmJHEJnZLrbXKqqh589pbDAdYfJvP3Sg0fncL5bzxV0gdSqWH0t0e7c9AMiHs5 5bxEHBXuVtNs1srF52gT0KlE84R2UOmZ9Kst7P3XgJtIGzuS5uSHqFmtknh9tj+/G/Kg3qDz njxM6xTGExNPHQuskwbvYDqA6/5Hslqis6D6EpMPGhRuUhPuE5Eb+PsxpV26UccZt51FqIIc Mwv+3AUPbF7v7s7rAE1BkbmClUGuYUGfqfndGT4V6fLpQH5F9kRdxmIm9FcMURUDvX4CBKZz gmwIZ4jgZ2jZ1VTy+MWIXRpgJIt5aim4liycyDoPk+fyYfdmQwARAQABtDFNYXhpbWlsaWFu IFd1dHRrZSA8czhtYXd1dHRAc3R1ZC51bmktc2FhcmxhbmQuZGU+iQIwBBMBCgAaBAsJCAcC FQoCFgECGQAFglcSYFwCngECmwEACgkQ7Ve7Ztu9/N6Nng/9Efrx3z5menrcwHILe2WX/i2i 8zFu8a3dqFZj0kgj8AumdUwbvOYv0mMBEG7c+6YNsQEw21mjKQGEw7GSOlN++K0xiZnlzULc DZlVxrH0Eg7fr/NNpQiJeCxFzxjMqMtitIbUh9BIFEnVOLsySLUoMRB77+/g8Lf0fJ5bTxfw 8xXg7has6p/J8Zc3Y19128o3BrBhDVYbYub+NeqwmHUdIbiPn+QsuhDpmvYniw5gsFm+KP7t YRpExeVT7ZuHFPiCQfHVbj0s4TzXMRFBrruOefreC2kg6e1YNpPRQolUYkc8kwIdPYF5oBC3 oRlgRiYMs+nGOyQcrPWz78PyycsuCrvOg0oDja41aNtL3PiZtqZf0Ih0GSNP6X0++I+ZIyR8 TZQyguRWb0z0anq1LhH/vRnXefH4zListwKwJViQsKPGXANu6qZpvwn65iH98+dT5uwKhHhl h3qTNx43WGOo57ETrsF8vpl++IotCFqihwUK6yV30xxZaOTa+p00QYzE34ZoRRgKdtclD0b1 aQciJ/k+BYjxy/vl8ZgiSpOLlI1jSncX6AKeq4KpmvbV96QdVrErlUsQULPRHiePi3hot9yS BRg7J5Z3mzLMt/rdfJIb8/bkxZGbqXl6LoxAvE1Io+fvFMOTSer47Los3MJO+smC/SstQczS BKOT0Cf+Ase5Ag0EVZWRmwEQALwwnvtVw/zFec+MNKgBwKt1MIG6EMBKc+OTIYM2tN4jcWla AbEcIZGkBSeoPJeTi4m3GQXhifGZK29VoDIUQjYYDWNtp6U8y0hLRnqSVY/YvcTDnK929n5r qMqO0wYf1fzhmPshIyD1jj96tqu0ppX7zE++VQ/VJgVIA8IGcNXUN21A/+rJKCJFAvBp+6u2 gNaUDfnqvPfTGtkq7A/D40Lo6y0KVu20R3W76iFWl6FEQzOe28VBnOjU/NbyzAzVUSgYCSfk YxhDiKfJRJvQd+VKUCAa+BSNoEPvDMKakvhApWUOncnNUbfXiH04fYSViu2NH2Ls3HLm+6xa Aaf9eUIU75A02xXUa6m+AccJQzCEJySeYJFVhJLSgZEbGwDZVdrRALolgYiIrwOHTitC2PLR ej8HeywQrn3PUGBwiYdOa19KTHZykbO0s0SHb6bvm3vgpAPPdZp+QWPOXx3aZz6dw4D867li sGVKMcKBcX9QCekVL7CW6lvvevUP5tBBYCshMvSTaN0BymBBwYrz8UB4RYJ4cUs5apd1mMfD 5Vm8EZf1DT15Q+K9+HsRQr3y/+AtHm0gd0DpXGfBH4H+54vyB9Aj3DVbyPMeFYv9UhyKALEo mprFM0tr0+SPh275xXlIxUvoC+3PlFM0swoLSmi2Tu9edjU6GuyL91w/9WTjABEBAAGJBD4E GAEIAAkFglWVkZsCmwICKQkQ7Ve7Ztu9/N7BXaAEGQEIAAYFAlWVkZsACgkQIA5mg0qOKkAo DhAAnms7o654V2uZWBsiiR2oEykGs/sIzxYcKrOi2RnkL6RAwhJgBr+WVpjQ2IS9IQ5Bxy8G OWhzyit2XvFYTWxGamrmyXol7IynGcl2U3WpmSQEPJx/QeyQ5lWLYzjn5bbdzNdY0mhUnRZ+ ke2tcttmvLsUKn2J/8lSyqBF4i4Yaj4p4LQ8n/K/eW9lIY+J/gVGDcrlZqOozXV9aClYDtgx L/c6/TPuDi0vgkhIaojwsSu38YmhmbYP03ntiLTrLbjnJXr0pYIlMRqUmNvPsphOR8cVGFnZ 50dVoWHSSJhoIESpu8Qz1qwvA9uNTDhe/nnr092diP78FWo4SENiKjrXA2fOjk0YoZA1uSL0 RbcRKAttPC88iBWUyBwYrhMBFKzJeDG+lvBID8gED205Jy7Mk8v7R9NqHpjJXST1avVMF7TX CH8OK7rgI9ATGLqJ31WoYZkCSFkYKYRbyarZnVKxMsQ1zhpjoEfuQlWaq2NgwS2cijWmKAmF V4Qv3FA5zAoEdzB9HCbT2DafITEUqjf111+WjNcfJvtfQcO7hghhMwFtW9Or9KqVKpEDraku uHUr6nVnBNYCliY80m/X5DXOZsKzehxfHht4t+CydGE2xRzIwzpos2ZebhkjWmghGS7G1JHA DgEk7zBKyVxJm/nwwNGk5MdY9sckx8XMiaA5lV2oDw/+K7mXo2qbEPnghGjN2bAqYbZd/Wdh 5SUwa5YvnfqWcSY7G8OA5pexnIV/5RRIdcc+RtrxADmfTYGVIvSfAS4uwALIgEd5LYdYBIaj xWLCyNghoQowLqZbIQQ4eOWd2xCF6srcTsIou2kJ97iiFtXgX3PthKn+fhdFYWktEDabDhgY SdqJVvs+Sk3lO41aJu5MSIsqWq+G0ZGumTtO/yR9x5RzA/qKn56S6Da8WjRF6iq/oyemifyC 74HXmmi6gd8HCWD+eEXNWVAVL/FlfYhL420olMcBgP+cMGJTpmWK5jCyaxHH4RFYg8AAdzn0 /Lc/Xr47IZBntCaLy3V1LSKvDSZackKOreBmxQrd2Qn5/seLYFWWl/rPvqib6hmoE17SjBI2 szi/t37JGXTl0ZkhSUp6FSC4YmoFrKJgxuX0q7CONZzdZ9G7mNOkUdg3QAaN6/EZQceGC/Dv i28jB57Y50OoOAcyJnSkS95lPobHcGbBDDIQVvcEBwhSir/coGXHk8tqMXCdhxDo9Tq1cSvA NeRYuJdrTdJM2FMll7QEtBcto0DNCNEecvZ+D/uqOU+InyJHpD4qDpQR8bqNJ3Fmehd54LYi ZK2G5/gRwF+8vnaeoy9fSs/CAw3icKPTcSSmy9bOk3I0fgAyb63xLF/sGHAOq5gkPg+9o79d HcbtD425Ag0EVZWRmwEQAKYFa3Y6d5D34YkaNBYvjU3mUlaS2uq7khoVxhnPiad496PzpxpF 76rwpAbh7+V+aqxFDldmydjV3REPgJKk5hnhJ2ndltaoy0CtzFOjUV2KkzzvG2YXADSKCqvL rtVx3wfAxOVxjPOlFzG57mvZd3MUlxOGJPvNbFJJY98OzjQGeCukITMO4mivublSlJy8hNkw bMgkAfBkuITNXllrLfTxch6wikunYlDrtI2X1/h6ygXn/m8dYWzDGv80PyzVHWNMz7JS5UuD 7PkkazkqLzH9HQ+xj2x7KOWIHs9BQp99OrZfUMcD54EfoM0JUG5kq0Xs099Z4UEFA2Pl+8mn n7z7NNZ1JSN0xjUuxhMu5deIkKEj8XGwB+6OXYEhF3mdh5T29C4LHDpp3fpa9LU+8Dlpq0HJ lwBx5ngXOfAmZrKAJhiy8kT3AfNskiVWxgYga2Kk2ku8vV4DkMai7kzK45t0/cDwdgugeck8 3x/7yR9XIrBwlt8N4bdJ3URbOtnuGuYjM5RTtqpadjVLLr+ZdhKPdM7qtPfnHotjRq+ban1T dA/zlCOW+s4g955kvafY29qnhx54y+DQJUwELAZCTA0fT/eHs0n6M/gILepMleBR7STA+Xqn I5aWlWn3Pp6nI8t3bz0T6sFEocD++YJNEr/J7yduvcNaI84j03iRMfPjABEBAAGJAh8EGAEI AAkFglWVkZsCmwwACgkQ7Ve7Ztu9/N4GJA//f21oF6/XClyTnbsNSBKLvbtb9CjKx+9c6B6k 1qHePSylFf+BsrKFMEdtyn40bfVnQqQ1GzNFFbzGiFkUlwM1BZMR0ogl6ahtJL3M4Tf7RkV6 FUhkov5HwYIXDjx9WdboLPPz4NQkomgcWyc0vAndtL1vYFizVLkxIdWonnv11M4MoQybCjv9 lm+UwmoqLkSvrWn3F6RMPwsc4HWDRHiBYNkCxYGlfVfQax1u3ENH7KfEnZAEEoxSBkaha1Tv /06wHjQ9w+7ZwueiB48MCQleDM4xP+Geom/VIhExdySrAtGZEP7DjCpcXTYL6491G1gDdStp zSU0odKKxp3xUgB7gFuegBsM4dXm02Q6tzr+oVLkCeTGWld3/DfyIVVi3f2w+g+JEE8W71Gx uIw4IwuxXr0sGo1gHnH8CD5ky0/dGYfW644oZ6DQRzDqp+7sJNGoSOmEbJ5k7IgkPlwb41jN Ez1miq/AIleDjVgM6ZP1g4eVAWgjATFqfv9y/WR1t1BvrcogGKdVLfRr6kDYwP2GzzCGz2Ki VtlPaPv52UYPa9zX6IT5hEOq4GSAVo2IHwtukyG10l7sanq7J6s5CumNukDzuJxJ+EgNYIxa EtdujUPJxlRQcFwqjbLEt2LQBJivwzRhRmQfQz5tt3c797Tsto875TRgvFHu+ezStimb9ew=
- Ironport-phdr: 9a23:aDZ5UBZmTxXswb2dKmtNiCn/LSx+4OfEezUN459isYplN5qZr8q8bnLW6fgltlLVR4KTs6sC17OP9fu6EjZdqdbZ6TZeKcQKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZ/JqorxBbFvHREd/pWyGh1IV6fgwvw6t2/8ZJ+7yhcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd5YBAfQPPehYrIfzqVUBohS8CgawH+7vxSNEi2Xx06Em3eksEwfL1xEgEdIUt3TUqc34OqAIXuG6zanIyDTDb/dX2Tjn7ojDbxAuoeyQXbJscsre11QkGgTejliTrIzqJT2U1vkRs2iH9OdgTv6vi3M6pA1rvzivwMYshpDSho0P0F/E7yF5z5wzJdKlUkJ0fMCrHYJWuiqHOYV2RcYiTHtpuCY80rAJpZ67fCwLyJQ/3RHfb+aIf5KO4h39SOacJypzinF9eL+nmhq//0etxvf4W8S1ylpHrDBJnsfMu3wVyhDe5MeKRuF580qgwzqC1g7e5vtaLUwol6fWLYMqzKQqmZoJq0vDGzf7mEXog6+ScUUp4vSo6/7mYrX6oZ+cMZV4ihv/M6g0h8y/B+U4PhEVX2eB4+u8zrnj8lf/QLpXlPE5j7fWvIjbJcQduKG5HxdY3pst5huwFTur1NUVkWMFIV5fZh6Kj5DlO1TUL/D5Cfe/jU6skDBux/3eJb3sAZDNIWLNkbf8YbZ991VRyBEvzdBC+p1YEKwBIPTyWkPor9zXFAU2Mxaww+n9DtVyy5kSVn+RDaOBKqPdrUeI5v4zI+mLfIIapDH9K+E86/HyiX85hEQScLKy3ZoXbXC4Bu5pL1+YYXrqmNcBEH0FshAwTOzw2xW+VmtYYG/3VKYh7Bk6DpinBMHNXNODmruEiQKyDpxTZ2RHA1bELmr0a4aJE6MXOCebPdJ9jhQfSaWtDZIn1FS1vQbgz7NhIqzY93tL5trYyNFp6riLxlkJ/jtuApHFijDffyRPhmoNAgQO8uV6qE15xE2E1PIi0edECNAV+vVIFxwzPITYxup2Tdz/CFqYI4W5DW2+S9DjOgkfC9I8x9hUPBRhAdS+iRaFxTjsHrkU0qeCDYYw+6TQmXT8dZ4klyT2kZI5hlxjefNhcHW8j/QlpRPPGoKPjkOY0r2jfL4Y1SjBsmuOnzKD
- Openpgp: preference=signencrypt
Hi,
I use a technique using `evar` and unification which is described in
Chapter 14.5 of CPDT [1].
Sincerely
Maximilian
[1] http://adam.chlipala.net/cpdt/cpdt.pdf#page=292&zoom=auto,-398,796
On 17/04/2019 00:04, Kaiyu Yang wrote:
> Hi folks,
>
> Is there a tactic in Coq for automatic forward reasoning? Suppose you
> have a lemma *forall (t1 : T1) (t2 : T2) ... (tn : Tn), C. *
> And you have T1, T2, Tk in your local context (k <= n). Is it possible
> to apply some tactic which automatically finds relevant hypotheses in
> the local context and gives you the result of forward
> reasoning: *forall (t_{k+1} : T_{k+1}), ... (tn : Tn), **C* ? Thanks!
>
> Best,
>
> --
> Kaiyu Yang
> Ph.D. student in computer science at Princeton University
> 35 Olden Street, Room 431
> Princeton, NJ 08540
> +1 (734)389-9696
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Tactic for Automatic Forward Reasoning, Kaiyu Yang, 04/17/2019
- Re: [Coq-Club] Tactic for Automatic Forward Reasoning, Maximilian Wuttke, 04/17/2019
- Re: [Coq-Club] Tactic for Automatic Forward Reasoning, Jason Gross, 04/17/2019
- Message not available
- Re: [Coq-Club] Tactic for Automatic Forward Reasoning, Kaiyu Yang, 04/17/2019
- Re: [Coq-Club] Tactic for Automatic Forward Reasoning, Maximilian Wuttke, 04/17/2019
Archive powered by MHonArc 2.6.18.