The Coq mailing list

["Ramsdell, John D." <ramsdell AT mitre.org>]

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

John

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

    On 08/01/2018 04:47 PM, Ramsdell, John D. wrote:
    > 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.
    
    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.