coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with automation with sets

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problem with automation with sets
Date: Wed, 1 Aug 2018 18:15:26 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:cN0o0hGw+2CSxUrPJlpmf51GYnF86YWxBRYc798ds5kLTJ78pcWwAkXT6L1XgUPTWs2DsrQY07SQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDuwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOtEsobyvV4OpgagCAmsAOPvyydIiWXy3aIgzu8sFhvJ0xE6ENILrHvZt8n6NLwIXuC0yKnE1zDDb/JK2Tvn9ofHbw0hrOiKULltcsTR0VEiGx7bgliTs4DoMS+Z2v4Tv2SB8eZsSP6jh3Y6pwxwoDWj3NkghpfVio4Py13I6z91zYkpKdC+VUV1e8SrEIFKuCGfL4Z2Qt0tQ2VvuCsizb0GpIK7fCcNyJQmwR7fZOWLc5OU4h35SOaeOy10i25+eL2lhhay9VKsyuj9VsmoylpFsDdKksTUunAM0Rzc9NSHR+Ng8ku/2juDzQ7e5v1eLUwqj6bXNYMtzqIompoWq0vDHyv2mEvsjK+Rc0Up4vKn5Pn9bbXjupCRLJN7ihrkPaQvnsyzG+E4MgkSX2SB5+uzyaDj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa7bmG9DGKmXJuLbnZ7d0rUBGmyQpytUKzp5dD/kqIPbyQkb1vZSMBxMwNgecyP3uCdE704ICH2+DH/nKY+vprVaU67d3cKG3b4gPtWOlcql317vVlXY83GQlU+ys1JoTZmq/G607cU6CaHvoxNIADSEHshdsFbW22m3HaiZaYjOJZ4x5/isyUd/0BpzKR4Trhb2dmiq3A88OPz0UOhW3CX7tMr68dbIMZSaVeZczlSEYWr+gTYBkzg2nqAa8wKFuL+6S/ywE85/vyYot6g==

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.

[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