The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Oops, I made typing mistake.

Theorem T m:
 (fix F n m := match n with O => match m with O => O | _ => O end | S n' => S n' + F n' m end) O m = O.

... = O, not ... = m.

My apologies.

On Tue, Dec 3, 2013 at 6:31 PM, Vincent <vincent.siles AT gmail.com> wrote:

If I correctly read your fixpoint:

(fix ..... ) 0 m = (match m with O => O | _ => O end) m = O

So your theorem is wrong.

Best,
V.


2013/12/3 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:

> How can I prove this?
>
> Theorem T m:
>  (fix F n m := match n with O => match m with O => O | _ => O end | S n' =>
> S n' + F n' m end) O m = m.
>
> Thanks in advance,
> Ilmars