Commit 4c1f59b0 authored by François Thiré's avatar François Thiré

fix bug in close_k + fix proof

parent 079f6d5b
......@@ -160,8 +160,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.
......@@ -243,4 +243,3 @@ with well_formed : context -> Prop :=
| WFVarK : forall Γ x A, Fresh_var Γ x -> Γ A : kind -> Γ, x : A
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ).
......@@ -4,6 +4,37 @@ Require Import List.
Require Import LPTerm.
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 FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Proof.
intros. induction t; try inversion H0.
......@@ -13,7 +44,8 @@ Proof.
+ destruct (in_app_or (FV A) (FV B) v H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
-- apply H2. intro. apply H4. simpl. right. easy. easy.
-- apply H2. intro. apply H4. simpl. right. easy.
assert (x <> v) by (apply (not_in_not_eq _ _ _ H4)).
-- induction H5. inversion H5 ; subst.
++ contradict H4. simpl. auto.
++ econstructor. apply H11.
......@@ -56,10 +88,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.
......@@ -117,7 +149,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.
......@@ -135,7 +167,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.
......@@ -146,5 +178,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