The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

One more:

Goal even 4 /\ even 22.

change (even 4) with (even 40).

On Oct 21, 2013, at 14:40 , Nuno Gaspar <nmpgaspar AT gmail.com> wrote:

wouldn't

Goal even(4).
replace (even 4) with (even 2); auto.

be easier.. :-)

2013/10/21 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.

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.