diff --git a/Coq/LPTerm.v b/Coq/LPTerm.v index 40eb3d5257dbae418bcbec19ea0fdd2472d8fe4e..8abe1e0842b44297061976599c193b67cc8d94e5 100644 --- a/Coq/LPTerm.v +++ b/Coq/LPTerm.v @@ -11,6 +11,8 @@ Parameter Var : Set. Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}. +(* ************ Terms ************ *) + Inductive term : Set := | TKind : term | TType : term @@ -29,6 +31,19 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity). Definition type : term := TType. Definition kind : term := TKind. +Fixpoint FV (t:term) : list Var := + match t with + | TKind => nil + | TType => nil + | TFree v => cons v nil + | TBound _ => nil + | TPi A B => (FV A) ++ (FV B) + | TAbs A B => (FV A) ++ (FV B) + | TApp t u => (FV t) ++ (FV u) + end. + +(* ************ Contexts ************ *) + Inductive context : Set := | CEmpty : context | CVar : Var -> term -> context -> context @@ -38,6 +53,13 @@ Notation "[ ]" := CEmpty (at level 0). Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 30, x at level 30). Notation "Γ ',' t '≡' u" := (CRel t u Γ) (at level 30, t at level 30). +Definition pop_context (c:context) : context := + match c with + | CEmpty => c + | CVar _ _ c => c + | CRel _ _ c => c + end. + Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80). Inductive InCtx : context -> Var -> term -> Prop := | INow : forall Γ x A, x : A ∈ (Γ, x : A) @@ -62,8 +84,10 @@ Fixpoint open_k (t u : term) (k : nat) := | TAbs ty te => TAbs (open_k ty u k) (open_k te u (S k)) | TPi ty te => TPi (open_k ty u k) (open_k te u (S k)) end. +Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24). + +Definition open (t u : term) := t [ 0 <- u ]. -Definition open (t u : term) := open_k t u 0. Fixpoint subst_k (t u : term) (z : Var) : term := match t with @@ -87,8 +111,11 @@ Fixpoint close_k (t : term) (k : nat) (z : Var) : term := | TPi ty te => TPi (close_k ty k z) (close_k ty (S k) z) end. +Definition close (t : term) (z : Var) : term := close_k t 0 z. -Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24). +Notation "A '~>' B" := (TPi A B) (at level 22, right associativity). +Notation "x ';' A '~>' B" := (TPi A (close B x)) (at level 22, A at level 21, right associativity). +Notation "x ';' A '=>' B" := (TAbs A (close B x)) (at level 22, A at level 21, right associativity). Definition ConvScheme := context -> term -> term -> Prop. @@ -145,10 +172,10 @@ Reserved Notation "Γ ✓" (at level 40). Inductive typing : context -> term -> term -> Prop := | TyAxiom : forall Γ x A, Γ ✓ -> x : A ∈ Γ -> Γ ⊢ (# x) : A | TyType : forall Γ, Γ ✓ -> Γ ⊢ type : kind -| TyPi : forall Γ A B s L, +| TyPi : forall L Γ A B s, Γ ⊢ A : type -> (forall x, ~(In x L) -> Γ , x : A ⊢ B : s) -> Γ ⊢ Π A ~ B : s -| TyAbs : forall Γ A B t s L, +| TyAbs : forall L Γ A B t s, Γ ⊢ A : type -> (forall x, ~ (In x L) -> Γ, x : A ⊢ B : s) -> (forall x, ~ (In x L) -> Γ, x : A ⊢ t : B) -> Γ ⊢ λ A ~ t : Π A ~ B @@ -157,6 +184,10 @@ Inductive typing : context -> term -> term -> Prop := where "Γ '⊢' t ':' A" := (typing Γ t A) with well_formed : context -> Prop := | WFEmpty : [ ] ✓ - | WFVar : forall Γ x A, Γ ⊢ A : type -> Γ ✓ -> Γ , x : A ✓ + | WFVarT : forall Γ x A, Γ ⊢ A : type -> Γ, x : A ✓ + | WFVarK : forall Γ x A, Γ ⊢ 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/STT.v b/Coq/STT.v index 9bd4c98694bed63b0fe5af60c46f792b50c5050b..070aec91c183af88b0bbf241a4df367f8fed5839 100644 --- a/Coq/STT.v +++ b/Coq/STT.v @@ -11,22 +11,59 @@ Parameter impl : Var. Parameter fa : Var. Parameter ε : Var. +Parameter a b c x y z F G X Y Z f g : Var. -Definition STT := - [], - type : TType, - ι : # type, - o : # type, - arrow : Π (# type) ~ Π (# type) ~ (# type), - η : Π (# type) ~ TType, - ε : Π ((# η) @ (# o)) ~ ((# η) @ (# o)), - impl : Π (TApp (# η) (# o)) ~ Π (TApp (# η) (# o)) ~ (TApp (# η) (# o)), - fa : - Π (# type) ~ Π (Π (TApp (# η) (TBound 0)) ~ (TApp (# η) (# o))) ~ (TApp (# η) (# o)), - λ (# type) ~ (λ (# type) ~ (# η) @ ((# arrow) @ (? 0) @ (? 1))) ≡ λ (# type) ~ (λ (# type) ~ (Π ((# η) @ (? 0)) ~ (# η) @ (? 1))) + +Theorem util_var_decl c x A : c ✓ -> (c ✓ -> c, x : A ✓) -> c, x : A ✓. +Proof. exact (fun x f => f x). Qed. + +Theorem util_rul_decl c t u : c ✓ -> (c ✓ -> c, t ≡ u ✓) -> c, t ≡ u ✓. +Proof. exact (fun x f => f x). Qed. + + +Definition STT := [] +, type : TType +, ι : # type +, o : # type +, arrow : # type ~> # type ~> # type +, η : # type ~> TType +, ε : # η @ # o ~> # η @ # o +, impl : # η @ # o ~> # η @ # o ~> # η @ # o +, fa : a ; # type ~> (# η @ # a ~> # η @ # o) ~> (# η @ # o) +, + x ; # type => y ; # type => # η @ (# arrow @ # x @ # y) + ≡ + x ; # type => y ; # type => (# η @ # x ~> # η @ # y) +, + x ; # type => y ; # type => # ε @ (# impl @ # x @ # y) + ≡ + x ; # type => y ; # type => (# ε @ # x ~> #ε @ # y) +, + a ; # type => f ; # type => # ε @ (#fa @ #a @ #f) + ≡ + a ; # type => f ; # type => z ; (#η @ #a) => # ε @ (#f @ #x) . Theorem STT_WF : STT ✓. Proof. - -Admitted. + try repeat apply util_rul_decl || apply util_var_decl. + constructor. + - intro. apply WFVarK. constructor. constructor. + - intro. constructor. apply TyAxiom. easy. repeat constructor. + - intro. constructor. apply TyAxiom. easy. repeat constructor. + - intro. constructor. apply TyPi. constructor. + + easy. + + repeat constructor. + + intros. apply TyPi. + * constructor. apply util_var_decl. + -- easy. + -- intro. apply WFVarT. apply TyAxiom. easy. repeat constructor. + -- repeat constructor. + * intros. apply TyAxiom. apply util_var_decl. apply util_var_decl. easy. intros. constructor. apply TyAxiom. easy. repeat constructor. intros. constructor. apply TyAxiom. easy. repeat constructor. repeat constructor. + - intro. apply WFVarK. constructor. + + constructor. easy. repeat constructor. + + intros. + constructor. constructor. constructor. easy. repeat constructor. + - intros. apply WFVarT. constructor. + + apply +Qed. diff --git a/Coq/WF.v b/Coq/WF.v new file mode 100644 index 0000000000000000000000000000000000000000..ba366acbc4d8b764f19d189fda2c55a1a6b8801b --- /dev/null +++ b/Coq/WF.v @@ -0,0 +1,81 @@ + +Require Import PeanoNat. +Require Import List. +Require Import LPTerm. + + +Theorem WF_var_decl : forall Γ x A, Γ, x : A ✓ -> Γ ✓. +Proof. + intros. + remember (Γ, x : A) as Γ0. + induction H. + - inversion HeqΓ0. + - inversion HeqΓ0. subst. induction H. + + easy. + + easy. + + apply IHtyping. easy. + + apply IHtyping. easy. + + apply IHtyping1. easy. + + apply IHtyping1. easy. + - inversion HeqΓ0. subst. induction H. + + easy. + + easy. + + apply IHtyping. easy. + + apply IHtyping. easy. + + apply IHtyping1. easy. + + apply IHtyping1. easy. + - inversion HeqΓ0. +Qed. + +Theorem WF_rul_decl : forall Γ t u, Γ, t ≡ u ✓ -> Γ ✓. +Proof. + intros. + remember (Γ, t ≡ u) as Γ0. + induction H. + - inversion HeqΓ0. + - inversion HeqΓ0. + - inversion HeqΓ0. + - subst. inversion HeqΓ0. subst. easy. +Qed. + +Theorem TyPreserv_var_decl : forall Γ x A c d, Γ ⊢ c : d -> Γ, x : A ✓ -> Γ, x : A ⊢ c : d. +Proof. + intros. + induction H. + - apply TyAxiom. easy. constructor. easy. + - apply TyType. easy. + - apply (TyPi (x :: L)). + + 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. + inversion H5. + -- subst. apply TyAxiom. constructor. +Qed. + +Theorem TyPreserv_rul_decl : forall Γ t u c d, Γ ⊢ c : d -> Γ, t ≡ u ⊢ c : d. +Proof. +Admitted. + + +Theorem TyPi2 : forall Γ A B s, Γ ⊢ A : type -> Γ ⊢ B : s -> Γ ⊢ Π A ~ B : s. +Proof. + intros. + apply (TyPi nil). + - 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. +Proof. + intros. + eapply (TyAbs nil). + - easy. + - intros. apply TyPreserv_var_decl. apply H0. + - intros. apply TyPreserv_var_decl. apply H1. +Qed. + + diff --git a/Coq/conversion.v b/Coq/conversion.v index 90a7c1b94c7a63a82f2c6acf9cb75cd177d1d293..75b74a6cc6b3963c5ba8a08f70d772591f1074c1 100644 --- a/Coq/conversion.v +++ b/Coq/conversion.v @@ -1,6 +1,6 @@ Require Import LPTerm. - +Require Import WF. Lemma no_type_kind : forall Γ A, Γ ⊢ kind : A -> False. @@ -22,15 +22,17 @@ Proof. intros. induction Γ. - inversion H0. - - inversion H. subst. - inversion H0 ; subst. - exact (IHΓ H5 H8). - - inversion H. subst. - inversion H0 ; subst. + - inversion H. + subst. inversion H0 ; subst. apply IHΓ. + + eapply WF_var_decl. apply H. + + easy. + + eapply IHΓ. eapply WF_var_decl. apply H. inversion H0. subst. easy. + - inversion H0; subst. + inversion H ; subst. + exists s,A,Γ. split. apply H5. split. apply H6. apply H4. - +exact (IHΓ H7 H10). + + apply IHΓ. eapply WF_rul_decl. apply H. easy. Qed. Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A ⊢ t →β u -> Γ ⊢ t →β u. diff --git a/Coq/properties.v b/Coq/properties.v index 69ef3d8c9d9e4bcb0dcc2be310d31717cb3bc2a6..519b6622b37cd7ad7fbda018fb9d2a7566ab0146 100644 --- a/Coq/properties.v +++ b/Coq/properties.v @@ -3,6 +3,11 @@ Require Import LPTerm. Require Import conversion. +Inductive Sort : Set := SKind | SType | SObject. + +Definition + + Lemma not_var_kind_gamma : forall Γ x, Γ ✓ -> x : kind ∈ Γ -> False. Proof.