The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Since I add first and subtract later, I don´t think this situation will happen. Anyway, it is just an example, and could be improved to ensure that arguments are in the range "A"-"Z" for lower and "a"-"z" for upper. But the point is on how to prove by induction on ascii.

2013/10/24 t x <txrev319 AT gmail.com>

I don't think the lemma is true. In Coq, (0 - 32) + 32 = 0 + 32 = 32.

On Thu, Oct 24, 2013 at 9:46 AM, Marcus Ramos <mvmramos AT gmail.com> wrote:

Hi,

This is probably a very basic question, but since I have no teacher to ask about, I guess whether any of you would give me a hint on how to prove the following theorem (a reduced version of the problem I am working with):

Require Import Ascii.

Definition upper (c: ascii): ascii := ascii_of_nat ((nat_of_ascii c)-32).

Definition lower (c: ascii): ascii := ascii_of_nat ((nat_of_ascii c)+32).

Theorem t:

   forall c: ascii,

   upper (lower c) = c.

It has to do with proving by induction over ascii, but I have no idea on how to do it. Once again, sorry for bothering with basic questions...

Thanks in advance,

Marcus.