adds a proof with well-founded induction and certified data

slides5.tex

@@ -133,8 +133,8 @@ Definition btree_size_ind
 \item The same pattern can be used for programming
 \end{itemize}
 \end{frame}
-\begin{frame}
-\frametitle{}
+\begin{frame}[fragile]
+\frametitle{Preparatory lemmas for {\tt bree\_size\_ind}}
 \begin{small}
 \begin{alltt}
 Lemma size1 {T} (a : T) t1 t2 : size t1 < size (Node a t1 t2).
@@ -151,6 +151,40 @@ Qed.
 \end{alltt}
 \end{small}
 \end{frame}
+\begin{frame}[fragile]
+\frametitle{A proof using {\tt btree\_size\_ind}}
+\begin{small}
+\begin{alltt}
+Lemma redo_count_rev_tree {T} (p : T -> bool) t :
+  count p (rev_tree t) = count p t.
+Proof.
+induction t as [t IH] using btree_size_ind.
+destruct t as [ | a t1 t2].
+  easy.
+simpl.
+rewrite IH.
+  rewrite IH.
+    rewrite (Nat.add_comm (count p t2)).
+    easy.
+  apply size1.
+apply size2.
+Qed.
+\end{alltt}
+\end{small}
+\end{frame}
+\begin{frame}
+\frametitle{Dependent components and certified data}
+\begin{itemize}
+\item In pairs, the two components are independent
+\item Extension: sigma-types where the second components depends on the first
+one
+\item Example: bounded integers \((n, h)\) where \(h\) is a proof that \(n\) is
+within bounds
+\item You need some for of ``proof irrelevance''
+\item Used extensively in the {\em Mathematical Components} library
+\item Recursive programming on bounded integers is slightly more complex
+\end{itemize}
+\end{frame}
 \end{document}