continued

itp-lesson/main.tex

@@ -3,7 +3,8 @@
 
 \usepackage{tikz}
 \usetikzlibrary{positioning,graphdrawing, arrows, chains, shapes, quotes,
-fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
+fit, calc, decorations.pathmorphing, decorations.shapes, matrix,
+overlay-beamer-styles}
 \usepackage{tcolorbox}
 \tcbuselibrary{theorems}
 
@@ -115,6 +116,12 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
 \end{frame}
 
 \begin{frame}{What we'll learn}
+	\begin{itemize}
+		\item Identify a formal proof
+		\item Produce a formal proof out of an informal statement
+		\item Compare formal proofs
+		\item Relate proofs and programs
+	\end{itemize}
 	% TODO alignement pedagogique &c.
 \end{frame}
 
@@ -424,7 +431,8 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
 
 \begin{frame}{Intuitionistic natural deduction}
 	% Sequent calculus: easy to progress, apply rules quasi blindly
-	\begin{block}{Sequent calculus}
+	% Sequent calculus: only introduction rules, no elimination rule
+	\begin{block}{Classical sequent calculus}
 		\[
 			\begin{array}{cc}
 				\begin{prooftree}
@@ -441,7 +449,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
 		\]
 	\end{block}
 
-	\begin{block}{Natural deduction}
+	\begin{block}{Intuitionistic natural deduction}
 		\[
 			\begin{prooftree}
 				\hypo{\Gamma \vdash A \lor B}
@@ -452,7 +460,7 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
 		\]
 	\end{block}
 	\begin{itemize}
-		\item Destructuring on the \alert{right} of \(\vdash\)
+		\item Introductions on the \alert{right} of \(\vdash\)
 		\item At most one formula on the right of \(\vdash\)
 	\end{itemize}
 	% First item doesn't change the expressiveness or provability
@@ -509,8 +517,28 @@ fit, calc, decorations.pathmorphing, decorations.shapes, matrix}
 	% But: with natural deduction, we may use contexts only for the axiom rule
 \end{frame}
 
-\begin{frame}{Writing proofs: named hypotheses}
-	% Name hypotheses
+\begin{frame}{Writing proofs: contexts}
+	% In natural deduction, contexts are only used for the axiom rule
+	% Named hypotheses in global context
+	\(\alpha : P, \beta : Q\) \hspace{6em}
+	\onslide<2->{\(\text{and-i}(\alpha, \beta)\)}
+	\vfill
+	\onslide<3->
+	How to extend context?
+	% What do we need? a notation that introduces an hypothesis, with a notion of
+	% scope: the hypothesis may be used only in the proof pi below
+	\vfill
+	\onslide<4->
+	\begin{tikzpicture}
+		\node (A) {%
+				\begin{prooftree}
+					\hypo{\pi}
+					\infer1{A, B \vdash C}
+					\infer1[imp-i]{A \vdash B \imp C}
+				\end{prooftree}
+			};
+		\node [right = 2cm of A, visible on=<5->] (B) { {\tabst{\beta}[B]\pi} };
+	\end{tikzpicture}
 \end{frame}
 
 \section{Formalising proof systems}