Commit 301fa1ca by Gaspard Ferey

### Fixed some proofs.

parent 2558937b
 ... ... @@ -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). ... ...
 ... ... @@ -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.
 ... ... @@ -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.
 ... ... @@ -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. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!