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 -----
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
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 -----
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"?
====================
