Commit 111b9de7 authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 4cb8ff35
...@@ -95,12 +95,7 @@ Notation "Σ ',' t '≡' u" := (SRel t u Σ) (at level 50, t at level 25, u at l ...@@ -95,12 +95,7 @@ Notation "Σ ',' t '≡' u" := (SRel t u Σ) (at level 50, t at level 25, u at l
Definition local_context : Set := list term. Definition local_context : Set := list term.
Definition context : Set := signature * local_context.
Notation "Σ ',' T" := (cons T Σ) (at level 50, T at level 25). Notation "Σ ',' T" := (cons T Σ) (at level 50, T at level 25).
(*
Notation "Σ ';' Γ" := (pair Σ Γ) (at level 35, Γ at level 25).
*)
Definition pop_context (Γ:local_context) : local_context := List.tl Γ. Definition pop_context (Γ:local_context) : local_context := List.tl Γ.
...@@ -111,14 +106,14 @@ Fixpoint defined_symb (Σ:signature) : list Var := ...@@ -111,14 +106,14 @@ Fixpoint defined_symb (Σ:signature) : list Var :=
| SRel _ _ Σ => (defined_symb Σ) | SRel _ _ Σ => (defined_symb Σ)
end. end.
Reserved Notation "x ':' A '∈' Σ" (at level 80, A at level 80, Σ at level 80). Reserved Notation "x ':' A '∈' Σ" (at level 85, A at level 25, Σ at level 50).
Inductive InCtx : signature -> Var -> term -> Prop := Inductive InCtx : signature -> Var -> term -> Prop :=
| INow : forall Σ x A, x : A (Σ, x : A) | INow : forall Σ x A, x : A (Σ, x : A)
| IAfterV : forall Σ A x y B, x : A Σ -> x <> y -> x : A (Σ, y : B) | IAfterV : forall Σ A x y B, x : A Σ -> x <> y -> x : A (Σ, y : B)
| IAfterR : forall Σ A x t u, x : A Σ -> x : A (Σ, t u) | IAfterR : forall Σ A x t u, x : A Σ -> x : A (Σ, t u)
where "x ':' A ∈ Σ" := (InCtx Σ x A). where "x ':' A ∈ Σ" := (InCtx Σ x A).
Reserved Notation "t '≡' u '∈' Σ" (at level 80, u at level 80, Σ at level 80). Reserved Notation "t '≡' u '∈' Σ" (at level 85, u at level 25, Σ at level 50).
Inductive InRelCtx : signature -> term -> term -> Prop := Inductive InRelCtx : signature -> term -> term -> Prop :=
| IRNow : forall Σ t u, t u (Σ, t u) | IRNow : forall Σ t u, t u (Σ, t u)
| IRAfterV : forall Σ t u y B, t u Σ -> t u (Σ, y : B) | IRAfterV : forall Σ t u y B, t u Σ -> t u (Σ, y : B)
...@@ -128,8 +123,8 @@ where "t '≡' u ∈ Σ" := (InRelCtx Σ t u). ...@@ -128,8 +123,8 @@ where "t '≡' u ∈ Σ" := (InRelCtx Σ t u).
Definition Defined_var Σ v := exists T, v : T Σ. Definition Defined_var Σ v := exists T, v : T Σ.
Definition Fresh_var Σ v := ~ (Defined_var Σ v). Definition Fresh_var Σ v := ~ (Defined_var Σ v).
Notation "x '∈' Σ" := (Defined_var Σ x) (at level 90, Σ at level 90). Notation "x '∈' Σ" := (Defined_var Σ x) (at level 85, Σ at level 50).
Notation "x '∉' Σ" := (Fresh_var Σ x) (at level 90, Σ at level 90). Notation "x '∉' Σ" := (Fresh_var Σ x) (at level 85, Σ at level 50).
Theorem defined_eq : forall Σ v, Defined_var Σ v <-> In v (defined_symb Σ). Theorem defined_eq : forall Σ v, Defined_var Σ v <-> In v (defined_symb Σ).
Proof. Proof.
...@@ -152,7 +147,7 @@ Qed. ...@@ -152,7 +147,7 @@ Qed.
(* ************ Substitution ************ *) (* ************ Substitution ************ *)
Reserved Notation "t '▷' u" (at level 70, u at level 25). Reserved Notation "t '▷' u" (at level 85, u at level 25).
Inductive R_Subterm : term -> term -> Prop := Inductive R_Subterm : term -> term -> Prop :=
| HSubRefl : forall x , x x | HSubRefl : forall x , x x
| HSubPi1 : forall x A B, A x -> (Π A ~ B) x | HSubPi1 : forall x A B, A x -> (Π A ~ B) x
...@@ -163,19 +158,74 @@ Inductive R_Subterm : term -> term -> Prop := ...@@ -163,19 +158,74 @@ Inductive R_Subterm : term -> term -> Prop :=
| HSubApp2 : forall x t u, u x -> (t @ u) x | HSubApp2 : forall x t u, u x -> (t @ u) x
where "t '▷' u" := (R_Subterm t u). 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)
| TApp l r => TApp (shift k l) (shift k r)
| TAbs ty te => TAbs (shift k ty) (shift (S k) te)
| TPi ty te => TPi (shift k ty) (shift (S k) te)
| _ => t
end.
Theorem close_shift : forall t, close t -> forall k, shift k t = t.
Proof.
intro. intro. induction t; intros; simpl; try easy.
- contradict H. intro. apply (H (? n) n (HSubRefl (? n))). easy.
- erewrite (IHt1 _ _). erewrite (IHt2 _ _). easy.
- erewrite (IHt1 _ _). erewrite (IHt2 _ _). easy.
- erewrite (IHt1 _ _). erewrite (IHt2 _ _). easy.
Unshelve.
eapply (close_subterm_comp _ _ _ H).
eapply (close_subterm_comp _ _ _ H).
eapply (close_subterm_comp _ _ _ H).
eapply (close_subterm_comp _ _ _ H).
eapply (close_subterm_comp _ _ _ H).
eapply (close_subterm_comp _ _ _ H).
Unshelve.
apply HSubPi1 ; apply HSubRefl.
apply HSubPi2 ; apply HSubRefl.
apply HSubAbs1; apply HSubRefl.
apply HSubAbs2; apply HSubRefl.
apply HSubApp1; apply HSubRefl.
apply HSubApp2; apply HSubRefl.
Qed.
Theorem ST_shift_r : forall t u k, close u -> t u -> shift k t u.
Proof.
Admitted.
Theorem ST_shift_l : forall t u k, close u -> shift k t u -> t u.
Proof.
Admitted.
Fixpoint subst_k (t u : term) (k : nat) := Fixpoint subst_k (t u : term) (k : nat) :=
match t with match t with
| TKind => t | TBound i => if Nat.eqb k i then shift k u else t
| TType => t
| TSymb _ => t
| TBound i => if Nat.eqb k i then u else t
| TApp l r => TApp (subst_k l u k) (subst_k r u k ) | TApp l r => TApp (subst_k l u k) (subst_k r u k )
| TAbs ty te => TAbs (subst_k ty u k) (subst_k te u (S k)) | TAbs ty te => TAbs (subst_k ty u k) (subst_k te u (S k))
| TPi ty te => TPi (subst_k ty u k) (subst_k te u (S k)) | TPi ty te => TPi (subst_k ty u k) (subst_k te u (S k))
| _ => t
end. end.
Notation "t '[' k '<-' u ']'" := (subst_k t u k) (at level 24). Notation "t '[' k '<-' u ']'" := (subst_k t u k) (at level 24).
Definition subst (t u : term) := t [ 0 <- u ]. Definition subst (t u : term) := t [ 0 <- u ].
Notation "t '[' v ']'" := (subst t v) (at level 24). Notation "t '[' v ']'" := (subst t v) (at level 24).
...@@ -187,7 +237,7 @@ Proof. ...@@ -187,7 +237,7 @@ Proof.
- inversion H. - inversion H.
- inversion H; subst. left. easy. - inversion H; subst. left. easy.
- destruct (k =? n) eqn:H3; subst. - destruct (k =? n) eqn:H3; subst.
+ right. simpl in H. rewrite H3 in H. easy. + right. simpl in H. rewrite H3 in H. eapply ST_shift_l. intro. intros. inversion H0. easy. apply H.
+ simpl in H. rewrite H3 in H. inversion H. + simpl in H. rewrite H3 in H. inversion H.
- inversion H; subst. - inversion H; subst.
+ pose proof (IHt1 _ _ _ H3). + pose proof (IHt1 _ _ _ H3).
...@@ -223,19 +273,17 @@ Qed. ...@@ -223,19 +273,17 @@ Qed.
Fixpoint close_k (t : term) (k : nat) (z : Var) : term := Fixpoint close_k (t : term) (k : nat) (z : Var) : term :=
match t with match t with
| TKind => t
| TType => t
| TBound i => t
| TSymb x => if var_dec x z then TBound k else t | TSymb x => if var_dec x z then TBound k else t
| TApp l r => TApp (close_k l k z) (close_k r k z) | TApp l r => TApp (close_k l k z) (close_k r k z)
| TAbs ty te => TAbs (close_k ty k z) (close_k te (S k) z) | TAbs ty te => TAbs (close_k ty k z) (close_k te (S k) z)
| TPi ty te => TPi (close_k ty k z) (close_k te (S k) z) | TPi ty te => TPi (close_k ty k z) (close_k te (S k) z)
| _ => t
end. end.
Definition close (t : term) (z : Var) : term := close_k t 0 z. Definition subst_symb (t : term) (z : Var) : term := close_k t 0 z.
Notation "'λ' x ':' A '~' B" := (TPi A (close B x)) (at level 22, A at level 21, right associativity). Notation "'λ' x ':' A '~' B" := (TPi A (subst_symb 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). Notation "'Π' x ':' A '=>' B" := (TAbs A (subst_symb B x)) (at level 22, A at level 21, right associativity).
Definition ConvScheme := signature -> term -> term -> Prop. Definition ConvScheme := signature -> term -> term -> Prop.
...@@ -286,19 +334,20 @@ Notation "Σ '⊢' t '≡Γ' u" := ((RSTClosure RW_Gamma ) Σ t u) (at lev ...@@ -286,19 +334,20 @@ Notation "Σ '⊢' t '≡Γ' u" := ((RSTClosure RW_Gamma ) Σ t u) (at lev
Notation "Σ '⊢' t '≡βΓ' u" := ((RSTClosure RW_Beta_Gamma) Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '≡βΓ' u" := ((RSTClosure RW_Beta_Gamma) Σ t u) (at level 40, t at level 25).
Notation "Σ '⊢' t '≡' u" := (Σ t ≡βΓ u) (at level 40, t at level 25). Notation "Σ '⊢' t '≡' u" := (Σ t ≡βΓ u) (at level 40, t at level 25).
Reserved Notation "Σ ';' Γ '⊢' t ':' A" (at level 40, Γ at level 30, t at level 25, A at level 25). Reserved Notation "Σ ';' Γ '⊢' t ':' A" (at level 40, Γ at level 30, t at level 25, A at level 25).
Reserved Notation "Σ 'WF'" (at level 40). Reserved Notation "Σ 'WF'" (at level 40).
Reserved Notation "Σ '+' Γ ✓" (at level 41). Reserved Notation "Σ ';' Γ '✓'" (at level 40, Γ at level 30).
Inductive typing : signature -> local_context -> term -> term -> Prop := Inductive typing : signature -> local_context -> term -> term -> Prop :=
| TyAxiom : forall Σ Γ x A, Σ + Γ -> (x : A Σ) -> (Σ ; Γ (# x) : A) | TyAxiom : forall Σ Γ x A, Σ;Γ -> x : A Σ -> Σ;Γ (# x) : A
| TyType : forall Σ Γ, Σ + Γ -> Σ;Γ type : kind | TyBoundH : forall Σ Γ A , Σ;Γ,A -> Σ;(Γ,A) (? 0) : A
| TyPi : forall Σ Γ A B s, | TyBoundN : forall Σ Γ n T A, Σ;Γ,A -> Σ ; Γ (? n) : T -> Σ;(Γ,A) (? (S n)) : T
Σ;Γ A : type -> Σ;(Γ,A) B : s -> Σ;Γ Π A ~ B : s | TyType : forall Σ Γ , Σ;Γ -> Σ;Γ type : kind
| TyAbs : forall Σ Γ A B t s, | TyPi : forall Σ Γ A B s , Σ;Γ A : type -> Σ;(Γ,A) B : s -> Σ;Γ Π A ~ B : s
Σ;Γ A : type -> Σ;(Γ,A) B : s -> Σ;(Γ,A) t : B -> Σ;Γ λ A ~ t : Π A ~ B | TyAbs : forall Σ Γ A B t s, Σ;Γ A : type -> Σ;(Γ,A) B : s ->
Σ;(Γ,A) t : 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
where "Σ ';' Γ '⊢' t ':' A" := (typing Σ Γ t A) where "Σ ';' Γ '⊢' t ':' A" := (typing Σ Γ t A)
with well_formed : signature -> Prop := with well_formed : signature -> Prop :=
| WFEmpty : [ ] WF | WFEmpty : [ ] WF
...@@ -307,6 +356,6 @@ with well_formed : signature -> Prop := ...@@ -307,6 +356,6 @@ with well_formed : signature -> Prop :=
| WFRel : forall Σ A s t u, Σ;nil A : s -> Σ;nil t : A -> Σ;nil u : A -> Σ WF -> Σ, t u WF | WFRel : forall Σ A s t u, Σ;nil A : s -> Σ;nil t : A -> Σ;nil u : A -> Σ WF -> Σ, t u WF
where "Σ 'WF'" := (well_formed Σ) where "Σ 'WF'" := (well_formed Σ)
with cwell_formed : signature -> local_context -> Prop := with cwell_formed : signature -> local_context -> Prop :=
| CWFEmpty : forall Σ, Σ WF -> Σ + nil | CWFEmpty : forall Σ, Σ WF -> Σ;nil
| CWFLVar : forall Σ Γ A, Σ;Γ A : type -> Σ + Γ -> Σ + (Γ,A) | CWFLVar : forall Σ Γ A, Σ;Γ A : type -> Σ;Γ -> Σ;Γ,A
where "Σ '+' Γ ✓" := (cwell_formed Σ Γ). where "Σ ';' Γ '✓'" := (cwell_formed Σ Γ).
...@@ -10,11 +10,11 @@ Proof. ...@@ -10,11 +10,11 @@ Proof.
induction H; inversion HeqΣ2; subst; easy. induction H; inversion HeqΣ2; subst; easy.
Qed. Qed.
Lemma context_WF : forall Σ Γ, Σ + Γ -> Σ WF. Lemma context_WF : forall Σ Γ, Σ;Γ -> Σ WF.
Proof. intros. induction H; easy. Qed. Proof. intros. induction H; easy. Qed.
Lemma loccontext_WF : forall Σ Γ t u, Σ;Γ t : u -> Σ + Γ . Lemma loccontext_WF : forall Σ Γ t u, Σ;Γ t : u -> Σ;Γ .
Proof. intros. induction H; easy. Qed. Proof. intros. induction H; easy. Qed.
Lemma types_WF : forall Σ Γ t u, Σ;Γ t : u -> Σ WF. Lemma types_WF : forall Σ Γ t u, Σ;Γ t : u -> Σ WF.
...@@ -58,8 +58,10 @@ Proof. ...@@ -58,8 +58,10 @@ Proof.
induction H0; intros. induction H0; intros.
- inversion H; subst. repeat eexists. econstructor. apply H0. apply H1. - inversion H; subst. repeat eexists. econstructor. apply H0. apply H1.
- inversion H; subst. repeat eexists. econstructor. apply H0. - inversion H; subst. repeat eexists. econstructor. apply H0.
- inversion H; subst. repeat eexists. econstructor. apply H0. apply H1.
- inversion H; subst. repeat eexists. econstructor. apply H0.
- inversion H; subst. - inversion H; subst.
+ repeat eexists. econstructor. apply H0_. apply H0_0. + repeat eexists. econstructor. apply H0_. apply H0_0.
+ apply IHtyping1. easy. + apply IHtyping1. easy.
+ apply IHtyping2. easy. + apply IHtyping2. easy.
- inversion H; subst. - inversion H; subst.
...@@ -197,12 +199,14 @@ Proof. ...@@ -197,12 +199,14 @@ Proof.
apply weak_comp_hΓ. apply weak_comp_hΓ.
Qed. Qed.
Theorem weak_typ_ : forall Σ Σ' Γ t u, Σ;Γ t : u -> Σ Σ' -> Σ' WF -> Σ' + Γ -> Σ';Γ t : u. Theorem weak_typ_ : forall Σ Σ' Γ t u, Σ;Γ t : u -> Σ Σ' -> Σ' WF -> Σ';Γ -> Σ';Γ t : u.
Proof. Proof.
intros. intros.
generalize dependent Σ'. generalize dependent Σ'.
induction H; intros. induction H; intros.
- apply TyAxiom. easy. eapply subset_var_decl. apply H1. easy. - apply TyAxiom. easy. eapply subset_var_decl. apply H1. easy.
- apply TyBoundH. easy.
- apply TyBoundN. easy. apply IHtyping. easy. easy. inversion H3; subst; easy.
- apply TyType. easy. - apply TyType. easy.
- eapply TyPi. - eapply TyPi.
+ apply IHtyping1. easy. easy. easy. + apply IHtyping1. easy. easy. easy.
...@@ -220,7 +224,7 @@ Proof. ...@@ -220,7 +224,7 @@ Proof.
+ eapply weak_conv. apply H1. easy. easy. + eapply weak_conv. apply H1. easy. easy.
Qed. Qed.
Theorem weak_checked : forall Σ Σ' Γ, Σ + Γ -> Σ Σ' -> Σ' WF -> Σ' + Γ . Theorem weak_checked : forall Σ Σ' Γ, Σ;Γ -> Σ Σ' -> Σ' WF -> Σ';Γ .
Proof. Proof.
intros. intros.
induction Γ. induction Γ.
...@@ -243,10 +247,10 @@ Proof. ...@@ -243,10 +247,10 @@ Proof.
repeat eexists. eapply weak_typ. apply H3. easy. easy. repeat eexists. eapply weak_typ. apply H3. easy. easy.
Qed. Qed.
Theorem checked_WF : forall Σ Γ, Σ + Γ -> Σ WF. Theorem checked_WF : forall Σ Γ, Σ;Γ -> Σ WF.
Proof. intros. induction Γ; inversion H; subst; try apply IHΓ; try easy. Qed. Proof. intros. induction Γ; inversion H; subst; try apply IHΓ; try easy. Qed.
Lemma vd_context_typ : forall Σ Γ t u, Σ; Γ t : u -> forall x A, (Σ, x : A) + Γ -> (Σ, x : A);Γ t : u. Lemma vd_context_typ : forall Σ Γ t u, Σ; Γ t : u -> forall x A, (Σ, x : A);Γ -> (Σ, x : A);Γ t : u.
Proof. Proof.
intros. intros.
eapply weak_typ. eapply weak_typ.
...@@ -256,10 +260,10 @@ Proof. ...@@ -256,10 +260,10 @@ Proof.
- eapply checked_WF. apply H0. - eapply checked_WF. apply H0.
Qed. Qed.
Lemma loc_context_cheked : forall Σ Γ A, Σ + (Γ, A) -> Σ + Γ . Lemma loc_context_checked : forall Σ Γ A, Σ;(Γ, A) -> Σ;Γ .
Proof. intros. inversion H; subst. easy. Qed. Proof. intros. inversion H; subst. easy. Qed.
Lemma vd_context_WF : forall Σ Γ x A, Σ + Γ -> (Σ, x : A) WF -> (Σ, x : A) + Γ . Lemma vd_context_WF : forall Σ Γ x A, Σ;Γ -> (Σ, x : A) WF -> (Σ, x : A);Γ .
Proof. Proof.
intros. intros.
eapply weak_checked. apply H. econstructor. inversion H0; subst; easy. easy. eapply weak_checked. apply H. econstructor. inversion H0; subst; easy. easy.
...@@ -343,29 +347,38 @@ Qed. ...@@ -343,29 +347,38 @@ Qed.
Definition inhabitable (Σ:signature) (T:term) : Prop := exists Γ t, Σ;Γ t : T. Definition inhabitable (Σ:signature) (T:term) : Prop := exists Γ t, Σ;Γ t : T.
Lemma bound_var_nontypable : forall Σ n T, ~ Σ;nil (? n) : T.
Proof.
Admitted.
Lemma abs_equiv : forall Σ Γ a A b B, Σ;Γ a : A -> Σ;(Γ,A) b : B -> Σ;Γ b[0 <- a] : B. Lemma abs_equiv : forall Σ Γ a A b B, Σ;Γ a : A -> Σ;(Γ,A) b : B -> Σ;Γ b[0 <- a] : B.
Proof. Proof.
intros. intros.
generalize dependent H. generalize dependent H.
remember (Γ, A) as Γ'. remember (Γ, A) as Γ'.
pose proof (ex_intro (fun x => Γ'=Γ,x) A HeqΓ'). generalize dependent HeqΓ'.
generalize dependent Γ. generalize dependent Γ.
induction H0; intros; simpl; subst. generalize dependent a.
- econstructor. exact (loc_context_cheked _ _ _ H). easy. generalize dependent A.
- econstructor. exact (loc_context_cheked _ _ _ H). induction H0; intros.
- econstructor. - simpl. subst. econstructor. exact (loc_context_checked _ _ _ H). easy.
+ apply IHtyping1. easy. easy. - inversion HeqΓ'; subst. easy.
- inversion HeqΓ'; subst. induction Γ0; subst.
+ contradict H0. apply bound_var_nontypable.
+ eapply TyBoundN.
* eapply loccontext_WF. apply H2.
* apply IHtyping1. easy. easy.
Admitted. Admitted.
Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u). Theorem FV_decl_u : forall Σ u, inhabitable Σ u -> (u = kind \/ typable Σ u).
Proof. Proof.
intros. do 2 destruct H. intros. do 2 destruct H.
induction H. induction H.
- right. eapply vardecl_typable2. eapply weak_WF. apply H. apply H0. - right. eapply vardecl_typable2. eapply checked_WF. apply H. apply H0.
- left. easy. - left. easy.
- exact IHtyping2. - exact IHtyping2.
- right. repeat eexists. econstructor. apply H. apply H0. - right. repeat eexists. econstructor. apply H. apply H0.
- right. destruct IHtyping1. inversion H1. - right. destruct IHtyping1. inversion H1.
destruct H1. destruct H1. inversion H1; subst. destruct H1. destruct H1. inversion H1; subst.
remember (Π A ~ B) as P. remember (Π A ~ B) as P.
inversion H; subst. inversion H; subst.
......
(** Start to implement lambda pi modulo with pretty printing.
TODO:
- Have a better pretty printing for binders
- no substitution
- Try a localy nameless representation, but not implemented
*)
Require Import PeanoNat. Require Import PeanoNat.
Require Import List. Require Import List.
...@@ -35,6 +29,29 @@ Definition type : term := TType. ...@@ -35,6 +29,29 @@ Definition type : term := TType.
Definition kind : term := TKind. Definition kind : term := TKind.
Reserved Notation "t '▷' u" (at level 70, 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.
(* ************ Free variables ************ *) (* ************ Free variables ************ *)
Fixpoint FV (t:term) : list Var := Fixpoint FV (t:term) : list Var :=
...@@ -48,45 +65,59 @@ Fixpoint FV (t:term) : list Var := ...@@ -48,45 +65,59 @@ Fixpoint FV (t:term) : list Var :=
| TApp t u => (FV t) ++ (FV u) | TApp t u => (FV t) ++ (FV u)
end. end.
Definition FV_free (t:term) := forall x, ~ t #x.
Fixpoint free_var_free (t:term) := match t with Lemma FV_free_st : forall t u, t u -> FV_free t -> FV_free u.
| TKind => True Proof. intros. intro. intro. exact (H0 _ (ST_trans _ _ _ H H1)). Qed.
| TType => True
| TFree 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 closed_FV : forall t, (free_var_free t) <-> (FV t) = nil. Theorem FV_are_subterms : forall t v, In v (FV t) <-> (t #v).
Proof. Proof.
intro. split ; intros. intro. split ; intros.
- induction t ; intros ; try easy. - induction t; try easy.
+ destruct H. simpl. + destruct H; subst.
assert (FV t1 = nil); auto. * constructor.
assert (FV t2 = nil); auto. * destruct H.
rewrite H1. rewrite H2. easy. + cbn in H. destruct (in_app_or _ _ _ H).
+ destruct H. simpl. * apply HSubPi1. apply IHt1. easy.
assert (FV t1 = nil); auto. * apply HSubPi2. apply IHt2. easy.
assert (FV t2 = nil); auto. + cbn in H. destruct (in_app_or _ _ _ H).
rewrite H1. rewrite H2. easy. * apply HSubAbs1. apply IHt1. easy.
+ destruct H. simpl. * apply HSubAbs2. apply IHt2. easy.
assert (FV t1 = nil); auto. + cbn in H. destruct (in_app_or _ _ _ H).
assert (FV t2 = nil); auto. * apply HSubApp1. apply IHt1. easy.
rewrite H1. rewrite H2. easy. * apply HSubApp2. apply IHt2. easy.
- induction t ; try easy. - induction t; try easy.
+ econstructor. + inversion H; subst. left. easy.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)). + simpl. apply in_or_app. inversion H; subst.
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)). * left; apply IHt1; easy.
+ econstructor. * right; apply IHt2; easy.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)). + simpl. apply in_or_app. inversion H; subst.
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)). * left; apply IHt1; easy.
+ econstructor. * right; apply IHt2; easy.
* apply IHt1. apply (proj1 (app_eq_nil (FV t1) (FV t2) H)). + simpl. apply in_or_app. inversion H; subst.
* apply IHt2. apply (proj2 (app_eq_nil (FV t1) (FV t2) H)). * left; apply IHt1; easy.
* right; apply IHt2; easy.
Qed. Qed.
Theorem closed_FV : forall t, (FV_free t) <-> (FV t) = nil.
Proof.
intro. split ; intros.
- induction t ; intros ; try easy.
+ pose proof (H v). contradiction H0. constructor.
+ epose proof (FV_free_st _ t1 _ H).
epose proof (FV_free_st _ t2 _ H).
simpl. rewrite (IHt1 H0). rewrite (IHt2 H1). easy.
+ epose proof (FV_free_st _ t1 _ H).
epose proof (FV_free_st _ t2 _ H).
simpl. rewrite (IHt1 H0). rewrite (IHt2 H1). easy.
+ epose proof (FV_free_st _ t1 _ H).
epose proof (FV_free_st _ t2 _ H).
simpl. rewrite (IHt1 H0). rewrite (IHt2 H1). easy.
- intro. intro.
destruct (FV_are_subterms t x).
pose proof (H2 H0).
rewrite -> H in H3. inversion H3.
Admitted.
...@@ -156,6 +187,7 @@ Qed. ...@@ -156,6 +187,7 @@ Qed.
(* ************ Locally nameless representation ************ *) (* ************ Locally nameless representation ************ *)
Fixpoint open_k (t u : term) (k : nat) := Fixpoint open_k (t u : term) (k : nat) :=
match t with match t with
| TKind => t | TKind => t
...@@ -170,37 +202,40 @@ Notation "t '[' k '<-' u ']'" := (open_k t u k) (at level 24). ...@@ -170,37 +202,40 @@ 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). Theorem open_k_FV : forall t u x k, open_k t u k #x -> t #x \/ u #x.
Proof. Proof.
intro. intro. intro. induction t. intro. induction t; intros.
- intros. contradict H. - inversion H.
- intros. contradict H. - inversion H.
- intros. destruct H. rewrite H. left. left. easy. contradict H. - inversion H; subst. left. constructor.
- intros. destruct (Nat.eq_dec k n); subst. - destruct (Nat.eq_dec k n); subst.
+ right. assert ((n =? n) = true). + right. assert ((n =? n) = true).
eapply Nat.eqb_eq ; easy. eapply Nat.eqb_eq ; easy.
cbn in H. rewrite H0 in H. easy. cbn in H. rewrite H0 in H. easy.
+ cbn in H. assert (~ (k =? n) = true). + cbn in H. assert (~ (k =? n) = true).
* intro. apply n0. eapply Nat.eqb_eq. easy. * 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. * pose proof (Bool.not_true_is_false (k =? n) H0). cbn in H. rewrite H1 in H. left. easy.
- intros. simpl. - inversion H; subst.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0. + destruct (IHt1 _ _ _ H3).
+ simpl. pose proof (IHt1 k H0). destruct H1. * left. apply HSubPi1. easy.
left. apply in_or_app. left. easy. right. easy. * right. easy.
+ simpl. pose proof (IHt2 (S k) H0). destruct H1. + destruct (IHt2 _ _ _ H3).
left. apply in_or_app. right. easy. right. easy. * left. apply HSubPi2. easy.
- intros. simpl. cbn in H. * right. easy.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [S k <- u])) x H). destruct H0. - inversion H; subst.
+ simpl. pose proof (IHt1 k H0). destruct H1. + destruct (IHt1 _ _ _ H3).
left. apply in_or_app. left. easy. right. easy. * left. apply HSubAbs1. easy.
+ simpl. pose proof (IHt2 (S k) H0). destruct H1. * right. easy.
left. apply in_or_app. right. easy. right. easy. + destruct (IHt2 _ _ _ H3).
- intros. simpl. cbn in H. * left. apply HSubAbs2. easy.
pose proof (in_app_or (FV (t1 [k <- u])) (FV (t2 [k <- u])) x H). destruct H0. * right. easy.
+ simpl. pose proof (IHt1 k H0). destruct H1. - inversion H; subst.
left. apply in_or_app. left. easy. right. easy. + destruct (IHt1 _ _ _ H3).
+ simpl. pose proof (IHt2 k H0). destruct H1. * left. apply HSubApp1. easy.
left. apply in_or_app. right. easy. right. easy. * right. easy.
+ destruct (IHt2 _ _ _ H3).
* left. apply HSubApp2. easy.
* right. easy.
Qed. Qed.
...@@ -208,12 +243,11 @@ Qed. ...@@ -208,12 +243,11 @@ Qed.
Definition open_v (t : term) (v : Var) := t [0 <- # v]. Definition open_v (t : term) (v : Var) := t [0 <- # v].
Notation "t '[' v ']'" := (open_v t v) (at level 24). Notation "t '[' v ']'" := (open_v t v) (at level 24).