The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Yet alternative trick is to prove a lemma

  Lemma even_SS : even (S (S x)) = even x.

and then to use rewrite to obtain some better control over the unfolding.

On 10/21/2013 02:40 PM, Nuno Gaspar 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
> <mailto: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
>     
> <mailto:Laurent.Thery AT inria.fr>>
>  wrote:
>
>         On 10/21/2013 01:48 PM, 
> michael.soegtrop AT intel.com
>         
> <mailto: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.