The Coq mailing list

[txrev319 AT gmail.com]

You're right. I screwed up. I incorrectly linked lower with -, when it was clearly defined with +. I think simpl, omega should solve this lemma.

Marcus Ramos <mvmramos AT gmail.com> wrote:

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.