The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Cedric,

 

yes, you are right. I used it as test case for the proof automation I am working on and tried to do it as mechanic as possible, but for sure I should have chosen values which fulfill the preconditions. I also think that x has to be <=100.

 

And yes, in POST1 p equals po cause of the assignment, so POST2 is never entered. Just POST0 is not trivially true.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Cedric Auger
Sent: Thursday, May 21, 2015 6:19 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Newbies Question

 

 

 

2015-05-21 17:51 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Laurent,

 

I gave it a quick try in Coq as an exercise. I transcribed your python to Coq Gallina and tried to prove:

 

Theorem simuok: forall d f x : nat, simu d f x = true.

 

Here simu returns the and of all asserts over all loop iterations. It shows quickly that this fails for d=f=x=0 (your python code agrees on this). So for what ranges should it hold? Or should it just hold for all d and x with f=679?

 

Best regards,

 

Michael

 

​Technically, that does not come into contradiction with POST0, POST1 and POST2, as "value(d,f,i,po,ko,x)" would have failed before reaching POSTn (the PRECOND statement).

I am not used to Python, and there are things, that I do not understand at all in this code, probably because I have wrong ideas on the semantics.​

I do not see how the POST2 branch can be entered. Didn’t we have a po←p 3 lines above? And for POST1 (which seems to be always entered for the exact same reason), how could POST1 not be trivially true, as 2 lines above, we also have ko←k?

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of FOURNIER Laurent
Sent: Thursday, May 21, 2015 11:26 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Newbies Question

 

Hello everyone,

I’m new on this mailing list…I do not know if posts can be in French or should be in English !

 

My concern is about the following Python code (can be translated in any language !)

________________________________________________

def value(d, f, i, p, k, x):

    assert d>0 and f>=d and x>=0 and x<=100 and i>0 and p>=0 and k>=0 #PRECOND

    if i == 1: return d, 1

    r, s = p if k==i-1 else p-1, 1 if p==1 else 0

    u, v = (i-1)*(p-1)+k+s, (i-1)*(p-1)+k+r

    if v > f: v = f

    t = ((100-x)*u+x*v)//100

    q = (t-1)//i

    return 1+q, t-i*q

 

def simu(d, f, x):

    print ('init:%d final:%d speed:%d' % (d, f, x))

    po, ko, to = d, 0, 0

    for i in range(1, f+10):

        p, k = value(d, f, i, po, ko, x)

        t, po, ko = k*p +(i-k)*(p-1), p, k

        assert p>0 and k>0                  #POST0

        if p == po: assert k<=ko         #POST1

        else: assert p<po and t>=to #POST2

        to = t

        print ('%d: %d*%d+%d*%d=%d' % (i, k, p, i-k, p-1, t))

 

if __name__ == '__main__':

    for j in range (1, 200): # for instance !

        for s in range(101):

            simu(d=j, f=679, x=s)

 

A simple simulation shows that the assertions in POST0,1,2 never raise, but I need a FORMAL PROOF that I can remove those 3 lines and be sure that the post-conditions will always be verified. (All parameters are integers and // means “integer division”)

 

I also need to put the proof in a LaTeX formatted paper if not too long.

 

Question: Is COQ the right tool to get this proof ?

(consider I do not know COQ and do not expect to spend 2 years in training for that)

If the answer is YES, which lab could be able to do the job (get the proof) ?

 

Merci d’avance pour votre aide,

 

Laurent Fournier, PhD.