...
 
Commits (2)
...@@ -59,7 +59,7 @@ Fixpoint closed (t:term) := match t with ...@@ -59,7 +59,7 @@ Fixpoint closed (t:term) := match t with
| TApp t u => (closed t) /\ (closed u) | TApp t u => (closed t) /\ (closed u)
end. end.
Theorem close_FV : forall t, (closed t) <-> (FV t) = nil. Theorem closed_FV : forall t, (closed t) <-> (FV t) = nil.
Proof. Proof.
intro. split ; intros. intro. split ; intros.
- induction t ; intros ; try easy. - induction t ; intros ; try easy.
...@@ -132,7 +132,7 @@ Fixpoint open_k (t u : term) (k : nat) := ...@@ -132,7 +132,7 @@ Fixpoint open_k (t u : term) (k : nat) :=
| TKind => t | TKind => t
| TType => t | TType => t
| TFree n => t | TFree n => t
| TBound i => if Nat.eq_dec k i then u else t | TBound i => if Nat.eqb k i then u else t
| TApp l r => TApp (open_k l u k) (open_k r u k) | TApp l r => TApp (open_k l u k) (open_k r u k)
| 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))
...@@ -141,6 +141,54 @@ Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24). ...@@ -141,6 +141,54 @@ 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) := t [ 0 <- u ].
Theorem open_k_FV : forall t u x k, In x (FV (open_k t u k)) -> In x (FV t) \/ In x (FV u).
Proof.
intro. intro. intro. induction t.
- intros. contradict H.
- intros. contradict H.
- intros. destruct H. rewrite H. left. left. easy. contradict H.
- intros. destruct (Nat.eq_dec k n); subst.
+ right. assert ((n =? n) = true).
eapply Nat.eqb_eq ; easy.
cbn in H. rewrite H0 in H. easy.
+ cbn in H. assert (~ (k =? n) = true).
* intro. apply n0. eapply Nat.eqb_eq. easy.
* pose proof (Bool.not_true_is_false (k =? n) H0). cbn in H. rewrite H1 in H. left. easy.
- intros. simpl.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0.
+ simpl. pose proof (IHt1 k H0). destruct H1.
left. apply in_or_app. left. easy. right. easy.
+ simpl. pose proof (IHt2 (S k) H0). destruct H1.
left. apply in_or_app. right. easy. right. easy.
- intros. simpl. cbn in H.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0.
+ simpl. pose proof (IHt1 k H0). destruct H1.
left. apply in_or_app. left. easy. right. easy.
+ simpl. pose proof (IHt2 (S k) H0). destruct H1.
left. apply in_or_app. right. easy. right. easy.
- intros. simpl. cbn in H.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [k <- u])) x H). destruct H0.
+ simpl. pose proof (IHt1 k H0). destruct H1.
left. apply in_or_app. left. easy. right. easy.
+ simpl. pose proof (IHt2 k H0). destruct H1.
left. apply in_or_app. right. easy. right. easy.
Qed.
(* Substitute DB_0 with a named var. *)
Definition open_v (t : term) (v : Var) := t [0 <- # v].
Notation "t '[' v ']'" := (open_v t v) (at level 24).
Theorem open_FV : forall t v x, In x (FV (open_v t v)) -> x = v \/ In x (FV t).
Proof.
intros. cbn in H.
destruct (open_k_FV t (# v) x 0 H).
+ right. easy.
+ left. destruct H0 ; easy.
Qed.
Fixpoint subst_k (t u : term) (z : Var) : term := Fixpoint subst_k (t u : term) (z : Var) : term :=
match t with match t with
...@@ -227,12 +275,12 @@ Inductive typing : context -> term -> term -> Prop := ...@@ -227,12 +275,12 @@ Inductive typing : context -> term -> term -> Prop :=
| TyType : forall Γ, Γ -> Γ type : kind | TyType : forall Γ, Γ -> Γ type : kind
| TyPi : forall L Γ A B s, | TyPi : forall L Γ A B s,
Γ A : type -> Γ A : type ->
(forall x, ~(In x L) -> Γ , x : A (close B x) : s) -> (forall x, ~(In x L) -> Γ , x : A B[x] : s) ->
Γ Π A ~ B : s Γ Π A ~ B : s
| TyAbs : forall L Γ A B t s, | TyAbs : forall L Γ A B t s,
Γ A : type -> Γ A : type ->
(forall x, ~ (In x L) -> Γ, x : A (close B x) : s) -> (forall x, ~ (In x L) -> Γ, x : A B[x] : s) ->
(forall x, ~ (In x L) -> Γ, x : A (close t x) : (close B x)) -> (forall x, ~ (In x L) -> Γ, x : A t[x] : B[x]) ->
Γ λ A ~ t : Π A ~ B Γ λ A ~ t : Π A ~ B
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u] | TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u]
| TyConv : forall Γ t A B s, (Γ t : A) -> (Γ B : s) -> Γ A B -> (Γ t : B) | TyConv : forall Γ t A B s, (Γ t : A) -> (Γ B : s) -> Γ A B -> (Γ t : B)
...@@ -243,3 +291,4 @@ with well_formed : context -> Prop := ...@@ -243,3 +291,4 @@ with well_formed : context -> Prop :=
| WFVarK : forall Γ x A, Fresh_var Γ x -> Γ A : kind -> Γ, 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 | WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ). where "Γ ✓" := (well_formed Γ).
...@@ -4,14 +4,86 @@ Require Import List. ...@@ -4,14 +4,86 @@ Require Import List.
Require Import LPTerm. Require Import LPTerm.
Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v. Theorem types_WF : forall Γ t u, Γ t : u -> Γ .
Proof. intros. induction H; easy. Qed.
Theorem vardecl_WF : forall Γ x A, Γ, x : A -> Γ .
Proof. Proof.
intros. intros.
intro. remember (Γ, x : A) as Γ2.
apply H. induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
now left.
Qed. Qed.
Theorem ruldecl_WF : forall Γ t u, Γ, t u -> Γ .
Proof.
intros.
remember (Γ, t u) as Γ2.
induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
Qed.
Inductive weaker : context -> context -> Prop :=
| WeakRefl : forall Γ , weaker Γ Γ
| WeakVarDecl : forall Γ x A, weaker Γ (Γ, x : A)
| WeakRulDecl : forall Γ t u, weaker Γ (Γ, t u)
| WeakNextVarDecl : forall Γ Γ' x A, weaker Γ Γ' -> weaker (Γ, x : A) (Γ', x : A)
| WeakNextRulDecl : forall Γ Γ' t u, weaker Γ Γ' -> weaker (Γ, t u) (Γ', t u).
Theorem subset_var_decl : forall Γ Γ' x A, weaker Γ Γ' -> x : A Γ -> x : A Γ'.
Proof.
intros.
induction H.
- easy.
- apply IAfterV. easy.
- apply IAfterR. easy.
- remember (Γ, x0 : A0) as Γ2. induction H0.
+ inversion HeqΓ2. subst. apply INow.
+ inversion HeqΓ2. subst. apply IAfterV. apply IHweaker. easy.
+ inversion HeqΓ2.
- remember (Γ, t u) as Γ2. induction H0 ; inversion HeqΓ2.
subst. apply IAfterR. apply IHweaker. easy.
Qed.
Theorem subset_rul_decl : forall Γ Γ' t u, weaker Γ Γ' -> t u Γ -> t u Γ'.
Proof.
intros.
induction H.
- easy.
- apply IRAfterV. easy.
- apply IRAfterR. easy.
- remember (Γ, x : A) as Γ2. induction H0.
+ inversion HeqΓ2.
+ inversion HeqΓ2. subst. apply IRAfterV. apply IHweaker. easy.
+ inversion HeqΓ2.
- remember (Γ, t0 u0) as Γ2. induction H0; inversion HeqΓ2.
+ subst. econstructor.
+ inversion HeqΓ2. subst. apply IRAfterR. apply IHweaker. easy.
Qed.
Theorem fresh_vars_weaker : forall Γ Γ' x, weaker Γ Γ' -> Fresh_var Γ' x -> Fresh_var Γ x.
Proof.
intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy.
Qed.
Theorem weak : forall Γ Γ' t u, Γ t : u -> weaker Γ Γ' -> Γ' -> Γ' t : u.
Proof.
intros.
generalize dependent Γ'.
induction H; intros.
- apply TyAxiom. easy. eapply subset_var_decl. apply H1. easy.
- apply TyType. easy.
- eapply TyPi.
+ apply IHtyping. easy. easy.
+ intro. intro. apply H1. apply H4. apply WeakNextVarDecl. easy. econstructor.
Admitted.
Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v.
Proof. intros. intro. apply H. now left. Qed.
Theorem FV_close : forall x y t, In x (FV t) -> x <> y -> forall n, In x (FV (close_k t n y)). Theorem FV_close : forall x y t, In x (FV t) -> x <> y -> forall n, In x (FV (close_k t n y)).
Proof. Proof.
intros x y t H x_neq_y. intros x y t H x_neq_y.
......