Commit ef3495bc authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 111b9de7
......@@ -28,6 +28,36 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity).
Definition type : term := TType.
Definition kind : term := TKind.
(* ************ Subterms ************ *)
Reserved Notation "t '▷' u" (at level 85, 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).
Lemma ST_trans : forall t u v, t u -> u v -> t v.
Proof.
intros. generalize dependent v. induction H; subst; intros.
- easy.
- apply HSubPi1. apply IHR_Subterm. easy.
- apply HSubPi2. apply IHR_Subterm. easy.
- apply HSubAbs1. apply IHR_Subterm. easy.
- apply HSubAbs2. apply IHR_Subterm. easy.
- apply HSubApp1. apply IHR_Subterm. easy.
- apply HSubApp2. apply IHR_Subterm. easy.
Qed.
Definition close (t:term) : Prop := forall u k, t u -> u <> TBound k.
Theorem close_subterm_comp : forall t u, t u -> close t -> close u.
Proof. intros. intro. intros. apply H0. apply (ST_trans _ _ _ H H1). Qed.
(* ************ Free variables ************ *)
......@@ -42,25 +72,18 @@ Fixpoint FV (t:term) : list Var :=
| TApp t u => (FV t) ++ (FV u)
end.
Definition free_var_free (t:term) := forall v, ~ (t #v).
Fixpoint free_var_free (t:term) := match t with
| TKind => True
| TType => True
| TSymb v => False
| TBound _ => True
| TPi A B => (free_var_free A) /\ (free_var_free B)
| TAbs A B => (free_var_free A) /\ (free_var_free B)
| TApp t u => (free_var_free t) /\ (free_var_free u)
end.
Theorem free_var_free_subterm : forall t u, t u -> free_var_free t -> free_var_free u.
Proof.
Admitted.
Theorem closed_FV : forall t, (free_var_free 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 v). constructor.
+ destruct H. simpl.
assert (FV t1 = nil); auto.
assert (FV t2 = nil); auto.
......@@ -79,7 +102,8 @@ Proof.
+ 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.
*)
Admitted.
(* ************ Contexts ************ *)
......@@ -147,34 +171,6 @@ Qed.
(* ************ Substitution ************ *)
Reserved Notation "t '▷' u" (at level 85, 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).
Lemma ST_trans : forall t u v, t u -> u v -> t v.
Proof.
intros. generalize dependent v. induction H; subst; intros.
- easy.
- apply HSubPi1. apply IHR_Subterm. easy.
- apply HSubPi2. apply IHR_Subterm. easy.
- apply HSubAbs1. apply IHR_Subterm. easy.
- apply HSubAbs2. apply IHR_Subterm. easy.
- apply HSubApp1. apply IHR_Subterm. easy.
- apply HSubApp2. apply IHR_Subterm. easy.
Qed.
Definition close (t:term) : Prop := forall u k, t u -> u <> TBound k.
Theorem close_subterm_comp : forall t u, t u -> close t -> close u.
Proof. intros. intro. intros. apply H0. apply (ST_trans _ _ _ H H1). Qed.
Fixpoint shift (k:nat) (t:term) :=
match t with
| TBound n => TBound (n + k)
......@@ -359,3 +355,9 @@ with cwell_formed : signature -> local_context -> Prop :=
| CWFEmpty : forall Σ, Σ WF -> Σ;nil
| CWFLVar : forall Σ Γ A, Σ;Γ A : type -> Σ;Γ -> Σ;Γ,A
where "Σ ';' Γ '✓'" := (cwell_formed Σ Γ).
Definition is_kind Γ t : Prop := Γ;nil t : TKind.
Definition is_type Γ t : Prop := exists T, Γ;nil t : T /\ is_kind Γ T.
Definition is_object Γ t : Prop := exists T, Γ;nil t : T /\ is_type Γ T.
Require Import List.
Require Import LPTerm.
Require Import WF.
......
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