diff options
Diffstat (limited to 'doc/Program.tex')
| -rw-r--r-- | doc/Program.tex | 850 |
1 files changed, 0 insertions, 850 deletions
diff --git a/doc/Program.tex b/doc/Program.tex deleted file mode 100644 index aa900ecb9..000000000 --- a/doc/Program.tex +++ /dev/null @@ -1,850 +0,0 @@ -\achapter{The Program Tactic} -\aauthor{Catherine Parent} -\label{Addoc-program} - -The facilities described in this document pertain to a special aspect of -the \Coq\ system: how to associate to a functional program, whose -specification is written in \gallina, a proof of its correctness. - -This methodology is based on the Curry-Howard isomorphism between -functional programs and constructive proofs. This isomorphism allows -the synthesis of a functional program from the constructive part of its -proof of correctness. That is, it is possible to analyze a \Coq\ proof, -to erase all its non-informative parts (roughly speaking, removing the -parts pertaining to sort \Prop, considered as comments, to keep only the -parts pertaining to sort \Set). - -This {\sl realizability interpretation} -was defined by Christine Paulin-Mohring in her PhD dissertation -\cite{Moh89b}, and -implemented as a {\sl program extraction} facility in previous versions of -\Coq~ by Benjamin Werner (see \cite{COQ93}). -However, the corresponding certified program -development methodology was very awkward: the user had to understand very -precisely the extraction mechanism in order to guide the proof construction -towards the desired algorithm. The facilities described in this chapter -attempt to do the reverse: i.e. to try and generate the proof of correctness -from the program itself, given as argument to a specialized tactic. -This work is based on the PhD dissertation of -Catherine Parent (see \cite{CPar95}) - -\asection{Developing certified programs: Motivations} -\label{program_proving} - -We want to develop certified programs automatically proved by the -system. That is to say, instead of giving a specification, an -interactive proof and then extracting a program, the user gives the -program he wants to prove and the corresponding specification. Using -this information, an automatic proof is developed which solves the -``informative'' goals without the help of the user. When the proof is -finished, the extracted program is guaranteed to be correct and -corresponds to the one given by the user. The tactic uses the fact -that the extracted program is a skeleton of its corresponding proof. - -\asection{Using {\tt Program}} -The user has to give two things: the specification (given as usual by -a goal) and the program (see section \ref{program-syntax}). Then, this program -is associated to the current goal (to know which specification it -corresponds to) and the user can use different tactics to develop an -automatic proof. - -\asubsection{\tt Realizer \term.} -\tacindex{Realizer} -\label{Realizer} -This command attaches a program {\term} to the current goal. This is a -necessary step before applying the first time the tactic {\tt -Program}. The syntax of programs is given in section \ref{program-syntax}. -If a program is already attached to the current subgoal, {\tt -Realizer} can be also used to change it. - -\asubsection{\tt Show Program.} -\comindex{Show Program}\label{Show Program} -The command \verb=Show Program= shows the program associated to the -current goal. The variant \verb=Show Program n= shows the program associated to -the nth subgoal. - -\asubsection{\tt Program.} -\tacindex{Program}\label{Program} -This tactics tries to build a proof of the current subgoal from the -program associated to the current goal. This tactic performs -\verb=Intros= then either one \verb=Apply= or one \verb=Elim= -depending on the syntax of the program. The \verb=Program= tactic -generates a list of subgoals which can be either logical or -informative. Subprograms are automatically attached to the informative -subgoals. - -When attached program are not automatically generated, an initial program -has to be given by {\tt Realizer}. - -\begin{ErrMsgs} -\item \errindex{No program associated to this subgoal}\\ -You need to attach a program to the current goal by using {\tt Realizer}. -Perhaps, you already attached a program but a {\tt Restart} or an -{\tt Undo} has removed it. -\item \errindex{Type of program and informative extraction of goal do not coincide} -\item \errindex{Cannot attach a realizer to a logical goal}\\ -The current goal is non informative (it lives in the world {\tt Prop} -of propositions or {\tt Type} of abstract sets) while it should lives -in the world {\tt Set} of computational objects. -\item \errindex{Perhaps a term of the Realizer is not an FW - term}\texttt{ and you then have to replace it by its extraction}\\ -Your program contains non informative subterms. -\end{ErrMsgs} - -\begin{Variants} -\item{\tt Program\_all.} - \tacindex{Program\_all}\label{Program_all}\\ - This tactic is equivalent to the composed tactic - \verb=Repeat (Program OrElse Auto)=. It repeats the \verb=Program= - tactic on every informative subgoal and tries the \verb=Auto= tactic - on the logical subgoals. Note that the work of the \verb=Program= - tactic is considered to be finished when all the informative subgoals - have been solved. This implies that logical lemmas can stay at the end - of the automatic proof which have to be solved by the user. -\item {\tt Program\_Expand} - \tacindex{Program\_Expand}\label{Program_Expand}\\ - The \verb=Program_Expand= tactic transforms the current program into - the same program with the head constant expanded. This tactic - particularly allows the user to force a program to be reduced before - each application of the \verb=Program= tactic. - - \begin{ErrMsgs} - \item \errindex{Not reducible}\\ - The head of the program is not a constant or is an opaque constant. - need to attach a program to the current goal by using {\tt Realizer}. - Perhaps, you already attached a program but a {\tt Restart} or an - {\tt Undo} has removed it. - \end{ErrMsgs} -\end{Variants} - -\asubsection{Hints for {\tt Program}} - -\begin{description} -\item[Mutual inductive types] The \verb=Program= tactic can deal with - mutual inductive types. But, this needs the use of - annotations. Indeed, when associating a mutual fixpoint program to a - specification, the specification is associated to the first (the - outermost) function defined by the fixpoint. But, the specifications - to be associated to the other functions cannot be automatically - derived. They have to be explicitly given by the user as - annotations. See section \ref{program-ex-mutual} for an example. - -\item[Constants] The \verb=Program= tactic is very sensitive to the - status of constants. Constants can be either opaque (their body - cannot be viewed) or transparent. The best of way of doing is to - leave constants opaque (this is the default). If it is needed after, - it is best to use the \verb=Transparent= command {\bf after} having - used the \verb=Program= tactic. -\end{description} - -\asection{Syntax for programs} -\label{program-syntax} -\asubsection{Pure programs} -The language to express programs is called \real\footnote{It - corresponds to \FW\ plus inductive definitions}. Programs are -explicitly typed\footnote{This information is not strictly needed but - was useful for type checking in a first experiment.} like terms -extracted from proofs. Some extra expressions have been added to have -a simpler syntax. - -This is the raw form of what we call pure programs. But, in fact, it -appeared that this simple type of programs is not sufficient. Indeed, -all the logical part useful for the proof is not contained in these -programs. That is why annotated programs are introduced. - -\asubsection{Annotated programs} -The notion of annotation introduces in a program a logical assertion -that will be used for the proof. The aim of the \verb=Program= tactic -is to start from a specification and a program and to generate -subgoals either logical or associated with programs. However, to find -the good specification for subprograms is not at all trivial in -general. For instance, if we have to find an invariant for a loop, or -a well founded order in a recursive call. - -So, annotations add in a program the logical part which is needed for -the proof and which cannot be automatically retrieved. This allows the -system to do proofs it could not do otherwise. - -For this, a particular syntax is needed which is the following: since -they are specifications, annotations follow the same internal syntax -as \Coq~terms. We indicate they are annotations by putting them -between \verb={= and \verb=}= and preceding them with \verb=:: ::=. -Since annotations are \Coq~terms, they can involve abstractions over -logical propositions that have to be declared. Annotated-$\lambda$ -have to be written between \verb=[{= and \verb=}]=. -Annotated-$\lambda$ can be seen like usual $\lambda$-bindings but -concerning just annotations and not \Coq~programs. - -\asubsection{Recursive Programs} -Programs can be recursively defined using the following syntax: \verb=<={\it - type-of-the-result}\verb=> rec= \index{rec@{\tt rec}} {\it - name-of-the-induction-hypothesis} \verb=:: :: {= {\it - well-founded-order-of-the-recursion} \verb=}= and then the body of -the program (see section \ref{program-examples}) which must always begin with -an abstraction [x:A] where A is the type of the arguments of the -function (also on which the ordering relation acts). - -\asubsection{Implicit arguments} - -A synthesis of implicit arguments has been added in order to -allow the user to write a minimum of types in a program. Then, it is -possible not to write a type inside a program term. This type has then -to be automatically synthesized. For this, it is necessary to indicate -where the implicit type to be synthesized appears. The syntax is the -current one of implicit arguments in \Coq: the question mark -\verb+?+. - -This synthesis of implicit arguments is not possible everywhere in a -program. In fact, the synthesis is only available inside a -\verb+Match+, a \verb+Cases+ or a \verb+Fix+ construction (where -\verb+Fix+ is a syntax for defining fixpoints). - -\asubsection{Grammar} -The grammar for programs is described in figure \ref{pgm-syntax}. - -\begin{figure} -\begin{tabular}{lcl} -{\pg} & ::= & {\ident}\\ - & $|$ & {\tt ?} \\ - & $|$ & {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\ - & $|$ & {\tt [} {\ident} {\tt ]} {\pg} \\ - & $|$ & {\tt (} {\ident} {\tt :} {\pg} {\tt )} {\pg} \\ - & $|$ & {\tt (} {\pgs} {\tt )} \\ - & $|$ & {\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt Match} {\pg} {\tt with} {\pgs} {\tt end} \\ - & $|$ & {\tt Cases} {\pg} {\tt of} \sequence{\eqn} {|} {\tt end} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt Cases} {\pg} {\tt of} - \sequence{\eqn} {|} {\tt end} \\ - & $|$ & {\tt Fix} {\ident} \verb.{.\nelist{\fixpg}{with} \verb.}. \\ - & $|$ & {\tt Cofix} {\ident} \{{\ident} {\tt :} {\pg} {\tt :=} {\pg} - {\tt with} {\ldots} {\tt with} {\ident} {\tt :} {\pg} {\tt :=} {\pg}\} \\ - & $|$ & {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\ - & $|$ & {\tt [\{} {\ident} {\tt :} {\term} {\tt \}]} {\pg} \\ - & $|$ & {\tt let} - {\tt (} {\ident} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt ,} {\dots} - {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt in} {\pg} \\ -% & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,} {\ldots} {\tt -% ,} {\ident} {\tt :} {\pg} {\tt ;} {\ldots} {\tt ;} {\ident} {\tt ,} -% {\ldots} {\tt ,} {\ident} {\tt :} {\pg} {\tt )} {\tt =} {\pg} {\tt -% in} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt let} {\tt (} {\ident} {\tt ,} - {\ldots} {\tt ,} {\ldots} {\tt ,} {\ident} {\tt )} {\tt =} {\pg} {\tt - in} {\pg} \\ - & $|$ & {\tt if} {\pg} {\tt then} {\pg} {\tt else} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt if} {\pg} {\tt then} {\pg} {\tt - else} {\pg} \\ - & $|$ & \verb=<={\pg}\verb=>={\tt rec} {\ident} {\tt ::} {\tt ::} \{ \term \} - {\tt [} {\ident} {\tt :} {\pg} {\tt ]} {\pg} \\ - {\pgs} & ::= & \pg \\ - & $|$ & {\pg} {\pgs}\\ -{\fixpg} & ::= & {\ident} {\tt [} \nelist{\typedidents}{;} {\tt ]} {\tt :} {\pg} {\tt :=} {\pg} \\ - & $|$ & {\ident} {\tt /} {\num} {\tt :} {\pg} {\tt :=} {\pg} {\tt ::} {\tt ::} \{ {\term} \} \\ -{\simplepattern} & ::= & {\ident} \\ - & $|$ & \verb!(! \nelist{\ident}{} \verb!)! \\ -{\eqn} & ::= & {\simplepattern} ~\verb!=>! ~\pg \\ -\end{tabular} -\caption{Syntax of annotated programs} -\label{pgm-syntax} -\end{figure} - -As for {\Coq} terms (see section \ref{term}), {\tt (}{\pgs}{\tt )} -associates to the left. The syntax of {\term} is the one in section. -The infix annotation operator \verb!:: ::! binds more than the -abstraction and product constructions. -\ref{term}. - -The reference to an identifier of the \Coq\ context (in particular a -constant) inside a program of the -language \real\ is a reference to its extracted contents. - -\asection{Examples} -\label{program-examples} -\asubsection{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: - -\begin{eqnarray*} -ack(0,n) & = & n+1 \\ -ack(n+1,0) & = & ack(n,1) \\ -ack(n+1,m+1) & = & ack(n,ack(n+1,m)) -\end{eqnarray*} - -An ML program following this specification can be: - -\begin{verbatim} -let rec ack = function - 0 -> (function m -> Sm) - | Sn -> (function 0 -> ack n 1 - | Sm -> ack n (ack Sn m)) -\end{verbatim} - -Suppose we give the following definition in \Coq~of a ternary relation -\verb=(Ack n m p)= in a Prolog like form representing $p=ack(n,m)$: - -\begin{coq_example*} -Inductive Ack : nat->nat->nat->Prop := - AckO : (n:nat)(Ack O n (S n)) - | AcknO : (n,p:nat)(Ack n (S O) p)->(Ack (S n) O p) - | AckSS : (n,m,p,q:nat)(Ack (S n) m q)->(Ack n q p) - ->(Ack (S n) (S m) p). -\end{coq_example*} -Then the goal is to prove that $\forall n,m .\exists p.(Ack~n~m~p)$, so -the specification is: - -\verb!(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: -\begin{coq_example*} -Fixpoint ack_func [n:nat] : nat -> nat := - Cases n of - O => [m:nat](S m) - | (S n') => Fix ack_func2 {ack_func2 [m:nat] : nat := - Cases m of - O => (ack_func n' (S O)) - | (S m') => (ack_func n' (ack_func2 m')) - end} - end. -\end{coq_example*} -The program is associated by using \verb=Realizer ack_func=. The -program is automatically expanded. Each realizer which is a constant -is automatically expanded. Then, by repeating the \verb=Program= -tactic, three logical lemmas are generated and are easily solved by -using the property Ack0, Ackn0 and AckSS. -\begin{coq_eval} -Goal (n,m:nat){p:nat|(Ack n m p)}. -Realizer ack_func. -\end{coq_eval} -\begin{coq_example} -Repeat Program. -\end{coq_example} - - -\asubsection{Euclidean Division} -This example shows the use of {\bf 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: -\begin{verbatim} -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) -\end{verbatim} -Suppose we give the following definition in \Coq~which describes what -has to be proved, ie, $\exists q \exists r.~(a=b*q+r \wedge ~b>r)$: -\begin{coq_eval} -Abort. -Require Arith. -\end{coq_eval} -\begin{coq_example*} -Inductive diveucl [a,b:nat] : Set - := divex : (q,r:nat)(a=(plus (mult q b) r))->(gt b r) - ->(diveucl a b). -\end{coq_example*} -The decidability of the ordering relation has to be proved first, by -giving the associated function of type \verb!nat->nat->bool!: -\begin{coq_example*} -Theorem le_gt_dec : (n,m:nat){(le n m)}+{(gt n m)}. -Realizer Fix le_gt_bool {le_gt_bool [n:nat] : nat -> bool := - Cases n of - | O => [m:nat]true - | (S n') => [m:nat]Cases m of - | O => false - | (S m') => (le_gt_bool n' m') - end - end}. -Program_all. -Save. -\end{coq_example*} -Then the specification is \verb!(b:nat)(gt b O)->(a:nat)(diveucl a b)!. -The associated program corresponding to the ML program will be: -\begin{coq_eval} -Definition lt := [n,m:nat](gt m n). -Theorem eucl_dev : (b:nat)(gt b O)->(a:nat)(diveucl a b). -\end{coq_eval} -\begin{coq_example*} -Realizer - [b:nat](<nat*nat>rec div :: :: { lt } - [a:nat]if (le_gt_dec b a) - then let (q,r) = (div (minus a b)) - in ((S q),r) - else (O,a)). -\end{coq_example*} -Where \verb=lt= is the well-founded ordering relation defined by: -\begin{coq_example} -Print lt. -\end{coq_example} -Note the syntax for recursive programs as explained before. The -\verb=rec= construction needs 4 arguments: the type result of the -function (\verb=nat*nat= because it returns two natural numbers) -between \verb=<= and \verb=>=, the name of the induction hypothesis -(which can be used for recursive calls), the ordering relation -\verb=lt= (as an annotation because it is a specification), and the -program itself which must begin with a $\lambda$-abstraction. The -specification of \verb=le_gt_dec= is known because it is a previous -lemma. -The term \verb!(le_gt_dec b a)! is seen by the \verb!Program! tactic -as a term of type \verb!bool! which satisfies the specification -\verb!{(le a b)}+{(gt a b)}!. -The tactics \verb=Program_all= or \verb=Program= can be used, and the -following logical lemmas are obtained: -\begin{coq_example} -Repeat Program. -\end{coq_example} -The subgoals 4, 5 and 6 are resolved by \verb=Auto= (if you use -\verb=Program_all= they don't appear, because \verb=Program_all= tries -to apply \verb=Auto=). The other ones have to be solved by the user. - - -\asubsection{Insertion sort} -This example shows the use of {\bf 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: -\begin{verbatim} -let sort a l = sortrec l where rec sortrec = function - [] -> [a] - | b::l' -> if a<b then a::b::l' else b::(sortrec l') -\end{verbatim} -Suppose we give the following definitions in \Coq: - -First, the decidability of the ordering relation: -\begin{coq_eval} -Reset Initial. -Require Le. -Require Gt. -\end{coq_eval} -\begin{coq_example*} -Fixpoint inf_dec [n:nat] : nat -> bool := -[m:nat]Cases n of - O => true - | (S n') => Cases m of - O => false - | (S m') => (inf_dec n' m') - end - end. -\end{coq_example*} - -The definition of the type \verb=list=: -\begin{coq_example*} -Inductive list : Set := nil : list | cons : nat -> list -> list. -\end{coq_example*} - -We define the property for an element \verb=x= to be {\bf in} a list -\verb=l= as the smallest relation such that: $\forall a \forall -l~(In~x~l) \Ra (In~x~(a::l))$ and $\forall l~(In~x~(x::l))$. -\begin{coq_example*} -Inductive In [x:nat] : list->Prop - := Inl : (a:nat)(l:list)(In x l) -> (In x (cons a l)) - | Ineq : (l:list)(In x (cons x l)). -\end{coq_example*} - -A list \verb=t'= is equivalent to a list \verb=t= with one added -element \verb=y= iff: $(\forall x~(In~x~t) \Ra (In~x~t'))$ and -$(In~y~t')$ and $\forall x~(In~x~t') \Ra ((In~x~t) \vee y=x)$. The -following definition implements this ternary conjunction. -\begin{coq_example*} -Inductive equiv [y:nat;t,t':list]: Prop := - equiv_cons : - ((x:nat)(In x t)->(In x t')) - -> (In y t') - ->((x:nat)(In x t')->((In x t)\/y=x)) - -> (equiv y t t'). -\end{coq_example*} - -Definition of the property of list to be sorted, still defined -inductively: -\begin{coq_example*} -Inductive sorted : list->Prop - := sorted_nil : (sorted nil) - | sorted_trans : (a:nat)(sorted (cons a nil)) - | sorted_cons : (a,b:nat)(l:list)(sorted (cons b l)) -> (le a b) - -> (sorted (cons a (cons b l))). -\end{coq_example*} -Then the specification is:\\ -\verb!(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: -\begin{coq_eval} -Lemma toto : (a:nat)(l:list)(sorted l)->{l':list|(equiv a l l')&(sorted l')}. -\end{coq_eval} -\begin{coq_example*} -Realizer - Fix list_insert{list_insert [a:nat; l:list] : list := - Cases l of - | nil => (cons a nil) - | (cons b m) => - if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } - then (cons b (list_insert a m)) - else (cons a (cons b m)) - end}. -\end{coq_example*} -% Realizer [a:nat][l:list] -% Match l with -% (cons a nil) -% [b,m,H]if (inf_dec b a) :: :: { {(le b a)}+{(gt b a)} } -% then (cons b H) -% else (cons a (cons b m)) -% end. -Note that we have defined \verb=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 \verb=Program_all= is used, a few logical -lemmas are obtained (which have to be solved by the user): -\begin{coq_example} -Program_all. -\end{coq_example} - - -\asubsection{Quicksort} -This example shows the use of {\bf 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: -\begin{verbatim} -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 -\end{verbatim} -Where \verb=splitting= is defined by: -\begin{verbatim} -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) -\end{verbatim} -Suppose we give the following definitions in \Coq: - -Declaration of the ordering relation: -\begin{coq_eval} -Reset Initial. -Require List. -Require Gt. -\end{coq_eval} -\begin{coq_example*} -Variable inf : A -> A -> Prop. -Definition sup := [x,y:A]~(inf x y). -Hypothesis inf_sup : (x,y:A){(inf x y)}+{(sup x y)}. -\end{coq_example*} -Definition of the concatenation of two lists: -\begin{coq_eval} -Write State toto. -\end{coq_eval} -\begin{coq_example*} -Fixpoint app [l:list] : list -> list - := [m:list]Cases l of - nil => m - | (cons a l1) => (cons a (app l1 m)) end. -\end{coq_example*} -\begin{coq_eval} -Restore State toto. -\end{coq_eval} -Definition of the permutation of two lists: -\begin{coq_eval} -Definition mil := [a:A][l,m:list](app l (cons a m)) : A->list->list->list. -Lemma mil_app : (a:A)(l,m,n:list)(mil a l (app m n))=(app (mil a l m) n). - Intros. - Unfold mil. - Elim (ass_app l (cons a m) n). - Auto. -Save. -\end{coq_eval} -\begin{coq_example*} -Inductive permut : list->list->Prop := - permut_nil : (permut nil nil) - |permut_tran : (l,m,n:list)(permut l m)->(permut m n)->(permut l n) - |permut_cmil : (a:A)(l,m,n:list) - (permut l (app m n))->(permut (cons a l) (mil a m n)) - |permut_milc : (a:A)(l,m,n:list) - (permut (app m n) l)->(permut (mil a m n) (cons a l)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve permut_nil permut_cmil permut_milc. -Lemma permut_cons : (a:A)(l,m:list)(permut l m)->(permut (cons a l) (cons a m)). - Intros. - Change (permut (cons a l) (mil a nil m)). - Auto. -Save. -Hints Resolve permut_cons. -Lemma permut_refl : (l:list)(permut l l). - Induction l ; Auto. -Save. -Hints Resolve permut_refl. -Lemma permut_sym : (l,m:list)(permut l m)->(permut m l). - Intros l m h1 ; Elim h1 ; Auto. - Intros l0 m0 n h2 h3 h4 h5. - Apply permut_tran with m0 ; Auto. -Save. -Hints Immediate permut_sym. -Lemma permut_app1 : (m1,n1,l:list)(permut m1 n1)->(permut (app l m1) (app l n1)). - Intros ; Elim l ; Simpl ; Auto. -Save. -Hints Resolve permut_app1. -Lemma permut_app_mil : (a:A)(l1,m1,l2,m2,n2:list) - (permut (app l1 m1) (app (app l2 m2) n2)) - -> (permut (app (cons a l1) m1) (app (mil a l2 m2) n2)). - Intros ; Simpl. - Elim (mil_app a l2 m2 n2). - Apply permut_cmil. - Elim (app_ass l2 m2 n2) ; Auto. -Save. -Hints Resolve permut_app_mil. -Lemma permut_app_app : (m1,m2,n1,n2 :list) - (permut m1 n1)->(permut m2 n2)->(permut (app m1 m2) (app n1 n2)). - Intros m1 m2 n1 n2 h1 h2. - Elim h1 ; Intros. - exact h2. - Apply permut_tran with (app m n2) ; Auto. - Apply permut_tran with (app m m2) ; Auto. - Auto. - Apply permut_sym ; Auto. -Save. -Hints Resolve permut_app_app. -Lemma permut_app : (m,m1,m2,n1,n2 :list)(permut m1 n1)->(permut m2 n2)-> - (permut m (app m1 m2))->(permut m (app n1 n2)). - Intros. - Apply permut_tran with (app m1 m2) ; Auto. -Save. -\end{coq_eval} -The definitions \verb=inf_list= and \verb=sup_list= allow to know if -an element is lower or greater than all the elements of a list: -\begin{coq_example*} -Section Rlist_. -Variable R : A->Prop. -Inductive Rlist : list -> Prop := - Rnil : (Rlist nil) - | Rcons : (x:A)(l:list)(R x)->(Rlist l)->(Rlist (cons x l)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve Rnil Rcons. -Lemma Rlist_app : (m,n:list)(Rlist m)->(Rlist n)->(Rlist (app m n)). - Intros m n h1 h2 ; Elim h1 ; Simpl ; Auto. -Save. -Hints Resolve Rlist_app. -Section Rlist_cons_. -Variable a : A. -Variable l : list. -Hypothesis Rc : (Rlist (cons a l)). -Lemma Rlist_cons : (R a)/\(Rlist l). - Inversion_clear Rc; Auto. -Save. -End Rlist_cons_. -Section Rlist_append. -Variable n,m : list. -Lemma Rlist_appd : (Rlist (app n m))->((Rlist n)/\(Rlist m)). -Elim n ; Simpl; Auto. -Intros a y h1 h2. -Elim (Rlist_cons a (app y m)) ; Auto. -Intros h3 h4; Elim h1 ; Auto. -Save. -End Rlist_append. -Hints Resolve Rlist_appd. -Lemma Rpermut : (m,n:list)(permut m n)->(Rlist m)->(Rlist n). - Intros m n h1 ; Elim h1 ; Unfold mil ; Auto. - Intros a l m0 n0 h2 h3 h4. - Elim (Rlist_cons a l); Auto. - Intros h5 h6; Elim (Rlist_appd m0 n0); Auto. - Intros a l m0 n0 h2 h3 h4. - Elim (Rlist_appd m0 (cons a n0)) ; Auto. - Intros h5 h6; Elim (Rlist_cons a n0) ; Auto. -Save. -\end{coq_eval} -\begin{coq_example*} -End Rlist_. -Hints Resolve Rnil Rcons. -\end{coq_example*} -\begin{coq_eval} -Hints Resolve Rlist_app. -\end{coq_eval} -\begin{coq_example*} -Section Inf_Sup. -Hypothesis x : A. -Hypothesis l : list. -Definition inf_list := (Rlist (inf x) l). -Definition sup_list := (Rlist (sup x) l). -End Inf_Sup. -\end{coq_example*} -\begin{coq_eval} -Hints Unfold inf_list sup_list. -\end{coq_eval} -Definition of the property of a list to be sorted: -\begin{coq_example*} -Inductive sort : list->Prop := - sort_nil : (sort nil) - | sort_mil : (a:A)(l,m:list)(sup_list a l)->(inf_list a m) - ->(sort l)->(sort m)->(sort (mil a l m)). -\end{coq_example*} -\begin{coq_eval} -Hints Resolve sort_nil sort_mil. -Lemma permutapp : (a0:A)(y,l1,l2:list)(permut y (app l1 l2))->(permut (cons a0 y) (app l1 (cons a0 l2))). -Intros. -exact (permut_cmil a0 y l1 l2 H). -Save. -Hints Resolve permutapp. -Lemma sortmil : (a:A)(x,x0,l1,l2:list)(sup_list a l1)->(inf_list a l2)->(sort x)->(sort x0)->(permut l1 x)->(permut l2 x0)->(sort (mil a x x0)). -Intros. -Apply sort_mil ; Auto. -Unfold sup_list ; Apply Rpermut with l1 ; Auto. -Unfold inf_list ; Apply Rpermut with l2 ; Auto. -Save. -\end{coq_eval} - -\noindent Then the goal to prove is -$\forall l~\exists m~(sort~m) \wedge (permut~l~m)$ and the specification is - -\verb!(l:list){m:list|(sort m)&(permut l m)!. - -\noindent Let us first prove a preliminary lemma. Let us define \verb=ltl= a -well-founded ordering relation. - -\begin{coq_example*} -Definition ltl := [l,m:list](gt (length m) (length l)). -\end{coq_example*} -\begin{coq_eval} -Hints Unfold ltl. -Lemma ltl_cons : (a,a0:A)(l1,y:list)(ltl l1 (cons a y))->(ltl l1 (cons a (cons a0 y))). -Unfold ltl; Simpl; Auto. -Save. -Hints Resolve ltl_cons. -Lemma ltl_cons_cons : (a,a0:A)(l2,y:list)(ltl l2 (cons a y))->(ltl (cons a0 l2) (cons a (cons a0 y))). -Unfold ltl; Simpl; Auto with arith.. -Save. -Hints Resolve ltl_cons_cons. -Require Wf_nat. -\end{coq_eval} -Let us then give a definition of \verb=Splitting_spec= corresponding -to\\ -$\exists l_1 \exists l_2.~(sup\_list~a~l_1) \wedge (inf\_list~a~l_2) -\wedge (l \equiv l_1@l_2) \wedge (ltl~l_1~(a::l)) \wedge -(ltl~l2~(a::l))$ and a theorem on this definition. -\begin{coq_example*} -Inductive Splitting_spec [a:A; l:list] : Set := - Split_intro : (l1,l2:list)(sup_list a l1)->(inf_list a l2) - ->(permut l (app l1 l2)) - ->(ltl l1 (cons a l))->(ltl l2 (cons a l)) - ->(Splitting_spec a l). -\end{coq_example*} -\begin{coq_example*} -Theorem Splitting : (a:A)(l:list)(Splitting_spec a l). -Realizer - Fix split {split [a:A;l:list] : list*list := - Cases l of - | nil => (nil,nil) - | (cons b m) => let (l1,l2) = (split a m) in - if (inf_sup a b) - then (* inf a b *) (l1,(cons b l2)) - else (* sup a b *) ((cons b l1),l2) - end}. -Program_all. -Simpl; Auto. -Save. -\end{coq_example*} -% Realizer [a:A][l:list] -% Match l with -% (* nil *) (nil,nil) -% (* cons *) [b,m,ll]let (l1,l2) = ll in -% if (inf_sup a b) -% then (* inf a b *) (l1,(cons b l2)) -% else (* sup a b *) ((cons b l1),l2) -% end. - -The associated {\real} program to the specification we wanted to first -prove and corresponding to the ML program will be: -\begin{coq_example*} -Lemma Quicksort: (l:list){m:list|(sort m)&(permut l m)}. -Realizer <list>rec quick :: :: { ltl } - [l:list]Cases l of - nil => nil - | (cons a m) => let (l1,l2) = (Splitting a m) in - (mil a (quick l1) (quick l2)) - end. -\end{coq_example*} -Then \verb=Program_all= gives the following logical lemmas (they have -to be resolved by the user): -\begin{coq_example} -Program_all. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\asubsection{Mutual Inductive Types} -\label{program-ex-mutual} -This example shows the use of {\bf mutual inductive types} with -\verb=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. - -\begin{coq_example*} -Section TreeForest. - -Variable A : Set. - -Mutual Inductive - tree : Set := node : A -> forest -> tree -with forest : Set := empty : forest - | cons : tree -> forest -> forest. - -Mutual Inductive Tree_Size : tree -> nat -> Prop := - Node_Size : (n:nat)(a:A)(f:forest)(Forest_Size f n) - ->(Tree_Size (node a f) (S n)) -with Forest_Size : forest -> nat -> Prop := - Empty_Size : (Forest_Size empty O) -| Cons_Size : (n,m:nat)(t:tree)(f:forest) - (Tree_Size t n) - ->(Forest_Size f m) - ->(Forest_Size (cons t f) (plus n m)). - -Hints Resolve Node_Size Empty_Size Cons_Size. -\end{coq_example*} - -Then, let us associate the two mutually dependent functions to compute -the size of a forest and a tree to the the following specification: - -\begin{coq_example*} -Theorem tree_size_prog : (t:tree){n:nat | (Tree_Size t n)}. - -Realizer [t:tree] -(Fix tree_size{ - tree_size [t:tree] : nat := let (a,f) = t in (S (forest_size f)) - 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). -\end{coq_example*} - -It is necessary to add an annotation for the \verb=forest_size= -function. Indeed, the global specification corresponds to the -specification of the \verb=tree_size= function and the specification -of \verb=forest_size= cannot be automatically inferred from the -initial one. - -Then, the \verb=Program_all= tactic can be applied: -\begin{coq_example} -Program_all. -Save. -\end{coq_example} - -% $Id$ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |