The Coq mailing list

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

Dear Christophe,

 

I think a direct translation of Python to Gallina might work except for:

 

-          while loops

-          recursive functions

-          function variables

 

I don’t think python has other potentially non terminating constructs. The object system might make it quite nasty, though.

 

But it is an interesting question how desirable this would be or for what purpose this should be used. It might be useful for converting parts of the Python standard library to Coq. But for proving properties of Python programs it is likely a better idea to have an inductive description of Python programs and some interpreter for this, so that one can make inductive proofs of general interesting properties of Python programs.

 

Best regards,

 

Michael

 

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Christophe Bal
Sent: Thursday, May 21, 2015 8:48 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Newbies Question

 

Thanks a lot.

 

Do you think that this kind if thing could be automated ?

 

I ask this because I will do a Python package, in a near future, that can produce a fine AST from Python code (and also other language). Then it could be interesting to see if a transformation from the AST to Coq could be done so as to launch verifications ?

 

Christophe BAL

Enseignant de mathématiques en Lycée et développeur Python amateur

---

French math teacher in a "Lycée" and Python amateur developer

 

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

Dear Christophe,

 

If your question is about the transcript from python to Coq, rather than the proof, please find it below. I did it quite quickly, so quite possible that I made a flaw. Maybe Laurent can comment on this. The main difference is that I used nat instead of Z. I did it like this because my automation system cannot handle Z well as yet, and I just wanted to give it a quick try out of curiosity. It is difficult to compare results with the python code, because simu doesn’t really compute a value one could compare for a few sample values besides the assert results. The basic structure of the code should be ok, though. The transcript is done pretty much 1:1 without some simplifications one could do.

 

Best regards,

 

Michael

 

 

Require Import Nat.

 

Definition value (d f i p k x : nat) : nat * nat :=

  match i with

  | 1 => (d,1)

  | _ =>

    let r := if k =? (i-1) then p else p-1 in

    let s := if p =? 1 then 1 else 0 in

    let u := (i-1)*(p-1)+k+s in

    let v := (i-1)*(p-1)+k+r in

    let v' := if f <? v then f else v in

    let t := ((100-x)*u+x*v')/100 in

    let q := (t-1)/i in

    (1+q, t-i*q)

  end.

 

Fixpoint simuloop (n i d f x po ko to: nat) : bool :=

  match n with

  | 0 => true

  | S n' =>

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

    let t := k*p +(i-k)*(p-1) in

    let po' := p in

    let ko' := k in

    let check :=

      andb (andb (0<?p) (0<?k))

      (if p =? po' then k<=?ko'

       else andb (p <? po') (to<=?t)) in

    let to' := t in

      andb check (simuloop n' (i+1) d f x po' ko' to')

  end.

 

Definition simu (d f x : nat) : bool :=

  simuloop (f+10-1) 1 d f x d 0 0.