Commit 5c323e66 authored by Gaspard Ferey's avatar Gaspard Ferey

Merge branch 'gaspard' of git.lsv.fr:fthire/LFMT into gaspard

parents 96befd6e 02d12cca
......@@ -208,8 +208,8 @@ Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
| TBound i => t
| TFree x => if var_dec x z then TBound k else t
| TApp l r => TApp (close_k l k z) (close_k r k z)
| TAbs ty te => TAbs (close_k ty k z) (close_k ty (S k) z)
| TPi ty te => TPi (close_k ty k z) (close_k ty (S k) z)
| TAbs ty te => TAbs (close_k ty k z) (close_k te (S k) z)
| TPi ty te => TPi (close_k ty k z) (close_k te (S k) z)
end.
Definition close (t : term) (z : Var) : term := close_k t 0 z.
......@@ -292,5 +292,3 @@ with well_formed : context -> Prop :=
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ).
......@@ -4,7 +4,6 @@ Require Import List.
Require Import LPTerm.
Theorem types_WF : forall Γ t u, Γ t : u -> Γ .
Proof. intros. induction H; easy. Qed.
......@@ -65,7 +64,7 @@ Qed.
Theorem fresh_vars_weaker : forall Γ Γ' x, weaker Γ Γ' -> Fresh_var Γ' x -> Fresh_var Γ x.
Proof.
intros. intro. apply H0. destruct H1.exists x0. eapply subset_var_decl. apply H. easy.
intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy.
Qed.
......@@ -79,38 +78,88 @@ Proof.
- eapply TyPi.
+ apply IHtyping. easy. easy.
+ intro. intro. apply H1. apply H4. apply WeakNextVarDecl. easy. econstructor.
*
Admitted.
Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v.
Proof. intros. intro. apply H. now left. Qed.
Theorem FV_close : forall x y t, In x (FV t) -> x <> y -> forall n, In x (FV (close_k t n y)).
Proof.
intros x y t H x_neq_y.
induction t ; try inversion H ; subst ; intros n.
- unfold close ; simpl. destruct (var_dec x y).
+ contradiction.
+ assumption.
- inversion H0.
- simpl ; apply in_or_app.
simpl in H ; apply in_app_or in H ; destruct H.
+ left ; now apply IHt1.
+ right. now apply IHt2.
- simpl ; apply in_or_app.
simpl in H ; apply in_app_or in H ; destruct H.
+ left ; now apply IHt1.
+ right. now apply IHt2.
- simpl ; apply in_or_app.
simpl in H ; apply in_app_or in H ; destruct H.
+ left ; now apply IHt1.
+ right. now apply IHt2.
Qed.
Theorem left_arr_type : forall Γ t u AB, Γ t ~> u : AB -> exists A, Γ t : A.
Proof.
intros.
remember (t ~> u) as w.
induction H ; try inversion Heqw.
- subst. exists type ; easy.
- subst. clear H2.
pose proof (IHtyping1 (eq_refl _)).
assumption.
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 Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Proof.
intros. induction t; try inversion H0.
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) v H0).
+ destruct (in_app_or (FV A) (FV B) v0 H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
-- apply H2. intro. apply H4. simpl. right. easy. 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) v H0).
+ destruct (in_app_or (FV A) (FV t) v0 H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
-- apply H4. intro. apply H6. simpl. right. easy. 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) v H0).
++ econstructor. apply H13.
+ destruct (in_app_or (FV t) (FV u) v0 H0).
* apply IHtyping1. easy.
* apply IHtyping2. easy.
+ apply IHtyping1. easy.
- contradict H1.
- destruct (in_app_or (FV t1) (FV t2) v H0).
+ apply IHt1.
- 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 FV_decl1 : forall Γ x A t u, Γ, x : A -> ~ In x (FV t) -> ~ In x (FV u) -> Γ t : u -> Γ, x: A t : u.
......@@ -136,10 +185,10 @@ Proof.
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.
......@@ -197,7 +246,7 @@ Proof.
+ 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.
......@@ -215,7 +264,7 @@ Proof.
intros.
apply (TyPi nil).
- easy.
- intros. apply TyPreserv_var_decl. 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.
......@@ -226,5 +275,3 @@ Proof.
- intros. apply TyPreserv_var_decl. apply H0.
- intros. apply TyPreserv_var_decl. apply H1.
Qed.
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