Prove functional programs

In this tutorial, we’ve already shown how Alt-Ergo can be used to reason about programs in several ways.

  • We have proven the equivalence between different implementations of functions.

  • We have been able to prove the correctness of functions, reasoning on all possible inputs, including the context, and incorporating hypotheses.

  • We have checked properties of intermediate values in a computation, such as the absence of overflow errors.

  • We have proven properties of while loops, including termination, using loop invariants and variants.

  • We have also worked directly on various forms of abstract specification.

Leveraging what we’ve seen in the previous chapters, we are now going to tackle problems which often arise in structured and functional programming.

Structured programming helps programmers master the complexity of their programs by organizing them into simple parts with simple interfaces. One of the approaches to it is to take advantage of rich type systems. Other advantages of rich type systems have been introduced in the previous chapter. This pairs well with functional programming, where functions are pure (their output depends only of their input and not on the context). By using functions as values, functional programming is also prone to good factorizations in code through higher-order functions, which can lead to more code that is both more concise and more readable.

  • We’re not going to look at new ways of reasoning to work with pure functions: their specification is simply going to be simpler, and we’re not going to have to include the context in our quantifiers, resulting in simpler goals.

  • Structured/functional programming makes great use of recursive functions. For the moment, we haven’t proved properties about recursive functions, although we have used them extensively. While Alt-Ergo doesn’t directly support induction, it can still be a great help for inductive reasoning.

  • Finally, we’ll see how to reason with higher-order functions in Alt-Ergo’s native language by modelling them with functional arrays.

Recursive functions and induction

Alt-Ergo and induction

Recursive functions occur frequently in functional programming, in particular when dealing with recursive data structures.

Proofs about recursive functions and recursive data structures can be made by (structural) induction.

Recall the principle of induction on natural numbers.

Induction on natural numbers

Given a property \(\mathcal{P}\) on natural numbers, in order to show that

\(\forall n\in\mathbb{N},\,\mathcal{P}(n)\),

it is sufficient to prove

\(\mathcal{P}(0)\)
and \(\forall n\in\mathbb{N},\, \mathcal{P}(n) \implies \mathcal{P}(n+1)\).

Informally, this says that if \(\mathcal{P}\) holds for the base case \(0\), and can be propagated to every successor of values for which \(\mathcal{P}\) holds, then it holds for every natural number.

Structual induction is a generalization of this.

Structural induction

Given a structure \(\mathbb{T}\) recursively defined by several constructors and a property \(\mathcal{P}\) on \(\mathbb{T}\), in order to prove that

\(\forall t\in\mathbb{T},\,\mathcal{P}(t)\),

is is sufficient to prove that

For each constructor \(c\) of \(\mathbb{T}\),
for all possible values \(a_1, \cdots, a_{k_c}\) of the arguments of \(c\),
if \(\mathcal{P}\) holds for each of the \(a_i\) (arguments of \(c\)) that is of type \(\mathbb{T}\),
then \(\mathcal{P}\) holds for \(c(a_1,\cdots,a_{k_c})\).

Informally, this says that if \(\mathcal{P}\) holds for all base cases (constructors with no arguments of type \(\mathbb{T}\)) and can propagated to every value of \(\mathbb{T}\) that can be constructed from values for which \(\mathcal{P}\) holds, then \(\mathcal{P}\) holds for every contructible value of \(\mathbb{T}\).

Induction on natural numbers is indeed a special case of structural induction, as natural numbers can be defined in the following way.

Illustration: structural induction on binary trees.

Consider the type on binary trees.

type 'a tree = Nil | Node of {left: 'a tree; val: 'a; right: 'a tree}

Structural induction allows us to say that a predicate p of type 'a tree -> bool is a tautology if

  • p(Nil) is true.

  • forall t1, t2: 'a tree. forall v:'a. p(t1) -> p(t2) -> p(t1,v,t2) is true.

Structural induction can be used similarly to prove properties of recursive functions, as we will see in the next subsections.

