The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

I am wondering if the performance of an OCaml code --extracted from a Coq formalisation-- would be different if a matrix data structure is modelled as a function type compared to a list of lists? During formalisations if it involves matrices, I assume them as a function type (A -> B -> C for finite type A and B) than a list of lists. Function type is nice for reasoning about correctness proofs, but when I extract OCaml code from the formlisation and need to call an OCaml function from main.ml, I create a function type (see the definition of mat below) at main.ml and pass it to the OCaml function. Another way I can achieve the same functionality is to create the matrix as a list of lists in main.ml and then use a search function that turns the list of lists into a function type (see the example fnmat). Below I have provided an OCaml code but it can also be implemented in Coq, although it may require some effort. Now the question is does it matter to the OCaml compiler?  I would also appreciate it if you know of any formalisations about matrix multiplication in Coq and could post them here.

Best,

Mukesh

(* function type *)
let mat (x : coq_Node) (y : coq_Node) : coq_RR = 
  match x, y with
  | A, A -> oneRR
  | A, B -> (Left 3, Left 5) 
  | B, A -> zeroRR 
  | A, C -> (Left 5, Left 4)
  | C, A -> zeroRR 
  | B, B -> oneRR
  | B, C -> (Left 2, Left 10) 
  | C, B -> zeroRR 
  | C, C -> oneRR  

(* Another way to encode the matrix mat *)
let listmat : (coq_Node * ((coq_Node * coq_RR) list)) list =
  [(A, [(A, oneRR); (B, (Left 3, Left 5)); (C, (Left 5, Left 4))]);
   (B, [(A, zeroRR); (B, oneRR); (C,  (Left 2, Left 10))]);
   (C, [(A, zeroRR); (B, zeroRR); (C, oneRR)])]

(* turn it into a function type *)
let fnmat : coq_Node -> coq_Node -> coq_RR = 
  fun (x : coq_Node) -> fun (y : coq_Node) -> List.assoc y (List.assoc x listmat)