Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Folding 'not'

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Folding 'not'


chronological Thread 
  • From: St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>
  • To: Coq Dev <coqletsgo AT yahoo.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Folding 'not'
  • Date: Mon, 11 Jul 2011 11:47:23 +0200

Hi,

A "fold_not" tactic is easy enough to write with Ltac. Here is a quick go at 
it:

Ltac fold_not :=
  match goal with
    | H : context g [?X -> False] |- _ =>
      let h := context g[not X] in
        change h in H; fold_not
    | _ => idtac
  end.

Goal forall A B C, ~A -> ~~B -> ~(A /\ B) -> ~C -> ~(B \/ A).
Proof.
  intuition.
  fold_not.
Abort.


Stéphane L.
On Mon, Jul 11, 2011 at 11:28 AM, Coq Dev 
<coqletsgo AT yahoo.com>
 wrote:
> 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).
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06




Archive powered by MhonArc 2.6.16.

Top of Page