Commit 2fc865ff authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 5237f34c
...@@ -49,17 +49,17 @@ Fixpoint FV (t:term) : list Var := ...@@ -49,17 +49,17 @@ Fixpoint FV (t:term) : list Var :=
end. end.
Fixpoint closed (t:term) := match t with Fixpoint free_var_free (t:term) := match t with
| TKind => True | TKind => True
| TType => True | TType => True
| TFree v => False | TFree v => False
| TBound _ => True | TBound _ => True
| TPi A B => (closed A) /\ (closed B) | TPi A B => (free_var_free A) /\ (free_var_free B)
| TAbs A B => (closed A) /\ (closed B) | TAbs A B => (free_var_free A) /\ (free_var_free B)
| TApp t u => (closed t) /\ (closed u) | TApp t u => (free_var_free t) /\ (free_var_free u)
end. end.
Theorem closed_FV : forall t, (closed t) <-> (FV t) = nil. Theorem closed_FV : forall t, (free_var_free t) <-> (FV t) = nil.
Proof. Proof.
intro. split ; intros. intro. split ; intros.
- induction t ; intros ; try easy. - induction t ; intros ; try easy.
......
...@@ -49,12 +49,65 @@ Proof. ...@@ -49,12 +49,65 @@ Proof.
- apply IHInRelCtx. eapply ruldecl_WF. apply H. easy. - apply IHInRelCtx. eapply ruldecl_WF. apply H. easy.
Qed. Qed.
Theorem conv_kind_not_typable : forall Γ t T, Γ t : T -> ~ (Γ t T). Reserved Notation "t '▷' u" (at level 40, u at level 25).
Inductive R_Subterm : term -> term -> Prop :=
| HSubRefl : forall x , x x
| HSubPi1 : forall x A B, A x -> (Π A ~ B) x
| HSubPi2 : forall x A B, B x -> (Π A ~ B) x
| HSubAbs1 : forall x A t, A x -> (λ A ~ t) x
| HSubAbs2 : forall x A t, t x -> (λ A ~ t) x
| HSubApp1 : forall x t u, t x -> (t @ u) x
| HSubApp2 : forall x t u, u x -> (t @ u) x
where "t '▷' u" := (R_Subterm t u).
Definition BV_closed (t:term) : Prop := forall k, ~ (t ? k).
Definition FV_closed (t:term) : Prop := forall v, ~ (t # v).
Theorem __ : forall t, BV_closed t -> forall k u, BV_closed (t[k <- u]).
Proof. Proof.
intros. intro. intro. intro.
induction H0. induction t; intros; simpl; try easy.
- contradiction (H n). econstructor.
-
Theorem __ : forall t u, closed t -> u t -> forall k v, u[k <- v] t.
Proof.
do 4 intro.
induction H0; intros.
-
Theorem conv_kind_not_typable : forall Γ t, Γ t →β kind -> forall T, ~ (Γ t : T).
Theorem conv_kind_not_typable : forall Γ t, Γ t →β kind -> forall T, ~ (Γ t : T).
Proof.
do 3 intro. remember kind as K.
destruct H.
destruct t.
- intros. intro.
remember ((λ A ~ TKind) @ u) as t.
destruct H; try inversion Heqt.
+ subst. inversion H.
* subst. destruct (var_inf L). pose proof (H8 x H1). eapply kind_not_typable. apply H2.
* subst.
+
Theorem conv_kind_not_typable : forall Γ t, Γ t kind -> forall T, ~ (Γ t : T).
Proof.
do 3 intro.
remember kind as K.
induction H.
- intros. subst. intro. eapply kind_not_typable. apply H.
- subst. induction H.
+ apply IHRSTClosure. easy.
Qed. 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