Commit 1788e90f authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 840ba284
......@@ -7,6 +7,7 @@
Require Import PeanoNat.
Require Import List.
Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
......@@ -31,6 +32,9 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity).
Definition type : term := TType.
Definition kind : term := TKind.
(* ************ Free variables ************ *)
Fixpoint FV (t:term) : list Var :=
match t with
| TKind => nil
......@@ -42,6 +46,48 @@ Fixpoint FV (t:term) : list Var :=
| TApp t u => (FV t) ++ (FV u)
end.
Fixpoint closed (t:term) := match t with
| TKind => True
| TType => True
| TFree v => False
| TBound _ => True
| TPi A B => (closed A) /\ (closed B)
| TAbs A B => (closed A) /\ (closed B)
| TApp t u => (closed t) /\ (closed u)
end.
Theorem close_FV : forall t, (closed t) <-> (FV t) = nil.
Proof.
intro. split ; intros.
- induction t ; intros ; try easy.
+ destruct H. simpl.
assert (FV t1 = nil); auto.
assert (FV t2 = nil); auto.
rewrite H1. rewrite H2. easy.
+ destruct H. simpl.
assert (FV t1 = nil); auto.
assert (FV t2 = nil); auto.
rewrite H1. rewrite H2. easy.
+ destruct H. simpl.
assert (FV t1 = nil); auto.
assert (FV t2 = nil); auto.
rewrite H1. rewrite H2. easy.
- induction t ; try easy.
+ econstructor.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
+ econstructor.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
+ econstructor.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)).
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)).
Qed.
(* ************ Contexts ************ *)
Inductive context : Set :=
......@@ -74,6 +120,11 @@ Inductive InRelCtx : context -> term -> term -> Prop :=
| IRAfterR : forall Γ t u v w, t u Γ -> t u (Γ, v w)
where "t '≡' u ∈ Γ" := (InRelCtx Γ t u).
Definition Defined_var Γ v := exists T, v : T Γ.
Definition Fresh_var Γ v := ~ (Defined_var Γ v).
(* ************ Locally nameless representation ************ *)
Fixpoint open_k (t u : term) (k : nat) :=
match t with
| TKind => t
......@@ -184,8 +235,8 @@ Inductive typing : context -> term -> term -> Prop :=
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
| WFEmpty : [ ]
| WFVarT : forall Γ x A, Γ A : type -> Γ, x : A
| WFVarK : forall Γ x A, Γ A : kind -> Γ, x : A
| WFVarT : forall Γ x A, Fresh_var Γ x -> Γ A : type -> Γ, x : A
| 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,53 @@ Require Import List.
Require Import LPTerm.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Proof.
intros. induction H.
- inversion H0. subst. exists A ; easy. inversion H2.
- inversion H0.
- apply IHtyping.
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.
......
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