Commit 4cb8ff35 authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 841cc4d3
...@@ -236,7 +236,14 @@ Proof. ...@@ -236,7 +236,14 @@ Proof.
eapply weak_checked. eapply loccontext_WF. apply H. easy. easy. eapply weak_checked. eapply loccontext_WF. apply H. easy. easy.
Qed. 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. 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. Lemma vd_context_typ : forall Σ Γ t u, Σ; Γ t : u -> forall x A, (Σ, x : A) + Γ -> (Σ, x : A);Γ t : u.
...@@ -244,26 +251,35 @@ Proof. ...@@ -244,26 +251,35 @@ Proof.
intros. intros.
eapply weak_typ. eapply weak_typ.
- apply H. - apply H.
- econstructor. pose proof (weak_WF _ _ H0). - econstructor. pose proof (checked_WF _ _ H0).
inversion H1; subst; easy. inversion H1; subst; easy.
- eapply weak_WF. apply H0. - eapply checked_WF. apply H0.
Qed. 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) + Γ . Lemma vd_context_WF : forall Σ Γ x A, Σ + Γ -> (Σ, x : A) WF -> (Σ, x : A) + Γ .
Proof. Proof.
intros. intros.
eapply weak_checked. apply H. econstructor. inversion H0; subst; easy. easy. eapply weak_checked. apply H. econstructor. inversion H0; subst; easy. easy.
Qed. 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. Lemma vardecl_typable2 : forall Σ x A, Σ WF -> x : A Σ -> typable Σ A.
Proof. 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. ...@@ -332,10 +348,13 @@ Proof.
intros. intros.
generalize dependent H. generalize dependent H.
remember (Γ, A) as Γ'. remember (Γ, A) as Γ'.
pose proof (ex_intro (fun x => Γ'=Γ,x) A HeqΓ').
generalize dependent Γ. generalize dependent Γ.
induction H0; intros. induction H0; intros; simpl; subst.
- simpl. econstructor. inversion HeqΓ'; subst. - econstructor. exact (loc_context_cheked _ _ _ H). easy.
eapply weak_checked. - econstructor. exact (loc_context_cheked _ _ _ H).
- econstructor.
+ apply IHtyping1. easy. easy.
Admitted. Admitted.
Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u). Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u).
...@@ -353,7 +372,7 @@ Proof. ...@@ -353,7 +372,7 @@ Proof.
+ +
repeat eexists. apply H. apply H0 repeat eexists. apply H. apply H0
Admitted
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment