coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] automating forward chaining

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] automating forward chaining
Date: Thu, 5 Nov 2015 08:10:15 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga03.intel.com
Ironport-phdr: 9a23:sf1mbxcle7XD/L1AyxnzpJLVlGMj4u6mDksu8pMizoh2WeGdxc69ZR7h7PlgxGXEQZ/co6odzbGG7ua7AydYsN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcaJKF0ZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePFyRrtBST8iLmod5cvxtBCFQxHFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63XzQBsr7QqwuXizmp4JqQx/hhSNNf2o88WrXg8F0yrlcrR29vRtn64/SfIyRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5XAg==

Dear Jonathan,

the trigger mechanism you propose would indeed be very useful. I make
extensive use of various variants (e.g. different simplification) of this
tactic:

(* Assert a lemma with the given arguments if the conclusion isn't yet
available as hypothesis *)

Ltac AutoAssert term :=
let HA := eval hnf in (TypeOf term) in
lazymatch goal with
| H : HA |- _ => fail
| |- _ => let H := fresh "AC_AutoAssert" in assert (H := term); hnf in
(type of H)
end.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] automating forward chaining, Jonathan Leivent, 11/05/2015
- Re: [Coq-Club] automating forward chaining, Clément Pit--Claudel, 11/05/2015
  - Re: [Coq-Club] automating forward chaining, Jonathan Leivent, 11/05/2015
- RE: [Coq-Club] automating forward chaining, Soegtrop, Michael, 11/05/2015