coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic for Automatic Forward Reasoning

From: Kaiyu Yang <kaiyuy AT princeton.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Tactic for Automatic Forward Reasoning
Date: Tue, 16 Apr 2019 18:04:46 -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:MJEx6hPNs87sqGHZ4mkl6mtUPXoX/o7sNwtQ0KIMzox0Lfj/rarrMEGX3/hxlliBBdydt6sdzbGM+Pi5ESxYuNDd6ShEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQLjYd4JKs91BTFrmdVd+9LwW9kOU+fkwzz68ut4JJv6Thct+4k+8VdTaj0YqM0QKBCAj87KW41/srrtRfCTQuL+HQRV3gdnwRLDQbY8hz0R4/9vSTmuOVz3imaJtD2QqsvWTu+9adrSQTnhzkBOjUk7WzYkM1wjKZcoBK8uxxyxpPfbY+JOPZieK7WYNUXTndDUMlMTSxMGoyzYYsBAeQCIOhWsZXyqkAUoheiHwShHv/jxiNKi3LwwKY00/4hEQbD3AE4GtwBqnXUrdXoNKwPU++61q/IzTreZP5R2jfy8onIcxA8ofCMRr9wadDRyUgpFwzZkFqQtYvlPzWP2usTrmeb8vNtWOSygGAkswF8uiWjytkvh4XTm44Z107I+T9kzIorJtC0UlB3bcOqHZdIqS2WK497TtkhTmxooio21KAKtJyhcCUFzJkqwQPUZeadfIiS+B3jUf6cITdmi3Jhf7Kynwy88VKhyu36Ssa7zkpKri1DktXWuX4D2RLc5tCGSvt74EihxS6C2x3N5uxHO0w4iLfXJ4A7zrItiJYesl7PEjHrlEj4lKOWc18r+ums6+TpeLXmoZqcOpd3ig7kM6QvmtG/AOQjPwgWRWib+OK826H98k3lR7VKiOc6nbfEv5DHPcgbvLK2AxdJ0oY/7BayFyup0NMBnXUeMF1FfA+HgJPyNlHVIPH4CO+/jE62nDdqwfDGJLzhDY/XInjNireyNYp6vkVb0U84yc1Vz5NSELAIZvzpCWHrs9mNLRY4IhH88u/hB50p1YofSH+eKreDMaXZvEOP4KQiL/TaN9xdgyr0N/Vwv62mtnQ+g1JIJfD0j6tSU2ixG7FdG2vcYXfohY5cQ18Qvww1QfDtjhuvfQMBPi/uDZJ53SkyDcedNamGXpqk2eHTxD26GJZbemdATF2ADCWwLtTWa7I3cCuXZ/RZvHkBXLmlRZUm0Ejz5hfgyrxsI/bT/GsVuY+xjdU=

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

[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