Commit 73d1039d by Gaspard Ferey

### Some proofs for full_db.

parent c340e2a1
 (** 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 List. ... ... @@ -34,6 +28,60 @@ Notation "t '@' u" := (TApp t u) (at level 21, left associativity). Definition type : term := TType. Definition kind : term := TKind. (* ************ Free variables ************ *) Fixpoint FV (t:term) : list Var := match t with | TKind => nil | TType => nil | TSymb v => cons v nil | TBound _ => nil | TPi A B => (FV A) ++ (FV B) | TAbs A B => (FV A) ++ (FV B) | TApp t u => (FV t) ++ (FV u) end. 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 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. simpl. assert (FV t1 = nil); auto. assert (FV t2 = nil); auto. rewrite H1. rewrite H2. easy. + destruct H. simpl. assert (FV t1 = nil); auto. assert (FV t2 = nil); auto. rewrite H1. rewrite H2. easy. - induction t ; try easy. + 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)). + 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)). + 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. (* ************ Contexts ************ *) Inductive signature : Set := ... ... @@ -42,46 +90,48 @@ Inductive signature : Set := | SRel : term -> term -> signature -> signature. Notation "[ ]" := SEmpty (at level 0). Notation "Γ ',' x ':' A" := (SVar x A Γ) (at level 50, x at level 30, A at level 30). Notation "Γ ',' t '≡' u" := (SRel t u Γ) (at level 50, t at level 30, u at level 30). Notation "Σ ',' x ':' A" := (SVar x A Σ) (at level 50, x at level 25, A at level 25). Notation "Σ ',' t '≡' u" := (SRel t u Σ) (at level 50, t at level 25, u at level 25). Definition local_context : Set := list term. Notation "Σ ',' T" := (cons T Σ) (at level 50, T at level 30). Definition context : Set := signature * local_context. Notation "Γ ';' Σ" := (pair Γ Σ) (at level 35, Σ at level 35). 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 Γ. Fixpoint defined_symb (Γ:signature) : list Var := match Γ with Fixpoint defined_symb (Σ:signature) : list Var := match Σ with | SEmpty => nil | SVar x _ Γ => cons x (defined_symb Γ) | SRel _ _ Γ => (defined_symb Γ) | SVar x _ Σ => cons x (defined_symb Σ) | SRel _ _ Σ => (defined_symb Σ) end. Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80). Reserved Notation "x ':' A '∈' Σ" (at level 80, A at level 80, Σ at level 80). Inductive InCtx : signature -> Var -> term -> Prop := | INow : forall Γ x A, x : A ∈ (Γ, x : A) | 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) where "x ':' A ∈ Γ" := (InCtx Γ x A). | INow : forall Σ x A, x : A ∈ (Σ, x : A) | 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) 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 80, u at level 80, Σ at level 80). Inductive InRelCtx : signature -> term -> term -> Prop := | IRNow : forall Γ t u, t ≡ u ∈ (Γ, t ≡ u) | IRAfterV : forall Γ t u y B, t ≡ u ∈ Γ -> t ≡ u ∈ (Γ, y : B) | IRAfterR : forall Γ t u v w, t ≡ u ∈ Γ -> t ≡ u ∈ (Γ, v ≡ w) where "t '≡' u ∈ Γ" := (InRelCtx Γ t u). | IRNow : forall Σ t u, t ≡ u ∈ (Σ, t ≡ u) | IRAfterV : forall Σ t u y B, t ≡ u ∈ Σ -> t ≡ u ∈ (Σ, y : B) | IRAfterR : forall Σ t u v w, t ≡ u ∈ Σ -> t ≡ u ∈ (Σ, v ≡ w) where "t '≡' u ∈ Σ" := (InRelCtx Σ t u). Definition Defined_var Γ v := exists T, v : T ∈ Γ. Definition Fresh_var Γ v := ~ (Defined_var Γ v). Definition Defined_var Σ v := exists T, v : T ∈ Σ. Definition Fresh_var Σ v := ~ (Defined_var Σ v). Notation "x '∈' Γ" := (Defined_var Γ x) (at level 90, Γ at level 90). Notation "x '∉' Γ" := (Fresh_var Γ x) (at level 90, Γ at level 90). Notation "x '∈' Σ" := (Defined_var Σ x) (at level 90, Σ at level 90). Notation "x '∉' Σ" := (Fresh_var Σ x) (at level 90, Σ at level 90). 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. intros. split; intros. ... ... @@ -89,20 +139,20 @@ Proof. + left. easy. + right. easy. + easy. - induction Γ. - induction Σ. + contradiction H. + destruct (var_dec v v0). * subst. econstructor. econstructor. * assert (v ∈ Γ). apply IHΓ. destruct H. contradiction n. easy. easy. * assert (v ∈ Σ). apply IHΣ. destruct H. contradiction n. easy. easy. destruct H0. econstructor. apply IAfterV. apply H0. easy. + assert (v ∈ Γ). apply IHΓ. exact H. + assert (v ∈ Σ). apply IHΣ. exact H. destruct H0. econstructor. apply IAfterR. apply H0. Qed. (* ************ Substitution ************ *) Reserved Notation "t '▷' u" (at level 40, u at level 25). 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 ... ... @@ -188,72 +238,75 @@ Notation "'λ' x ':' A '~' B" := (TPi A (close B x)) (at level 22, A at level 2 Notation "'Π' x ':' A '=>' B" := (TAbs A (close B x)) (at level 22, A at level 21, right associativity). Definition ConvScheme := context -> term -> term -> Prop. Definition ConvScheme := signature -> term -> term -> Prop. Inductive RW_Head_Beta : ConvScheme := RWBeta : forall Γ A t u, RW_Head_Beta Γ ((λ A ~ t) @ u) (subst_k t u 0). RWBeta : forall Σ A t u, RW_Head_Beta Σ ((λ A ~ t) @ u) (subst_k t u 0). Inductive RW_Head_Gamma : ConvScheme := RWRel : forall Γ Σ t u, t ≡ u ∈ Γ -> RW_Head_Gamma (Γ;Σ) t u. RWRel : forall Σ t u, t ≡ u ∈ Σ -> RW_Head_Gamma Σ t u. Inductive ContextClosure (Cv:ConvScheme) : ConvScheme := | CCHere : forall Γ t u , Cv Γ t u -> ContextClosure Cv Γ t u | CCApp1 : forall Γ f g t, Cv Γ f g -> ContextClosure Cv Γ (TApp f t) (TApp g t) | CCApp2 : forall Γ f t u, Cv Γ t u -> ContextClosure Cv Γ (TApp f t) (TApp f u) | CCAbs1 : forall Γ A B t, Cv Γ A B -> ContextClosure Cv Γ (TAbs A t) (TApp B t) | CCAbs2 : forall Γ A t u, Cv Γ t u -> ContextClosure Cv Γ (TAbs A t) (TAbs A u) | CCPi1 : forall Γ A B C, Cv Γ A B -> ContextClosure Cv Γ (TPi A C) (TApp B C) | CCPi2 : forall Γ A B C, Cv Γ B C -> ContextClosure Cv Γ (TPi A B) (TApp A C). | CCHere : forall Σ t u , Cv Σ t u -> ContextClosure Cv Σ t u | CCApp1 : forall Σ f g t, Cv Σ f g -> ContextClosure Cv Σ (TApp f t) (TApp g t) | CCApp2 : forall Σ f t u, Cv Σ t u -> ContextClosure Cv Σ (TApp f t) (TApp f u) | CCAbs1 : forall Σ A B t, Cv Σ A B -> ContextClosure Cv Σ (TAbs A t) (TApp B t) | CCAbs2 : forall Σ A t u, Cv Σ t u -> ContextClosure Cv Σ (TAbs A t) (TAbs A u) | CCPi1 : forall Σ A B C, Cv Σ A B -> ContextClosure Cv Σ (TPi A C) (TApp B C) | CCPi2 : forall Σ A B C, Cv Σ B C -> ContextClosure Cv Σ (TPi A B) (TApp A C). Inductive ConvUnion (C1:ConvScheme) (C2:ConvScheme) : ConvScheme := | CV1 : forall Γ t u , C1 Γ t u -> ConvUnion C1 C2 Γ t u | CV2 : forall Γ t u , C2 Γ t u -> ConvUnion C1 C2 Γ t u. | CV1 : forall Σ t u , C1 Σ t u -> ConvUnion C1 C2 Σ t u | CV2 : forall Σ t u , C2 Σ t u -> ConvUnion C1 C2 Σ t u. Inductive RTClosure (C:ConvScheme) : ConvScheme := | RWRule : forall Γ t u , C Γ t u -> RTClosure C Γ t u | RWRefl : forall Γ t , RTClosure C Γ t t | RWTrans : forall Γ t u v, RTClosure C Γ t u -> RTClosure C Γ u v -> RTClosure C Γ t v. | RWRule : forall Σ t u , C Σ t u -> RTClosure C Σ t u | RWRefl : forall Σ t , RTClosure C Σ t t | RWTrans : forall Σ t u v, RTClosure C Σ t u -> RTClosure C Σ u v -> RTClosure C Σ t v. Inductive RSTClosure (C:ConvScheme) : ConvScheme := | CVRefl : forall Γ t , RSTClosure C Γ t t | CVSym : forall Γ t u , RSTClosure C Γ t u -> RSTClosure C Γ u t | CVTrans : forall Γ t u v, RSTClosure C Γ t u -> RSTClosure C Γ u v -> RSTClosure C Γ t v | CVRule : forall Γ t u , C Γ t u -> RSTClosure C Γ t u. | CVRefl : forall Σ t , RSTClosure C Σ t t | CVSym : forall Σ t u , RSTClosure C Σ t u -> RSTClosure C Σ u t | CVTrans : forall Σ t u v, RSTClosure C Σ t u -> RSTClosure C Σ u v -> RSTClosure C Σ t v | CVRule : forall Σ t u , C Σ t u -> RSTClosure C Σ t u. Definition RW_Beta : ConvScheme := ContextClosure RW_Head_Beta. Definition RW_Gamma : ConvScheme := ContextClosure RW_Head_Gamma. Definition RW_Beta_Gamma : ConvScheme := ConvUnion RW_Beta RW_Gamma. Notation "Γ '⊢' t '→β' u" := ( RW_Head_Beta Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '→Γ' u" := ( RW_Head_Gamma Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪β' u" := ( RW_Beta Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪Γ' u" := ( RW_Gamma Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪βΓ' u" := ( RW_Beta_Gamma Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪β*' u" := ((RTClosure RW_Beta ) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪Γ*' u" := ((RTClosure RW_Gamma ) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '↪βΓ*' u" := ((RTClosure RW_Beta_Gamma) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '≡β' u" := ((RSTClosure RW_Beta ) Γ t u) (at level 40, t at level 25). Notation "Γ '⊢' t '≡Γ' u" := ((RSTClosure RW_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). Reserved Notation "ΓΣ '⊢' t ':' A" (at level 40, t at level 25, A at level 25). Reserved Notation "ΓΣ ✓" (at level 40). Inductive typing : context -> term -> term -> Prop := | TyAxiom : forall Γ Σ x A, Γ;Σ ✓ -> x : A ∈ Γ -> Γ;Σ ⊢ (# x) : A | TyType : forall Γ Σ, Γ;Σ ✓ -> Γ;Σ ⊢ type : kind | TyPi : forall Γ Σ A B s, Γ;Σ ⊢ A : type -> Γ;(Σ,A) ⊢ B : s -> Γ;Σ ⊢ Π A ~ B : s | 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] | TyConv : forall Γ Σ t A B s, Γ;Σ ⊢ t : A -> Γ;Σ ⊢ B : s -> Γ;Σ ⊢ A ≡ B -> Γ;Σ ⊢ t : B where "ΓΣ '⊢' t ':' A" := (typing ΓΣ t A) with well_formed : context -> Prop := | WFEmpty : [ ]; nil ✓ | WFVarT : forall Γ x A, x ∉ Γ -> Γ; nil ⊢ A : type -> Γ, x : A; nil ✓ | WFVarK : forall Γ x A, x ∉ Γ -> Γ; nil ⊢ A : kind -> Γ, x : A; nil ✓ | WFRel : forall Γ A s t u, Γ;nil ⊢ A : s -> Γ;nil ⊢ t : A -> Γ;nil ⊢ u : A -> Γ;nil ✓ -> Γ, t ≡ u;nil ✓ | WFLVar : forall Γ Σ A, Γ;Σ ⊢ A : type -> Γ;(Σ,A) ✓ where "ΓΣ ✓" := (well_formed ΓΣ). Notation "Σ '⊢' t '→β' u" := ( RW_Head_Beta Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '→Γ' u" := ( RW_Head_Gamma Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪β' u" := ( RW_Beta Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪Γ' u" := ( RW_Gamma Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪βΓ' u" := ( RW_Beta_Gamma Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪β*' u" := ((RTClosure RW_Beta ) Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪Γ*' u" := ((RTClosure RW_Gamma ) Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '↪βΓ*' u" := ((RTClosure RW_Beta_Gamma) Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '≡β' u" := ((RSTClosure RW_Beta ) Σ t u) (at level 40, t at level 25). Notation "Σ '⊢' t '≡Γ' u" := ((RSTClosure RW_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). 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 "Σ '+' Γ ✓" (at level 41). Inductive typing : signature -> local_context -> term -> term -> Prop := | TyAxiom : forall Σ Γ x A, Σ + Γ ✓ -> (x : A ∈ Σ) -> (Σ ; Γ ⊢ (# x) : A) | TyType : forall Σ Γ, Σ + Γ ✓ -> Σ;Γ ⊢ type : kind | TyPi : forall Σ Γ A B s, Σ;Γ ⊢ A : type -> Σ;(Γ,A) ⊢ B : s -> Σ;Γ ⊢ Π A ~ B : s | 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] | TyConv : forall Σ Γ t A B s, Σ;Γ ⊢ t : A -> Σ;Γ ⊢ B : s -> (Σ ⊢ A ≡ B) -> Σ;Γ ⊢ t : B where "Σ ';' Γ '⊢' t ':' A" := (typing Σ Γ t A) with well_formed : signature -> Prop := | WFEmpty : [ ] WF | WFVarT : forall Σ x A, x ∉ Σ -> Σ;nil ⊢ A : type -> Σ WF -> Σ, x : A WF | WFVarK : forall Σ x A, x ∉ Σ -> Σ;nil ⊢ A : kind -> Σ WF -> Σ, x : A WF | WFRel : forall Σ A s t u, Σ;nil ⊢ A : s -> Σ;nil ⊢ t : A -> Σ;nil ⊢ u : A -> Σ WF -> Σ, t ≡ u WF where "Σ 'WF'" := (well_formed Σ) with cwell_formed : signature -> local_context -> Prop := | CWFEmpty : forall Σ, Σ WF -> Σ + nil ✓ | CWFLVar : forall Σ Γ A, Σ;Γ ⊢ A : type -> Σ + Γ ✓ -> Σ + (Γ,A) ✓ where "Σ '+' Γ ✓" := (cwell_formed Σ Γ).
 ... ... @@ -2,6 +2,10 @@ Require Import List. Require Import LPTerm. Require Import WF. Require Import conversion. Require Import properties. Parameter OtherVars : Set. ... ...
 STT.vo STT.glob STT.v.beautified: STT.v ./LPTerm.vo STT.vio: STT.v ./LPTerm.vio STT.vo STT.glob STT.v.beautified: STT.v ./LPTerm.vo ./WF.vo ./conversion.vo ./properties.vo STT.vio: STT.v ./LPTerm.vio ./WF.vio ./conversion.vio ./properties.vio
 ... ... @@ -3,123 +3,134 @@ Require Import PeanoNat. Require Import List. Require Import LPTerm. Lemma types_WF : forall Γ t u, Γ ⊢ t : u -> Γ ✓. Proof. intros. induction H; easy. Qed. Lemma vardecl_WF : forall Γ x A, Γ, x : A ✓ -> Γ ✓. Lemma vardecl_WF : forall Σ x A, Σ, x : A WF -> Σ WF. Proof. intros. remember (Γ, x : A) as Γ2. induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0. remember (Σ, x : A) as Σ2. induction H; inversion HeqΣ2; subst; easy. Qed. Lemma ruldecl_WF : forall Γ t u, Γ, t ≡ u ✓ -> Γ ✓. Lemma context_WF : forall Σ Γ, Σ + Γ ✓ -> Σ WF. Proof. intros. induction H; easy. Qed. Lemma loccontext_WF : forall Σ Γ t u, Σ;Γ ⊢ t : u -> Σ + Γ ✓. Proof. intros. induction H; easy. Qed. Lemma types_WF : forall Σ Γ t u, Σ;Γ ⊢ t : u -> Σ WF. Proof. intros. eapply context_WF. eapply loccontext_WF. apply H. Qed. Lemma ruldecl_WF : forall Σ t u, Σ, t ≡ u WF -> Σ WF. Proof. intros. remember (Γ, t ≡ u) as Γ2. induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0. remember (Σ, t ≡ u) as Σ2. induction H; inversion HeqΣ2; subst; eapply types_WF; apply H0. Qed. Theorem lemma_open_k_FV : forall x B t, In x (FV B) -> forall k, In x (FV (B[k <- t])). Theorem lemma_open_k_FV : forall x B t, B ▷ # x -> forall k, B[k <- t] ▷ # x. Proof. do 4 intro. induction B; intros; try inversion H. - subst. left. easy. - inversion H0. - simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H). + left. eapply IHB1. easy. + right. eapply IHB2. easy. - simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H). + left. eapply IHB1. easy. + right. eapply IHB2. easy. - simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H). + left. eapply IHB1. easy. + right. eapply IHB2. easy. induction B; intros; try inversion H; subst; simpl. - easy. - apply HSubPi1. apply IHB1. easy. - apply HSubPi2. apply IHB2. easy. - apply HSubAbs1. apply IHB1. easy. - apply HSubAbs2. apply IHB2. easy. - apply HSubApp1. apply IHB1. easy. - apply HSubApp2. apply IHB2. easy. Qed. Theorem lemma_open_FV : forall x B t, In x (FV B) -> In x (FV (B[t])). Proof. intros. exact (lemma_open_k_FV x B (# t) H 0). Qed. Theorem lemma_open_FV : forall x B, B ▷ # x -> forall t, B[t] ▷ # x. Proof. intros. eapply lemma_open_k_FV. easy. Qed. Definition typable (Σ:signature) (t:term) : Prop := exists Γ T, Σ;Γ ⊢ t : T. Theorem FV_decl_t : forall Γ t u, Γ ⊢ t : u -> forall v, In v (FV t) -> v ∈ Γ. Lemma vardecl_typable : forall Σ x A, Σ, x : A WF -> typable Σ A. Proof. intros. inversion H; subst; repeat eexists; apply H4. Qed. Theorem ST_typable : forall Σ t t', t ▷ t' -> typable Σ t -> typable Σ t'. Proof. intros. induction H. - inversion H0. subst. exists A. easy. inversion H2. - inversion H0. - destruct (in_app_or (FV A) (FV B) v H0). + apply IHtyping. easy. + destruct (var_inf (v :: L)). assert (v ∈ Γ, x : A). * apply H2. ++ intro. apply H4. right. easy. ++ apply lemma_open_FV. easy. * inversion H5. inversion H6; subst. ++ contradiction H4. left. easy. ++ exists x0. easy. - destruct (in_app_or (FV A) (FV t) v H0). + apply IHtyping. easy. + destruct (var_inf (v :: L)). assert (v ∈ Γ, x : A). * apply H4. ++ intro. apply H6. right. easy. ++ apply lemma_open_FV. easy. * inversion H7. inversion H8; subst. ++ contradiction H6. left. easy. ++ exists x0. easy. - destruct (in_app_or (FV t) (FV u) v H0). intros. unfold typable in H0. intros. destruct H0 as [Γ H0]. destruct H0 as [T]. induction H0; intros. - 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_. apply H0_0. + apply IHtyping1. easy. + apply IHtyping2. easy. - inversion H; subst. + repeat eexists. econstructor. apply H0_. apply H0_0. easy. + apply IHtyping1. easy. + apply IHtyping3. easy. - inversion H; subst. + repeat eexists. econstructor. apply H0_. apply H0_0. + apply IHtyping1. easy. + apply IHtyping2. easy. - apply IHtyping1. easy. Qed. Reserved Notation "Γ '⊂' Γ'" (at level 80). Theorem FV_decl_t : forall Σ t, typable Σ t -> forall v, t ▷ # v -> v ∈ Σ. Proof. intros. pose proof (ST_typable _ _ (# v) H0 H). do 2 destruct H1. remember (# v) as va. induction H1; inversion Heqva; subst. - econstructor. apply H2. - apply IHtyping1. easy. easy. easy. Qed. Reserved Notation "Σ '⊂' Σ'" (at level 80). Inductive weaker : context -> context -> Prop := | WeakRefl : forall Γ , Γ ⊂ Γ | WeakVarDecl : forall Γ x A, x ∉ Γ -> Γ ⊂ Γ, x : A | WeakRulDecl : forall Γ t u, Γ ⊂ Γ, t ≡ u | WeakNextVarDecl : forall Γ Γ' x A, Γ ⊂ Γ' -> Γ, x : A ⊂ Γ', x : A | WeakNextRulDecl : forall Γ Γ' t u, Γ ⊂ Γ' -> Γ, t ≡ u ⊂ Γ', t ≡ u where "Γ '⊂' Γ'" := (weaker Γ Γ'). Inductive weaker : signature -> signature -> Prop := | WeakRefl : forall Σ , Σ ⊂ Σ | WeakVarDecl : forall Σ x A, x ∉ Σ -> Σ ⊂ Σ, x : A | WeakRulDecl : forall Σ t u, Σ ⊂ Σ, t ≡ u | WeakNextVarDecl : forall Σ Σ' x A, Σ ⊂ Σ' -> Σ, x : A ⊂ Σ', x : A | WeakNextRulDecl : forall Σ Σ' t u, Σ ⊂ Σ' -> Σ, t ≡ u ⊂ Σ', t ≡ u where "Σ '⊂' Σ'" := (weaker Σ Σ'). Theorem subset_var_decl : forall Γ Γ' x A, Γ ⊂ Γ' -> x : A ∈ Γ -> x : A ∈ Γ'. Theorem subset_var_decl : forall Σ Σ' x A, Σ ⊂ Σ' -> x : A ∈ Σ -> x : A ∈ Σ'. Proof. intros. induction H. - easy. - apply IAfterV. easy. intro. subst. contradiction H. econstructor. exact H0. - 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. easy. + inversion HeqΓ2. - remember (Γ, t ≡ u) as Γ2. induction H0 ; inversion HeqΓ2. - remember (Σ, x0 : A0) as Σ2. induction H0. + inversion HeqΣ2. subst. apply INow. + inversion HeqΣ2. subst. apply IAfterV. apply IHweaker. easy. 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, Γ ⊂ Γ' -> t ≡ u ∈ Γ -> t ≡ u ∈ Γ'. Theorem subset_rul_decl : forall Σ Σ' t u, Σ ⊂ Σ' -> 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. - 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. + inversion HeqΣ2. subst. apply IRAfterR. apply IHweaker. easy. Qed. Theorem fresh_vars_weaker : forall Γ Γ' x, Γ ⊂ Γ' -> x ∉ Γ' -> x ∉ Γ. Theorem fresh_vars_weaker : forall Σ Σ' x, Σ ⊂ Σ' -> x ∉ Σ' -> x ∉ Σ. Proof. intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy. Qed. Notation weak_compatibility C := (forall Γ A B, C Γ A B -> forall Γ', Γ ⊂ Γ' -> Γ' ✓ -> C Γ' A B). Notation weak_compatibility C := (forall Σ A B, C Σ A B -> forall Σ', Σ ⊂ Σ' -> Σ' WF -> C Σ' A B). Theorem weak_comp_hβ : weak_compatibility RW_Head_Beta. Proof. intros. inversion H. econstructor. Qed. ... ... @@ -137,7 +148,7 @@ Notation weak_comp_func F := (forall (C:ConvScheme), weak_compatibility C -> wea Theorem weak_comp_Union : forall (C C':ConvScheme), weak_compatibility C -> weak_compatibility C' -> weak_compatibility (ConvUnion C C'). Proof. intros. generalize dependent Γ'. intros. generalize dependent Σ'. induction H1; intros. + apply CV1. eapply H. apply H1. easy. easy. + apply CV2. eapply H0. apply H1. easy. easy. ... ... @@ -145,7 +156,7 @@ Qed. Theorem weak_comp_CC : weak_comp_func ContextClosure. Proof. intros. generalize dependent Γ'. intros. generalize dependent Σ'. induction H0; intros. + apply CCHere. eapply H. apply H0. easy. easy. + apply CCApp1. eapply H. apply H0. easy. easy. ... ... @@ -158,7 +169,7 @@ Qed. Theorem weak_comp_RT : weak_comp_func RTClosure. Proof. intros. generalize dependent Γ'. intros. generalize dependent Σ'. induction H0; intros. - apply RWRule. eapply H. apply H0. easy. easy. - apply RWRefl. ... ... @@ -167,7 +178,7 @@ Qed. Theorem weak_comp_RST : weak_comp_func RSTClosure. Proof. intros. generalize dependent Γ'. intros. generalize dependent Σ'. induction H0; intros. - apply CVRefl. - apply CVSym. apply IHRSTClosure. easy. easy. ... ... @@ -176,7 +187,7 @@ Proof. Qed. Theorem weak_conv : forall Γ A B, Γ ⊢ A ≡ B -> forall Γ', Γ ⊂ Γ' -> Γ' ✓ -> Γ' ⊢ A ≡ B. Theorem weak_conv : forall Σ A B, Σ ⊢ A ≡ B -> forall Σ', Σ ⊂ Σ' -> Σ' WF -> Σ' ⊢ A ≡ B. Proof. apply weak_comp_RST. apply weak_comp_Union. ... ... @@ -186,48 +197,75 @@ Proof. apply weak_comp_hΓ. Qed. Theorem weak_typ : forall Γ Γ' t u, Γ ⊢ t : u -> Γ ⊂ Γ' -> Γ' ✓ -> Γ' ⊢ t : u. Theorem weak_typ_ : forall Σ Σ' Γ t u, Σ;Γ ⊢ t : u -> Σ ⊂ Σ' -> Σ' WF -> Σ' + Γ ✓ -> Σ';Γ ⊢ t : u. Proof. intros. generalize dependent Γ'. generalize dependent Σ'. induction H; intros. - apply TyAxiom. easy. eapply subset_var_decl. apply H1. easy. - apply TyType. easy. - eapply TyPi. + apply IHtyping. easy. easy. + intros. apply H1. assert (~ In x ( (defined_vars Γ') ++ L)). * apply H4. * intro. apply H4. apply in_or_app. right. easy. * econstructor. easy. * econstructor. ++ intro. apply H4. apply in_or_app. left. apply defined_eq. easy. ++ apply IHtyping. easy. easy. + apply IHtyping1. easy. easy. easy. + apply IHtyping2. easy. easy. econstructor. apply IHtyping1. easy. easy. easy. easy. - eapply TyAbs. + apply IHtyping. easy. easy. + intros. apply H1. assert (~ In x ( (defined_vars Γ') ++ L)). * apply H6. * intro. apply H6. apply in_or_app. right. easy. * econstructor. easy. * econstructor. ++ intro. apply H6. apply in_or_app. left. apply defined_eq. easy. ++ apply IHtyping. easy. easy. + intros. apply H3. * intro. apply H6. apply in_or_app. right. easy. * econstructor. easy. * econstructor. ++ intro. apply H6. apply in_or_app. left. apply defined_eq. easy. ++ apply IHtyping. easy. easy. + apply IHtyping1. easy. easy. easy. + apply IHtyping2. easy. easy. econstructor. apply IHtyping1. easy. easy. easy. easy. + apply IHtyping3. easy. easy. econstructor. apply IHtyping1. easy. easy. easy. easy. - eapply TyApp. + apply IHtyping1. easy. easy.