[Coq-Club] Problem with automation with sets

[Ramsdell, John D.]

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.

[Adam Chlipala]

Post by Ramsdell, John D.
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.

Maybe the problem is that you are expecting [auto] to make progress on
subgoals without solving them completely?  In fact, [auto] and [eauto]
are all-or-nothing.

It's not clear how [auto] could decide which of several rules to apply
next, if it doesn't know which of them will lead to a complete proof. 
For instance, some rules could reduce provable subgoals to contradictory
subgoals.

For this particular case, the [constructor] tactic would do what you want.

[Ramsdell, John D.]

Oh my, it's just that simple. Sorry to bother you all.

John

-----Original Message-----
From: <coq-club-***@inria.fr> on behalf of Adam Chlipala <***@csail.mit.edu>
Reply-To: "coq-***@inria.fr" <coq-***@inria.fr>
Date: Wednesday, August 1, 2018 at 6:16 PM
To: "coq-***@inria.fr" <coq-***@inria.fr>
Subject: Re: [Coq-Club] Problem with automation with sets

Post by Ramsdell, John D.
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.

Maybe the problem is that you are expecting [auto] to make progress on
subgoals without solving them completely? In fact, [auto] and [eauto]
are all-or-nothing.

It's not clear how [auto] could decide which of several rules to apply
next, if it doesn't know which of them will lead to a complete proof.
For instance, some rules could reduce provable subgoals to contradictory
subgoals.

For this particular case, the [constructor] tactic would do what you w