From 1788e90f0e1f87f05c604738314566e53531f561 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Thu, 13 Sep 2018 14:41:26 +0200 Subject: [PATCH] WIP --- Coq/LPTerm.v | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++-- Coq/WF.v | 47 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 100 insertions(+), 2 deletions(-) diff --git a/Coq/LPTerm.v b/Coq/LPTerm.v index 8abe1e0..590a763 100644 --- a/Coq/LPTerm.v +++ b/Coq/LPTerm.v @@ -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 Γ). diff --git a/Coq/WF.v b/Coq/WF.v index ba366ac..a61b8da 100644 --- a/Coq/WF.v +++ b/Coq/WF.v @@ -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. -- 2.24.1