coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Core hint database question

From: Anton Trunov <anton.a.trunov AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Core hint database question
Date: Thu, 28 Dec 2017 12:28:41 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f175.google.com
Ironport-phdr: 9a23:GJqnRBW87Ad5Y8N73Jl8WmgGKYLV8LGtZVwlr6E/grcLSJyIuqrYYxCAt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlsN+g61Urg+iqRJx3YDaZ5qYNOZnfqPYYd8aRXZNU8RXWidcAo28dYwPD+8ZMOtEqYn9u1wOrR2jDgeyHuPv1zlIhnjo3aYn1OkuCwfG3BAnH9IIqnjbts/5NLsIUeCoyqnIyivDYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7GgFWIsYHpIS+Z2+AXv2WY7+dsT/+jh3Akpg1rvzSixMchhpHUio8RxF3I7zh1zYk3KNGiVUJ3fdypHIFNuyycKoB4WNktQ3tytyY/0rAGuYC0fCwNyJk/wh7Qcf2Hc4yR7hPtTuadPS50hHx4dL+9hxu+60egyur7Vsm71FZFsDBJncXLtnAIzxDT686HReVh/kq5xzqDywTe5vtHLE00j6bXNoAtz70qmpYOs0nOHjf6mEDsg6+XckUk9PKo6+PiYrj+vJCcMZN0igb4Mqg0gMOzG/g4MhITX2id/uS8yqbu/UL8QLpQj/02lrPVv4zdJcQevqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnQE01JVU449eIrAHOvP6HEHr5/LCCRpsGgqoxOCvNM9g0IQAETaGBLOeNuXb90OS++QoPcGDYYYUvHD2LP1ztK2mtmMwhVJIJfrh5pAQcn3tRvk=

Dear list,

The following simplified piece of code illustrates an issue we are having in
our project:

Goal forall (m : nat), exists n, m = n /\ m = n.
intros m; eexists; split.
- trivial.
- (* The goal at this point is m = m + 0, but I’d expect it to be m = m *)
Abort.

I believe that this happens because the core hint database has these two
hints in this order:
…
In the database core:
…
simple apply plus_n_O(level 0, pattern ?META123 = ?META123 + 0, id 0)
simple apply @eq_refl(level 0, pattern ?META22 = ?META22 :> ?META21, id 0)
…

because after the following piece of Vernacular everything works as expected:
Remove Hints plus_n_O eq_refl : core.
Hint Resolve plus_n_O eq_refl : core.

Is there any reason for the standard library to prefer plus_n_O over eq_refl
when dealing with a goal of the form [[m = ?n]]?

—
Best wishes,
Anton Trunov
IMDEA Software Institute

[Coq-Club] Core hint database question, Anton Trunov, 12/28/2017
- Re: [Coq-Club] Core hint database question, Théo Zimmermann, 12/28/2017