coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic for Automatic Forward Reasoning

From: Kaiyu Yang <kaiyuy AT princeton.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Tactic for Automatic Forward Reasoning
Date: Tue, 16 Apr 2019 21:37:00 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kaiyuy AT princeton.edu; spf=Pass smtp.mailfrom=kaiyuy AT princeton.edu; spf=Pass smtp.helo=postmaster AT Princeton.EDU
Ironport-phdr: 9a23:jGcoeBfWgR9RzPF6pg4swJ4AlGMj4u6mDksu8pMizoh2WeGdxcS+ZB7h7PlgxGXEQZ/co6odzbaP6ua7AydcvN7B6ClELMUUEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/N6o90BXErmVHd+lZxW5jOFafkwrh6suq85Nv7jhct+g9+8JcVKnxYrg1Q6FfADk6KW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8YpMAAOoPP+lWr4fzqVgToxWgGQahH/ngxiNSi3LswaE2z+YsHAfb1wIgBdIOt3HUoc3wOqgIUOC0zLTIxijBYPxM3zf955XDfxciof6WXLJxcdfRyEk0GgPdlFWQqIrlMC+L2eQRtGib6fBsWvyyhG46sgx8pCWkyMkrionMnI0Vy1bE+D1lz4Y1Id24SVZ7bsSgEJRKrS2aMZV5Qt86T250uCY6zrwGuYahcygO0psr3QTTa/qZfIiU5B/oSeWfIS9giX54Zr6yhAy+/VW9xuHiTMW4zUhGoylfntXSq3wA1wTf5tabRvZ55Eus2jaC2xrN5u1ZI004j6rWJpAnz7UtjJQcq17DETXzmEjujK+ZaEEk+u+w5ur9eLXmp5mcOJNqhQHiNaQunNazD+s2PAcAR2Sb+OK826P//UDhXblGkP47nrPEvJzHO8gXvLO1DxFW34o59RqzEjer3MwdnXYdLVJFfByHj5LuO1HLOP34Du2wg1WskTd2x/HLJaXhAo/MLnjFjLjuY6p960layAYp099Q+o9UBqkbIP3vQk/xqMDYDhghPgOoxObnEcxx2Z8aWWKSGaCUK7jSsF+N5uI3OeaAfo4VuDDnK/gk/fHil3E5mUVONZWuiNEcb2n9FfB7KW2YZ2Dti5EPCy1C6gE5VanhjECIeT9VfXe7GawmsGIVEoWjWKTKR5GwyI2I2ijzSp5fZ3FbG3iUC3bufIiYXPFKZS6PdJwy2gcYXKSsHtdynSqlsxX3nuI+f7jkvxYAvJem7+BboujalBU87ztxVpnPy3uMSWp5gmQOATI6wfIm+BEv+hK4yaF9xsdgO5lT6vdOC1poDYTdyed3F9f0HC/tQ4XQEQr0cpCdGTg0C+kJ7ZoWeU8kRoe6lBHF1Ce2BLlTmrCWVsQ5

Thanks Maximilian, I'll check it out.

On Tue, Apr 16, 2019 at 8:05 PM Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de> wrote:

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

Kaiyu Yang
Ph.D. student in computer science at Princeton University
35 Olden Street, Room 431

Princeton, NJ 08540
+1 (734)389-9696

[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