From 301fa1cab820b1974b53016de4da2708474963ac Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Mon, 17 Sep 2018 16:50:47 +0200 Subject: [PATCH] Fixed some proofs. --- Coq/LPTerm.v | 1 - Coq/WF.v | 163 +++-------------------------------------------- Coq/conversion.v | 72 +-------------------- Coq/properties.v | 7 +- 4 files changed, 17 insertions(+), 226 deletions(-) diff --git a/Coq/LPTerm.v b/Coq/LPTerm.v index aabd3ce..45332e7 100644 --- a/Coq/LPTerm.v +++ b/Coq/LPTerm.v @@ -243,7 +243,6 @@ Fixpoint close_k (t : term) (k : nat) (z : Var) : term := Definition close (t : term) (z : Var) : term := close_k t 0 z. -Notation "A '~>' B" := (TPi A B) (at level 22, right associativity). Notation "x ';' A '~>' B" := (TPi A (close B x)) (at level 22, A at level 21, right associativity). Notation "x ';' A '=>' B" := (TAbs A (close B x)) (at level 22, A at level 21, right associativity). diff --git a/Coq/WF.v b/Coq/WF.v index 541f7d5..f1bf528 100644 --- a/Coq/WF.v +++ b/Coq/WF.v @@ -253,10 +253,10 @@ Proof. + right. now apply IHt2. Qed. -Theorem left_arr_type : forall Γ t u AB, Γ ⊢ t ~> u : AB -> exists A, Γ ⊢ t : A. +Theorem left_arr_type : forall Γ t u AB, Γ ⊢ Π t ~ u : AB -> exists A, Γ ⊢ t : A. Proof. intros. - remember (t ~> u) as w. + remember (Π t ~ u) as w. induction H ; try inversion Heqw. - subst. exists type ; easy. - subst. clear H2. @@ -337,161 +337,16 @@ Proof. Qed. - -Theorem FV_decl1 : forall Γ t u, Γ ⊢ t : u -> forall v, In v (FV t) -> v ∈ Γ. -Proof. - intros Γ t ; revert Γ ; induction t; intros ; try inversion H0. - - subst. induction H. - + inversion H0. subst. exists A ; easy. inversion H2. - + inversion H0. - + destruct (in_app_or (FV A) (FV B) v0 H0). - * apply IHtyping. easy. - * destruct (var_inf (v0 :: L)). assert (Defined_var (Γ, x : A) v0). - -- apply H2. intro. apply H4. simpl. right. easy. - assert (x <> v0) by (apply (not_in_not_eq _ _ _ H4)). - apply FV_close ; [assumption | now apply not_eq_sym]. - -- induction H5. inversion H5 ; subst. - ++ contradict H4. simpl. auto. - ++ econstructor. apply H11. - + destruct (in_app_or (FV A) (FV t) v0 H0). - * apply IHtyping. easy. - * destruct (var_inf (v0 :: L)). assert (Defined_var (Γ, x : A) v0). - -- apply H4. intro. apply H6. simpl. right. easy. - assert (x <> v0) by (apply (not_in_not_eq _ _ _ H6)). - apply FV_close ; [assumption | now apply not_eq_sym]. - -- induction H7. inversion H7; subst. - ++ contradict H6. simpl. auto. - ++ econstructor. apply H13. - + destruct (in_app_or (FV t) (FV u) v0 H0). - * apply IHtyping1. easy. - * apply IHtyping2. easy. - + apply IHtyping1. easy. - - contradict H1. - - simpl in H0. - pose proof (left_arr_type Γ t1 t2 u H). - destruct H1. - apply in_app_or in H0 ; destruct H0. - + eapply IHt1 ; eassumption. - + admit. - - admit. - - admit. -Qed. - -Theorem right_arr_type : forall Γ t u AB, Γ ⊢ t ~> u : AB -> - exists A L, forall x, ~In x L -> Γ, x : A ⊢ close u x : type \/ u = type . -Proof. -Admitted. - -Theorem FV_decl1 : forall Γ x A t u, Γ, x : A ✓ -> ~ In x (FV t) -> ~ In x (FV u) -> Γ ⊢ t : u -> Γ, x: A ⊢ t : u. -Proof. - do 5 intro. - generalize Γ. - induction t. - - intros. remember TKind as t'. induction H2 ; inversion Heqt'. - subst. econstructor. apply IHtyping1. easy. easy. easy. - - apply TyAxiom. easy. econstructor. easy. - - apply TyType. easy. - - apply (TyPi ((FV B) ++ (FV s) ++ L)). - + apply IHtyping. easy. intro. apply H0. simpl. apply in_or_app. auto. simpl. easy. - + intros. -Qed. - - -Theorem FV_decl1 : forall Γ x A y B, - ~ In x (FV B) -> ~ In y (FV A) -> Γ, x : A, y : B ✓ -> Γ, y : B, x : A ✓. -Proof. - intros. - remember (Γ, x : A) as Γ0. - remember (Γ0, y : B) as Γ1. - induction H1. - - inversion HeqΓ1. - - - - - -Theorem FV_decl1 : forall Γ x A y B t u, Γ, x : A, y : B ✓ -> ~ In x (FV t) -> ~ In x (FV u) -> Γ ⊢ t : u -> Γ, x: A ⊢ t : u. - -Theorem FV_decl1 : forall Γ x A t u, Γ, x : A ✓ -> ~ In x (FV t) -> ~ In x (FV u) -> Γ ⊢ t : u -> Γ, x: A ⊢ t : u. -Proof. - intros. - induction H2. - - apply TyAxiom. easy. econstructor. easy. - - apply TyType. easy. - - apply (TyPi ((FV B) ++ (FV s) ++ L)). - + apply IHtyping. easy. intro. apply H0. simpl. apply in_or_app. auto. simpl. easy. - + intros. -Qed. - -Theorem WF_var_decl : forall Γ x A, Γ, x : A ✓ -> Γ ✓. -Proof. - intros. - remember (Γ, x : A) as Γ0. - induction H. - - inversion HeqΓ0. - - inversion HeqΓ0. subst. induction H. - + easy. - + easy. - + apply IHtyping. easy. - + apply IHtyping. easy. - + apply IHtyping1. easy. - + apply IHtyping1. easy. - - inversion HeqΓ0. subst. induction H. - + easy. - + easy. - + apply IHtyping. easy. - + apply IHtyping. easy. - + apply IHtyping1. easy. - + apply IHtyping1. easy. - - inversion HeqΓ0. -Qed. - -Theorem WF_rul_decl : forall Γ t u, Γ, t ≡ u ✓ -> Γ ✓. -Proof. - intros. - remember (Γ, t ≡ u) as Γ0. - induction H. - - inversion HeqΓ0. - - inversion HeqΓ0. - - inversion HeqΓ0. - - subst. inversion HeqΓ0. subst. easy. -Qed. - Theorem TyPreserv_var_decl : forall Γ x A c d, Γ ⊢ c : d -> Γ, x : A ✓ -> Γ, x : A ⊢ c : d. Proof. - intros. - induction H. - - apply TyAxiom. easy. constructor. easy. - - apply TyType. easy. - - apply (TyPi (x :: L)). - + apply IHtyping. easy. - + intros. - assert (Γ, x0 : A0 ⊢ B : s). apply (H1 x0). intro. apply H3. right. easy. - - remember (Γ, x0 : A0) as Γ0. - induction H4. - * subst. - inversion H5. - -- subst. apply TyAxiom. constructor. + intros. eapply weak_typ. + apply H. econstructor. + inversion H0; subst. easy. easy. easy. Qed. -Theorem TyPreserv_rul_decl : forall Γ t u c d, Γ ⊢ c : d -> Γ, t ≡ u ⊢ c : d. +Theorem TyPreserv_rul_decl : forall Γ t u c d, Γ ⊢ c : d -> Γ, t ≡ u ✓ -> Γ, t ≡ u ⊢ c : d. Proof. -Admitted. - - -Theorem TyPi2 : forall Γ A B s, Γ ⊢ A : type -> Γ ⊢ B : s -> Γ ⊢ Π A ~ B : s. -Proof. - intros. - apply (TyPi nil). - - easy. - - intros. apply TyPreserv_var_decl. easy. -Qed. - -Theorem TyAbs2 : forall Γ A B s t, Γ ⊢ A : type -> Γ ⊢ B : s -> Γ ⊢ t : B -> Γ ⊢ λ A ~ t : Π A ~ B. -Proof. - intros. - eapply (TyAbs nil). - - easy. - - intros. apply TyPreserv_var_decl. apply H0. - - intros. apply TyPreserv_var_decl. apply H1. + intros. eapply weak_typ. + apply H. econstructor. + inversion H0; subst. easy. Qed. diff --git a/Coq/conversion.v b/Coq/conversion.v index 75b74a6..4e5cd5c 100644 --- a/Coq/conversion.v +++ b/Coq/conversion.v @@ -12,11 +12,6 @@ Proof. easy. Qed. -Lemma inversion_typing : forall Γ t A, Γ ⊢ t : A -> Γ ✓. -Proof. - intros. induction H ; easy. -Qed. - Lemma inversion_rel : forall Γ t u, Γ ✓ -> t ≡ u ∈ Γ -> exists s A Δ, Δ ⊢ t : A /\ Δ ⊢ u : A /\ Δ ⊢ A : s. Proof. intros. @@ -24,76 +19,15 @@ Proof. - inversion H0. - inversion H. subst. inversion H0 ; subst. apply IHΓ. - + eapply WF_var_decl. apply H. + + eapply vardecl_WF. apply H. + easy. - + eapply IHΓ. eapply WF_var_decl. apply H. inversion H0. subst. easy. + + eapply IHΓ. eapply vardecl_WF . apply H. inversion H0. subst. easy. - inversion H0; subst. inversion H ; subst. + exists s,A,Γ. split. apply H5. split. apply H6. apply H4. - + apply IHΓ. eapply WF_rul_decl. apply H. easy. -Qed. - -Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A ⊢ t →β u -> Γ ⊢ t →β u. -Proof. - intros. induction H; econstructor. -Qed. - -Lemma context_var_conv_Γ2 : forall Γ x A t u, Γ, x : A ⊢ t →Γ u -> Γ ⊢ t →Γ u. -Proof. - intros. - remember (Γ, x : A) as Γ0. - induction H. rewrite HeqΓ0 in H. - inversion H. subst. econstructor. easy. -Qed. - -Lemma context_var_conv_β : forall Γ x A t u, Γ, x : A ⊢ t ↪β u -> Γ ⊢ t ↪β u. -Proof. - intros. - remember (Γ, x : A) as Γ0. - induction H; rewrite HeqΓ0 in H. - - econstructor. induction H. econstructor. - - apply CCApp1. apply (context_var_conv_β2 Γ x A). easy. - - apply CCApp2. apply (context_var_conv_β2 Γ x A). easy. - - apply CCAbs1. apply (context_var_conv_β2 Γ x A). easy. - - apply CCAbs2. apply (context_var_conv_β2 Γ x A). easy. - - apply CCPi1. apply (context_var_conv_β2 Γ x A). easy. - - apply CCPi2. apply (context_var_conv_β2 Γ x A). easy. -Qed. - -Lemma context_var_conv_Γ : forall Γ x A t u, Γ, x : A ⊢ t ↪Γ u -> Γ ⊢ t ↪Γ u. -Proof. - intros. - remember (Γ, x : A) as Γ0. - induction H; rewrite HeqΓ0 in H. - - econstructor. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCApp1. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCApp2. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCAbs1. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCAbs2. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCPi1. apply (context_var_conv_Γ2 Γ x A). easy. - - apply CCPi2. apply (context_var_conv_Γ2 Γ x A). easy. -Qed. - -Lemma context_var_conv_βΓ : forall Γ x A t u, Γ, x : A ⊢ t ↪βΓ u -> Γ ⊢ t ↪βΓ u. -Proof. - intros. - remember (Γ, x : A) as Γ0. - destruct H. - - left ; eapply context_var_conv_β ; now rewrite <- HeqΓ0. - - right ; eapply context_var_conv_Γ ; now rewrite <- HeqΓ0. -Qed. - -Lemma context_var_conv : forall Γ x A t u, Γ, x : A ⊢ t ≡ u -> Γ ⊢ t ≡ u. -Proof. - intros. - remember (Γ, x : A) as Γ0. - induction H. - - econstructor. - - eapply CVSym ; now eapply IHRSTClosure. - - eapply CVTrans ; [eapply IHRSTClosure1 | eapply IHRSTClosure2] ; easy. - - eapply CVRule ; eapply context_var_conv_βΓ ; now rewrite <- HeqΓ0. + + apply IHΓ. eapply ruldecl_WF. apply H. easy. Qed. diff --git a/Coq/properties.v b/Coq/properties.v index 519b662..6c94649 100644 --- a/Coq/properties.v +++ b/Coq/properties.v @@ -5,9 +5,12 @@ Require Import conversion. Inductive Sort : Set := SKind | SType | SObject. -Definition - +Theorem kind_not_typable : forall Γ T, Γ ⊢ kind : T -> False. +Proof. + intros. + induction H. +Admitted. Lemma not_var_kind_gamma : forall Γ x, Γ ✓ -> x : kind ∈ Γ -> False. Proof. -- 2.24.1