coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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
Archive powered by MhonArc 2.6.16.