ATTENTION tout lovers of Church & Kleene Lambda Calculus / wish my French were good enough / I'd tell you so much more / Darling je vous aime beaucoups ... if you want to feel real nice / ask M. le docteur de rock n roll pour advice ... / Iles des Sourds / cliquez ici pour The Zombies

Cliquez les fiches pour le plus grande.

the strangest e-list I belong to (since U.N.C.L.E. shut down Silk Road) is Coq-Club, a c-Space meeting locus for the world's lovers of theorem proving assistants and the Lambda calculus of Church and Kleen. You know who you are. You might be a Dutch Power Cow (cf. Vleeptron Link List).

Cette homme posted to Coq-Club that he was a newbie, so he asked if he could only post in English.

I am hoping I can pump Laurent for stuff I need. I sent him the above Donald Evans faux stamps. I think that's fair. Unexpected Surprise Eyeball Beauty from an imaginary French-speaking archipelago!

Suis romanceur btw. That's my day job.

======================
 
If you know anything about Python, or own a Python, or lots of Pythons (Florida has a gazillion giant unwanted Burmese pythons that eat pet dogs and small humans), SVP Leave A Comment. I have Python issues and I need help.

I know a woman whose pet constrictor trapped her in her kitchen, kept her just out of reach of the phone, and spent an hour swallowing her before she managed to get help. He had devoured most of her left arm and wanted more. I don't know what we taste like, but those Ecuadorian rugby lads do. Polar bears like to hunt and kill us, but they don't like the way we taste, so they sniff us and then walk off without eating us. I hate when fresh-killed protein goes to waste like that.

===========

salut Laurent Fournier --

Suis anglophone de USA. I have been on Coq-Club for 4 years. All posts have been en anglais, jamais français.

I do not know if this is a Rule or Law of Coq-Club, or only a generally observed convention.

Bob

Massachusetts USA

P.S. Do you like Python? Did you use BASIC (or dialect of BASIC) before Python?

----- Original Message -----

From: FOURNIER Laurent

To: coq-club@inria.fr

Sent: Thursday, May 21, 2015 5:26 AM

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=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.

============

salut Laurent Fournier --

Finally ... my first Coq-Club e-mail pas en anglais!

----- Original Message -----

From: DAVID PEREIRA

To: coq-club@inria.fr

Sent: Saturday, June 06, 2015 7:58 AM

Subject: Re: [Coq-Club] Partial application is not allowed while using Function

Olá Marcus,

Acabei de ver a tua mensagem! Se quiseres eu posso tentar ajudar-te… consegues dar-me mais algum context (por exemplo o ficheiro em que ela falha)? Se quiseres manda-me o ficheiro e eu tento ajudar-te aqui…

Um alternativa pode ser usares of Program Fixpoint (embora este seja melhor para raciocinar sobre funções com tipos dependentes).

Diz coisas ;-)

Um abraço,

David

I have never had to "work" to be fluent in English, my head was born with English.

When I can't get to Europe, I drive a half-day north to Montreal to stretch my francais. They all understand my fine, expensive ecole Parisienne because most of their movies and TV and music are Parisienne.

But Parisiennes can't understand a thing Quebecers say, it's like Finno-Ugric to Parisiennes.

What communication I've managed in other languages, I thank my Latin class. The Romans taught EVERYONE (and killed them if they didn't speak Latin right ... Miss Murphy only gave me bad grades and Dirty Looks).

But next vie I will choose a language I can use to talk to the Living rather than aux les Mortes.

* * *

SVP if you can spare a little time to help a pathetic and perdu amateur ...

Tell me your thoughts about Python. How did you get to Python?

I have Python on my ordinateur, but I have barely touched it.

Should I invest heavily in learning Python? Or should I find a better HLL language for my programming needs?

Any help you can offer, any tips ... at this moment my beloved ability to code has been Shut Off, and I need a new platform to get back to coding.

Bob le Potzer du Coq

Massachusetts USA

PS: Ton "saintexupery" est Antoine de? Have you read "Vol de Nuit"?

====================