curry-howard

diff --git a/examples/exhaustion-naive.py b/examples/exhaustion-naive.py
@@ -0,0 +1,3 @@
+for n in N:
+    for m in N:
+        assert p(n, m) == 1

diff --git a/examples/fake-theorem.py b/examples/fake-theorem.py
@@ -0,0 +1,2 @@
+f(n + m) % (f(n) * f(m)) == 0
+

diff --git a/examples/typechecking.c b/examples/typechecking.c
@@ -0,0 +1,9 @@
+unsigned int f(unsigned int n)
+{
+  if (n == 0) return 0;
+  else return n * f(n - 1);
+}
+
+// error: implicit conversion from 'float' to 
+// 'unsigned int' changes value from 0.5 to 0
+f(0.5f); 

diff --git a/examples/typecheking.c b/examples/typecheking.c
@@ -0,0 +1,8 @@
+unsigned int f(unsigned int n)
+{
+  if (n == 0) return 0;
+  else return n * f(n - 1);
+}
+
+f(0.5f); 
+// error: implicit conversion from 'float' to 'unsigned int' changes value from 0.5 to 0

diff --git a/sections/curry.tex b/sections/curry.tex
@@ -79,6 +79,47 @@
   \end{figure}
 \end{frame}
 
+\begin{frame}[fragile]{Métodos Não-Numéricos?}
+  \begin{itemize}
+    \item Objection!
+  \end{itemize}
+
+  \pause
+
+  \begin{columns}
+    \begin{column}{.3\linewidth}
+      \[
+        n! \cdot m! \mid (n + m)!
+      \]
+    \end{column}
+    \begin{column}{.5\linewidth}
+      \inputminted{python}{examples/fake-theorem.py}
+    \end{column}
+  \end{columns}
+  
+  \pause
+
+  \begin{align*}
+    p : \mathbb{N} \times \mathbb{N} & \to \{0, 1\} \\
+    (n, m) & \mapsto
+    \begin{cases}
+      1 & \text{se}\ n! \cdot m! \mid (n + m) ! \\
+      0 & \text{caso contrário} \\
+    \end{cases}
+  \end{align*}
+  
+  \pause
+
+  \begin{itemize}
+    \item Nenhum computador é capaz de checar que \(p(n, m) = 1\) para todos
+      \(n, m\)
+      \begin{figure}
+        \centering
+        \inputminted{python}{examples/exhaustion-naive.py}
+      \end{figure}
+  \end{itemize}
+\end{frame}
+
 \subsection{A Correspondência de Curry-Howard}
 
 \begin{frame}{A Correspondência de Curry-Howard}
@@ -100,7 +141,7 @@
           \(A\ \text{ou}\ B\) 
             & \(\leftrightsquigarrow\) 
             & \(\{\text{provas de}\ A \} \cup \{\text{provas de}\ B \}\) \\
-          \(A \Rightarrow B\)
+          \(A \implies B\)
             & \(\leftrightsquigarrow\) 
             & \(\{\text{provas de}\ A \} \to \{\text{provas de}\ B \}\) \\
         \end{tabular}
@@ -117,25 +158,26 @@
         \centering
         \inputminted{python}{examples/types.py}
       \end{figure}
+  \end{itemize}
+\end{frame}
 
-      \pause
-
-    \item Se eu conseguir contruir um valor to tipo \texttt{AndAB} eu provei
-      que vale \(A \ \text{e} \ B\)
+\begin{frame}[fragile]{A Correspondência de Curry-Howard}
+  \begin{itemize}
+    \item Computadores são muito bons em checar tipos!
+      \begin{figure}
+        \centering
+        \inputminted{c}{examples/typechecking.c}
+      \end{figure}
 
-      \pause
+    \item Linguagens estaticamente tipadas
 
-    \item Mas o Python não sabe checar se o valor que eu construi é de fato do
-      tipo \texttt{AndAB}
+    \item Provar que vale \(A\) corresponde a construir um elemento do tipo
+      \(\{\text{provas de}\ A\}\)
   \end{itemize}
 \end{frame}
 
 \begin{frame}{Provadores de Teoremas}
   \begin{itemize}
-    \item Linguagens estaticamente tipadas
-
-      \pause
-
     \item Fixo certas coisas que quero impor que sejam verdade
       \begin{itemize}
         \item Dados \(x\) e \(y\), existe o tipo \texttt{x = y} das provas de
@@ -150,6 +192,10 @@
 
       \pause
 
+    \item Tipos dependentes
+
+      \pause
+
     \item Provadores de Teoremas
       \begin{itemize}
         \item Coq (\url{https://coq.inria.fr/})