coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with automation with sets

From: "Ramsdell, John D." <ramsdell AT mitre.org>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Problem with automation with sets
Date: Wed, 1 Aug 2018 20:47:02 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ramsdell AT mitre.org; spf=Pass smtp.mailfrom=ramsdell AT mitre.org; spf=Pass smtp.helo=postmaster AT smtpvmsrv1.mitre.org
Ironport-phdr: 9a23:y2TygxesT5U3ZDRiKOqtW0OIlGMj4u6mDksu8pMizoh2WeGdxcS6bB7h7PlgxGXEQZ/co6odzbaO7ea4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYL5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyuqR1/zJLbbo6aL/d+YrjSfdYGSWZdRMtcVSpMCZ68YYsVCOoBOP5Vo4fhqVQUqBu+HhSjC/3ryj9MnnP9wKk00+MhEQHAwQcuEcgCvHrJp9jyLqcdS+W1zLLVwjrda/NW3Szw6I3JchA9u/GDQ6h8cc3LyUkgDg7IiEibp4/9Pz6Ny+gAt3aX4/BgWO6xkWIrtgV8rze1yssxhITEh5oZxk3A+Cln2oo5ONy1RFJhbdOkDZdcrSKXOoluTsMsXW5luzo2x7gDtJGhYSQF0pYqyhvCZ/GIc4WH+RfuWPuMLjhkhH9ofaywihmx/EWvzOD3S9O630xQriVfl9nBrnAN2ALX6siAUvZ95UKh2SqX1wDN7+FEOlo0lbTGJ5I7x74wl4YTsV7dESPsn0X2lqCWel0l+uiu9evnfq3rqoKYOoNqkA3zMroiltaiDek8PQUCRXWX9Oq92bH7+E32WrRKjvk4kqnDt5DaINwWprSjDA9QyYYs9giwDzOi0NkDmHkHLU5FeAiZgITzPFHOOv/4Ae+lg1uwiDdr2+zGPrr5D5rRKXjDia7tcqp5605B0wU+1stf5pJRCrEZOv3/QE7xtNrCDh84KQO42ejnCM8unr8ZDCiEBbbcO6fPu3eJ4PguKq+CfsVd7D36Mr0u4+PkpX4/g14UO6ezi8g5cne9S75cKkCCbXfohpNJM2AKuEISCqai3EeLVCVfanK2d6c9+is2ToW8AtGQFciWnLWd0XLjTdVtbWdcBwXUSCa6R8C/Q/4JLRmqDIpkmz0AW6KmTtZ4hxSvqBX3jb19IbiNo3FKhdfYzNFwotbru1Qq7zUtVpaY0n2XQidzhGxaH2ZrjpA6mlR0zxK46YY9g/FcEoYJtehMTh8kMIXG0bU8DtHuQA+Hec2GGg+r
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

I am having an odd problem using automation with Ensembles. For some reason,
I am unable to make use of its hints. I am sure the problem's resolution
will be easy found by one of you experts. Here is a simple example of the
problem.

-----
Require Export Ensembles.

Lemma disjoint:
forall U A B, Disjoint U A B.
Proof.
intros.
auto with sets.

At this point, I would expect Coq to automatically apply Disjoint_intro, the
name of the constructor used to define Disjoint in Ensembles, but alas, no
such luck. Auto with sets does nothing.

If one types "Print Hint *", one sees there is something in the sets
database. The relevant line reads:

For Disjoint -> simple apply Disjoint_intro(level 1, pattern Disjoint
?META196 ?META197 ?META198, id 0)

Any ideas as to why nothing is happening? The same problem exists for
identifiers that have an unfold hint.

I am using Coq 8.8.1.

John

[Coq-Club] Problem with automation with sets, Ramsdell, John D., 08/01/2018
- Re: [Coq-Club] Problem with automation with sets, Adam Chlipala, 08/02/2018
  - Re: [Coq-Club] Problem with automation with sets, Ramsdell, John D., 08/02/2018