\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}