Require Import definitions. Require Import List. Require Import Bool. Section Inference. Lemma eq_pol_dec : forall (p1 p2: polarity), {p1 = p2} + {p1 <> p2}. Proof. intros p1 p2; case p1; case p2; auto; right; intro h; discriminate h. Defined. Lemma eq_typ_dec : forall (t1 t2: typ), {t1 = t2} + {t1 <> t2}. Proof. intro t1; induction t1. intro t2; case t2; auto. intros t t0 p. right. intro h. discriminate h. intro t2; case t2. right; intro h; discriminate h. intros t t0 p0. destruct (IHt1_1 t); destruct (IHt1_2 t0); destruct (eq_pol_dec p p0); try (right; intro h; inversion h; auto || left; rewrite e; rewrite e0; rewrite e1; reflexivity). left; rewrite e; rewrite e0; rewrite e1; reflexivity. Defined. Fixpoint infer (e: env) (t: trm) {struct t} : option typ := match t with | Var v => match (nth v e None) with | Some (covariant,t) => Some t | Some (nonvariant,t) => Some t | _ => None end | Cst c => Some (sigma c) | App u v => match infer e u with | None => None | Some t => match t with | int => None | arrow t1 t2 p => match infer (inv_pol p e) v with | Some t' => if (eq_typ_dec t1 t') then Some t2 else None | _ => None end end end | Abs p t1 u => match infer ((Some (p,t1))::e) u with | Some t2 => Some (arrow t1 t2 p) | None => None end end. End Inference. Section Unicity. Theorem unicity : forall (e: env) (t: trm) (t1: typ), type e t t1 -> forall (t2: typ), type e t t2 -> t1 = t2. Proof. intros e t t1 h; induction h; intros t3 h'. inversion_clear h'; rewrite H0 in H; inversion_clear H; reflexivity. inversion_clear h'; rewrite H0 in H; inversion_clear H; reflexivity. inversion_clear h'; reflexivity. inversion_clear h'; pose (f := IHh1 (arrow t0 t3 p0) H); inversion f; reflexivity. inversion_clear h'; rewrite (IHh t4 H); reflexivity. Qed. End Unicity. Section Utilities. Lemma option_case : forall (q: option (polarity * typ)), (exists p, exists t, q = Some (p,t)) \/ q = None. Proof. intro q; case q. intros (a,b); left; exists a; exists b; reflexivity. right; reflexivity. Qed. Lemma option_case2 : forall (ty: option typ), (ty = Some int) \/ (exists t1, exists t2, exists p, ty = Some (arrow t1 t2 p)) \/ ty = None. Proof. intro ty; case ty. intro t; case t. left; reflexivity. intros t0 t1 p; right; left; exists t0; exists t1; exists p; reflexivity. right; right; reflexivity. Qed. Lemma option_case3 : forall (ty: option typ), (exists t, ty = Some t) \/ ty = None. Proof. intro ty; case ty. intro t; left; exists t; reflexivity. right; reflexivity. Qed. Lemma option_case4 : forall (t: option typ), {ty | t = Some ty} + {t = None}. Proof. intro t; case t. intro t0; left; exists t0; reflexivity. right; reflexivity. Qed. Lemma nth_case : forall (n: nat) (e: env), (exists t, nth n e None = Some (pair nonvariant t)) \/ (exists t, nth n e None = Some (pair covariant t)) \/ (exists t, nth n e None = Some (pair contravariant t)) \/ nth n e None = None. Proof. intros n e; case (nth n e None). intros (p,t); case p. left; exists t; reflexivity. right; left; exists t; reflexivity. right; right; left; exists t; reflexivity. right; right; right; reflexivity. Qed. End Utilities. Section Correction. (* Correction de l'inférence de types *) Lemma infer_cor : forall (t: trm) (e: env) (ty: typ), infer e t = Some ty -> type e t ty. Proof. intros t; induction t. intros e ty h; simpl in h; destruct (nth_case n e). destruct H; rewrite H in h; inversion h; rewrite <- H1; apply varn; assumption. destruct H. destruct H; rewrite H in h; inversion h; rewrite <- H1; constructor; assumption. destruct H. destruct H; rewrite H in h; inversion h. rewrite H in h; inversion h. simpl; intros e ty h; inversion_clear h; constructor. intros e ty h; simpl in h; destruct (option_case2 (infer e t1)). rewrite H in h; discriminate h. destruct H. destruct H; destruct H; destruct H; rewrite H in h; destruct (option_case3 (infer (inv_pol x1 e) t2)). destruct H0; rewrite H0 in h; destruct (eq_typ_dec x x2). inversion h; rewrite H2 in *; econstructor. eexact (IHt1 e (arrow x ty x1) H). rewrite e0; exact (IHt2 (inv_pol x1 e) x2 H0). discriminate h. rewrite H0 in h; discriminate h. rewrite H in h; discriminate h. intros e ty h; simpl in h; destruct (option_case3 (infer (Some (p, t) :: e) t0)). destruct H; rewrite H in h; inversion_clear h; constructor; exact (IHt (Some (p, t) :: e) x H). rewrite H in h; discriminate h. Qed. End Correction. Section Completeness. (* Complétude de l'inférence de types *) Lemma infer_com : forall (t: trm) (e: env) (ty: typ), type e t ty -> infer e t = Some ty. Proof. intros t e ty h; induction h; simpl; auto. rewrite H; reflexivity. rewrite H; reflexivity. rewrite IHh1; rewrite IHh2; case (eq_typ_dec t1 t1). intros _; reflexivity. intro h; elim h; reflexivity. rewrite IHh; reflexivity. Qed. End Completeness. Section Decidability. (* Décidabilité de l'inférence de types *) Theorem decidabilite : forall (e: env) (t: trm), {ty | type e t ty} + {forall ty, ~ type e t ty}. Proof. intros e t; destruct (option_case4 (infer e t)). left; destruct s; exists x; apply infer_cor; assumption. right; intros ty h; rewrite (infer_com t e ty h) in e0; discriminate e0. Qed. End Decidability.