The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 24 Oct 2013 16:43:11 -0200,
Marcus Ramos 
<marcus.ramos AT univasf.edu.br>
 a écrit :

> Thanks for all the replies. I fixed the example, so now I think it
> can be proved in all cases:
> 
> Require Import Ascii.
> Require Import NPeano.
> 
> Definition change_case (c: ascii): ascii :=
>    let c': nat := nat_of_ascii c in
>    if andb (65 <=? c') (c' <=? 90) then ascii_of_nat (c'+32)
>    else if andb (97 <=? c') (c' <=? 122) then ascii_of_nat (c'-32)
>    else c.
> 
> Lemma change:
>    forall c: ascii,
>    change_case (change_case c) = c.
> Proof.
> intros [[][][][][][][][]].
> reflexivity.
> reflexivity.
> ...
> 
> My question however remains: do I have to write "reflexivity" 256
> times (that is, consider 256 different goals) in order to prove this
> lemma? Or is there an easier way to do this?
> 
> Best Regards,
> Marcus.

intros [[][][][][][][][]]; reflexivity.

This should do it. Simply replace '.' by ';'. For more information,
read the reference manual, or hope someone will explain it.

But again, flipping the right bit is a lot simpler than converting
to nat (and way more efficient).