(* types simples *) Inductive Ts (A : Set) : Set := | atom : A -> Ts (A) | fleche : Ts (A) -> Ts (A) -> Ts (A). (* termes *) Inductive term (C : Set) (V : Set) : Set := | cst : C -> term C V | var : V -> term C V | app : term C V -> term C V -> term C V | lam : term C (option V) -> term C V. (* injectivité - pour les ensembles de variables *) Definition injective (V1 V2 : Set) (g : V1 -> V2) := forall x y : V1, g x = g y -> x = y. (* Une injection utile *) Definition option_inj (V1 V2 : Set) (inj : V1 -> V2) : (option V1) -> (option V2) := (fun (v : option V1) => match v with | None => None | Some v => Some (inj v) end). (* C'est bien une injection *) Lemma is_inj_option_inj (V1 V2 : Set) (inj : V1 -> V2) : injective V1 V2 inj -> injective (option V1) (option V2) (option_inj V1 V2 inj). intros. unfold injective. intros. destruct x ; destruct y ; inversion H0. assert (K := H v v0 H2). rewrite K. reflexivity. reflexivity. Qed. (* injection des termes dans des espaces plus grands *) Fixpoint inj_tm (C : Set) (V1 V2 : Set) (inj : V1 -> V2) (t : term C V1) {struct t} : term C V2 := match t with | cst c => cst C V2 c | var v => var C V2 (inj v) | app t1 t2 => app C V2 (inj_tm C V1 V2 inj t1) (inj_tm C V1 V2 inj t2) | lam u => lam C V2 (inj_tm C (option V1) (option V2) (option_inj V1 V2 inj) u) end. Lemma is_inj_inj_tm (C : Set) (V1 V2 : Set) (inj : V1 -> V2) : injective V1 V2 inj -> injective (term C V1) (term C V2) (fun (t : term C V1) => inj_tm C V1 V2 inj t). intros. intro. generalize V2 inj H. clear V2 inj H. induction x ; intros ; destruct y ; inversion H0. reflexivity. assert (K := H v v0 H2). rewrite K ; reflexivity. assert (K1 := IHx1 V2 inj H y1 H2). assert (K2 := IHx2 V2 inj H y2 H3). rewrite K1 ; rewrite K2 ; reflexivity. assert (K := IHx (option V2) (option_inj V V2 inj) (is_inj_option_inj V V2 inj H) y H2). rewrite K ; reflexivity. Qed. (* restriction de l'application de typage sur variables *) Definition restrict (V : Set) (A : Set) (tauo : (option V) -> Ts(A)) (v : V) : Ts(A) := tauo (Some v). (* ***************************************************** *) (* Bon jugement de typage *) (* ***************************************************** *) Inductive jgmt (C : Set) (V : Set) (A : Set)(tau_c : C -> Ts(A)) : forall tau_v : V -> Ts(A), forall t : term C V, forall T : Ts(A), Prop := | ax_c : forall tau_v : V -> Ts(A), forall c : C, jgmt C V A tau_c tau_v (cst C V c) (tau_c c) | ax_v : forall tau_v : V -> Ts(A), forall x : V, jgmt C V A tau_c tau_v (var C V x) (tau_v x) | ae : forall tau_v : V -> Ts(A), forall u v : term C V, forall a b : Ts(A), jgmt C V A tau_c tau_v u (fleche A a b) -> jgmt C V A tau_c tau_v v a -> jgmt C V A tau_c tau_v (app C V u v) b | ai : forall tauo : (option V) -> Ts(A), forall u : term C (option V), forall a b : Ts(A), jgmt C (option V) A tau_c tauo u b -> (tauo None) = a -> jgmt C V A tau_c (restrict V A tauo) (lam C V u) (fleche A a b). (* Axiomes d'extensionnalité *) Axiom extensionnalite_1 : forall A B : Set, forall f g : A -> B, (forall x : A, f x = g x) -> f = g. Lemma extensionnalite_2 : forall A B : Set, forall f g : A -> B, f = g -> forall x : A, f x = g x. intros. rewrite H ; reflexivity. Qed. (* Axiome de Proof Irrelevance *) Axiom PI : forall P : Prop, forall p1 p2 : P, p1 = p2. (* Jugement de typage avec variables supplémentaires *) Lemma adtocontext (C : Set) (V : Set) (A : Set) (tau_c : C -> Ts(A)) (tau_v : V -> Ts(A)) (t : term C V) (T : Ts(A)) (V' : Set) (inj : V -> V') (tau_v' : V' -> Ts(A)) : injective V V' inj -> (forall v : V, tau_v v = tau_v' (inj v)) -> jgmt C V A tau_c tau_v t T -> jgmt C V' A tau_c tau_v' (inj_tm C V V' inj t) T. unfold inj_tm. induction t ; intros ; inversion H1. apply ax_c. cut (tau_v v = tau_v' (inj v)) ; intros. rewrite H5. apply ax_v. apply H0. apply ae with a. apply IHt1 with tau_v ; assumption. apply IHt2 with tau_v ; assumption. cut (tau_v' = restrict V' A (fun v : option V' => match v with | None => a | Some v => tau_v' v end)); intros. rewrite H7. apply ai. apply IHt with tauo ; intros. apply is_inj_option_inj ; assumption. unfold option_inj. destruct v. rewrite <- H0. pose (K := extensionnalite_2 V (Ts A) (restrict V A tauo) tau_v H4 v). apply K. assumption. assumption. reflexivity. apply extensionnalite_1 ; intros v. unfold restrict. reflexivity. Qed. (* ************************************************** *) (* Signature *) (* ************************************************** *) Record sign : Type := {C : Set ; A : Set ; fi : C -> Ts(A) }. (* Définition pour simplifier les notations *) Definition jgmt_sign (S : sign) (V : Set) (tau_x : V -> Ts(A S)) (t : term (C S) V) (T : Ts(A S)) := jgmt (C S) V (A S) (fi S) tau_x t T. (* extension du morphisme des types atomiques *) Fixpoint phi_tp (A B : Set) (fi : A -> Ts(B)) (t : Ts(A)) {struct t} : Ts(B) := match t with | atom t => fi t | fleche t1 t2 => fleche B (phi_tp A B fi t1) (phi_tp A B fi t2) end. (* ensemble vide de variables *) Inductive Vide : Set :=. Definition tau_vide (A : Set) (v : Vide) : Ts(A) := match v with end. (* ************************************************** *) (* Lexique *) (* ************************************************** *) (* Relation vérifiée par un lexique *) Definition rel_lex (S1 S2 : sign) (fi_c : (C S1) -> term (C S2) Vide) (fi_a : (A S1) -> Ts(A S2)) := forall c : (C S1), jgmt_sign S2 Vide (tau_vide (A S2)) (fi_c c) (phi_tp (A S1) (A S2) fi_a ((fi S1) c)). Record lex (abs obj : sign) : Type := { fi__c : (C abs) -> term (C obj) Vide; fi__a : (A abs) -> Ts(A obj); lrel : rel_lex abs obj fi__c fi__a }. Notation fi_c := (fi__c _ _). Notation fi_a := (fi__a _ _). Notation rel := (lrel _ _). (* Lemme pour prouver des égalités de lexiques *) Lemma prove_some_eq_lex (S1 S2 : sign) (l1 l2 : lex S1 S2) : fi_a l1 = fi_a l2 -> fi_c l1 = fi_c l2 -> l1 = l2. intros. destruct l1 ; destruct l2. simpl in *|-*. generalize lrel1. rewrite <- H0 ; rewrite <- H. intros. assert (lrel0 = lrel2). apply PI. rewrite H1. reflexivity. Qed. (* ***************************** *) Definition inj_vide (A : Set) : Vide -> A. intros ; destruct H. Qed. Lemma is_inj_vide (A : Set) : injective Vide A (inj_vide A). intros ; unfold injective ; intros ; destruct x. Qed. Lemma is_inj_id (V : Set) : injective V V (fun v : V => v). unfold injective ; auto. Qed. Lemma fun_inj_vide : (inj_vide Vide)=(fun v : Vide => v). apply extensionnalite_1 ; intros. destruct x. Qed. Lemma inj_tm_V_V (C : Set) (V : Set) (t : term C V) : t = inj_tm C V V (fun v : V => v) t. induction t ; simpl ; try reflexivity. rewrite <- IHt1. rewrite <- IHt2. reflexivity. unfold option_inj. cut ( (fun v : option V => v)= (fun v : option V => match v with | Some v0 => Some v0 | None => None (A:=V) end)) ; intros. rewrite <- H. rewrite <- IHt. reflexivity. apply extensionnalite_1 ; intros. destruct x ; reflexivity. Qed. (* extension du morphisme des constantes *) Fixpoint phi_tm (C1 C2 : Set) (fi : C1 -> term C2 Vide) (V : Set) (t : term C1 V) {struct t} : term C2 V := match t with | cst c => inj_tm C2 Vide V (inj_vide V) (fi c) | var x => var C2 V x | app u v => app C2 V (phi_tm C1 C2 fi V u) (phi_tm C1 C2 fi V v) | lam u => lam C2 V (phi_tm C1 C2 fi (option V) u) end. (* extension types dans lui-même *) Definition phi_tp_a (A : Set) : (A -> Ts(A)) -> Ts(A) -> Ts(A) := phi_tp A A. (* extension termes dans lui-même *) Definition phi_tm_a (C : Set) (V : Set) : (C -> term C Vide) -> forall V : Set, term C V -> term C V := phi_tm C C. (* Définitions pour simplifier les notations *) Definition phi_term_lex (abs obj : sign) (l : lex abs obj) (V : Set) (t : term (C abs) V) := phi_tm (C abs) (C obj) (fi_c l) V t. Definition phi_type_lex (abs obj : sign) (l : lex abs obj) (T : Ts(A abs)) := phi_tp (A abs) (A obj) (fi_a l) T. Lemma perm_phi_restr : forall A1 A2 : Set, forall V : Set, forall fi : A1 -> Ts A2, forall tau : option V -> Ts A1, (fun v : V => phi_tp A1 A2 fi (restrict V A1 tau v)) = restrict V A2 (fun v : option V => phi_tp A1 A2 fi (tau v)). intros. unfold restrict. reflexivity. Qed. (* Lemme prouvant l'extension de la relation *) Lemma ext_rel : forall abs obj : sign, forall l : lex abs obj, forall V : Set, forall tau : V -> Ts (A abs), forall t : term (C abs) V, forall T : Ts(A abs), jgmt_sign abs V tau t T -> jgmt_sign obj V (fun v => phi_tp (A abs) (A obj) (fi_a l) (tau v)) (phi_tm (C abs) (C obj) (fi_c l) V t) (phi_tp (A abs) (A obj) (fi_a l) T). unfold jgmt_sign. induction t ; intros. simpl phi_tm. apply adtocontext with (fun v : Vide => match v return (Ts (A obj)) with end). apply is_inj_vide. intros ; destruct v. inversion H. apply (rel l). inversion H. unfold phi_tm. apply (@ax_v (C obj) V (A obj) (fi obj) (fun v0 : V => phi_tp (A abs) (A obj) (fi_a l) (tau v0))). (* obligé sinon il cherche à unifier 'v' et 'tau v' *) (* qui n'ont pas le même type ! *) inversion H. unfold phi_tm in * |-*. apply ae with (phi_tp (A abs) (A obj) (fi_a l) a). apply (@IHt1 tau (fleche (A abs) a T)). assumption. apply IHt2. assumption. inversion H. rewrite perm_phi_restr. unfold phi_tm. unfold phi_tp. apply ai. apply IHt. assumption. rewrite H3. reflexivity. Qed. (* *************************************************** *) (* Identité *) (* *************************************************** *) Lemma eq_phi_tp_id : forall S : sign, forall c : (C S), (fi S c) = (phi_tp (A S) (A S) (fun a : A S => atom (A S) a) (fi S c)). intros. induction (fi S c). simpl. reflexivity. simpl. rewrite <- IHt1. rewrite <- IHt2. reflexivity. Qed. Definition fi_c_id (S : sign) := fun c : (C S) => cst (C S) Vide c. Definition fi_a_id (S : sign) := fun a : (A S) => atom (A S) a. Lemma rel_id : forall S : sign, forall c : (C S), jgmt_sign S Vide (tau_vide (A S)) (fi_c_id S c) (phi_tp (A S) (A S) (fi_a_id S) ((fi S) c)). intros. unfold jgmt_sign. unfold fi_a_id. rewrite <- eq_phi_tp_id. unfold fi_c_id. apply ax_c. Qed. (* construction du lexique identité *) Definition lex_id (S : sign) := Build_lex S S (fi_c_id S) (fi_a_id S) (rel_id S). (* *************************************************** *) (* Composition *) (* *************************************************** *) Lemma phi_tp_vide (S2 S3 : sign) (fi_a2 : (A S2) -> Ts(A S3)) : tau_vide (A S3) = (fun v => phi_tp (A S2) (A S3) fi_a2 (tau_vide (A S2) v)). intros. apply extensionnalite_1. intros. destruct x. Qed. Definition fi_c_comp (S1 S2 S3 : sign) (fi_c1 : (C S1) -> term (C S2) Vide) (fi_c2 : (C S2) -> term (C S3) Vide) := fun c : (C S1) => phi_tm (C S2) (C S3) fi_c2 Vide (fi_c1 c). Definition fi_a_comp (S1 S2 S3 : sign) (fi_a1 : (A S1) -> Ts(A S2)) (fi_a2 : (A S2) -> Ts(A S3)) := fun a : (A S1) => phi_tp (A S2) (A S3) fi_a2 (fi_a1 a). Lemma phi_tp_comp (S1 S2 S3 : sign) (fi_a1 : (A S1) -> Ts(A S2)) (fi_a2 : (A S2) -> Ts(A S3)) : forall T : Ts(A S1), (phi_tp (A S1) (A S3) (fi_a_comp S1 S2 S3 fi_a1 fi_a2) T) = (phi_tp (A S2) (A S3) fi_a2 (phi_tp (A S1) (A S2) fi_a1 T)). intros. induction T ; simpl. reflexivity. rewrite IHT1. rewrite IHT2. reflexivity. Qed. Lemma rel_comp (S1 S2 S3 : sign) (l1 : lex S1 S2) (l2 : lex S2 S3) : forall c : (C S1), jgmt_sign S3 Vide (tau_vide (A S3)) ((fi_c_comp S1 S2 S3 (fi_c l1) (fi_c l2) c)) (phi_tp (A S1) (A S3) (fi_a_comp S1 S2 S3 (fi_a l1) (fi_a l2)) ((fi S1) c)). intros. rewrite phi_tp_vide with S2 S3 (fi_a l2). rewrite phi_tp_comp. unfold fi_c_comp. apply ext_rel. apply (rel l1). Qed. (* construction du lexique composition *) Definition lex_comp (S1 S2 S3 : sign) (l1 : lex S1 S2) (l2 : lex S2 S3) := Build_lex S1 S3 (fi_c_comp S1 S2 S3 (fi_c l1) (fi_c l2)) (fi_a_comp S1 S2 S3 (fi_a l1) (fi_a l2)) (rel_comp S1 S2 S3 l1 l2). (* ************************************************ *) (* Vérification des propriétés pour catégorie *) (* ************************************************ *) (* identité gauche *) Lemma comp_lex_id_g (S1 S2 : sign) (l : lex S1 S2) : lex_comp S1 S1 S2 (lex_id S1) l = l. destruct l. unfold lex_comp. unfold rel_lex in *|-. apply prove_some_eq_lex ; simpl. apply extensionnalite_1 ; intros. reflexivity. apply extensionnalite_1 ; intros. unfold fi_c_comp ; simpl. rewrite fun_inj_vide ; symmetry. apply (inj_tm_V_V (C S2) Vide (fi__c0 x)). Qed. (* identité droite *) Lemma comp_lex_id_d (S1 S2 : sign) (l : lex S1 S2) : lex_comp S1 S2 S2 l (lex_id S2) = l. destruct l. unfold lex_comp. unfold rel_lex in *|-. apply prove_some_eq_lex ; simpl. apply extensionnalite_1 ; intros ; unfold fi_a_comp ; simpl. generalize (fi__a0 x). simple induction t ; intros ; simpl ; try reflexivity. rewrite H ; rewrite H0 ; reflexivity. unfold fi_c_comp ; simpl. apply extensionnalite_1 ; intros. generalize (fi__c0 x). simple induction t ; try intros ; simpl ; try reflexivity. rewrite H ; rewrite H0 ; reflexivity. rewrite H ; reflexivity. Qed. (* Associativité injection *) Lemma comp_inj (S3 : sign) (V1 : Set) (t : term (C S3) V1) : forall (V V0 : Set) (inj : V -> V0) (inj1 : V1 -> V), inj_tm (C S3) V V0 inj (inj_tm (C S3) V1 V inj1 t) = inj_tm (C S3) V1 V0 (fun v1 : V1 => inj (inj1 v1)) t. induction t ; simpl ; intros. reflexivity. reflexivity. rewrite IHt1 ; rewrite IHt2 ; reflexivity. rewrite IHt. assert ( (fun v1 : option V => option_inj V0 V1 inj (option_inj V V0 inj1 v1)) = (option_inj V V1 (fun v1 : V => inj (inj1 v1))) ) ; intros. apply extensionnalite_1 ; intros. destruct x ; simpl ; reflexivity. rewrite H ; reflexivity. Qed. (* Commutativité inj et phi_tm *) Lemma comp_inj_phi_tm (V0 : Set) (S2 S3 : sign) (fi__c2 : C S2 -> term (C S3) Vide) : forall t : term (C S2) V0, forall V : Set, forall (inj : V0 -> V), inj_tm (C S3) V0 V inj (phi_tm (C S2) (C S3) fi__c2 V0 t) = phi_tm (C S2) (C S3) fi__c2 V (inj_tm (C S2) V0 V inj t). induction t ; simpl. intros. assert ((fun v : Vide => inj (inj_vide V v)) = inj_vide V0). apply extensionnalite_1 ; intros. destruct x. rewrite <- H. apply comp_inj. reflexivity. intros. rewrite IHt1. rewrite IHt2. reflexivity. intros. rewrite IHt. reflexivity. Qed. (* associativité pour termes *) Lemma comp_c_comp_V (V : Set) (S1 S2 S3 : sign) (fi__c1 : C S1 -> term (C S2) Vide) (fi__c2 : C S2 -> term (C S3) Vide) : forall t : term (C S1) V, phi_tm (C S1) (C S3) (fun c : C S1 => phi_tm (C S2) (C S3) fi__c2 Vide (fi__c1 c)) V t = phi_tm (C S2) (C S3) fi__c2 V (phi_tm (C S1) (C S2) fi__c1 V t). induction t ; simpl. apply comp_inj_phi_tm. reflexivity. rewrite IHt1. rewrite IHt2. reflexivity. rewrite IHt. reflexivity. Qed. (* associativité pour constantes *) Lemma comp_c_comp (S0 S1 S2 S3 : sign) (fi__c0 : C S0 -> term (C S1) Vide) (fi__c1 : C S1 -> term (C S2) Vide) (fi__c2 : C S2 -> term (C S3) Vide) : (fi_c_comp S0 S1 S3 fi__c0 (fi_c_comp S1 S2 S3 fi__c1 fi__c2)) = (fi_c_comp S0 S2 S3 (fi_c_comp S0 S1 S2 fi__c0 fi__c1) fi__c2) . intros. unfold fi_c_comp ; simpl. apply extensionnalite_1 ; intros. generalize (fi__c0 x). apply comp_c_comp_V. Qed. (* associativité pour atomes *) Lemma comp_a_comp (S0 S1 S2 S3 : sign) (fi__a0 : A S0 -> Ts (A S1)) (fi__a1 : A S1 -> Ts (A S2)) (fi__a2 : A S2 -> Ts (A S3)) : (fi_a_comp S0 S1 S3 fi__a0 (fi_a_comp S1 S2 S3 fi__a1 fi__a2)) = (fi_a_comp S0 S2 S3 (fi_a_comp S0 S1 S2 fi__a0 fi__a1) fi__a2) . intros. apply extensionnalite_1 ; intros. unfold fi_a_comp ; simpl. induction (fi__a0 x) ; intros ; simpl. reflexivity. rewrite <- IHt1 ; rewrite <- IHt2 ; reflexivity. Qed. (* Associativité *) Lemma comp_lex_ass (S0 S1 S2 S3 : sign) (l0 : lex S0 S1) (l1 : lex S1 S2) (l2 : lex S2 S3) : lex_comp S0 S1 S3 l0 (lex_comp S1 S2 S3 l1 l2) = lex_comp S0 S2 S3 (lex_comp S0 S1 S2 l0 l1) l2. destruct l0. destruct l1. destruct l2. apply prove_some_eq_lex ; simpl. apply comp_a_comp. apply comp_c_comp. Qed.