Commit 840ba284 authored by Gaspard Ferey's avatar Gaspard Ferey

WIP.

parent 75ccb503
...@@ -11,6 +11,8 @@ Parameter Var : Set. ...@@ -11,6 +11,8 @@ Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}. Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
(* ************ Terms ************ *)
Inductive term : Set := Inductive term : Set :=
| TKind : term | TKind : term
| TType : term | TType : term
...@@ -29,6 +31,19 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity). ...@@ -29,6 +31,19 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity).
Definition type : term := TType. Definition type : term := TType.
Definition kind : term := TKind. 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 := Inductive context : Set :=
| CEmpty : context | CEmpty : context
| CVar : Var -> term -> context -> context | CVar : Var -> term -> context -> context
...@@ -38,6 +53,13 @@ Notation "[ ]" := CEmpty (at level 0). ...@@ -38,6 +53,13 @@ Notation "[ ]" := CEmpty (at level 0).
Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 30, x at level 30). 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). 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). Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80).
Inductive InCtx : context -> Var -> term -> Prop := Inductive InCtx : context -> Var -> term -> Prop :=
| INow : forall Γ x A, x : A (Γ, x : A) | INow : forall Γ x A, x : A (Γ, x : A)
...@@ -62,8 +84,10 @@ Fixpoint open_k (t u : term) (k : nat) := ...@@ -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)) | 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)) | TPi ty te => TPi (open_k ty u k) (open_k te u (S k))
end. 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 := Fixpoint subst_k (t u : term) (z : Var) : term :=
match t with match t with
...@@ -87,8 +111,11 @@ Fixpoint close_k (t : term) (k : nat) (z : Var) : term := ...@@ -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) | TPi ty te => TPi (close_k ty k z) (close_k ty (S k) z)
end. 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. Definition ConvScheme := context -> term -> term -> Prop.
...@@ -145,10 +172,10 @@ Reserved Notation "Γ ✓" (at level 40). ...@@ -145,10 +172,10 @@ Reserved Notation "Γ ✓" (at level 40).
Inductive typing : context -> term -> term -> Prop := Inductive typing : context -> term -> term -> Prop :=
| TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A | TyAxiom : forall Γ x A, Γ -> x : A Γ -> Γ (# x) : A
| TyType : forall Γ, Γ -> Γ type : kind | TyType : forall Γ, Γ -> Γ type : kind
| TyPi : forall Γ A B s L, | TyPi : forall L Γ A B s,
Γ A : type -> Γ A : type ->
(forall x, ~(In x L) -> Γ , x : A B : s) -> Γ Π A ~ B : s (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 -> Γ A : type ->
(forall x, ~ (In x L) -> Γ, x : A B : s) -> (forall x, ~ (In x L) -> Γ, x : A B : s) ->
(forall x, ~ (In x L) -> Γ, x : A t : B) -> Γ λ A ~ t : Π A ~ B (forall x, ~ (In x L) -> Γ, x : A t : B) -> Γ λ A ~ t : Π A ~ B
...@@ -157,6 +184,10 @@ Inductive typing : context -> term -> term -> Prop := ...@@ -157,6 +184,10 @@ Inductive typing : context -> term -> term -> Prop :=
where "Γ '⊢' t ':' A" := (typing Γ t A) where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop := with well_formed : context -> Prop :=
| WFEmpty : [ ] | 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 | WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ). where "Γ ✓" := (well_formed Γ).
...@@ -11,22 +11,59 @@ Parameter impl : Var. ...@@ -11,22 +11,59 @@ Parameter impl : Var.
Parameter fa : Var. Parameter fa : Var.
Parameter ε : Var. Parameter ε : Var.
Parameter a b c x y z F G X Y Z f g : Var.
Definition STT :=
[], Theorem util_var_decl c x A : c -> (c -> c, x : A ) -> c, x : A .
type : TType, Proof. exact (fun x f => f x). Qed.
ι : # type,
o : # type, Theorem util_rul_decl c t u : c -> (c -> c, t u ) -> c, t u .
arrow : Π (# type) ~ Π (# type) ~ (# type), Proof. exact (fun x f => f x). Qed.
η : Π (# type) ~ TType,
ε : Π ((# η) @ (# o)) ~ ((# η) @ (# o)),
impl : Π (TApp (# η) (# o)) ~ Π (TApp (# η) (# o)) ~ (TApp (# η) (# o)), Definition STT := []
fa : , type : TType
Π (# type) ~ Π (Π (TApp (# η) (TBound 0)) ~ (TApp (# η) (# o))) ~ (TApp (# η) (# o)), , ι : # type
λ (# type) ~ (λ (# type) ~ (# η) @ ((# arrow) @ (? 0) @ (? 1))) λ (# type) ~ (λ (# type) ~ (Π ((# η) @ (? 0)) ~ (# η) @ (? 1))) , 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 . Theorem STT_WF : STT .
Proof. Proof.
try repeat apply util_rul_decl || apply util_var_decl.
Admitted. 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.
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.
Require Import LPTerm. Require Import LPTerm.
Require Import WF.
Lemma no_type_kind : forall Γ A, Γ kind : A -> False. Lemma no_type_kind : forall Γ A, Γ kind : A -> False.
...@@ -22,15 +22,17 @@ Proof. ...@@ -22,15 +22,17 @@ Proof.
intros. intros.
induction Γ. induction Γ.
- inversion H0. - inversion H0.
- inversion H. subst. - inversion H.
inversion H0 ; subst. subst. inversion H0 ; subst. apply IHΓ.
exact (IHΓ H5 H8). + eapply WF_var_decl. apply H.
- inversion H. subst. + easy.
inversion H0 ; subst. + eapply IHΓ. eapply WF_var_decl. apply H. inversion H0. subst. easy.
- inversion H0; subst.
inversion H ; subst.
+ exists s,A,Γ. + exists s,A,Γ.
split. apply H5. split. apply H5.
split. apply H6. apply H4. split. apply H6. apply H4.
+exact (IHΓ H7 H10). + apply IHΓ. eapply WF_rul_decl. apply H. easy.
Qed. Qed.
Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A t →β u -> Γ t →β u. Lemma context_var_conv_β2 : forall Γ x A t u, Γ, x : A t →β u -> Γ t →β u.
......
...@@ -3,6 +3,11 @@ Require Import LPTerm. ...@@ -3,6 +3,11 @@ Require Import LPTerm.
Require Import conversion. Require Import conversion.
Inductive Sort : Set := SKind | SType | SObject.
Definition
Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False. Lemma not_var_kind_gamma : forall Γ x, Γ -> x : kind Γ -> False.
Proof. Proof.
......
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