The Coq mailing list

[Christophe Bal <projetmbc AT gmail.com>]

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.