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

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

\special{papersize=297mm,210mm}


\begin{document}
\thispagestyle{empty}


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

\begin{coq_example}

Lemma uno:(A,A1:Prop) 
      (((((((((((A1->A)->A)->A)->A)->A)->A)->A)->A)->A)->A)->A)->A1->A.
Auto.
Auto 8.
Save.
\end{coq_example}

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

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

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

\begin{coq_example}
Inductive factorial:nat->nat->Prop:=
   fac0:(factorial O (S O))
 | facS:(n,p:nat)(factorial n p)->(factorial (S n) (mult (S n) p)).

Theorem fact:(n:nat){p:nat | (factorial n p)}.
Proof.
Induction n;
[ Split with (S O); Constructor 1
| Intros n0 rec; Case rec; Intros p q ].
Split with (mult (S n0) p); Constructor 2; Auto.
Defined.

Require Export Arith.
\end{coq_example}

 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{coq_example}
Fixpoint tailfact [n:nat]:nat->nat :=
    [m:nat]Cases n of
              O => (m)
        | (S x) => (tailfact x (mult (S x) m))
           end.
Definition fact_tail := [n:nat](tailfact n (S O)).
Definition esq: (P:nat*nat->Set)
                   ((x:nat)(P (O,x)))
                 ->((x,y:nat)(P (x,y))->(P ((S x),y)))
                        -> (t:nat*nat)(P t).
Proof.
Intros.
Case t.
Intros.
Elim n.
Apply H.
Intros.
Apply H0.
Auto.
Defined.
Definition Tailfact:nat*nat->nat.
Proof.
Apply (esq [_:(nat*nat)]nat).
Exact [x:nat]x.
Exact [x,_:nat; z:nat](mult (S x) z).
Defined.
\end{coq_example}

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{coq_example}
Require PolyList.

Fixpoint sumalista [l:(list nat)]:nat:=
   Cases l of nil => O
      |(cons x l) => (plus x (sumalista l))
   end.

 Fixpoint aux_sumalistail [l:(list nat)]:nat->nat:=
  [ac:nat]Cases l of 
             nil => ac
     |(cons x l) => (aux_sumalistail l (plus x ac))
          end.

Print aux_sumalistail.

Lemma aux1:(l:(list nat); n:nat)
 (aux_sumalistail l (S n))=(S (aux_sumalistail l n)).
Proof.
Induction l; Simpl; Auto.
Intros.
Replace (plus a (S n)) with (S (plus a n)).
Apply (H (plus a n)).
Auto with *.
Qed.

Lemma aux:(l:(list nat); n,m:nat)
        (aux_sumalistail l (plus n m))=(plus n (aux_sumalistail l m)).
Proof.
Induction n; Simpl; Auto.
Intros n0 H.
Intro m.
Rewrite <- (H m).
Apply aux1.
Qed.


Definition nsumalista := [l:(list nat)]let f=(
Fix aux_sumalistail
  {aux_sumalistail [l:(list nat)] : nat->nat :=
     [ac:nat]
      Cases l of
        nil => ac
      | (cons x l0) => (aux_sumalistail l0 (plus x ac))
      end} ) in (aux_sumalistail l O).

Print nsumalista.

Lemma verif : (l:(list nat))(nsumalista l)=(sumalista l).
Proof.
Induction l; Simpl; Auto.
Intros.
Simpl.
Unfold nsumalista.
Simpl.
Unfold nsumalista in H.
Replace (plus a (0)) with a.
Rewrite <- H.
Rewrite <- (aux l0 a O).
Replace (plus a O) with a.
Auto with *.
Auto with *.
Qed.

Recursive Extraction nsumalista.

\end{coq_example}

\end{document}