The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi,

Sometimes fold works only if you provide the full term.

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

Alternatively, you could write a tactic to do that automatically.
This example is maybe not the best one because you do not
control where you fold the nots:

======================
Ltac fold_not := match goal with
 | |- context [?x -> False] => fold (not x)
 | H: context [?x -> False] |- _ => fold (not x) in H
end.
======================

Cheers,

--
gallais



On 11 July 2011 11:28, 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).
>