coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Questions about info_eauto and info_auto

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Questions about info_eauto and info_auto
Date: Wed, 23 Mar 2016 23:41:22 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:KUzqGx2/eN8LlGtzsmDT+DRfVm0co7zxezQtwd8ZsegVL/ad9pjvdHbS+e9qxAeQG96Lu7Qd1KGL4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6CyZ3onL3js7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGBCE4WcAGm4RlAFUCgLB4VmuRZv6tS3hquNVwziAe8D6UOZnCnyZ8653RUqw2288PDkj/TSPhw==

Hi All,

I recently stumbled upon the info_eauto tactic on a forum, and have found it very useful. For instance, running

Hint Constructors or.

Example easyy : forall p q, p /\ q -> q /\ p.

Proof. intros. destruct H. info_eauto.

prints this very helpful output:

Debug: (* info eauto : *)

Debug: apply conj.

Debug: exact H0.

Debug: exact H.

My first question is, why isn't this tactic in the 8.5 manual?

Second, one would expect that if there is an info_eauto, then there should also be an info_auto, but when I try to invoke info_auto, coq reports:

Warning: The "info_auto" tactic does not print traces anymore. Use "Info 1

auto", instead.

But the output from "Info 1 auto" tends to be incredibly unhelpful. Using "Info 1 auto" in place of "info_eauto" in the same example from above yields:

<unknown>;[> refine H0 | refine H ]

which is certainly not very enlightening. So why is there no info_auto?

~Scott Constable

[Coq-Club] Questions about info_eauto and info_auto, scott constable, 03/24/2016