This page: bit.ly/coqosxp2022

A Coq tutorial about accounts and financial transactions

This page is meant to be used as a playground to experiment with Coq, directly in your web-browser.

A Coq header

It is the tradition in Coq to have a very crude language and packages that can be loaded at will by users to provide the primitives that will be used by users. For this example, we will load packages describing simple string operations, arithmetic with unbounded integers, lists and classical logical reasoning.

Require Import String ZArith List Classical. Open Scope string_scope. Open Scope Z_scope.

A little example about bank account management

The advantage of higher-order logic is that we can reason about programs depending on fragments that have not been developed yet. To illustrate this, we propose an example of banking transactions relying on a database of accounts, where we suppose only the existence of two functions to access the value at a key in a given state of the database and to update the value at a key.

In the following Coq fragment, we open a section to give ourself a space where we make a few assumptions of existence. We assert the type of accounts and the two function operating on accounts exist. We also express properties about these functions, more precisely we describe how these functions interact together.

Section assume_database_operations. Variable accounts : Type. Variable get : string -> accounts -> Z. Variable set : string -> Z -> accounts -> accounts. Hypothesis get_after_set_same_key : forall db k v, get k (set k v db) = v. Hypothesis get_after_set_diff_key : forall db k k' v, k <> k' -> get k' (set k v db) = get k' db.

Explaining the get and set functions and their properties

In this code fragment, line 4 declares that we open a new section. Line 6 declares that we assume the existence of a type of data named accounts. Lines 8 and 9 assumes the existence of two functions and gives their type. Line 8 says that the function get takes two arguments: the first has type string and the second one has type accounts, the return value has type Z, a type for unbounded integers. Line 9 says that function set has three arguments and returns a value of type accounts. stringLines 11-12 assume that calling the function get on a database of accounts obtained by set returns the set value, if the same key is used for both set and get.

Lines 14-15 assume that calling the function get on a database obtained by set returns the same value as in the previous database, if the two keys used for set and get are different.

The forall sign (inverted A) and the arrow are obtained by typing "forall" and "->". The "different" sign (a slashed equal sign), is obtained by typing <>. Applying a function to several arguments is written by typing the name of the function and then the arguments separated by blank space. Parentheses are used only if one of the arguments is itself obtained through a function call.

An initial database

We also assume the existence of an initial database, where all possible accounts have value 0.

Variable init_db : accounts. Hypothesis init_zero : forall k, get k init_db = 0.

Reasoning abstractly on incomplete code

While in section assume_database_operations, we can write new code depending on get and set and we can simulate its execution, by performing elementary proofs.

For instance, here is a piece of code that defines a new database of accounts with specifc values for a variety of keys

Definition db5 := let db1 := set "Alice" 10 init_db in let db2 := set "Bernard" 5 db1 in let db3 := set "Claude" 30 db2 in let db4 := set "Alice" 15 db3 in set "Denis" 7 db4.

This code is incomplete, because we do not know how get and set are implemented. But we can execute this code symbolically thanks to the behavior rules get_after_set_same_key, get_after_set_diff_key, and init_zero. The symbolic execution will happen by performing proofs.

Lemma db5_denis : get "Denis" db5 = 7. Proof. unfold db5. rewrite get_after_set_same_key.

In Line 26, we assert that we want the execution of get db5 "Denis" to return the value 7. Line 27 has no effect other than making our script more readable. Line 28 expands the definition of db5. Line 29 is used to recognize that the current statement we want to prove contains an instance of get_after_set_same_key and replaces that instance by the corresponding value. After executing that line, the goal contains an obvious statement. We can solve this goal by using a very simply proof command: easy.

easy. Qed.

More automation

Time is too short to explain how automation works in the Coq system. For the examples given on this page, we will need a proof finisher that is slightly stronger than the command named easy. Here is how we define it:

Ltac obvious := solve[easy | ring | auto].

A proof that uses both properties of get and set

Now we can prove something similar for the name Alice.

Lemma db5_alice : get "Alice" db5 = 15. Proof. unfold db5. rewrite get_after_set_diff_key. rewrite get_after_set_same_key. obvious. obvious. Qed.

