From 012a0ba06a3761d3c5f285121ed24ba840eb2a06 Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Thu, 16 May 2024 11:30:40 +0200
Subject: [PATCH] Add presentation.tex

---
 RapportPresentation/ex-presentation.tex | 147 ++++++++++++++++++++----
 1 file changed, 126 insertions(+), 21 deletions(-)

diff --git a/RapportPresentation/ex-presentation.tex b/RapportPresentation/ex-presentation.tex
index bde9878..358d77b 100644
--- a/RapportPresentation/ex-presentation.tex
+++ b/RapportPresentation/ex-presentation.tex
@@ -1,9 +1,24 @@
 \documentclass{beamer}
 
+\usepackage[T1]{fontenc}
+\usepackage{listings}
+\usepackage{syntax}
 \usepackage[utf8]{inputenc}
+\newcommand{\Hquad}{\hspace{0.2em}}
 
-\title{Présentation finale projet 2}
-\author{Titi et toto}
+\lstset{
+ language=caml,
+ columns=[c]fixed,
+ basicstyle=\small\ttfamily,
+ keywordstyle=\bfseries,
+ upquote=true,
+ commentstyle=,
+ breaklines=true,
+ showstringspaces=false
+ }
+
+\title{Présentation Projet Fonctionnel}
+\author{Marwan AZIZI et Augustin LUCAS}
 \institute{}
 \date{}
 
@@ -11,38 +26,128 @@
 % pour compiler : tapez pdflatex ex-presentation
 % regardez ensuite le fichier ex-presentation.pdf
 
+% 1. grammaire du lcalcul simmplement typé
+
+
+% on a fait pieuvre, assistant de preuve pour la logique intuitionniste documentclass
+%
+
+% fonctionne grâce à Curry-Howard -> insister sur l'utilisation des refs
+% montrer l'exmple du apply généralisé
+% fiabilité
+
 \begin{document}
 
 \maketitle
 
-\begin{frame}{Nous avons bien ri}
+\begin{frame}{Introduction}
+  % On a fait pieuvre, assistant de preuve pour la logique intuitionniste
+  Pieuvre, un assistant de preuve pour la logique intuitionniste
+  \pause
+  \vspace{0.2in}
 
-  \begin{itemize}
-  \item nous avons codé en Haskell
+  Prouvable
+  $$A \rightarrow B \rightarrow (A \wedge B)$$
+  Pas prouvable
+  $$A \rightarrow \neg \neg A$$
 
-  \item nous avons utilisé une imprimante 3D
-
-    \pause
-
-
-  \item notre programme ne marche pas sur des entrées de taille $>10$
-
-  \end{itemize}
-  
 \end{frame}
 
-\begin{frame}{Conclusions}
+\begin{frame}{Comment ça marche}
+  Par la correspondance de Curry-Howard
+  \vspace{0.2in}
 
-  \begin{itemize}
-  \item ce qu'il reste à améliorer
+  Preuve $\Leftrightarrow$ programme du $\lambda$-calcul simplement typé
+\end{frame}
 
-  \item ce qui pourrait être ajouté
+\begin{frame}{lambda-calcul}
+  la grammaire
+\end{frame}
 
-  \item ce qui devrait être totalement repris
+%! liste des tactiques
+\begin{frame}{Tactiques}
+  Commandes:
 
-  \item ce qui a été le plus difficile
-  \end{itemize}
+  \lstinline{Goal}
+
+  \lstinline{Undo}
+
+  \lstinline{Qed}
+
+  Tactiques:
+
+  \lstinline{exact}
+
+  \lstinline{assumption}
+
+  \lstinline{destruct}
+
+  \lstinline{intros}
+
+  \lstinline{intro}
+
+  \lstinline{cut}
+
+  \lstinline{apply}
+
+  \lstinline{left}
+
+  \lstinline{right}
+
+  \lstinline{split}
+\end{frame}
+
+\begin{frame}{Exemple}
+  Prouvons $(A \rightarrow B \rightarrow C) \rightarrow A \rightarrow B \rightarrow C$
+\end{frame}
+
+\begin{frame}
+  % présenter les buts, les trous
+  \frametitle{Prouvons $(A \rightarrow B \rightarrow C) \rightarrow A \rightarrow B \rightarrow C$}
+
+  Preuve: %rajouter les types
+  \only<1>{$$?$$}
+  \only<2>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow ?$$}
+  \only<3>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad ? \Hquad ?)$$}
+  \only<4>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad x_1 \Hquad ?)$$}
+  \only<5-6>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad x_1 \Hquad x_2)$$}
+
+  Interface:
+
+  \onslide<2-5>\lstinline{H2 : B}
+
+  \onslide<2-5>\lstinline{H1 : A}
+
+  \onslide<2-5>\lstinline{H0 : A -> B -> C}
+
+  \onslide<1>\lstinline{(A -> B -> C) -> A -> B -> C}
   
+  \onslide<2>\lstinline{C}
+
+  \onslide<4>\lstinline{B}
+
+  \onslide<3>\lstinline{A}
+
+  \onslide<5>\lstinline{No more goals.}
+
+  \onslide<1->\lstinline{===========================}
+  
+  \onslide<1->\lstinline{Goal (A -> B -> C) -> A -> B -> C.}
+
+  \onslide<2->\lstinline{intros.}
+
+  \onslide<3->\lstinline{apply H0.}
+
+  \onslide<4->\lstinline{exact H1.}
+
+  \onslide<5->\lstinline{exact H2.}
+  
+  \onslide<6->\lstinline{Qed.}
+\end{frame}
+
+
+\begin{frame}
+  \frametitle{Fiabilité}
 \end{frame}
 
 \end{document}