The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

A shorter version of Laurent's script is

remember 2 as n eqn:H.
simpl; rewrite H.

(it does pretty much the same thing under the hood)

On 21 October 2013 14:24, Laurent Théry <Laurent.Thery AT inria.fr> wrote:

On 10/21/2013 01:48 PM, michael.soegtrop AT intel.com wrote:

Fixpoint even (n:nat) : Prop :=
   match n with
   | 0 => True
   | 1 => False
   | S (S p) => even p
   end.

Eval simpl in even(4).

One possible trick is to artificially reduce the number of constructors so to stop the expansion.


Goal even(4).
assert (exists n, 2 = n) by (exists 2; auto).
case H; intros n H1; rewrite H1.
simpl; rewrite <-H1.