\documentclass[11pt]{article}
\setlength{\textheight}{25cm}
\setlength{\textwidth}{15cm} 
\setlength{\oddsidemargin}{.5cm}
\setlength{\evensidemargin}{.5cm}
\setlength{\topmargin}{0cm}

\begin{document}
\thispagestyle{empty}

Sobre \verb"if .. then .. else" en {\sf Coq}.

\section{1}
Si {\tt X,Y} y {\tt C:Set, F:X->C,  G:Y->C} y {\tt H1:X+Y}, 
 entonces el término {\tt if H1 then F else G} 
tiene tipo {\tt C} y representa el término:

\begin{verbatim}
Cases H1 of
  (inl x) => (F x)
| (inr x) => (G x)
end
\end{verbatim}

\section{2}.

También, 
Si {\tt A,B:Prop, H:{A}+{B}, f:A->C} y {\tt g:B->C},  entonces el término 
{\tt if H then f else g} 
tiene tipo {\tt C} y representa el término:

\begin{verbatim}
Cases H of
  (left x) => (f x)
| (right x) => (g x)
end
\end{verbatim}

\section{3}.
Se tiene que:
\begin{flushleft}
\texttt{Coq~{<}~Parameter~b:bool.}\\
\texttt{b~is~assumed}\\
\medskip
\texttt{Coq~{<}~Parameter~C:Set.}\\
\texttt{C~is~assumed}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Parameters~x,y:C.}\\
\texttt{x~is~assumed}\\
\texttt{y~is~assumed}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Check~(if~b~then~x~else~y).}\\
\texttt{(if~b~then~x~else~y)}\\
\texttt{~~~~~:~C}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Check~Cases~b~of}\\
\texttt{Coq~{<}~~~~true~={>}~x}\\
\texttt{Coq~{<}~~|false~={>}~y}\\
\texttt{Coq~{<}~~~~~~~~end.}\\
\texttt{(if~b~then~x~else~y)}\\
\texttt{~~~~~:~C}\\
\end{flushleft}

De hecho, el tipo bool es isomorfo a la suma de dos conjuntos con un solo
elemento (uno con el elemento "true" y otro con el elemento "false")


\section{4}.
En {\tt DecBool.v} (directorio {\tt Bool} de {\tt Therories}) 
escrito por P. Mohring, se
define el programa 

\begin{flushleft}
\texttt{Coq~{<}~Definition~ifdec~:~(A,B:Prop)(C:Set)(\{A\}+\{B\})-{>}C-{>}C-{>}C}\\
\texttt{Coq~{<}~~~~:=~[A,B,C,H,x,y]if~H~then~[\_]x~else~[\_]y.}\\
\texttt{ifdec~is~defined}\\
\end{flushleft}

Nótese que {\tt (ifdec A B C):{A}+{B})->C->C->C} es el caso 2 anterior 
con {\tt f:A->C}
la funcion constante que vale siempre {\tt x} y {\tt g:B->C} la 
constante {\tt y}.


\section{5}.
Si {\tt X:Set} y {\tt P:X->Prop} es un predicado, para cada {\tt x:X}
 tenemos una proposición
{\tt (P x)}. 
Si este predicado es decidible (es decir existe {\tt H:(x:X){(P x)}+{~(P
x)})}, entonces, dado cualquier {\tt C:Set, f:(x:X)(P x)->C} y 
{\tt g:(x:X)~(P x)->C}, se
puede construir la expresión {\tt [x:X]if (H x) then (f x) else (g x)}


