coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extern Hints behave differently with auto and eauto (Coq 8.5)

From: Sigurd Schneider <sigurd.schneider AT cdl.uni-saarland.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Extern Hints behave differently with auto and eauto (Coq 8.5)
Date: Tue, 8 Mar 2016 14:22:17 +0100 (CET)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sigurd.schneider AT cdl.uni-saarland.de; spf=None smtp.mailfrom=sigurd.schneider AT cdl.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-phdr: 9a23:QWL5CRFt19KdJCCqMPxVFp1GYnF86YWxBRYc798ds5kLTJ75osqwAkXT6L1XgUPTWs2DsrQf27WQ4/yrAzxIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbip9aJM01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4nU2oLiBYAOAPF6hz7Uprr+n/ht+VgwiXcJsb2S701VTm4x6xnTFn1jiZCLDcw6mXejMA2gK8N80HpnAB234OBONLdD/F5ZK6IJd4=

Dear all,

the example below shows that eauto executes an Hint Extern
after another Hint Extern has solved the goal. In contrast,
auto does not do this.

Is this the intended behavior?

The behavior of auto has the advantage that possibly
time-consuming Extern Hints with higher cost are only
executed if necessary.

Parameter T : Prop.
Parameter t : T.

Hint Extern 1 (T) => apply t.
Ltac diverge a := diverge a.
Hint Extern 2 (T) => diverge idtac.

Lemma test : T.
Proof.
auto. (* executes the first hint, succeeds, and never executes
the second hint. *)
Qed.

Lemma test2 : T.
Proof.
eauto. (* executes the first and second hint;
the latter of which results in a "stack overflow",
and eauto does not solve the goal. *)
Abort.

Best regards,
Sigurd

[Coq-Club] Extern Hints behave differently with auto and eauto (Coq 8.5), Sigurd Schneider, 03/08/2016