Commit 5237f34c by Gaspard Ferey

### WIP

parent 4a8ab344
 ... ... @@ -294,7 +294,7 @@ Notation "Γ '⊢' t '≡β' u" := ((RSTClosure RW_Beta ) Γ t u) (at lev Notation "Γ '⊢' t '≡Γ' u" := ((RSTClosure RW_Gamma ) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '≡βΓ' u" := ((RSTClosure RW_Beta_Gamma) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '≡' u" := (Γ ⊢ t ≡βΓ u) (at level 40, t at level 25). Notation "Γ '⊢' t '≡' u" := (Γ ⊢ t ≡βΓ u) (at level 40, t at level 25). Reserved Notation "Γ '⊢' t ':' A" (at level 40, t at level 25). Reserved Notation "Γ ✓" (at level 40). ... ...
 ... ... @@ -3,15 +3,6 @@ Require Import LPTerm. Require Import WF. Lemma no_type_kind : forall Γ A, Γ ⊢ kind : A -> False. Proof. intros. remember kind as x. induction H ; try inversion Heqx. apply IHtyping1. easy. Qed. Lemma inversion_rel : forall Γ t u, Γ ✓ -> t ≡ u ∈ Γ -> exists s A Δ, Δ ⊢ t : A /\ Δ ⊢ u : A /\ Δ ⊢ A : s. Proof. intros. ... ...
 Require Import LPTerm. Require Import WF. Require Import conversion. Inductive Sort : Set := SKind | SType | SObject. Theorem kind_not_typable2 : forall Γ T t, Γ ⊢ t : T -> ~ (t = kind). Proof. intros. induction H; try easy. Qed. Theorem kind_not_typable : forall Γ T, Γ ⊢ kind : T -> False. Proof. intros. pose proof (kind_not_typable2 _ _ _ H). easy. Qed. Lemma not_var_kind_gamma : forall Γ x, Γ ✓ -> x : kind ∈ Γ -> False. Lemma not_var_kind_gamma : forall Γ x, Γ ✓ -> ~ (x : kind ∈ Γ). Proof. induction Γ ; intros. - inversion H0. - inversion H0 ; subst. + inversion H ; subst. inversion H3 ; subst. eapply no_type_kind ; eassumption. + inversion H ; subst ; eapply IHΓ ; eassumption. - inversion H0 ; subst ; inversion H ; subst ; eapply IHΓ ; eassumption. intros. intro. remember (kind) as K. induction H0. - remember (Γ, x : A) as Γ'. destruct H; inversion HeqΓ'. + subst. apply (kind_not_typable _ _ H0). + subst. apply (kind_not_typable _ _ H0). - apply IHInCtx. eapply vardecl_WF. apply H. easy. -apply IHInCtx. eapply ruldecl_WF. apply H. easy. Qed. Lemma not_rel_kind_gamma_left : forall Γ t, Γ, kind ≡ t ✓ -> False. Proof. intros Γ t H ; inversion H ; subst ; eapply no_type_kind ; eassumption. Qed. Proof. intros; inversion H ; subst ; eapply kind_not_typable ; 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. Proof. intros; inversion H ; subst ; eapply kind_not_typable ; eassumption. Qed. Lemma rel_kind_in_left : forall Γ t, Γ ✓ -> kind ≡ t ∈ Γ -> 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_left ; eassumption. + eapply IHΓ. * now inversion Γwf. * eassumption. intros. remember (kind) as K. induction H0; subst. - eapply not_rel_kind_gamma_left. apply H. - apply IHInRelCtx. eapply vardecl_WF. apply H. easy. - apply IHInRelCtx. eapply ruldecl_WF. apply H. easy. 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. intros. remember (kind) as K. induction H0; subst. - eapply not_rel_kind_gamma_right. apply H. - apply IHInRelCtx. eapply vardecl_WF. apply H. easy. - apply IHInRelCtx. eapply ruldecl_WF. apply H. easy. Qed. Inductive of_typed_kind : term -> Prop := | IKType : of_typed_kind type | IKPiType : forall A B, of_typed_kind B -> of_typed_kind (Π A ~ B). Lemma inhabit_kind : forall Γ t, Γ ✓ -> Γ ⊢ t : kind -> of_typed_kind t. Theorem conv_kind_not_typable : forall Γ t T, Γ ⊢ t : T -> ~ (Γ ⊢ t ≡ T). Proof. intros. remember kind as x. induction H0 ; subst. - exfalso ; eapply not_var_kind_gamma ; eassumption. - constructor. - assert (Γ, x : A ✓). constructor ; eassumption. pose proof (IHtyping2 H0 eq_refl). now constructor. - inversion Heqx. - intros. intro. induction H0. Qed. Lemma inverse_kind : forall Γ t, Γ ✓ -> forall u, Γ ⊧ u ≡ t -> u = kind <-> t = kind. Lemma kind_conv : forall Γ t T, Γ ⊢ t : T -> Γ ⊢ type ≡ t -> type = t. Proof. intros. induction H0. remember kind as K. induction H. - easy. - split ; intro. apply IHConv2 ; now apply IHConv1. apply IHConv1 ; now apply IHConv2. - split ; intro ; now apply IHConv. - split ; intro. + inversion H0. + (* FALSE because t and u might not be typable *) admit. - 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. - subst; try easy. Lemma type_kind : forall Γ A, Γ ⊢ type : A -> A = kind. Proof. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!