Require Import LPTerm. 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. 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. 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. 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 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. 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. 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. - 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. + (* 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. Lemma type_kind : forall Γ A, Γ ⊢ type : A -> A = kind. Proof. intros. remember type as x. induction H ; try inversion Heqx. - easy. - apply IHtyping1 in H2. pose proof (inversion_typing Γ t A H). subst. pose proof (inverse_kind Γ B H3 kind H1). now apply H2. Qed.