coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Folding 'not'

From: Coq Dev <coqletsgo AT yahoo.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Folding 'not'
Date: Mon, 11 Jul 2011 10:28:36 +0100 (BST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Subject:To:MIME-Version:Content-Type; b=PaKvaVA1nv2GKc9k+pBByRuVjD4NNNeCfZv3w6byhfLXjV4VmZIUnUmahcGbtmqLrD7zip5DKJXEG6ihS1tKXEJZCUNvXMBQRuq2zKDyoQajR+abvB9ff5uKOL9i/B1HNVIrUFFm7wM793VZWyKbt7jho4E6bqv/gfYaO/QzrCQ=;

Is it possible to fold a "not" after it has been unfolded? For instance:

Goal ~ (1 < 2) -> True.
unfold not. fold not.

The " -> False" remains after the "fold not" operation.

Alternatively, is there an easy way to do an Ltac or Tactic Notation to obtain this behavior, for instance "fold_not in H" to fold corresponding definitions in a hypothesis?

Actually, the main reason I'd like to do it, is because of the intuition tactic, which unfolds 'not's into implications. If there would be a way to disable this behavior, it might be equally useful (decompose [and ex], for instance, does not help splitting the goal).

[Coq-Club] Folding 'not', Coq Dev
- Re: [Coq-Club] Folding 'not', gallais @ ensl.org
- Re: [Coq-Club] Folding 'not', St�phane Lescuyer
- [Coq-Club] Re : Folding 'not', Coq Dev
  - [Coq-Club] Re : Folding 'not', Coq Dev
- <Possible follow-ups>
- Re: [Coq-Club] Folding 'not', Paolo Herms
  - Re: [Coq-Club] Folding 'not', St�phane Lescuyer