From 4cb8ff35bb1b6ba74d72106f9f006868dd55a2b9 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Thu, 20 Sep 2018 11:45:06 +0200 Subject: [PATCH] WIP --- Coq/full_db/WF.v | 47 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 33 insertions(+), 14 deletions(-) diff --git a/Coq/full_db/WF.v b/Coq/full_db/WF.v index 2744784..15f6aba 100644 --- a/Coq/full_db/WF.v +++ b/Coq/full_db/WF.v @@ -236,7 +236,14 @@ Proof. eapply weak_checked. eapply loccontext_WF. apply H. easy. easy. Qed. -Theorem weak_WF : forall Σ Γ, Σ + Γ ✓ -> Σ WF. +Theorem weak_typable : forall Σ Σ' t, Σ' WF -> Σ ⊂ Σ' -> typable Σ t -> typable Σ' t. +Proof. + intros. + inversion H1. inversion H2. + repeat eexists. eapply weak_typ. apply H3. easy. easy. +Qed. + +Theorem checked_WF : forall Σ Γ, Σ + Γ ✓ -> Σ WF. Proof. intros. induction Γ; inversion H; subst; try apply IHΓ; try easy. Qed. Lemma vd_context_typ : forall Σ Γ t u, Σ; Γ ⊢ t : u -> forall x A, (Σ, x : A) + Γ ✓ -> (Σ, x : A);Γ ⊢ t : u. @@ -244,26 +251,35 @@ Proof. intros. eapply weak_typ. - apply H. - - econstructor. pose proof (weak_WF _ _ H0). + - econstructor. pose proof (checked_WF _ _ H0). inversion H1; subst; easy. - - eapply weak_WF. apply H0. + - eapply checked_WF. apply H0. Qed. +Lemma loc_context_cheked : forall Σ Γ A, Σ + (Γ, A) ✓ -> Σ + Γ ✓. +Proof. intros. inversion H; subst. easy. Qed. + Lemma vd_context_WF : forall Σ Γ x A, Σ + Γ ✓ -> (Σ, x : A) WF -> (Σ, x : A) + Γ ✓. Proof. intros. eapply weak_checked. apply H. econstructor. inversion H0; subst; easy. easy. Qed. -Lemma weak_typable : forall Σ x A t, (Σ, x : A) WF -> typable Σ t -> typable (Σ, x : A) t. -Proof. - intros. destruct H0. destruct H0. eexists. eexists. - eapply weak_typ. apply H0. econstructor. inversion H; easy. easy. -Qed. - Lemma vardecl_typable2 : forall Σ x A, Σ WF -> x : A ∈ Σ -> typable Σ A. Proof. -Admitted. + intros. + generalize dependent H. + induction H0; intros. + - assert (typable Σ A). + + inversion H; subst. + * repeat eexists. apply H4. + * repeat eexists. apply H4. + + eapply weak_typable. easy. apply WeakVarDecl. inversion H; subst; easy. easy. + - eapply weak_typable. easy. apply WeakVarDecl. inversion H1; subst; easy. apply IHInCtx. + inversion H1; easy. + - eapply weak_typable. easy. apply WeakRulDecl. apply IHInCtx. + inversion H; easy. +Qed. @@ -332,10 +348,13 @@ Proof. intros. generalize dependent H. remember (Γ, A) as Γ'. + pose proof (ex_intro (fun x => Γ'=Γ,x) A HeqΓ'). generalize dependent Γ. - induction H0; intros. - - simpl. econstructor. inversion HeqΓ'; subst. - eapply weak_checked. + induction H0; intros; simpl; subst. + - econstructor. exact (loc_context_cheked _ _ _ H). easy. + - econstructor. exact (loc_context_cheked _ _ _ H). + - econstructor. + + apply IHtyping1. easy. easy. Admitted. Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u). @@ -353,7 +372,7 @@ Proof. + repeat eexists. apply H. apply H0 - +Admitted -- 2.24.1