\documentclass[11pt,a4paper,landscape]{article}

\textwidth=27cm   \textheight=18cm
\hoffset=-7.5cm   \voffset=-3cm

\special{papersize=297mm,210mm}


\begin{document}
\thispagestyle{empty}
\LARGE


Una nota sobre la t\'actica \verb"Auto":

\begin{flushleft}
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Lemma~uno:(A,A1:Prop)~}\\
\texttt{Coq~{<}~~~~~~~(((((((((((A1-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A1-{>}A.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(A,A1:Prop)}\\
\texttt{~~~~(((((((((((A1-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A1-{>}A}\\
\medskip
\texttt{Coq~{<}~Auto.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(A,A1:Prop)}\\
\texttt{~~~~(((((((((((A1-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A)-{>}A1-{>}A}\\
\medskip
\texttt{Coq~{<}~Auto~8.}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Save.}\\
\texttt{Auto.}\\
\texttt{Auto~8~with~.}\\
\texttt{uno~is~defined}\\
\end{flushleft}

Las proyecciones del tipo existencial \verb"sig" en \verb"Set":

\begin{flushleft}
\texttt{Coq~{<}~(*}\\
\texttt{Coq~{<}~pro1~=~}\\
\texttt{Coq~{<}~[A:Set;~P:(A-{>}Prop);~H:(\{x:A~|~(P~x)\})](let~(x,~\_)~=~H~in~x)}\\
\texttt{Coq~{<}~~~~~~:~(A:Set;~P:(A-{>}Prop))\{x:A~|~(P~x)\}-{>}A}\\
\texttt{Coq~{<}~pro2~=~}\\
\texttt{Coq~{<}~[A:Set;~P:(A-{>}Prop);~H:(\{x:A~|~(P~x)\})]}\\
\texttt{Coq~{<}~~({<}[H0:(\{x:A~|~(P~x)\})](P~(pro1~A~P~H0)){>}let~(\_,~pr)~=~H~in~pr)}\\
\texttt{Coq~{<}~~~~~~:~(A:Set;~P:(A-{>}Prop);~H:(\{x:A~|~(P~x)\}))(P~(pro1~A~P~H))}\\
\texttt{Coq~{<}~*)}\\
\end{flushleft}

Especificaci\'on, implementaci\'on y prueba:

\begin{flushleft}
\texttt{Coq~{<}~Inductive~factorial:nat-{>}nat-{>}Prop:=}\\
\texttt{Coq~{<}~~~~fac0:(factorial~O~(S~O))}\\
\texttt{Coq~{<}~~|~facS:(n,p:nat)(factorial~n~p)-{>}(factorial~(S~n)~(mult~(S~n)~p)).}\\
\texttt{Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~Coq~{<}~factorial~is~defined}\\
\texttt{factorial\_ind~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Theorem~fact:(n:nat)\{p:nat~|~(factorial~n~p)\}.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(n:nat)\{p:nat~|~(factorial~n~p)\}}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Induction~n;}\\
\texttt{Coq~{<}~[~Split~with~(S~O);~Constructor~1}\\
\texttt{Coq~{<}~|~Intros~n0~rec;~Case~rec;~Intros~p~q~].}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~rec~:~\{p:nat~|~(factorial~n0~p)\}}\\
\texttt{~~p~:~nat}\\
\texttt{~~q~:~(factorial~n0~p)}\\
\texttt{~~============================}\\
\texttt{~~~\{p0:nat~|~(factorial~(S~n0)~p0)\}}\\
\medskip
\texttt{Coq~{<}~Split~with~(mult~(S~n0)~p);~Constructor~2;~Auto.}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Defined.}\\
\texttt{Induction~n;}\\
\texttt{[~Split~with~(S~O);~Constructor~1}\\
\texttt{|~Intros~n0~rec;~Case~rec;~Intros~p~q~].}\\
\texttt{Split~with~(mult~(S~n0)~p);~Constructor~2;~Auto.}\\
\texttt{fact~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Require~Export~Arith.}\\
\end{flushleft}

 Los siguientes esultados no se podrian obtener si terminamos la prueba  
con Qed o Saved en lugar de Defined.

\begin{verbatim}
 Resultados. No se podrian obtener si terminamos la prueba
               con Qed o Saved en lugar de Defined.
Coq < Eval Compute in (pro1 nat (factorial (4)) (fact (4))).
     = (24)
     : nat
Coq < Eval Compute in (pro2 nat (factorial (4)) (fact (4))).
     = (facS (3) (6) (facS (2) (2) (facS (1) (1) (facS (0) (1) fac0))))
     : (factorial (4) (pro1 nat (factorial (4)) (fact (4))))

Coq < Eval Simpl in (factorial (4) (pro1 nat (factorial (4)) (fact (4)))).
     = (factorial (4) (24))
     : Prop
\end{verbatim}


\section{Extracci\'on}

En la version 6.3 que usais teneis que hacer
\begin{verbatim}
Require Extraction.
Write Caml File "factorial" [fact].
\end{verbatim}

Esto produce el fichero \verb"factorial.ml" compilable en Caml:
\begin{verbatim}	
type nat =
    O
  | S of nat;;

                  type 'A sig = 'A;; OMITIR

let rec plus n m =
  match n with
    O -> m
  | S p -> S (plus p m);;

let rec mult n m =
  match n with
    O -> O
  | S p -> plus m (mult p m);;

let rec fact = function
  O -> S O
| S n0 -> mult (S n0) (fact n0);;
\end{verbatim}

Se pueden definir las funciones de traducci\'on del tipo para hacer c\'alculos
en Caml:

\begin{verbatim}
 let rec natint = function
    O -> 0
  |S x -> (natint x)+1;;

 let rec intnat = function
   0 -> O
  |x -> (S (intnat (x-1)));;
\end{verbatim}

Estas versiones no {\em tail--recursivas} pueden cambiarse, como sigue,
para obtener versiones que lo sean:
\begin{verbatim}
let newnatind n = let rec auxnatind (n,m)= match n with O->m 
                          |(S x) -> auxnatind (x, (m+1))
in auxnatind (n,0);;


let newfact n = let rec auxfact (n,m)= match n with 0 -> m
                          |x -> auxfact (x-1, x*m)
in auxfact (n,1);;
\end{verbatim}

Tambi\'en en {\sf Coq}:

\begin{flushleft}
\texttt{Coq~{<}~Fixpoint~tailfact~[n:nat]:nat-{>}nat~:=}\\
\texttt{Coq~{<}~~~~~[m:nat]Cases~n~of}\\
\texttt{Coq~{<}~~~~~~~~~~~~~~~O~={>}~(m)}\\
\texttt{Coq~{<}~~~~~~~~~|~(S~x)~={>}~(tailfact~x~(mult~(S~x)~m))}\\
\texttt{Coq~{<}~~~~~~~~~~~~end.}\\
\texttt{tailfact~is~recursively~defined}\\
\medskip
\texttt{Coq~{<}~Definition~fact\_tail~:=~[n:nat](tailfact~n~(S~O)).}\\
\texttt{fact\_tail~is~defined}\\
\medskip
\texttt{Coq~{<}~Definition~esq:~(P:nat*nat-{>}Set)}\\
\texttt{Coq~{<}~~~~~~~~~~~~~~~~~~~~((x:nat)(P~(O,x)))}\\
\texttt{Coq~{<}~~~~~~~~~~~~~~~~~~-{>}((x,y:nat)(P~(x,y))-{>}(P~((S~x),y)))}\\
\texttt{Coq~{<}~~~~~~~~~~~~~~~~~~~~~~~~~-{>}~(t:nat*nat)(P~t).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(P:(nat*nat-{>}Set))}\\
\texttt{~~~~((x:nat)(P~((0),x)))}\\
\texttt{~~~~-{>}((x,y:nat)(P~(x,y))-{>}(P~((S~x),y)))}\\
\texttt{~~~~-{>}(t:(nat*nat))(P~t)}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~============================}\\
\texttt{~~~(P~t)}\\
\medskip
\texttt{Coq~{<}~Case~t.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~============================}\\
\texttt{~~~(n,n0:nat)(P~(n,n0))}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(P~(n,n0))}\\
\medskip
\texttt{Coq~{<}~Elim~n.}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(P~((0),n0))}\\
\texttt{subgoal~2~is:}\\
\texttt{~(n1:nat)(P~(n1,n0))-{>}(P~((S~n1),n0))}\\
\medskip
\texttt{Coq~{<}~Apply~H.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(n1:nat)(P~(n1,n0))-{>}(P~((S~n1),n0))}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~n1~:~nat}\\
\texttt{~~H1~:~(P~(n1,n0))}\\
\texttt{~~============================}\\
\texttt{~~~(P~((S~n1),n0))}\\
\medskip
\texttt{Coq~{<}~Apply~H0.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~P~:~nat*nat-{>}Set}\\
\texttt{~~H~:~(x:nat)(P~((0),x))}\\
\texttt{~~H0~:~(x,y:nat)(P~(x,y))-{>}(P~((S~x),y))}\\
\texttt{~~t~:~nat*nat}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~n1~:~nat}\\
\texttt{~~H1~:~(P~(n1,n0))}\\
\texttt{~~============================}\\
\texttt{~~~(P~(n1,n0))}\\
\medskip
\texttt{Coq~{<}~Auto.}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Defined.}\\
\texttt{Intros.}\\
\texttt{Case~t.}\\
\texttt{Intros.}\\
\texttt{Elim~n.}\\
\texttt{Apply~H.}\\
\texttt{Intros.}\\
\texttt{Apply~H0.}\\
\texttt{Auto.}\\
\texttt{esq~is~defined}\\
\medskip
\texttt{Coq~{<}~Definition~Tailfact:nat*nat-{>}nat.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~nat*nat-{>}nat}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Apply~(esq~[\_:(nat*nat)]nat).}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~nat-{>}nat}\\
\texttt{subgoal~2~is:}\\
\texttt{~nat-{>}nat-{>}nat-{>}nat}\\
\medskip
\texttt{Coq~{<}~Exact~[x:nat]x.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~nat-{>}nat-{>}nat-{>}nat}\\
\medskip
\texttt{Coq~{<}~Exact~[x,\_:nat;~z:nat](mult~(S~x)~z).}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Defined.}\\
\texttt{Apply~(esq~[\_:(nat*nat)]nat).}\\
\texttt{Exact~[x:nat]x.}\\
\texttt{Exact~[x,\_:nat;~z:nat](mult~(S~x)~z).}\\
\texttt{Tailfact~is~defined}\\
\end{flushleft}

Por ejemplo:
\begin{verbatim}
 Eval Compute in (Tailfact ((8),(1))).
     = (40320)
     : nat
\end{verbatim}

Un ejemplo m\'as: suma de los elementos de una lista:
\begin{flushleft}
\texttt{Coq~{<}~Require~PolyList.}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Fixpoint~sumalista~[l:(list~nat)]:nat:=}\\
\texttt{Coq~{<}~~~~Cases~l~of~nil~={>}~O}\\
\texttt{Coq~{<}~~~~~~~|(cons~x~l)~={>}~(plus~x~(sumalista~l))}\\
\texttt{Coq~{<}~~~~end.}\\
\texttt{sumalista~is~recursively~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~~Fixpoint~aux\_sumalistail~[l:(list~nat)]:nat-{>}nat:=}\\
\texttt{Coq~{<}~~~[ac:nat]Cases~l~of~}\\
\texttt{Coq~{<}~~~~~~~~~~~~~~nil~={>}~ac}\\
\texttt{Coq~{<}~~~~~~|(cons~x~l)~={>}~(aux\_sumalistail~l~(plus~x~ac))}\\
\texttt{Coq~{<}~~~~~~~~~~~end.}\\
\texttt{aux\_sumalistail~is~recursively~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Print~aux\_sumalistail.}\\
\texttt{aux\_sumalistail~=~}\\
\texttt{Fix~aux\_sumalistail}\\
\texttt{~~\{aux\_sumalistail~[l:(list~nat)]~:~nat-{>}nat~:=}\\
\texttt{~~~~~[ac:nat]}\\
\texttt{~~~~~~Cases~l~of}\\
\texttt{~~~~~~~~nil~={>}~ac}\\
\texttt{~~~~~~|~(cons~x~l0)~={>}~(aux\_sumalistail~l0~(plus~x~ac))}\\
\texttt{~~~~~~end\}}\\
\texttt{~~~~~:~(list~nat)-{>}nat-{>}nat}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Lemma~aux1:(l:(list~nat);~n:nat)}\\
\texttt{Coq~{<}~~(aux\_sumalistail~l~(S~n))=(S~(aux\_sumalistail~l~n)).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(l:(list~nat);~n:nat)}\\
\texttt{~~~~(aux\_sumalistail~l~(S~n))=(S~(aux\_sumalistail~l~n))}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Induction~l;~Simpl;~Auto.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~============================}\\
\texttt{~~~(a:nat;~l0:(list~nat))}\\
\texttt{~~~~((n:nat)(aux\_sumalistail~l0~(S~n))=(S~(aux\_sumalistail~l0~n)))}\\
\texttt{~~~~-{>}(n:nat)}\\
\texttt{~~~~~~~(aux\_sumalistail~l0~(plus~a~(S~n)))}\\
\texttt{~~~~~~~~=(S~(aux\_sumalistail~l0~(plus~a~n)))}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(n:nat)(aux\_sumalistail~l0~(S~n))=(S~(aux\_sumalistail~l0~n))}\\
\texttt{~~n~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~(plus~a~(S~n)))}\\
\texttt{~~~~=(S~(aux\_sumalistail~l0~(plus~a~n)))}\\
\medskip
\texttt{Coq~{<}~Replace~(plus~a~(S~n))~with~(S~(plus~a~n)).}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(n:nat)(aux\_sumalistail~l0~(S~n))=(S~(aux\_sumalistail~l0~n))}\\
\texttt{~~n~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~(S~(plus~a~n)))}\\
\texttt{~~~~=(S~(aux\_sumalistail~l0~(plus~a~n)))}\\
\texttt{subgoal~2~is:}\\
\texttt{~(S~(plus~a~n))=(plus~a~(S~n))}\\
\medskip
\texttt{Coq~{<}~Apply~(H~(plus~a~n)).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(n:nat)(aux\_sumalistail~l0~(S~n))=(S~(aux\_sumalistail~l0~n))}\\
\texttt{~~n~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(S~(plus~a~n))=(plus~a~(S~n))}\\
\medskip
\texttt{Coq~{<}~Auto~with~*.}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Qed.}\\
\texttt{Induction~l;~Simpl;~Auto.}\\
\texttt{Intros.}\\
\texttt{Replace~(plus~a~(S~n))~with~(S~(plus~a~n)).}\\
\texttt{Apply~(H~(plus~a~n)).}\\
\texttt{Auto~with~"*".}\\
\texttt{aux1~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Lemma~aux:(l:(list~nat);~n,m:nat)}\\
\texttt{Coq~{<}~~~~~~~~~(aux\_sumalistail~l~(plus~n~m))=(plus~n~(aux\_sumalistail~l~m)).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(l:(list~nat);~n,m:nat)}\\
\texttt{~~~~(aux\_sumalistail~l~(plus~n~m))=(plus~n~(aux\_sumalistail~l~m))}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Induction~n;~Simpl;~Auto.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~n~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(n0:nat)}\\
\texttt{~~~~((m:nat)}\\
\texttt{~~~~~~(aux\_sumalistail~l~(plus~n0~m))=(plus~n0~(aux\_sumalistail~l~m)))}\\
\texttt{~~~~-{>}(m:nat)}\\
\texttt{~~~~~~~(aux\_sumalistail~l~(S~(plus~n0~m)))}\\
\texttt{~~~~~~~~=(S~(plus~n0~(aux\_sumalistail~l~m)))}\\
\medskip
\texttt{Coq~{<}~Intros~n0~H.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~H~:~(m:nat)}\\
\texttt{~~~~~~~(aux\_sumalistail~l~(plus~n0~m))=(plus~n0~(aux\_sumalistail~l~m))}\\
\texttt{~~============================}\\
\texttt{~~~(m:nat)}\\
\texttt{~~~~(aux\_sumalistail~l~(S~(plus~n0~m)))}\\
\texttt{~~~~~=(S~(plus~n0~(aux\_sumalistail~l~m)))}\\
\medskip
\texttt{Coq~{<}~Intro~m.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~H~:~(m:nat)}\\
\texttt{~~~~~~~(aux\_sumalistail~l~(plus~n0~m))=(plus~n0~(aux\_sumalistail~l~m))}\\
\texttt{~~m~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l~(S~(plus~n0~m)))}\\
\texttt{~~~~=(S~(plus~n0~(aux\_sumalistail~l~m)))}\\
\medskip
\texttt{Coq~{<}~Rewrite~{<}-~(H~m).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~n~:~nat}\\
\texttt{~~n0~:~nat}\\
\texttt{~~H~:~(m:nat)}\\
\texttt{~~~~~~~(aux\_sumalistail~l~(plus~n0~m))=(plus~n0~(aux\_sumalistail~l~m))}\\
\texttt{~~m~:~nat}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l~(S~(plus~n0~m)))}\\
\texttt{~~~~=(S~(aux\_sumalistail~l~(plus~n0~m)))}\\
\medskip
\texttt{Coq~{<}~Apply~aux1.}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Qed.}\\
\texttt{Induction~n;~Simpl;~Auto.}\\
\texttt{Intros~n0~H.}\\
\texttt{Intro~m.}\\
\texttt{Rewrite~{<}-~(H~m).}\\
\texttt{Apply~aux1.}\\
\texttt{aux~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Definition~nsumalista~:=~[l:(list~nat)]let~f=(}\\
\texttt{Coq~{<}~Fix~aux\_sumalistail}\\
\texttt{Coq~{<}~~~\{aux\_sumalistail~[l:(list~nat)]~:~nat-{>}nat~:=}\\
\texttt{Coq~{<}~~~~~~[ac:nat]}\\
\texttt{Coq~{<}~~~~~~~Cases~l~of}\\
\texttt{Coq~{<}~~~~~~~~~nil~={>}~ac}\\
\texttt{Coq~{<}~~~~~~~|~(cons~x~l0)~={>}~(aux\_sumalistail~l0~(plus~x~ac))}\\
\texttt{Coq~{<}~~~~~~~end\}~)~in~(aux\_sumalistail~l~O).}\\
\texttt{nsumalista~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Print~nsumalista.}\\
\texttt{nsumalista~=~}\\
\texttt{[l:(list~nat)]}\\
\texttt{~[f:=Fix~aux\_sumalistail}\\
\texttt{~~~~~~~\{aux\_sumalistail~[l:(list~nat)]~:~nat-{>}nat~:=}\\
\texttt{~~~~~~~~~~[ac:nat]}\\
\texttt{~~~~~~~~~~~Cases~l~of}\\
\texttt{~~~~~~~~~~~~~nil~={>}~ac}\\
\texttt{~~~~~~~~~~~|~(cons~x~l0)~={>}~(aux\_sumalistail~l0~(plus~x~ac))}\\
\texttt{~~~~~~~~~~~end\}](aux\_sumalistail~l~(0))}\\
\texttt{~~~~~:~(list~nat)-{>}nat}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Lemma~verif~:~(l:(list~nat))(nsumalista~l)=(sumalista~l).}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~============================}\\
\texttt{~~~(l:(list~nat))(nsumalista~l)=(sumalista~l)}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Induction~l;~Simpl;~Auto.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~============================}\\
\texttt{~~~(a:nat;~l0:(list~nat))}\\
\texttt{~~~~(nsumalista~l0)=(sumalista~l0)}\\
\texttt{~~~~-{>}(nsumalista~(cons~a~l0))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(nsumalista~l0)=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(nsumalista~(cons~a~l0))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Simpl.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(nsumalista~l0)=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(nsumalista~(cons~a~l0))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Unfold~nsumalista.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(nsumalista~l0)=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~(cons~a~l0)~(0))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Simpl.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(nsumalista~l0)=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~(plus~a~(0)))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Unfold~nsumalista~in~H.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~(plus~a~(0)))=(plus~a~(sumalista~l0))}\\
\medskip
\texttt{Coq~{<}~Replace~(plus~a~(0))~with~a.}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~a)=(plus~a~(sumalista~l0))}\\
\texttt{subgoal~2~is:}\\
\texttt{~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Rewrite~{<}-~H.}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~a)=(plus~a~(aux\_sumalistail~l0~(0)))}\\
\texttt{subgoal~2~is:}\\
\texttt{~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Rewrite~{<}-~(aux~l0~a~O).}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~a)=(aux\_sumalistail~l0~(plus~a~(0)))}\\
\texttt{subgoal~2~is:}\\
\texttt{~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Replace~(plus~a~O)~with~a.}\\
\texttt{3~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~(aux\_sumalistail~l0~a)=(aux\_sumalistail~l0~a)}\\
\texttt{subgoal~2~is:}\\
\texttt{~a=(plus~a~(0))}\\
\texttt{subgoal~3~is:}\\
\texttt{~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Auto~with~*.}\\
\texttt{2~subgoals}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~a=(plus~a~(0))}\\
\texttt{subgoal~2~is:}\\
\texttt{~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Auto~with~*.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~l~:~(list~nat)}\\
\texttt{~~a~:~nat}\\
\texttt{~~l0~:~(list~nat)}\\
\texttt{~~H~:~(aux\_sumalistail~l0~(0))=(sumalista~l0)}\\
\texttt{~~============================}\\
\texttt{~~~a=(plus~a~(0))}\\
\medskip
\texttt{Coq~{<}~Qed.}\\
\texttt{Induction~l;~Simpl;~Auto.}\\
\texttt{Intros.}\\
\texttt{Simpl.}\\
\texttt{Unfold~nsumalista.}\\
\texttt{Simpl.}\\
\texttt{Unfold~nsumalista~in~H.}\\
\texttt{Replace~(plus~a~(0))~with~a.}\\
\texttt{Rewrite~{<}-~H.}\\
\texttt{Rewrite~{<}-~(aux~l0~a~O).}\\
\texttt{Replace~(plus~a~O)~with~a.}\\
\texttt{Auto~with~"*".}\\
\texttt{Auto~with~"*".}\\
\texttt{{<}Your~Tactic~Text~here{>}}\\
\texttt{Error:~Attempt~to~save~an~incomplete~proof}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Recursive~Extraction~nsumalista.}\\
\texttt{type~'A~list~=}\\
\texttt{~~~~nil}\\
\texttt{~~|~cons~of~'A~*~'A~list}\\
\texttt{type~nat~=}\\
\texttt{~~~~O}\\
\texttt{~~|~S~of~nat}\\
\texttt{let~rec~plus~n~m~=}\\
\texttt{~~match~n~with}\\
\texttt{~~~~O~-{>}~m}\\
\texttt{~~|~S~p~-{>}~S~(plus~p~m)}\\
\texttt{let~rec~aux\_sumalistail~l~ac~=}\\
\texttt{~~match~l~with}\\
\texttt{~~~~nil~-{>}~ac}\\
\texttt{~~|~cons~(x,~l0)~-{>}~aux\_sumalistail~l0~(plus~x~ac)}\\
\texttt{let~nsumalista~l~=}\\
\texttt{~~aux\_sumalistail~l~O}\\
\medskip
\texttt{Coq~{<}~}\\
\end{flushleft}

\end{document}




