Commit 96626c22 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Preuve de CurryHoward pour la logique minimale.

parent fd8049c6
......@@ -83,7 +83,7 @@
\date{\today}
\begin{document}
\includegraphics[scale=0.4]{logo_ens.png} \hfill \includegraphics[scale=0.1]{logo-irif.png}
\includegraphics[scale=0.45]{logo_ens.png} \hfill \includegraphics[scale=0.1]{logo-irif.png}
\begin{center}
\vspace*{1em}
{\LARGE Rapport de stage} \\ \vspace{1em}
......@@ -138,7 +138,7 @@ Par la suite, il a été à propos d'ajouter d'autres aspects de la logique à c
L'encodage \verb+NatDed+ existant déjà avant le stage. \`A ce moment là, il contenait déjà un système de déduction naturelle avec des séquents, ainsi qu'un grand nombre de lemmes et résultats utiles, y compris sur la méta-théorie. Deux méthodes sont possibles pour établir une preuve dans cette encodage : une méthode constructive, reposant sur le prédicat \verb+Pr+ dont la définition est donnée en annexe \ref{pr}, qui permet de construire une preuve pas à pas, mais n'est pas forcément pratique à utiliser pour démontrer des résultats méta-théoriques. L'autre méthode, \verb+Valid+, permet de vérifier qu'une dérivation est bien formée (cela implique donc de fournir directement une dérivation complète, ce qui alourdi considérablement le style des preuves). Le choix qui a été fait pour stage est d'utiliser \verb+Pr+ systématiquement.
En ce qui concerne la façon d'encoder les formules de la logique du premier ordre, Pierre Letouzey avait choisi un système \emph{locally nameless}, i.e. où les variables liées sont représentées par des indices de \textsc{de Bruijn} et les variables libres par un nom du type \verb+FVar string+ (par exemple $x$ s'écrira \verb+FVar "x"+). En parallèle de cette convention, une équivalence avec un système reposant totalement sur des variables nommées était proposées, mais quoiqu'elle eût peut se révéler fort utile, cette équivalence n'a guère été utilisée pendant le stage.
En ce qui concerne la façon d'encoder les formules de la logique du premier ordre, Pierre Letouzey avait choisi un système \emph{locally nameless}, i.e. où les variables liées sont représentées par des indices de \textsc{de Bruijn} et les variables libres par un nom du type \verb+FVar string+ (par exemple $x$ s'écrira \verb+FVar "x"+). En parallèle de cette convention, une équivalence avec un système reposant totalement sur des variables nommées était proposée, mais quoiqu'elle eût peut se révéler fort utile, cette équivalence n'a guère été utilisée pendant le stage.
\medskip
\emph{A priori}, il s'agit du premier codage Coq de la déduction naturelle qui allie les trois aspects suivants :
......
......@@ -103,81 +103,26 @@ Proof.
unfold IsTheorem in *.
destruct H. destruct H0.
split.
+ unfold Wf in *.
intuition.
* assert (check th (A -> B)%form = true -> check th B = true).
{
assert (check th (A -> B)%form = check th A && check th B).
{ auto. }
assert (check th A && check th B = check th A &&& check th B).
{ apply andb_lazy_alt. }
rewrite H8 in H5.
intro.
rewrite H5 in H9.
assert (check th A = true /\ check th B = true).
{ apply andb_true_iff. rewrite H8. assumption. }
destruct H10.
assumption.
}
apply H5. assumption.
* assert (BClosed (A -> B)%form -> BClosed A /\ BClosed B).
{
intro.
unfold BClosed in *.
cbn in H5.
apply max_0 in H5.
assumption.
}
apply H5 in H0.
destruct H0.
assumption.
* assert (FClosed (A -> B)%form -> FClosed A /\ FClosed B).
{
intro.
unfold FClosed in *.
cbn in H5.
assert (forall s s', Names.Empty (Names.union s s') -> Names.Empty s /\ Names.Empty s').
{ split. namedec. namedec. }
eapply H8 in H5.
assumption.
}
apply H5 in H6.
destruct H6.
assumption.
+ rewrite Op_wf in H.
apply H.
+ destruct H1.
destruct H2.
exists (x ++ x0).
destruct H1. destruct H2.
split.
* assert (forall l l', Forall (IsAxiom th) l -> Forall (IsAxiom th) l' -> Forall (IsAxiom th) (l ++ l')).
{
intros.
induction l.
- auto.
- simpl. apply Forall_cons.
++ inversion H5. assumption.
++ apply IHl. inversion H5. assumption.
}
apply H5; assumption.
* rewrite Forall_forall in *.
intro f.
rewrite in_app_iff.
intuition.
* apply R_Imp_e with (A := A).
- apply Pr_weakening with (s := x A -> B); auto.
apply SubSeq.
assert (forall A (x : list A) x0, ListSubset x (x ++ x0)).
{ intros. induction x1.
++ unfold ListSubset. intros. inversion H5.
++ unfold ListSubset. intros. inversion H5.
** rewrite H6. simpl. apply in_eq.
** simpl. right. apply IHx1. assumption.
}
apply H5.
apply SubSeq. red.
intro f.
rewrite in_app_iff. intuition.
- apply Pr_weakening with (s := x0 A); auto.
apply SubSeq.
assert (forall A (x : list A) x0, ListSubset x0 (x ++ x0)).
{ intros. induction x1.
++ unfold ListSubset. intros. simpl. assumption.
++ unfold ListSubset. intros. unfold ListSubset in IHx1. simpl. right. apply IHx1. assumption.
}
apply H5.
apply SubSeq. red.
intro f.
rewrite in_app_iff. intuition.
Qed.
(** We can "fix" a proof made with things not in the signature,
......
......@@ -308,7 +308,7 @@ Proof.
simp.
apply R_And_e2 in H.
apply R_Imp_e with (A := ( #0 C /\ x #0)); [ assumption | ].
apply R_Ex_i with (t := B). cbn. fold C. fold B. fold x.
apply R_Ex_i with (t := B). simp.
apply R_And_i.
-- set (Ax2 := _ <-> _). inst_axiom Ax2 [ B ].
simp.
......@@ -318,4 +318,12 @@ Proof.
inst_axiom eq_refl [ B ].
-- apply R'_Ax.
Qed.
\ No newline at end of file
Lemma Succ : IsTheorem Intuiti ZF
(∀∃∀ (#0 #1 <-> #0 = #2)
-> ∀∀∃∀ (#0 #1 <-> #0 #3 \/ #0 #2)
-> ∀∃ succ (#1) (#0)).
Admitted.
Lemma Successor : IsTheorem Intuiti ZF (∀∃ succ (#1) (#0)).
Admitted.
\ No newline at end of file
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