...

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. intros. remember (Γ, x : A) as Γ2. induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0. 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. Proof. intros. intros. intro. induction H. apply H. - easy. now left. - 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. 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. ... ...