Commit 05190ea1 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Fin CurryHoward + ajustement rapport.

parent 0be0f0f1
......@@ -37,8 +37,8 @@ Inductive typed : context -> term -> type -> Prop :=
| Type_Couple : forall Γ u v σ τ, typed Γ u σ -> typed Γ v τ -> typed Γ (Couple u v) (And σ τ)
| Type_Pi1 : forall Γ u σ τ, typed Γ u (And σ τ) -> typed Γ (Pi1 u) σ
| Type_Pi2 : forall Γ u σ τ, typed Γ u (And σ τ) -> typed Γ (Pi2 u) τ
| Type_Case : forall Γ u v1 v2 τ1 τ2 σ, typed Γ u (Or τ1 τ2) -> typed Γ v1 (Arr τ1 σ)
-> typed Γ v2 (Arr τ2 σ) -> typed Γ (Case u v1 v2) σ
| Type_Case : forall Γ u v1 v2 τ1 τ2 σ, typed Γ u (Or τ1 τ2) -> typed (τ1 :: Γ) v1 σ
-> typed (τ2 :: Γ) v2 σ -> typed Γ (Case u v1 v2) σ
| Type_I1 : forall Γ u σ τ, typed Γ u σ -> typed Γ (I1 u) (Or σ τ)
| Type_I2 : forall Γ u σ τ, typed Γ u τ -> typed Γ (I2 u) (Or σ τ).
......@@ -82,6 +82,7 @@ Proof.
- apply R_And_i; intuition.
- apply R_And_e1 with (B := to_form τ). intuition.
- apply R_And_e2 with (A := to_form σ). intuition.
- apply R_Or_e with (A := to_form τ1) (B := to_form τ2); intuition; cbn in *.
+
- apply R_Or_e with (A := to_form τ1) (B := to_form τ2); intuition.
- apply R_Or_i1 with (B := to_form τ). intuition.
- apply R_Or_i2 with (A := to_form σ). intuition.
Qed.
\ No newline at end of file
......@@ -290,7 +290,7 @@ Lemma AntiHereditarity :
Pr logic (Γ ⊢ A = B).
\end{minted}
Une fois ces résultats établis, j'ai facilement pu créer les tactiques qui nous intéressaient, où il s'agissait essentiellement d'appliquer le théorème idoine et de simplifier à l'aide de tactiques de calcul spécifiques, telles que \verb+calc+ ou \verb+cbm+ qui ont été écrites par Pierre Letouzey pour faciliter la manipulation d'ensembles finis et de listes.
Une fois ces résultats établis, j'ai facilement pu créer les tactiques qui nous intéressaient, où il s'agissait essentiellement d'appliquer le théorème idoine et de simplifier à l'aide de tactiques de calcul spécifiques, telles que \verb+calc+ ou \verb+cbm+, qui ont été écrites par Pierre Letouzey pour faciliter la manipulation d'ensembles finis et de listes.
\smallskip
% TODO
......@@ -329,6 +329,9 @@ Grâce à ce résultat, la preuve d'un théorème $\phi$ utilisant des lemmes au
Cette partie reprend les concepts et les constructions du cours de $\lambda$-calcul de Jean Goubault-Larrecq \cite{polylam}. Par ailleurs, on se placera toujours dans le cadre de la \emph{logique intuitionniste}.
% TODO
% on utilise la preuve pour redémontrer le premier résultat démontré dans le stage
\subsubsection{Logique minimale intuitionniste}
\subsubsection{Faux et opérateur $\nabla$}
......@@ -509,7 +512,7 @@ u, v, \ldots ::&= x, y, \ldots & \text{variables}\\
&| \; \langle u, v \rangle & \text{couple} \\
&| \; \pi_1 u & \text{première projection} \\
&| \; \pi_2 u & \text{seconde projection} \\
&| \; \mathtt{case} \, u \, \mathtt{of} \, v_1 \; | \; v_2 & \text{filtrage par motif} \\
&| \; \mathtt{case} \, u \, \mathtt{of} \, \iota_1 x_1 \mapsto v_1 \; | \; \iota_2 x_2 \mapsto v_2 & \text{filtrage par motif} \\
&| \; \iota_1 u & \text{première injection} \\
&| \; \iota_2 u & \text{seconde injection}
\end{align*} et celle des types est \begin{align*}
......@@ -558,9 +561,9 @@ Les règles de typage sont :
\text{
\begin{prooftree}
\hypo{\Gamma \vdash u : \sigma \vee \tau}
\hypo{\Gamma \vdash v_1 : \sigma \Rightarrow \mu}
\hypo{\Gamma \vdash v_2 : \tau \Rightarrow \mu}
\infer3[pattern]{\Gamma \vdash \mathtt{case} \, u \, \mathtt{of} \, v_1 \; | \; v_2 : \mu}
\hypo{\Gamma, x_1 : \sigma \vdash v_1 : \mu}
\hypo{\Gamma, x_2 : \tau \vdash v_2 : \mu}
\infer3[pattern]{\Gamma \vdash \mathtt{case} \, u \, \mathtt{of} \, \iota_1 x_1 \mapsto v_1 \; | \; \iota_2 x_2 \mapsto v_2 : \mu}
\end{prooftree}} \\
& \\
\text{
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment