<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">% Any piece of code related to font selection in the following preambule
% (document class, font package, font selection commands ...) should be
% reported in `coq-sample.mp'.

\documentclass[8pt]{beamer}
\usetheme{Warsaw}

\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage[varg]{txfonts}

\usepackage{graphicx}
\makeatletter
\def\Gin@def@bp#1\relax#2#3{\gdef#2{#3}}
\newsavebox{\graphicsbox}
\newcommand*{\drv}[1]{%
\sbox{\graphicsbox}{\includegraphics{#1}}%
\raisebox{\Gin@lly bp}%
{\usebox{\graphicsbox}}}
\makeatother

\title{Une construction de preuve en logique minimale}
\institute{INF462 -- Master S\&amp;T Informatique -- Bordeaux 1}
\date{}

\begin{document}

\begin{frame}
\titlepage
\end{frame}

\ttfamily
\itshape
\small

\begin{frame}
\begin{block}{}
%
% coq-tex output
%
\begin{overlayarea}{\textwidth}{.5\textheight}
\only&lt;1&gt;{%
  \textup{Coq~{&lt;}~Variables~P~Q~R~:~Prop.}\\
  P~is~assumed\\
  Q~is~assumed\\
  R~is~assumed\\
  \medskip
  \textup{%
  Coq~{&lt;}~Lemma~imp\_perm~:~(P~-{&gt;}~(Q~-{&gt;}~R))~-{&gt;}~(Q~-{&gt;}~(P~-{&gt;}~R)).}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~============================\\
  ~~~\textcolor{blue}{(P~-{&gt;}~Q~-{&gt;}~R)~-{&gt;}~Q~-{&gt;}~P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}~Proof.}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;2&gt;{%
  \textup{Coq~{&lt;}~Variables~P~Q~R~:~Prop.}\\
  P~is~assumed\\
  Q~is~assumed\\
  R~is~assumed\\
  \medskip
  \textup{%
  Coq~{&lt;}~Lemma~imp\_perm~:~(P~-{&gt;}~(Q~-{&gt;}~R))~-{&gt;}~(Q~-{&gt;}~(P~-{&gt;}~R)).}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~============================\\
  ~~~\textcolor{blue}{(P~-{&gt;}~Q~-{&gt;}~R)~-{&gt;}~Q~-{&gt;}~P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}~Proof.}\\
  \medskip
  \textup{Coq~{&lt;}~~~intro~H.}}
\only&lt;3&gt;{%
  \textup{Coq~{&lt;}~~~intro~H.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~============================\\
  ~~~\textcolor{blue}{Q~-{&gt;}~P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;4&gt;{%
  \textup{Coq~{&lt;}~~~intro~H.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~============================\\
  ~~~\textcolor{blue}{Q~-{&gt;}~P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}~~~intro~q.}}
\only&lt;5&gt;{%
  \textup{Coq~{&lt;}~~~intro~q.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~============================\\
  ~~~\textcolor{blue}{P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;6&gt;{%
  \textup{Coq~{&lt;}~~~intro~q.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~============================\\
  ~~~\textcolor{blue}{P~-{&gt;}~R}\\
  \medskip
  \textup{Coq~{&lt;}~~~intro~p.}}
\only&lt;7&gt;{%
  \textup{Coq~{&lt;}~~~intro~p.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{R}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;8&gt;{%
  \textup{Coq~{&lt;}~~~intro~p.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{R}\\
  \medskip
  \textup{Coq~{&lt;}~~~apply~H.}}
\only&lt;9&gt;{%
  \textup{Coq~{&lt;}~~~apply~H.}\\
  2~subgoals\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{P}\\
  subgoal~2~is:\\
  ~\textcolor{blue}{Q}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;10&gt;{%
  \textup{Coq~{&lt;}~~~apply~H.}\\
  2~subgoals\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{P}\\
  subgoal~2~is:\\
  ~\textcolor{blue}{Q}\\
  \medskip
  \textup{Coq~{&lt;}~~~assumption.}}
\only&lt;11&gt;{%
  \textup{Coq~{&lt;}~~~assumption.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{Q}\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;12&gt;{%
  \textup{Coq~{&lt;}~~~assumption.}\\
  1~subgoal\\
  ~~\\
  ~~P~:~Prop\\
  ~~Q~:~Prop\\
  ~~R~:~Prop\\
  ~~H~:~P~-{&gt;}~Q~-{&gt;}~R\\
  ~~q~:~Q\\
  ~~p~:~P\\
  ~~============================\\
  ~~~\textcolor{blue}{Q}\\
  \medskip
  \textup{Coq~{&lt;}~~~assumption.}}
\only&lt;13&gt;{%
  \textup{Coq~{&lt;}~~~assumption.}\\
  Proof~completed.\\
  \medskip
  \textup{Coq~{&lt;}}}
\only&lt;14&gt;{%
  \textup{Coq~{&lt;}~~~assumption.}\\
  Proof~completed.\\
  \medskip
  \textup{Coq~{&lt;}~Qed.}}
\only&lt;15&gt;{%
  \textup{Coq~{&lt;}~Qed.}\\
  intro~H.\\
  intro~q.\\
  intro~p.\\
  apply~H.\\
  assumption.\\
  assumption.\\
  imp\_perm~is~defined\\
  \medskip
  \textup{Coq~{&lt;}~}}
\end{overlayarea}
\end{block}
\begin{block}{}
%
% derivation tree
%
\begin{overprint}
\begin{gather*}
\only&lt;1-2&gt;	{\drv{coq-sample.0}}
\only&lt;3-4&gt;	{\drv{coq-sample.1}}
\only&lt;5-6&gt;	{\drv{coq-sample.2}}
\only&lt;7-8&gt;	{\drv{coq-sample.3}}
\only&lt;9-10&gt;	{\drv{coq-sample.4}}
\only&lt;11-12&gt;	{\drv{coq-sample.5}}
\only&lt;13-15&gt;	{\drv{coq-sample.6}}
\end{gather*}
\end{overprint}
\end{block}
\end{frame}
\end{document}
</pre></body></html>