Formal Verification for OCaml

let rec map = fun f l →
match l with [] → [] | x::xs → f x :: map f xs
and fold_left = fun f a l →
match l with [] → a | x::xs → fold_left f (f a x) xs
and comp = fun f g x → f (g x)
and mul = fun a b → a * b
and id = fun x → x the task is to prove fold_left mul 3 [10] ⇒ 30

Hi @DonCorleone, is this a homework question? We do not permit this forum to be used for simply exchanging homework solutions, although if you have specific questions about something you do not understand in OCaml or formal verification, you are free to ask those.

2 Likes

Hello. I am not sure what you exactly need because you did not really explain it clearly.

A formal verification approach could use a proof assistant like Coq, whose programming language, Gallina, is an advanced version of OCaml with dependent types and a specific relation to logic called the Curry-Howard isomorphism. However, it is clearly overkill on this kind of example because the proof you are asking for can be done just by computing the left hand term (reflexivity).

Maybe you were asked to give details about the reduction in OCaml that leads to this result?

From Coq Require Import List.
Import ListNotations.

Fixpoint map {A B : Type} (f : A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: xs => f x :: map f xs
  end.

Fixpoint fold_left {A B : Type} (f : A -> B -> A) (a : A) (l : list B) : A :=
  match l with
  | [] => a
  | x :: xs => fold_left f (f a x) xs
  end.

Definition mul (a b : nat) : nat := a * b.

Goal fold_left mul 3 [10] = 30.
Proof. reflexivity. Qed.

The advantage of a proof assistant is that you could prove for example that the product of a list containing 0 is always 0. This is a more general results than your computation and Coq allows to reason about that.

exactly, I wanted such proof… thank you.