Commit ae8b4805 authored by François Thiré's avatar François Thiré

There is still an issue

parent fdb4d4f0
yu(** Start to implement lambda pi modulo with pretty printing.
(** Start to implement lambda pi modulo with pretty printing.
TODO:
- Have a better pretty printing for binders
- no substitution
......@@ -61,18 +61,16 @@ Reserved Notation "Γ '⊢' t ':' A" (at level 45, t at level 55, A at level 55)
Reserved Notation "Γ ✓" (at level 100).
Reserved Notation "Γ ⊧ t '≡' u" (at level 50, t at level 45).
Inductive Beta : term -> term -> Prop := .
Definition substk (t u : term) (k : nat) : term := t. (* TODO *)
Inductive Conv (Γ: context) : term -> term -> Prop :=
| CVRefl : forall t, Conv Γ t t
| CVTrans : forall t u v, Conv Γ t u -> Conv Γ u v -> Conv Γ t v
| CVSym : forall t u, Conv Γ t u -> Conv Γ u t
| CVBeta : forall t u, Beta t u -> Conv Γ t u
| CVBeta : forall A t u, Conv Γ ((λ A ~ t) @ u) (substk t u 0)
| CVRel : forall t u, t u Γ -> Conv Γ t u
| CVCtx : forall t u f, Conv Γ t u -> Conv Γ (f t) (f u).
Definition substk (t u : term) (k : nat) : term := t. (* TODO *)
Notation "t '[' k '<-' u ']'" := (substk t u k) (at level 40, u at level 20).
Notation "Γ ⊧ t '≡' u" := (Conv Γ t u).
......@@ -127,12 +125,6 @@ Proof.
apply H1.
Qed.
Lemma empty_conv : forall t u, ([ ]) t u -> t = u.
Proof.
intros.
induction H ; subst ; try easy.
Qed.
Lemma context_var_conv : forall Γ x A t u, Γ, x : A t u -> Γ t u.
Proof.
intros ; induction H.
......@@ -145,15 +137,77 @@ Proof.
- now apply CVCtx.
Qed.
Lemma inverse_kind : forall Γ t, Γ -> Γ kind t -> t = kind.
Lemma not_rel_kind_gamma_left : forall Γ t, Γ ; kind t -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma not_rel_kind_gamma_right : forall Γ t, Γ ; t kind -> False.
Proof.
intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption.
Qed.
Lemma rel_kind_in_left : forall Γ t, Γ -> kind t Γ -> False.
Proof.
intros Γ.
induction Γ ; intros.
- inversion H0 ; subst ; try apply empty_conv in H0 ; try easy. rewrite H1,H0 ; easy.
- apply IHΓ.
+ now inversion H.
+ eapply context_var_conv ; eassumption.
- (* TODO: harder than expected *)
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_left ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
Lemma rel_kind_in_right : forall Γ t, Γ -> t kind Γ -> False.
Proof.
intros Γ.
induction Γ ; intros u Γwf H.
- inversion H.
- eapply IHΓ ; inversion H ; subst.
+ now inversion Γwf.
+ eassumption.
- inversion H ; subst.
+ eapply not_rel_kind_gamma_right ; eassumption.
+ eapply IHΓ.
* now inversion Γwf.
* eassumption.
Qed.
Lemma inverse_kind : forall Γ t, Γ -> forall u, Γ u t -> u = kind <-> t = kind.
Proof.
intros.
induction H0.
- easy.
- split ; intro.
apply IHConv2 ; now apply IHConv1.
apply IHConv1 ; now apply IHConv2.
- split ; intro ; now apply IHConv.
- split ; intro.
+ inversion H0.
+ (* STUCK! Not provable... *)
- inversion H0 ; split ; intro ; subst.
+ exfalso ; eapply not_rel_kind_gamma_left ; eassumption.
+ exfalso ; eapply not_rel_kind_gamma_right ; eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_left.
* inversion H ; subst ; eassumption.
* eassumption.
+ exfalso ; eapply rel_kind_in_right.
* inversion H ; subst ; eassumption.
* eassumption.
- split. admit. (* a better definition of context is needed here *)
Admitted.
Lemma type_kind : forall Γ A, Γ type : A -> A = kind.
......@@ -165,5 +219,6 @@ Proof.
- apply IHtyping1 in H2.
pose proof (inversion_typing Γ t A H).
subst.
now apply (inverse_kind Γ B H3 H1).
pose proof (inverse_kind Γ B H3 kind H1).
now apply H2.
Qed.
......@@ -141,7 +141,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{lemma}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : A$.
If $\tkind$ is already not a subterm of $t$ we are done. \\
Otherwise $t$ is neither a variable nor $\ttype$ so only three rules can be applied:
\begin{itemize}
......@@ -183,8 +183,6 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
Same proof as the precedent lemma.
\end{proof}
Notice that if we want to be pedantic, the proofs above need actually to prove a mutual judgment since the congruence relation and the typing judgements are mutually defined.
% \newpage
% \section{A simple wellformedness condition}
......
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