Higher-level tools are able to generate induction principles for every algebraic datatype. However, Alt-Ergo cannot neither generate by itself the subgoals necessary to prove something by induction, nor conclude once they are proven. Nevertheless, it can often be a great help to prove those subgoals.

Because of this, it can be used under the hood of an higher-level tool, whose sole responsibility will be say: “let’s this by induction on that”, to unfold the induction principle, and let Alt-Ergo prove the rest.

We’ll look at an example of this in the next subsection.

Example/Exercise: list append

In this subsection, we’re going to prove properties about lists, a recursive data structure.

First, implement the recursive function append, which concatenates two lists.

Exercise

type 'a list = Nil | Cons of {h:'a; t:'a list}

function append(l1: 'a list, l2: 'a list):'a list =
    (* YOUR CODE HERE
    
    
    
    *)
    
(* Tests *)
logic l1, l2: int list
axiom l1_def: l1 = Cons(1,Cons(2,Cons(3,Nil)))
axiom l2_def: l2 = Cons(4,Cons(5,Nil))
    
goal test_1: append(l1, l2)   = Cons(1,Cons(2,Cons(3,Cons(4,Cons(5,Nil)))))
goal test_2: append(l2, l1)   = Cons(4,Cons(5,Cons(3,Cons(2,Cons(1,Nil)))))
goal test_3: append(l1, Nil)  = append(Nil, l1) = l1
goal test_4: append(Nil, Nil) = Nil

Solution

type 'a list = Nil | Cons of {h:'a; t:'a list}

function append(l1: 'a list, l2: 'a list):'a list =
    match l1 with
    | Nil       -> l2
    | Cons(h,t) -> Cons(h,append(t,l2))
    end
    
(* Tests *)
logic l1, l2: int list
axiom l1_def: l1 = Cons(1,Cons(2,Cons(3,Nil)))
axiom l2_def: l2 = Cons(4,Cons(5,Nil))
    
goal test_1: append(l1, l2)   = Cons(1,Cons(2,Cons(3,Cons(4,Cons(5,Nil)))))
goal test_2: append(l2, l1)   = Cons(4,Cons(5,Cons(3,Cons(2,Cons(1,Nil)))))
goal test_3: append(l1, Nil)  = append(Nil, l1) = l1
goal test_4: append(Nil, Nil) = Nil

Let’s try to prove properties about the recursive function append.

It should be clear that Nil is an identity element for append, i.e. that forall l:'a list. append(Nil, l) = l and forall l:'a list. append(l, Nil) = l.

While the former can easily be proven by Alt-Ergo (check it!), the latter is more difficult: it requires induction on l.

In order to prove this property, having decided that we want to prove it by induction, an higher-level tool could generate the following code.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end
    
(** Proving append_l_nil by induction *)

