Commit d929c4c8 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Enrichissement du lambda calcul avec la conjonction.

parent b93cf0be
(* A link with Lambda Calculus. *)
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs Mix List.
Import ListNotations.
Open Scope list.
Inductive term :=
| Var : nat -> term
| App : term -> term -> term
| Abs : term -> term
| Nabla : term -> term.
| Nabla : term -> term
| Couple : term -> term -> term
| Pi1 : term -> term
| Pi2 : term -> term.
Inductive type :=
| Arr : type -> type -> type
| Atom : name -> type
| Bot : type.
| Bot : type
| And : type -> type -> type.
Definition context := list type.
Inductive typed : context -> term -> type -> Prop :=
| Type_Ax : forall Γ τ n, nth_error Γ n = Some τ -> typed Γ (Var n) τ
| Type_App : forall Γ u v σ μ, typed Γ u (Arr σ μ) -> typed Γ v σ -> typed Γ (App u v) μ
| Type_Abs : forall Γ u σ μ, typed (σ :: Γ) u μ -> typed Γ (Abs u) (Arr σ μ)
| Type_Nabla : forall Γ u τ, typed Γ u Bot -> typed Γ (Nabla u) τ.
| Type_Var : forall Γ τ n, nth_error Γ n = Some τ -> typed Γ (Var n) τ
| Type_App : forall Γ u v σ τ, typed Γ u (Arr σ τ) -> typed Γ v σ -> typed Γ (App u v) τ
| Type_Abs : forall Γ u σ τ, typed (σ :: Γ) u τ -> typed Γ (Abs u) (Arr σ τ)
| Type_Nabla : forall Γ u τ, typed Γ u Bot -> typed Γ (Nabla u) τ
| 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) τ.
Notation "u @ v" := (App u v) (at level 20) : lambda_scope.
Notation "∇ u" := (Nabla u) (at level 20) : lambda_scope.
Notation "σ -> μ" := (Arr σ μ) : lambda_scope.
Notation "u , v" := (Couple u v) (at level 20) : lambda_scope.
Notation "σ -> τ" := (Arr σ τ) : lambda_scope.
Notation "σ /\ τ" := (And σ τ) : lambda_scope.
Notation "# n" := (Var n) (at level 20, format "# n") : lambda_scope.
Delimit Scope lambda_scope with lam.
......@@ -43,6 +54,7 @@ Fixpoint to_form (t : type) : formula :=
| Arr u v => ((to_form u) -> (to_form v))%form
| Atom a => Pred a []
| Bot => False
| And u v => ((to_form u) /\ (to_form v))%form
end.
Definition to_ctxt (Γ : context) := List.map to_form Γ.
......@@ -87,7 +99,7 @@ Proof.
- intros.
inversion H. clear Γ0 u0 H1 H0.
rewrite<- H3 in H. clear H3.
specialize IHu with (τ := μ) (Γ := σ :: Γ).
specialize IHu with (τ := τ0) (Γ := σ :: Γ).
cbn. apply R_Imp_i.
intuition.
- intros.
......@@ -95,4 +107,22 @@ Proof.
specialize IHu with (τ := Bot) (Γ := Γ). cbn in IHu.
apply R_Fa_e.
intuition.
- intros.
inversion H. clear Γ0 H2 H0 H1.
rewrite<- H4 in H. clear H4.
cbn. apply R_And_i.
+ specialize IHu1 with (τ := σ) (Γ := Γ).
intuition.
+ specialize IHu1 with (τ := τ) (Γ := Γ).
intuition.
- intros.
inversion H. clear Γ0 u0 σ H1 H0 H3.
apply R_And_e1 with (B := to_form τ0).
specialize IHu with (τ := τ /\ τ0) (Γ := Γ).
intuition.
- intros.
inversion H. clear Γ0 u0 τ0 H1 H0 H3.
apply R_And_e2 with (A := to_form σ).
specialize IHu with (τ := σ /\ τ) (Γ := Γ).
intuition.
Qed.
\ No newline at end of file
......@@ -50,7 +50,6 @@
\newcommand{\NJ}{\mathsf{NJ}_1}
\newcommand{\NK}{\mathsf{NK}_1}
\newcommand{\fonc}[5]{#1 :
\left|
\begin{array}{ccc}
......@@ -136,7 +135,7 @@ Le but du stage a été d'enrichir l'encodage de \verb+NatDed+ déjà existant,
\verb+NatDed+ étant à l'origine assez rustique, il était pédagogiquement intéressant de le rendre plus \textit{user-friendly}, mais aussi d'ajouter un certain nombre d'exemples et d'applications (la théorie $\ZF$ par exemple), qui manquaient au projet initial.
Par la suite, il a été à propos d'ajouter d'autres aspects de la logique à cet encodage, tels que le $\lambda$-calcul, la théorie des ensembles et éventuellement la logique intuitionniste (en particulier les modèles de Kripke), qui sont tous des point abordés dans le cours donné par Pierre Letouzey. En effet, le $\lambda$-calcul est un élément essentiel de la construction des assistants de preuve tels que Coq.
Par la suite, il a été à propos d'ajouter d'autres aspects de la logique à cet encodage, tels que le $\lambda$-calcul, la théorie des ensembles et éventuellement la logique intuitionniste (en particulier les modèles de \textsc{Kripke}), qui sont tous des point abordés dans le cours donné par Pierre Letouzey. En effet, le $\lambda$-calcul est un élément essentiel de la construction des assistants de preuve tels que Coq.
\subsection{Encodage existant et état de l'art}
......@@ -244,7 +243,7 @@ Par ailleurs, les débuts de preuve avaient tendance à être particulièrement
Quelques propriétés utiles étaient par ailleurs sans cesse utilisées. Si la transitivité et la symétrie de l'égalité font partie de toute théorie égalitaire qui se respecte, le besoin de règles de dérivation telles que \begin{prooftree*}
\hypo{\Gamma \vdash u = v}
\infer1[sym]{\Gamma \vdash v = u}
\end{prooftree*} se fait cruellement ressentir. En l'état, l'utilisation de l'axiome de symétrie de l'égalité nécessitait d'avoir recours à la tactique \verb+assert+ pour rajouter un jugement précisant que le séquent $\PA \vdash \forall x \forall y, x = y \Rightarrow y = x$ était dérivable, puis d'utiliser les règles d'élimination adéquates. Il en va de même pour les axiomes du type $\forall x \forall y, x = y \Rightarrow \Succ (x) = \Succ (y)$.
\end{prooftree*} se fait cruellement ressentir. En l'état, l'utilisation de l'axiome de symétrie de l'égalité nécessitait d'avoir recours à la tactique \verb+assert+ pour rajouter un jugement précisant que le séquent $\PA \vdash \forall x \forall y, x = y \Rightarrow y = x$ est dérivable, puis d'utiliser les règles d'élimination adéquates. Il en va de même pour les axiomes du type $\forall x \forall y, x = y \Rightarrow \Succ (x) = \Succ (y)$.
Enfin, certaines tactiques et règles définies dans l'encodage de \verb+NatDed+ étaient passablement pénibles à utiliser. Entre autres, on peut citer \verb+R_All_i+, la règle d'introduction du quantificateur universel, qui engendrait un grand nombre de buts ennuyants à démontrer. On peut également mentionner tous les résultats faisant intervenir des ensembles finis, par exemple le lemme d'affaiblissement, car la représentation de ces ensembles en Coq est surprenante et se prête fort mal à des tactiques de simplification usuelles telles que \verb+cbn+ ou \verb+omega+.
......@@ -252,8 +251,14 @@ Enfin, certaines tactiques et règles définies dans l'encodage de \verb+NatDed+
Afin de régler les susmentionnés problèmes, j'ai mis au point un certain nombre de tactiques censées rendre les preuves plus courtes et plus lisibles, en somme plus proches des preuves que l'ont ferait sur papier. L'objectif ultime étant que l'on puisse facilement voir émerger l'arbre de dérivation du séquent que l'on est en train de démontrer. Afin de constater l'apport de ces nouvelles tactiques, une mise en regard des preuves du lemme \verb+ZeroRight+ avant et après simplifications et proposée en annexe \ref{beforeafter_zeroright}.
\subsubsection{Pour les débuts de preuve}
% Parler de la généralité de la tactique rec
\subsubsection{Pour raccourcir certains raisonnements}
\subsubsection{Pour utiliser des lemmes auxiliaires}
\section{Théorie des ensembles de {\sc Zermelo-Fraenkel}}
......@@ -340,15 +345,15 @@ Inductive Pr (l:logic) : sequent -> Prop :=
La syntaxe des $\lambda$-termes est la suivante :
\begin{align*}
u, v, \ldots ::&= x & \text{variable}\\
u, v, \ldots ::&= x, y, \ldots & \text{variables}\\
&| \; uv & \text{application} \\
&| \; \lambda x \cdot u & \text{abstraction} \\
&| \; \nabla u & \text{erreur} \\
&| \; \nabla u & \text{nabla} \\
&| \; \langle u, v \rangle & \text{couple} \\
&| \; \pi_1 u & \text{première projection} \\
&| \; \pi_2 u & \text{seconde projection}
\end{align*} et celle des types est \begin{align*}
\sigma, \tau, \ldots ::&= a & \text{variable de type} \\
\sigma, \tau, \ldots ::&= a, b, \ldots & \text{variables de type} \\
&| \; \sigma \Rightarrow \tau & \text{type flèche} \\
&| \; \bot & \text{faux} \\
&| \; \sigma \wedge \tau & \text{type conjonction}.
......@@ -357,7 +362,7 @@ u, v, \ldots ::&= x & \text{variable}\\
Les règles de typage sont :
\[ \begin{array}{lcr}
\text{\begin{prooftree}
\infer0[ax]{\Gamma, x : \tau \vdash x : \tau}
\infer0[var]{\Gamma, x : \tau \vdash x : \tau}
\end{prooftree}} & &
\text{\begin{prooftree}
\hypo{\Gamma \vdash u : \sigma \Rightarrow \tau}
......
......@@ -3,7 +3,6 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import ROmega.
Require Import Defs NameProofs Mix Meta Theories PreModels Models Peano.
Import ListNotations.
Local Open Scope bool_scope.
......
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