en coq:
\begin{flushleft}
\texttt{Coq~{<}~Require~DecBool.}\\
\medskip
\texttt{Coq~{<}~Parameter~X:Set.}\\
\texttt{X~is~assumed}\\
\medskip
\texttt{Coq~{<}~Parameter~P:X-{>}Prop.}\\
\texttt{P~is~assumed}\\
\medskip
\texttt{Coq~{<}~Parameter~H:(x:X)\{(P~x)\}+\{\char'176(P~x)\}.}\\
\texttt{H~is~assumed}\\
\medskip
\texttt{Coq~{<}~Parameter~C:Set.}\\
\texttt{Error:~C~already~exists}\\
\medskip
\texttt{Coq~{<}~Parameter~f:(x:X)(P~x)-{>}C.}\\
\texttt{f~is~assumed}\\
\medskip
\texttt{Coq~{<}~Parameter~g:(x:X)\char'176(P~x)-{>}C.}\\
\texttt{g~is~assumed}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Check~[x:X]if~(H~x)~then~(f~x)~else~(g~x).}\\
\texttt{[x:X]Cases~(H~x)~of}\\
\texttt{~~~~~~~(left~x0)~={>}~(f~x~x0)}\\
\texttt{~~~~~|~(right~x0)~={>}~(g~x~x0)}\\
\texttt{~~~~~end}\\
\texttt{~~~~~:~X-{>}C}\\
\end{flushleft}

\section{6}.
En particular, si {\tt C = bool, (f x x0)=true} y {\tt (g x x0)=false}, 
entonces, dado
un {\tt x:X} para el cual {\tt (H x) =  (left x0)} para algún {\tt x0:(P x)}
 (o sea {\tt (P x)} es
verdadera pues tiene una prueba), el resultado de la anteror función será
{\tt true}. Y si, por el contrario, {\tt (H x) = (right x0)} para algún 
{\tt x0:~(P x)}, el
resultado será {\tt false}

\begin{flushleft}
\texttt{Coq~{<}~DecBool.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Parameter~X:Set.}\\
\texttt{Error:~X~already~exists}\\
\medskip
\texttt{Coq~{<}~Parameter~P:X-{>}Prop.}\\
\texttt{Error:~P~already~exists}\\
\medskip
\texttt{Coq~{<}~Parameter~H:(x:X)\{(P~x)\}+\{\char'176(P~x)\}.}\\
\texttt{Error:~H~already~exists}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Definition~disc:=[x:X]if~(H~x)~then~[\_]true~else~[\_]false.}\\
\texttt{disc~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Check~disc.}\\
\texttt{disc}\\
\texttt{~~~~~:~X-{>}bool}\\
\end{flushleft}

O también:

\begin{flushleft}
\texttt{Coq~{<}~Section~discriminante.}\\
\medskip
\texttt{Coq~{<}~Definition~ifdec:=[A,B:Prop;~C:Set;~H:(\{A\}+\{B\});~x,y:C]}\\
\texttt{Coq~{<}~~Cases~H~of}\\
\texttt{Coq~{<}~~~~(left~\_)~={>}~x}\\
\texttt{Coq~{<}~~|~(right~\_)~={>}~y}\\
\texttt{Coq~{<}~~end.}\\
\texttt{ifdec~is~defined}\\
\medskip
\texttt{Coq~{<}~Variable~X:Set.}\\
\texttt{X~is~assumed}\\
\medskip
\texttt{Coq~{<}~Variable~P:X-{>}Prop.}\\
\texttt{P~is~assumed}\\
\medskip
\texttt{Coq~{<}~Variable~H:(x:X)\{(P~x)\}+\{\char'176(P~x)\}.}\\
\texttt{H~is~assumed}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Definition~~disc:=[x:X](ifdec~(P~x)~\char'176(P~x)~bool~(H~x)~true~false).}\\
\texttt{disc~is~defined}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~End~discriminante.}\\
\texttt{Error:~ifdec~already~exists}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Check~disc.}\\
\texttt{disc}\\
\texttt{~~~~~:~X-{>}bool}\\
\end{flushleft}

Es decir, si tenemos un predicado {\tt P}  decidible sobre {\tt X:Set}, 
entonces
podemos definir la función {\em característica} que vale {\tt true}
 en los {\tt x:X} donde se
cumple {\tt (P x)} y {\tt false} en los que no.

\begin{flushleft}
\texttt{Coq~{<}~Lemma~uno:~(X:Set;~P:(X-{>}Prop);~H:((x:X)\{(P~x)\}+\{\char'176(P~x)\});~x:X)(P~x)-{>}(disc~X~P~H}\\
\texttt{Coq~{<}~x)=true.}\\
\texttt{Toplevel~input,~characters~76-77}\\
\texttt{{>}~Lemma~uno:~(X:Set;~P:(X-{>}Prop);~H:((x:X)\{(P~x)\}+\{\char'176(P~x)\});~x:X)(P~x)-{>}(disc~X~P~H}\\
\texttt{{>}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\char'136}\\
\texttt{Error:~In~environment}\\
\texttt{X~:~Set}\\
\texttt{P~:~X-{>}Prop}\\
\texttt{H~:~(x:X)\{(P~x)\}+\{\char'176(P~x)\}}\\
\texttt{X0~:~Set}\\
\texttt{P0~:~X0-{>}Prop}\\
\texttt{H0~:~(x:X0)\{(P0~x)\}+\{\char'176(P0~x)\}}\\
\texttt{x~:~X0}\\
\texttt{p~:~(P0~x)}\\
\texttt{The~term~X0~has~type~Set~while~it~is~expected~to~have~type~X}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Unfold~disc.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Case~(H~x).}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Intros.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Simpl.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Auto.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Intros.}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Elim~(n~H0).}\\
\texttt{Error:~Unknown~command~of~the~non~proof-editing~mode}\\
\medskip
\texttt{Coq~{<}~Qed.}\\
\texttt{Error:~No~focused~proof~(No~proof-editing~in~progress).}\\
\medskip
\texttt{Coq~{<}~}\\
\texttt{Coq~{<}~Lemma~dos:~(X:Set;~P:(X-{>}Prop);~H:((x:X)\{(P~x)\}+\{\char'176(P~x)\});~x:X)(disc}\\
\texttt{Coq~{<}~X~P~H~x)=true~-{>}~(P~x).}\\
\texttt{Toplevel~input,~characters~70-71}\\
\texttt{{>}~X~P~H~x)=true~-{>}~(P~x).}\\
\texttt{{>}~\char'136}\\
\texttt{Error:~In~environment}\\
\texttt{X~:~Set}\\
\texttt{P~:~X-{>}Prop}\\
\texttt{H~:~(x:X)\{(P~x)\}+\{\char'176(P~x)\}}\\
\texttt{X0~:~Set}\\
\texttt{P0~:~X0-{>}Prop}\\
\texttt{H0~:~(x:X0)\{(P0~x)\}+\{\char'176(P0~x)\}}\\
\texttt{x~:~X0}\\
\texttt{The~term~X0~has~type~Set~while~it~is~expected~to~have~type~X}\\
\end{flushleft}

Otras observaciones:

\begin{description}
\item[a] Si {\tt n,m:nat, h:(le n m)}, y si 
{\tt P:Prop} y {\tt p,q:P}, entonces 
podemos escribir:

\begin{flushleft}
\texttt{Coq~{<}~Cases~h~of}\\
\texttt{Coq~{<}~~~le\_n~={>}~p}\\
\texttt{Coq~{<}~|~(le\_S~m~\_)~={>}~q}\\
\texttt{Coq~{<}~end.}\\
\texttt{Toplevel~input,~characters~0-5}\\
\texttt{{>}~Cases~h~of}\\
\texttt{{>}~\char'136\char'136\char'136\char'136\char'136}\\
\texttt{Syntax~error:~illegal~begin~of~vernac}\\
\end{flushleft}

pero en ningún caso podemos escribir:
\begin{verbatim}
Cases (le n m) of
\end{verbatim}

porque {\tt (le n m)} no tiene tipo inductivo.


\item[b] Sobre los mecanismos de decision:

\begin{flushleft}
\texttt{Coq~{<}~Lemma~decision:~(n:nat)\{n=O\}+\{\char'176(n=O)\}.}\\
\texttt{1~subgoal}\\
\texttt{~~}\\
\texttt{~~X~:~Set}\\
\texttt{~~P~:~X-{>}Prop}\\
\texttt{~~H~:~(x:X)\{(P~x)\}+\{\char'176(P~x)\}}\\
\texttt{~~============================}\\
\texttt{~~~(n:nat)\{n=O\}+\{\char'176n=O\}}\\
\medskip
\texttt{Coq~{<}~Proof.}\\
\medskip
\texttt{Coq~{<}~~Destruct~n;[Left;Trivial~|~Clear~n;Intro;Right;Discriminate].}\\
\texttt{Subtree~proved!}\\
\medskip
\texttt{Coq~{<}~Qed.}\\
\texttt{Destruct~n;~[~Left;~Trivial~|~Clear~n;~Intro;~Right;~Discriminate~].}\\
\texttt{decision~is~defined}\\
\end{flushleft}
\end{description}
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Lazy vs Eager]

Unnamed_thm < Definition cata_nat:=[C:Set][a:C][f:C->C]
               (nat_rec [_:nat]C a [_:nat]f).Unnamed_thm < 
cata_nat is defined

Unnamed_thm < Definition iter:=(cata_nat ((nat->nat)->nat) ([f:nat->nat](f
(S O)))
                     ([h:(nat->nat)->nat][k:nat->nat](k (h k)))).
Unnamed_thm < iter is defined

Unnamed_thm < 
Unnamed_thm < Definition iteracion:=[f:nat->nat][n:nat](iter n f).iteracion
is defined

Unnamed_thm < Definition H_Ack:=(cata_nat nat->nat S iteracion).
H_Ack is defined

Unnamed_thm < Require Arith.

Unnamed_thm < Eval Compute in (if true then O else (H_Ack (4) (1))).
     = (0)
     : nat
Unnamed_thm < Eval Compute in (if false then O else (H_Ack (4) (1))).


Unnamed_thm < Definition MIF:=[b:bool;n,m:nat](if b then n else m).
MIF is defined

Unnamed_thm < Eval Compute in (MIF true O (H_Ack (4) (1))).


Unnamed_thm < Eval Lazy Beta in (MIF true O (H_Ack (4) (1))).
     = (MIF true (0) (H_Ack (4) (1)))
     : nat
Unnamed_thm < Eval Lazy Beta Delta Iota in (MIF true O (H_Ack (4) (1))).
     = (0)
     : nat
-------------------------------------------