The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

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.