Skip to Content.
Sympa Menu

coq-club - [Coq-Club]Forward-reasoning analogue of 'auto'?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Forward-reasoning analogue of 'auto'?


chronological Thread 
  • From: Adam Chlipala <adamc AT cs.berkeley.edu>
  • To: coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club]Forward-reasoning analogue of 'auto'?
  • Date: Mon, 09 Oct 2006 15:21:57 -0700
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

People comparing Coq to Isabelle seem most frequently to say that Isabelle has much better automation. It seems to me that what is missing to make Coq as easy to use "out of the box" is a forward-chaining version of the 'auto' family of tactics. That is, there ought to be a way to register lemmas that are applied based on pattern matching in hypotheses rather than goals.

I think this "forward auto" could work fine without any backtracking. I'm envisioning adding tactics like 'inversion', 'injection', and 'discriminate' as "forward auto" hints. In other words, these are "simplifications" with no chance to "head down the wrong path."

It would also be appropriate to have analogues of 'Hint Constructors' that stock inversion, injection, and discrimination hints for particular inductive types. The inversion Hint command would probably need to be the most complicated, since applying 'inversion' doesn't always lead to "making progress," but I'm sure some heuristic for "useful inversions" could handle the majority of cases.

So am I missing some canonical way of doing this kind of thing in Coq today?





Archive powered by MhonArc 2.6.16.

Top of Page