18.4 Examples

18.4 Examples

18.4.1 Ackermann Function

Let us give the specification of Ackermann's function. We want to prove that for every n and m, there exists a p such that ack(n,m)=p with:

ack(0,n) =   n+1
ack(n+1,0) =   ack(n,1)
ack(n+1,m+1) =   ack(n,ack(n+1,m))


An ML program following this specification can be:
let rec ack = function
        0  -> (function m -> Sm)
      | Sn -> (function  0  -> ack n 1
                       | Sm -> ack n (ack Sn m))


Suppose we give the following definition in Coq of a ternary relation (Ack n m p) in a Prolog like form representing p=ack(n,m):

Coq < Inductive Ack : nat->nat->nat->Prop :=
Coq < AckO : (n:nat)(Ack O n (S n))
Coq < | AcknO : (n,p:nat)(Ack n (S O) p)->(Ack (S n) O p)
Coq < | AckSS : (n,m,p,q:nat)(Ack (S n) m q)->(Ack n q p)
Coq < ->(Ack (S n) (S m) p).
Then the goal is to prove that " n,m .$ p.(Ack n m p), so the specification is:

(n,m:nat){p:nat|(Ack n m p)}. The associated Real program corresponding to the above ML program can be defined as a fixpoint:
Coq < Fixpoint ack_func [n:nat] : nat -> nat :=
Coq < Cases n of
Coq < O => [m:nat](S m)
Coq < | (S n') => Fix ack_func2 {ack_func2 [m:nat] : nat :=
Coq < Cases m of
Coq < O => (ack_func n' (S O))
Coq < | (S m') => (ack_func n' (ack_func2 m'))
Coq < end}
Coq < end.
The program is associated by using Realizer ack_func. The program is automatically expanded. Each realizer which is a constant is automatically expanded. Then, by repeating the Program tactic, three logical lemmas are generated and are easily solved by using the property Ack0, Ackn0 and AckSS.
Coq < Repeat Program.
3 subgoals
  
  ack_func : (n,m:nat){p:nat | (Ack n m p)}
  n : nat
  m : nat
  ============================
   (Ack O m (S m))
subgoal 2 is:
 (Ack (S n') O n0)
subgoal 3 is:
 (Ack (S n') (S m') n0)


18.4.2 Euclidean Division

This example shows the use of recursive programs. Let us give the specification of the euclidean division algorithm. We want to prove that for a and b (b>0), there exist q and r such that a=b*q+r and b>r.

An ML program following this specification can be: 
let div b a = divrec a where rec divrec = function
        if (b<=a) then let (q,r) = divrec (a-b) in (Sq,r)
                  else (0,a)
Suppose we give the following definition in Coq which describes what has to be proved, ie, $ q $ r. (a=b*q+r Ù  b>r):
Coq < Inductive diveucl [a,b:nat] : Set
Coq < := divex : (q,r:nat)(a=(plus (mult q b) r))->(gt b r)
Coq < ->(diveucl a b).
The decidability of the ordering relation has to be proved first, by giving the associated function of type nat->nat->bool:
Coq < Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}.

Coq < Realizer [n:nat]Match n with
Coq < (* O *) [m:nat]true
Coq < (* S *) [n',H,m]Cases m of
Coq < O => false
Coq < | (S m') => (H m')
Coq < end
Coq < end.

Coq < Program_all.

Coq < Save.
Then the specification is (b:nat)(gt b O)->(a:nat)(diveucl a b). The associated program corresponding to the ML program will be:
Coq < Realizer
Coq < [b:nat](<nat*nat>rec div :: :: { lt }
Coq < [a:nat]if (le_gt_dec b a)
Coq < then let (q,r) = (div (minus a b))
Coq < in ((S q),r)
Coq < else (O,a)).
Where lt is the well-founded ordering relation defined by:
Coq < Print lt.
lt = [n,m:nat](gt m n)
     : nat->nat->Prop
Note the syntax for recursive programs as explained before. The rec construction needs 4 arguments: the type result of the function (nat*nat because it returns two natural numbers) between < and >, the name of the induction hypothesis (which can be used for recursive calls), the ordering relation lt (as an annotation because it is a specification), and the program itself which must begin with a l-abstraction. The specification of le_gt_dec is known because it is a previous lemma. The term (le_gt_dec b a) is seen by the Program tactic as a term of type bool which satisfies the specification {(le a b)}+{(gt a b)}. The tactics Program_all or Program can be used, and the following logical lemmas are obtained:
Coq < Repeat Program.
6 subgoals
  
  b : nat
  H : (gt b O)
  a : nat
  ============================
   (well_founded nat lt)
subgoal 2 is:
 (lt (minus a0 b) a0)
subgoal 3 is:
 a0=(plus (mult (S q) b) r)
subgoal 4 is:
 (gt b r)
subgoal 5 is:
 a0=(plus (mult O b) a0)
subgoal 6 is:
 (gt b a0)
The subgoals 4, 5 and 6 are resolved by Auto (if you use Program_all they don't appear, because Program_all tries to apply Auto). The other ones have to be solved by the user.

18.4.3 Insertion sort

This example shows the use of annotations. Let us give the specification of a sorting algorithm. We want to prove that for a sorted list of natural numbers l and a natural number a, we can build another sorted list l', containing all the elements of l plus a.

An ML program implementing the insertion sort and following this specification can be: 
let sort a l = sortrec l where rec sortrec = function
        []    -> [a]
      | b::l' -> if a<b then a::b::l' else b::(sortrec l')
Suppose we give the following definitions in Coq:

First, the decidability of the ordering relation:
Coq < Fixpoint inf_dec [n:nat] : nat -> bool :=
Coq < [m:nat]Cases n of
Coq < O => true
Coq < | (S n') => Cases m of
Coq < O => false
Coq < | (S m') => (inf_dec n' m')
Coq < end
Coq < end.


The definition of the type list:
Coq < Inductive list : Set := nil : list | cons : nat -> list -> list.


We define the property for an element x to be in a list l as the smallest relation such that: " a " l (In x l) Þ (In x (a::l)) and " l (In x (x::l)).
Coq < Inductive In [x:nat] : list->Prop
Coq < := Inl : (a:nat)(l:list)(In x l) -> (In x (cons a l))
Coq < | Ineq : (l:list)(In x (cons x l)).


A list t' is equivalent to a list t with one added element y iff: (" x (In x t) Þ (In x t')) and (In y t') and " x (In x t') Þ ((In x t) Ú y=x). The following definition implements this ternary conjunction.
Coq < Inductive equiv [y:nat;t,t':list]: Prop :=
Coq < equiv_cons :
Coq < ((x:nat)(In x t)->(In x t'))
Coq < -> (In y t')
Coq < ->((x:nat)(In x t')->((In x t)\/y=x))
Coq < -> (equiv y t t').


Definition of the property of list to be sorted, still defined inductively:
Coq < Inductive sorted : list->Prop
Coq < := sorted_nil : (sorted nil)
Coq < | sorted_trans : (a:nat)(sorted (cons a nil))
Coq < | sorted_cons : (a,b:nat)(l:list)(sorted (cons b l)) -> (le a b)
Coq < -> (sorted (cons a (cons b l))).
Then the specification is:
(a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}.

The associated Real program corresponding to the ML program will be:
Coq < Realizer
Coq < [a:nat][l:list]
Coq < Match l with
Coq < (cons a nil)
Coq < [b,m,H]if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} }
Coq < then (cons b H)
Coq < else (cons a (cons b m))
Coq < end.
Note that we have defined inf_dec as the program realizing the decidability of the ordering relation on natural numbers. But, it has no specification, so an annotation is needed to give this specification. This specification is used and then the decidability of the ordering relation on natural numbers has to be proved using the index program.

Suppose Program_all is used, a few logical lemmas are obtained (which have to be solved by the user):
Coq < Program_all.
8 subgoals
  
  a : nat
  l : list
  F : (l:list)(sorted l)->{l':list| (equiv a l l') & (sorted l')}
  l0 : list
  H : (sorted nil)
  ============================
   (equiv a nil (cons a nil))
subgoal 2 is:
 (sorted (cons a nil))
subgoal 3 is:
 (sorted (cons n' l1))
subgoal 4 is:
 (sorted l1)
subgoal 5 is:
 (equiv a (cons n l1) (cons n x))
subgoal 6 is:
 (sorted (cons n x))
subgoal 7 is:
 (equiv a (cons n l1) (cons a (cons n l1)))
subgoal 8 is:
 (sorted (cons a (cons n l1)))


18.4.4 Quicksort

This example shows the use of programs using previous programs. Let us give the specification of Quicksort. We want to prove that for a list of natural numbers l, we can build a sorted list l', which is a permutation of the previous one.

An ML program following this specification can be: 
let rec quicksort l = function
   []   -> []
 | a::m -> let (l1,l2) = splitting a m in
                 let m1 = quicksort l1 and
                 let m2 = quicksort l2 in m1@[a]@m2
Where splitting is defined by: 
let rec splitting a l = function
        []   -> ([],[])
      | b::m -> let (l1,l2) = splitting a m in
                 if a<b then (l1,b::l2)
                        else (b::l1,l2)
Suppose we give the following definitions in Coq:

Declaration of the ordering relation:
Coq < Variable inf : A -> A -> Prop.

Coq < Definition sup := [x,y:A]~(inf x y).

Coq < Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}.
Definition of the concatenation of two lists:
Coq < Fixpoint app [l:list] : list -> list
Coq < := [m:list]Cases l of
Coq < nil => m
Coq < | (cons a l1) => (cons a (app l1 m)) end.
Definition of the permutation of two lists:
Coq < Inductive permut : list->list->Prop :=
Coq < permut_nil : (permut nil nil)
Coq < |permut_tran : (l,m,n:list)(permut l m)->(permut m n)->(permut l n)
Coq < |permut_cmil : (a:A)(l,m,n:list)
Coq < (permut l (app m n))->(permut (cons a l) (mil a m n))
Coq < |permut_milc : (a:A)(l,m,n:list)
Coq < (permut (app m n) l)->(permut (mil a m n) (cons a l)).
The definitions inf_list and sup_list allow to know if an element is lower or greater than all the elements of a list:
Coq < Section Rlist_.

Coq < Variable R : A->Prop.

Coq < Inductive Rlist : list -> Prop :=
Coq < Rnil : (Rlist nil)
Coq < | Rcons : (x:A)(l:list)(R x)->(Rlist l)->(Rlist (cons x l)).
Coq < End Rlist_.

Coq < Hint Rnil Rcons.
Coq < Section Inf_Sup.

Coq < Hypothesis x : A.

Coq < Hypothesis l : list.

Coq < Definition inf_list := (Rlist (inf x) l).

Coq < Definition sup_list := (Rlist (sup x) l).

Coq < End Inf_Sup.
Definition of the property of a list to be sorted:
Coq < Inductive sort : list->Prop :=
Coq < sort_nil : (sort nil)
Coq < | sort_mil : (a:A)(l,m:list)(sup_list a l)->(inf_list a m)
Coq < ->(sort l)->(sort m)->(sort (mil a l m)).
Then the goal to prove is " l $ m (sort m) Ù (permut l m) and the specification is

(l:list){m:list|(sort m)&(permut l m).

Let us first prove a preliminary lemma. Let us define ltl a well-founded ordering relation.
Coq < Definition ltl := [l,m:list](gt (length m) (length l)).
Let us then give a definition of Splitting_spec corresponding to
$ l1 $ l2. (sup_list a l1) Ù (inf_list a l2) Ù (l º l1@l2) Ù (ltl l1 (a::l)) Ù (ltl l2 (a::l)) and a theorem on this definition.
Coq < Inductive Splitting_spec [a:A; l:list] : Set :=
Coq < Split_intro : (l1,l2:list)(sup_list a l1)->(inf_list a l2)
Coq < ->(permut l (app l1 l2))
Coq < ->(ltl l1 (cons a l))->(ltl l2 (cons a l))
Coq < ->(Splitting_spec a l).
Coq < Theorem Splitting : (a:A)(l:list)(Splitting_spec a l).

Coq < Realizer [a:A][l:list]
Coq < Match l with
Coq < (* nil *) (nil,nil)
Coq < (* cons *) [b,m,ll]let (l1,l2) = ll in
Coq < if (inf_sup a b)
Coq < then (* inf a b *) (l1,(cons b l2))
Coq < else (* sup a b *) ((cons b l1),l2)
Coq < end.

Coq < Program_all.

Coq < Simpl; Auto.

Coq < Save.
The associated Real program to the specification we wanted to first prove and corresponding to the ML program will be:
Coq < Lemma Quicksort: (l:list){m:list|(sort m)&(permut l m)}.

Coq < Realizer <list>rec quick :: :: { ltl }
Coq < [l:list]Cases l of
Coq < nil => nil
Coq < | (cons a m) => let (l1,l2) = (Splitting a m) in
Coq < (mil a (quick l1) (quick l2))
Coq < end.
Then Program_all gives the following logical lemmas (they have to be resolved by the user):
Coq < Program_all.
3 subgoals
  
  a : list
  ============================
   (well_founded list ltl)
subgoal 2 is:
 (sort (app x0 (cons a0 x)))
subgoal 3 is:
 (permut (cons a0 m) (app x0 (cons a0 x)))


18.4.5 Mutual Inductive Types

This example shows the use of mutual inductive types with Program. Let us give the specification of trees and forest, and two predicate to say if a natural number is the size of a tree or a forest.

Coq < Section TreeForest.

Coq <
Coq < Variable A : Set.

Coq <
Coq < Mutual Inductive
Coq < tree : Set := node : A -> forest -> tree
Coq < with forest : Set := empty : forest
Coq < | cons : tree -> forest -> forest.

Coq <
Coq < Mutual Inductive Tree_Size : tree -> nat -> Prop :=
Coq < Node_Size : (n:nat)(a:A)(f:forest)(Forest_Size f n)
Coq < ->(Tree_Size (node a f) (S n))
Coq < with Forest_Size : forest -> nat -> Prop :=
Coq < Empty_Size : (Forest_Size empty O)
Coq < | Cons_Size : (n,m:nat)(t:tree)(f:forest)
Coq < (Tree_Size t n)
Coq < ->(Forest_Size f m)
Coq < ->(Forest_Size (cons t f) (plus n m)).

Coq <
Coq < Hint Node_Size Empty_Size Cons_Size.


Then, let us associate the two mutually dependent functions to compute the size of a forest and a tree to the the following specification:

Coq < Theorem tree_size_prog : (t:tree){n:nat | (Tree_Size t n)}.

Coq < Realizer [t:tree]
Coq < (Fix tree_size{
Coq < tree_size [t:tree] : nat := let (a,f) = t in (S (forest_size f))
Coq < with forest_size /1 : forest -> nat
Coq < := ([f:forest]Cases f of
Coq < empty => O
Coq < | (cons t f') => (plus (tree_size t) (forest_size f'))
Coq < end)
Coq < :: :: {(f:forest) {n:nat | (Forest_Size f n)}}}
Coq < t).


It is necessary to add an annotation for the forest_size function. Indeed, the global specification corresponds to the specification of the tree_size function and the specification of forest_size cannot be automatically inferred from the initial one.

Then, the Program_all tactic can be applied:
Coq < Program_all.
Subtree proved!

Coq < Save.
Realizer
  [t:tree]
   (Fix tree_size{tree_size [t:tree] : nat := 
                    Case t of [a,f:?](S (forest_size f))
                              end
                  with
                  forest_size/1 : forest->nat := 
                    ([f:forest]
                      Cases f of
                        empty => O
                      | (cons t f') =>
                            (plus (tree_size t) (forest_size f'))
                      end)
                     :: :: {(f:forest){n:nat | (Forest_Size f n)}}} t).
Program_all.
tree_size_prog is defined


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.7.3.html at 8/10/98