coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proof of overflow resistance adder

From: fritjof AT uni-bremen.de
To: coq-club AT inria.fr
Subject: [Coq-Club] proof of overflow resistance adder
Date: Wed, 7 Feb 2018 10:56:16 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT smtp.uni-bremen.de
Ironport-phdr: 9a23:cYSwrxapA4TPDbdCdBQCgBv/LSx+4OfEezUN459isYplN5qZocu/bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA38G/ZlNF+gqFUrx29uhNwzZXZYJ2JOPdkYq/RYckXSGhHU81MVyJBGIS8b44XAuoPJ+ZYrpX9p1kJrRuwHgSsGeXvyj5RinDtx601zeEhHh/A3AA6At0BrnLZp8j2OqcKSe250afFwDrZY/9LxTvx9pLEfxA9rf2WQL58bdLdxVQhGg7KlFmctJDpMy2P2ugTrmSW7PBsWfyhhmMprQx6vyKhyd02iobTg4IY0lDE+jt9wIYyPdC4U0t7YcK8EJdKqiGaMYp2Tto5TGFypik6z6MJuZihcCcX1psr3x/fa/qZfIiU+h/vSeicLDhiiH54ZL6zmQy+/Ei8xuHmS8W4zE5Gri9fndnNsnAN2QbT6s+CSvZl8EehwzeP1xzR6uFDL0A5jrfbK5ggwrIpjZUTq1rMHirol0XwlqOZa1sr9vCy6+v7erXmuoOcN4hshw7iNaQug9WzDvg8MggTRGeW4v+81b3m/U3hWrpGlPw2kq/DsJDbP8sXvKC5AxUGmrokvh24FnKt1MkStXgBNlNMPhyd3KbzPFSbLur5EfW4jXyxljYuzerLO7DnRJnAfSuLq6voYbsosx0U8wE0190Kv8sFWIFEG+r6XwrKjPKdCxY4NwKuxOO+VYdg0IJbU3iCB6Kfdq/f4wbRurAfZtKUbYpQgw7TbuA/7qez32I/mBoXZ6Ss0J1RZH3qRq07cXXcWmLlh5I6KUlPvgc6S7ay2kaHTSYVenCzGqgm6zQ2DsSqANWbSw==

Hi,

I try to proof the following definition:

Definition max := 256 -1. (* 2^8 -1 *)

Definition adder (a b:nat) : option nat :=
if le_lt_dec a (max-b)
then
Some (a+b)
else
None.

With the theorem:
Theorem adder_no_overflow : forall a b: nat, a <= (max-b) <-> adder a b =
Some (a+b).
Proof.
intros a b.
unfold adder.
case (le_lt_dec a (max-b)).
split.
reflexivity. (* proof 1/3 *)
rewrite <- l.
reflexivity. (* proof 2/3 *)

(* stuck here *) (* proof 3/3 *)
Qed.

The part where I stuck is:
1 subgoal
a, b : nat
______________________________________(1/1)
max - b < a -> a <= max - b <-> None = Some (a + b)

In every way I have to show: None = Some (a+b), what fails.

My approach is to show that for:
* a <= max-b -> Some (a+b) will be returned
* a > max-b -> None will be returned.

Can someone point me into the right direction or do I oversee something?

--f.

[Coq-Club] proof of overflow resistance adder, fritjof, 02/07/2018
- Re: [Coq-Club] proof of overflow resistance adder, Laurent Thery, 02/07/2018