predicate append_l_nil_prop(l:'a list) =
    append(l, Nil) = l

goal append_l_nil_rec :
    forall l:'a list.
    match l with
    | Nil       ->  append_l_nil_prop(l)
    | Cons(_,t) -> (append_l_nil_prop(t) -> append_l_nil_prop(l))
    end
    
(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)

axiom append_nil_l :
    forall l: 'a list. append_l_nil_prop(l)

Note that Alt-Ergo is able to prove this ! Notice was happened.

  • The property append(l, Nil) = l, which we would have called \(\mathcal{P}\) before, has been explicitely stated as the predicate append_l_nil_prop.

  • Alt-Ergo is unable to prove our real goal append_nil_l directly.
    Thus, we rather prove the hypotheses of the induction principle on list, by proving append_l_nil_rec.

  • The induction principle is unfolded in append_l_nil_rec with pattern matching.

  • Alt-Ergo cannot conlude append_nil_l by applying an induction principle, so it is added as an axiom for further goals.
    Because of this, further proofs will assume that the lemma append_l_nil_rec has been proven.

Exercise

Prove that append is associative. In other words, you want to prove that forall l1, l2, l3:'a list. append(l1,append(l2,l3)) = append(append(l1,l2),l3) is Valid.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end
    
(* Proving append_associative by induction *)

(* YOUR CODE HERE













*)

Solution

Here is a proof by induction on l1.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end
    
(* Proving append_associative by induction *)

predicate append_assoc_prop(l1:'a list) =
    forall l2, l3:'a list.
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)

goal append_assoc_rec :
    forall l1:'a list.
    match l1 with
    | Nil         ->  append_assoc_prop(l1)
    | Cons(_,t1)  -> (append_assoc_prop(t1) -> append_assoc_prop(l1))
    end

(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)
    
axiom append_assoc :
    forall l1:'a list. append_assoc_prop(l1)

Help Alt-Ergo: custom triggers

Alt-Ergo proved to be of great help, but it is not always so easy.

For example, let’s have a look a the function rev below. We would like to prove that is it involutive.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end

function rev(l:'a list):'a list =
    match l with
    | Nil        -> Nil
    | Cons(h, t) -> append(rev(t),Cons(h, Nil))
    end
    
goal rev_involutive:
    forall l:'a list. rev(rev(l)) = l

First, on some version of Alt-Ergo, you may notice a typing error. This can be solved by helping the type checker via a type annotation.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end

function rev(l:'a list):'a list =
    match l with
    | Nil        -> (Nil : 'a list)
    | Cons(h, t) -> append(rev(t),Cons(h, (Nil : 'a list)))
    end
    
goal rev_involutive:
    forall l:'a list. rev(rev(l)) = l

The goal is hard enough to require induction, so we could try this. We may also add the goals proven on append to help the prover.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end
    
(* Those have been proven before *)
predicate append_l_nil_prop(l:'a list) =
    append(l, Nil) = l
axiom append_nil_l :
    forall l: 'a list. append_l_nil_prop(l)
predicate append_assoc_prop(l1:'a list, l2:'a list, l3:'a list) =
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)
axiom append_assoc :
    forall l1, l2, l3:'a list. append_assoc_prop(l1,l2,l3)

function rev(l:'a list):'a list =
    match l with
    | Nil        -> (Nil : 'a list)
    | Cons(h, t) -> append(rev(t),Cons(h, (Nil : 'a list)))
    end
    
(* Proving rev_involutive by induction *)

predicate rev_involutive_prop(l:'a list) =
    rev(rev(l)) = l

goal rev_involutive_rec :
    forall l:'a list.
    match l with
    | Nil       ->  rev_involutive_prop(l)
    | Cons(h,t) -> (rev_involutive_prop(t) -> rev_involutive_prop(l))
    end

(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)
    
axiom rev_involutive :
    forall l:'a list. rev_involutive_prop(l)

A lemma is actually necessary (you could find it by trying to prove the goal by hand or with an interactive theorem prover).

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end

(* Those have been proven before *)
predicate append_l_nil_prop(l:'a list) =
    append(l, Nil) = l
axiom append_nil_l :
    forall l: 'a list. append_l_nil_prop(l)
predicate append_assoc_prop(l1:'a list, l2:'a list, l3:'a list) =
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)
axiom append_assoc :
    forall l1, l2, l3:'a list. append_assoc_prop(l1,l2,l3)

function rev(l:'a list):'a list =
    match l with
    | Nil        -> (Nil : 'a list)
    | Cons(h, t) -> append(rev(t),Cons(h, (Nil : 'a list)))
    end
    
(* Proving the lemma rev_append by induction *)

predicate rev_append_prop(l:'a list) = 
    forall x:'a.
    rev(append(l, Cons(x,Nil))) = Cons(x, rev(l))

goal rev_append_rec :
    forall l:'a list.
    match l with
    | Nil       ->  rev_append_prop(l)
    | Cons(_,t) -> (rev_append_prop(t) -> rev_append_prop(l))
    end

(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)
    
axiom rev_append :
    forall l:'a list. rev_append_prop(l)

Strangely, this is not enough !

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end

(* Those have been proven before *)
predicate append_l_nil_prop(l:'a list) =
    append(l, Nil) = l
axiom append_nil_l :
    forall l: 'a list. append_l_nil_prop(l)
predicate append_assoc_prop(l1:'a list, l2:'a list, l3:'a list) =
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)
axiom append_assoc :
    forall l1, l2, l3:'a list. append_assoc_prop(l1,l2,l3)

function rev(l:'a list):'a list =
    match l with
    | Nil        -> (Nil : 'a list)
    | Cons(h, t) -> append(rev(t),Cons(h, (Nil : 'a list)))
    end
    
(* The lemma rev_append has been proved before *)
predicate rev_append_prop(l:'a list) = 
    forall x:'a. rev(append(l, Cons(x,Nil))) = Cons(x, rev(l))
axiom rev_append :
    forall l:'a list. rev_append_prop(l)
        
(* Proving rev_involutive by induction *)

predicate rev_involutive_prop(l:'a list) =
    rev(rev(l)) = l

goal rev_involutive_rec :
    forall l:'a list.
    match l with
    | Nil       ->  rev_involutive_prop(l)
    | Cons(h,t) -> (rev_involutive_prop(t) -> rev_involutive_prop(l))
    end
    
(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)

axiom rev_involutive :
    forall l:'a list. rev_involutive_prop(l)

Using the debugger, we could see that the lemma rev_append isn’t used at the right time.

This can be fixed by adding a little annotation in the quantifier of rev_append to help Alt-Ergo.

type 'a list = Nil | Cons of { h:'a; t:'a list } 

function append(l1:'a list, l2:'a list): 'a list =
    match l1 with
    | Nil        -> l2
    | Cons(h, t) -> Cons(h, append(t,l2))
    end
    
(* Those have been proven before *)
predicate append_l_nil_prop(l:'a list) =
    append(l, Nil) = l
axiom append_nil_l :
    forall l: 'a list. append_l_nil_prop(l)
predicate append_assoc_prop(l1:'a list, l2:'a list, l3:'a list) =
    append(l1, append(l2, l3)) = append(append(l1, l2), l3)
axiom append_assoc :
    forall l1, l2, l3:'a list. append_assoc_prop(l1,l2,l3)

function rev(l:'a list):'a list =
    match l with
    | Nil        -> (Nil : 'a list)
    | Cons(h, t) -> append(rev(t),Cons(h, (Nil : 'a list)))
    end
    
(* The lemma rev_append has been proved before *)
predicate rev_append_prop(l:'a list) = 
    forall x:'a. rev(append(l, Cons(x,Nil))) = Cons(x, rev(l))
axiom rev_append :
    forall l:'a list [l]. rev_append_prop(l)
        
(* Proving rev_involutive by induction *)

predicate rev_involutive_prop(l:'a list) =
    rev(rev(l)) = l

goal rev_involutive_rec :
    forall l:'a list.
    match l with
    | Nil       ->  rev_involutive_prop(l)
    | Cons(h,t) -> (rev_involutive_prop(t) -> rev_involutive_prop(l))
    end

(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)
    
axiom rev_involutive :
    forall l:'a list. rev_involutive_prop(l)

So what happened here ? We have used manual triggers for the first time.

Quantifiers are a central part of what makes first-order logic undecidable.

When Alt-Ergo sees code like

predicate p(x: int) = [...]
axiom a:
    forall x:int. p(x)

It cannot use all this the axiom a for all values of x at the same time (although some rewriting rules can be used in specific cases). Because of this, Alt-Ergo must choose some values of x for which it will had p(x) to its set of known truths. We say that Alt-Ergo instantiates the quantified variable x.

There is not perfect way to do this, so Alt-Ergo uses heuristics. Its heuristic is based on triggers. Each universal quantifier in Alt-Ergo’s native language holds a set of triggers, which look for patterns in the set of (closed) terms already seen by Alt-Ergo.

For instance, if P(x) is used as an instantiation pattern for the following axiom ax1,

logic P,Q,R : int -> prop
axiom ax1 : forall x:int. (P(x) or Q(x)) -> R(x)
goal g1 : P(1) -> R(1)
goal g2 : Q(2) -> R(2)

then, among the set {P(1), R(1), Q(2), R(2)} of known terms, only P(1) can be used by the matching algorithm to create the instance ((P(1) or Q(1)) -> R(1) of ax1 , which implies that only g1 is proved.

Alt-Ergo tries to automatically find good triggers for quantifiers, using heuristics.

However, it is possible to help Alt-Ergo by choosing triggers manually. Triggers can be written using various patterns, and using conjunction and disjonction. Check the documentation for more details on triggers.

Note that too few triggers will mean that goal cannot be proved, but too many triggers will drown Alt-Ergo in useless axioms, resulting in a timeout.

Warning

Manual triggers seem to work better when using the CDCL (Conflict Driven Clause-Learning) SAT-solver under the hood of Alt-Ergo, rather than with the Tableaux-like SAT-solver.

Higher-order functions and functional arrays

In functional programming, higher-order functions (functions which can take functions as input or output) are often used for code factorization.

Higher-order functions cannot be implemented directly in Alt-Ergo, but it is still possible to model them and to reason about them.

An example of such function is the function map, which applies a function to all elements of a list.

In OCaml, map could be defined like this.

type 'a list = Nil | Cons of 'a * 'a list

let rec map f = function 
    | Nil       -> Nil
    | Cons(h,t) -> Cons(f h, map f t)

Similarly, in WhyML (the language used in Why3), we could write the following.

use list.List

function map (f:'a->'b) (l:list 'a) : list 'b =
    match l with
    | Nil      -> Nil
    | Cons h t -> Cons (f h) (map f t)
    end

Representation of higher-order functions with functional arrays

This higher-order function can be represented with farray: the type of polymorphic functional arrays in Alt-Ergo’s native language.

  • Polymorphic functional arrays are arrays which can be created with any index and value type. Default index type is int.

    <t> farray is the type of farrays with index type int and value type <t>
    (<ti>,<tv>) farray is the type of farrays with index type <ti> and value type <tv>

  • They are a persistent structure, and support update (with f[<index>] <- <value>) and access (with f[<index>]).

For more information:

  • You may check the documentation to learn about Alt-Ergo’s native language’s version of polymorphic functional arrays, as well as their syntax.

  • You may have a look at this course, given at Cornell University, to learn about functional arrays as persistent structures.

  • You may check this section of Software Foundations to see another use of functional arrays, to model the context, or state, of imperative programms.

Here is how we could represent map in Alt-Ergo’s native language. (We help the type checker with a type annotation).

type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end

Note that any function (with a single argument) could be represented as a farray, turning an input type in a index type, and an output type in a value type.

A possible way to represent functions with several arguments as farray would be to currify them. (Another way would be to introduce a tuple type).

Representations of partial evaluation are possible as well.

type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end
    
logic map_partial: ('a, 'b) farray -> ('a list, 'b list) farray
axiom map_partial_def:
    forall f: ('a,'b) farray, l: 'a list. map(f,l) = map_partial(f)[l]

map_partial being a function with a single argument, it could be abstracted as a farray if needed.

type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end
    
logic map_partial: ('a, 'b) farray -> ('a list, 'b list) farray
axiom map_partial_def:
    forall f: ('a,'b) farray, l: 'a list. map(f,l) = map_partial(f)[l]
    
logic map_partial_abstr: (('a, 'b) farray, ('a list, 'b list) farray) farray

(* One possible definition, by abstraction *)
axiom map_partial_abstr_def_from_concrete:
    forall f: ('a,'b) farray. map_partial_abstr[f] = map_partial(f)
    
(* Another definition, avoiding the concrete partial function *)
axiom map_partial_abstr_def_from_parent:
    forall f:('a,'b) farray, l: 'a list. map_partial_abstr[f][l] = map(f,l)

A proof on higher-order functions

Another higher-order function is comp, which takes to functions as input and outputs their composition.

Let’s try to prove the following goal, which states that lifting a composition to a function on lists is the same as the composition of functions which have both been lifted.

The previous sentence was a complicated way of saying what’s more clearly written in the goal below, or expressed by saying that the following diagram commutes (where \(L(t):=\)t list).

../_images/diagram.svg 
type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end
    
logic map_partial: ('a, 'b) farray -> ('a list, 'b list) farray
axiom map_partial_def:
    forall f: ('a,'b) farray, l: 'a list. map(f,l) = map_partial(f)[l]

    
logic comp : ('b,'c) farray, ('a,'b) farray -> ('a,'c) farray
axiom comp_def:
    forall f: ('b,'c) farray, g: ('a,'b) farray, x:'a.
    comp(f,g)[x] = f[g[x]]
    

goal map_comp:
    forall f: ('b,'c) farray, g: ('a,'b) farray.
    map_partial(comp(f,g)) = comp(map_partial(f),map_partial(g))

Note that while functions cannot be used directly compared in Alt-Ergo’s native language, functional arrays can, and functional extensionality is true on farrays.

logic f,g: 'a -> 'b

axiom equal_on_elements: forall x:'a. f(x) = g(x)

goal equal: f=g

logic f,g: ('a, 'b) farray

axiom equal_on_elements: forall x:'a. f[x] = g[x]

goal equal: f=g

Thanks to this, we can reason directly on elements, and prove map_comp by induction on l.

Exercise

Do this.

Warning

The current version of Alt-Ergo is not yet strong enough to prove this goal using universal quantifiers on all types \(A\), \(B\) and \(C\).

Use int rather 'b when stating your predicates and goals. This will help Alt-Ergo.

You can try using other types instead of int: they should all work as well.

type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end
    
logic map_partial: ('a, 'b) farray -> ('a list, 'b list) farray
axiom map_partial_def:
    forall f: ('a,'b) farray, l: 'a list. map(f,l) = map_partial(f)[l]

    
logic comp : ('b,'c) farray, ('a,'b) farray -> ('a,'c) farray
axiom comp_def:
    forall f: ('b,'c) farray, g: ('a,'b) farray, x:'a.
    comp(f,g)[x] = f[g[x]]

(* YOUR CODE HERE
















*)

Solution

type 'a list = Nil | Cons of {h: 'a; t: 'a list}

function map (f: ('a,'b) farray, l: 'a list): 'b list =
    match l with
    | Nil        -> (Nil : 'b list)
    | Cons(h, t) -> Cons(f[h], map(f, t))
    end
    
logic map_partial: ('a, 'b) farray -> ('a list, 'b list) farray
axiom map_partial_def:
    forall f: ('a,'b) farray, l: 'a list. map(f,l) = map_partial(f)[l]

    
logic comp : ('b,'c) farray, ('a,'b) farray -> ('a,'c) farray
axiom comp_def:
    forall f: ('b,'c) farray, g: ('a,'b) farray, x:'a.
    comp(f,g)[x] = f[g[x]]

predicate map_comp_prop(l: 'c list) =
    forall f: (int,'c) farray, g:('a,int) farray.
    map_partial(comp(f,g))[l] = comp(map_partial(f),map_partial(g))[l]
    
goal map_comp_rec:
    forall l:'c list.
    match l with
    | Nil       ->  map_comp_prop(l)
    | Cons(_,t) -> (map_comp_prop(t) -> map_comp_prop(l))
    end

(* WARNING: deduction of the next axiom from the previous goal is performed outside of Alt-Ergo's control *)
    
axiom map_comp:
    forall l:'c list. map_comp_prop(l)