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

\begin{document}
\thispagestyle{empty}

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

\section{}
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{}.

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{}.
Se tiene que:
\begin{coq_example}
Section ejemplo1.
Variable b:bool.
Variable C:Set.

Variables x,y:C.

Check (if b then x else y).

Check Cases b of
   true => x
 |false => y
       end.
End ejemplo1.
\end{coq_example}

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{}.
En {\tt DecBool.v} (directorio {\tt Bool} de {\tt Therories}) 
escrito por P. Mohring, se
define el programa 

\begin{coq_example}
Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
   := [A,B,C,H,x,y]if H then [_]x else [_]y.
\end{coq_example}

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{}.
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{coq_example}
Section ejemplo2.
Variable X:Set.
Variable P:X->Prop.
Variable H:(x:X){(P x)}+{~(P x)}.
Variable C:Set.
Variable f:(x:X)(P x)->C.
Variable g:(x:X)~(P x)->C.

Check [x:X]if (H x) then (f x) else (g x).
End ejemplo2.
\end{coq_example}

\section{}.
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{coq_example}
Section ejemplo3.
Variable X:Set.
Variable P:X->Prop.
Variable H:(x:X){(P x)}+{~(P x)}.

Definition disc:=[x:X]if (H x) then [_]true else [_]false.
End ejemplo3.
Check disc.
\end{coq_example}

O también:

\begin{coq_example}
Section discriminante.
Definition ifdec':=[A,B:Prop; C:Set; H:({A}+{B}); x,y:C]
 Cases H of
   (left _) => x
 | (right _) => y
 end.
Variable X:Set.
Variable P:X->Prop.
Variable H:(x:X){(P x)}+{~(P x)}.

Definition  disc':=[x:X](ifdec' (P x) ~(P x) bool (H x) true false).
End discriminante.
Check disc'.
\end{coq_example}

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{coq_example}
Lemma uno: (X:Set; P:(X->Prop); H:((x:X){(P x)}+{~(P x)}); x:X)(P x)
->(disc X P H x)=true.

Proof.
Intros.
Unfold disc.
Case (H x).
Intros.
Simpl.
Auto.

Intros.
Elim (n H0).
Qed.

Lemma dos: (X:Set; P:(X->Prop); H:((x:X){(P x)}+{~(P x)}); x:X)(disc
X P H x)=true -> (P x).
\end{coq_example}

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{verbatim}
Cases h of
  le_n => p
| (le_S m _) => q
end.
\end{verbatim}

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

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


\item[b] Sobre los mecanismos de decisión:

\begin{coq_example}
Lemma decision: (n:nat){n=O}+{~(n=O)}.
Proof.
 Destruct n;[Left;Trivial | Clear n;Intro;Right;Discriminate].
Qed.
\end{coq_example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\item[Lazy vs Eager]
\begin{coq_example}
Definition cata_nat:=[C:Set][a:C][f:C->C]
               (nat_rec [_:nat]C a [_:nat]f).


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

Definition iteracion:=[f:nat->nat][n:nat](iter n f).

Definition H_Ack:=(cata_nat nat->nat S iteracion).

Require Arith.

Eval Compute in (if true then O else (H_Ack (4) (1))).

(*Eval Compute in (if false then O else (H_Ack (4) (1))).*) 


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

(*Eval Compute in (MIF true O (H_Ack (3) (1))).*)


Eval Lazy Beta in (MIF true O (H_Ack (4) (1))).
Eval Lazy Beta Delta Iota in (MIF true O (H_Ack (4) (1))).
(*-------------------------------------------*)

Definition foo:=[x:nat]O.

(* Eval Compute in (foo (H_Ack (4) (1))).*)

Eval Lazy Beta Delta in (foo (H_Ack (4) (1))).
\end{coq_example}
 
\end{description}

\end{document}.