The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 15, 2013 at 8:03 PM, Cedric Auger 
<sedrikov AT gmail.com>
 wrote:

> Fixpoint size_mod_2 x :=
>   match x with
>     | shapeA x' => size_mod_2' x'
>     | shapeB => true
>   end
> with size_mod_2' x :=
>   match x with
>     | shapeA' x' => negb (size_mod_2 x')
>     | shapeB' => true
>   end.
>
> Goal forall x, (shapeA (shapeA' x)) <> x.
>   intros x H; apply (f_equal size_mod_3) in H; simpl in *; destruct
> (size_mod_2 x); discriminate.
> Qed.

Yep, works fine. But only for that exact case, of course. Nesting the
goal one deeper makes it fail. :-) So I'd still prefer the general
size function. It's easier to understand, too. But like you said, it's
funny to use. ;-)

--
www.mhelvens.net