Note that line 34 generates two goals. The first goal is solved by lines 35-36. The second goal is kept for later and gets solved at line 37.

Your turn: solve an exercise

By reproducing the steps of db5_alice, you should be able to write a lemma stating the expected value for Claude and Bernard. (* This is a comment. *) (* Please enter you own sequence of commands to state lemmas expressing the values of accounts for Claude and Bernard in the database db5. *)

More advance programming: a transfer operation

We can now program a general operation to transfer money from one account to another.

(* How would you write such a function? Define a function that takes as input a database, an emitter and a receiver, both of type string, and an amount, of type Z. Name your function student_transfer. *)

Here is our solution

Definition transfer (emitter receiver : string) (amount : Z) (db : accounts) : accounts := let v1 := get emitter db - amount in let db1 := set emitter v1 db in let v2 := get receiver db1 + amount in set receiver v2 db1.

Expected values of accounts after a transfer

If we transfer an amount a from account x to account y, and in y's account before the transfer was n, what should be the value in y's account after the transfer? Write a statement that expresses it, and prove it.

(* If you cannot finish the proof, you can write "Admitted." instead of "Qed." The proof is marked as unfinished, but the tool lets you proceed to the later parts of the script. *)

Our solution to the last exercise

Lemma transfer_receiver : forall db emitter receiver amount, emitter <> receiver -> get receiver (transfer emitter receiver amount db) = get receiver db + amount. Proof. intros db emitter receiver amount. intros emitter_n_receiver. unfold transfer. rewrite get_after_set_same_key. rewrite get_after_set_diff_key. obvious. obvious. Qed.

The lesson of the last proof is that the naive expectation about the resulting amount for the receiver is not satisfied if the emitter and receiver are the same person. The proof process makes it clear: in this sense, it helps catching potential bugs by showing that easy general statements are sometimes not provable. By doing so, it forces users to document more precisely the conditions under which code behaves as expected.

Making the code more concrete

When we close the section assume_database_operations, we obtain a higher-order transfer function, that will work on top of any database implementation, as long as such a database satisfies the required properties.

End assume_database_operations. Check transfer. Check transfer_receiver.

The last Checkbcommand shows that the proof we did for transfer_receiver still holds, but it requires that we provide the datatype for account databases, the two functions get and set and the proofs that they have the right properties.

.

A naive implementation based on lists of pairs

As a first illustration, we show that the datatype can be encoded using lists of pairs, which record in order all the set operations that have been done since the beginning. This has the advantage that the set operation takes constant time, but the get operation has a complexity that grows with time (especially for accounts that are seldom modified).

Definition l_accounts := list (string * Z). Definition l_get (k : string) (accounts : l_accounts) : Z := match find (fun p => String.eqb k (fst p)) accounts with | None => 0 | Some (_, v) => v end. Definition l_set (k : string) (v : Z) (accounts : l_accounts) : l_accounts := (k, v) :: accounts. Lemma l_get_after_set_same_key : forall (db : l_accounts) (k : string) (v : Z), l_get k (l_set k v db) = v. Proof. intros db k v; unfold l_set, l_get; simpl. Search (?x =? ?x)%string. rewrite String.eqb_refl. easy. Qed. Lemma l_get_after_set_diff_key : forall (db : l_accounts) (k k' : string) (v : Z), k <> k' -> l_get k' (l_set k v db) = l_get k' db. Proof. intros db k k' v k_n_k'. unfold l_get, l_set. simpl. assert (testk'k : (k' =? k)%string = false). rewrite String.eqb_neq. auto. rewrite testk'k. easy. Qed.

We can now show that the transfer function works in this setting.

Definition l_transfer := transfer _ l_get l_set. Lemma l_transfer_receiver : forall db emitter receiver amount, emitter <> receiver -> l_get receiver (l_transfer emitter receiver amount db) = l_get receiver db + amount. Proof. exact (transfer_receiver _ _ _ l_get_after_set_same_key l_get_after_set_diff_key). Qed.

The function l_transfer is the function transfer specialised on this naive implementation of account databases. Developing a more efficient implementation is also possible in a few lines. Contact Yves Bertot at Inria for more information.