17.4 Examples
17.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)
17.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 Fix le_gt_bool {le_gt_bool [n:nat] : nat -> bool :=
Coq < Cases n of
Coq < | O => [m:nat]true
Coq < | (S n') => [m:nat]Cases m of
Coq < | O => false
Coq < | (S m') => (le_gt_bool n' 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)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 (0))
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 (0) 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.
17.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 < Fix list_insert{list_insert [a:nat; l:list] : list :=
Coq < Cases l of
Coq < | nil => (cons a nil)
Coq < | (cons b m) =>
Coq < if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} }
Coq < then (cons b (list_insert a m))
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
list_insert : (a:nat; l:list)
(sorted l)->{l':list| (equiv a l l') & (sorted l')}
a : nat
l : list
H : (sorted nil)
============================
(equiv a nil (cons a nil))
subgoal 2 is:
(sorted (cons a nil))
subgoal 3 is:
(sorted (cons n' m))
subgoal 4 is:
(sorted m)
subgoal 5 is:
(equiv a (cons b m) (cons b x))
subgoal 6 is:
(sorted (cons b x))
subgoal 7 is:
(equiv a (cons b m) (cons a (cons b m)))
subgoal 8 is:
(sorted (cons a (cons b m)))
17.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 < Hints Resolve 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
Coq < Fix split {split [a:A;l:list] : list*list :=
Coq < Cases l of
Coq < | nil => (nil,nil)
Coq < | (cons b m) => let (l1,l2) = (split a m) 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)))
17.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 < Hints Resolve 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 <
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