coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Difference between eapply and eauto - does eapply silently call simpl in case unification fails while eauto does not?
Date: Fri, 20 Feb 2015 10:50:42 +0000
Accept-language: de-DE, en-US

Dear Coq users,

I have a case where

eapply A; eapply B; eapply C.

solves the goal, but

eauto using A,B,C.

does not, which is unexpected from the documentation of eauto and eapply. I also found that

eapply A; simpl; eauto using B,C.

does solve the goal. Also adding a Hint Extern which calls simpl does solve the goal.

So I wonder if eapply silently calls simpl in case it cannot unify.

Most interesting is the question if eapply does other silent simplifications eauto does not do.

Best regards,

Michael

[Coq-Club] Difference between eapply and eauto - does eapply silently call simpl in case unification fails while eauto does not?, Soegtrop, Michael, 02/20/2015