Initial import of compcert

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1277 insertions, 0 deletions

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
new file mode 100644
index 00000000..d15dbb88
--- /dev/null
+++ b/backend/RTLtyping.v
@@ -0,0 +1,1277 @@
+(** Typing rules and a type inference algorithm for RTL. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Op.
+Require Import Registers.
+Require Import RTL.
+Require Import union_find.
+
+(** * The type system *)
+
+(** Like Cminor and all intermediate languages, RTL can be equipped with
+  a simple type system that statically guarantees that operations
+  and addressing modes are applied to the right number of arguments
+  and that the arguments are of the correct types.  The type algebra
+  is trivial, consisting of the two types [Tint] (for integers and pointers)
+  and [Tfloat] (for floats).  
+
+  Additionally, we impose that each pseudo-register has the same type
+  throughout the function.  This requirement helps with register allocation,
+  enabling each pseudo-register to be mapped to a single hardware register
+  or stack location of the correct type.
+
+
+  The typing judgement for instructions is of the form [wt_instr f env instr],
+  where [f] is the current function (used to type-check [Ireturn] 
+  instructions) and [env] is a typing environment associating types to
+  pseudo-registers.  Since pseudo-registers have unique types throughout
+  the function, the typing environment does not change during type-checking
+  of individual instructions.  One point to note is that we have two
+  polymorphic operators, [Omove] and [Oundef], which can work both
+  over integers and floats.
+*)
+
+Definition regenv := reg -> typ.
+
+Section WT_INSTR.
+
+Variable env: regenv.
+Variable funct: function.
+
+Inductive wt_instr : instruction -> Prop :=
+  | wt_Inop:
+      forall s,
+      wt_instr (Inop s)
+  | wt_Iopmove:
+      forall r1 r s,
+      env r1 = env r ->
+      wt_instr (Iop Omove (r1 :: nil) r s)
+  | wt_Iopundef:
+      forall r s,
+      wt_instr (Iop Oundef nil r s)
+  | wt_Iop:
+      forall op args res s,
+      op <> Omove -> op <> Oundef ->
+      (List.map env args, env res) = type_of_operation op ->
+      wt_instr (Iop op args res s)
+  | wt_Iload:
+      forall chunk addr args dst s,
+      List.map env args = type_of_addressing addr ->
+      env dst = type_of_chunk chunk ->
+      wt_instr (Iload chunk addr args dst s)
+  | wt_Istore:
+      forall chunk addr args src s,
+      List.map env args = type_of_addressing addr ->
+      env src = type_of_chunk chunk ->
+      wt_instr (Istore chunk addr args src s)
+  | wt_Icall:
+      forall sig ros args res s,
+      match ros with inl r => env r = Tint | inr s => True end ->
+      List.map env args = sig.(sig_args) ->
+      env res = match sig.(sig_res) with None => Tint | Some ty => ty end ->
+      wt_instr (Icall sig ros args res s)
+  | wt_Icond:
+      forall cond args s1 s2,
+      List.map env args = type_of_condition cond ->
+      wt_instr (Icond cond args s1 s2)
+  | wt_Ireturn: 
+      forall optres,
+      option_map env optres = funct.(fn_sig).(sig_res) ->
+      wt_instr (Ireturn optres).
+
+End WT_INSTR.
+
+(** A function [f] is well-typed w.r.t. a typing environment [env],
+   written [wt_function env f], if all instructions are well-typed,
+   parameters agree in types with the function signature, and
+   names of parameters are pairwise distinct. *)
+
+Record wt_function (env: regenv) (f: function) : Prop :=
+  mk_wt_function {
+    wt_params:
+      List.map env f.(fn_params) = f.(fn_sig).(sig_args);
+    wt_norepet:
+      list_norepet f.(fn_params);
+    wt_instrs:
+      forall pc instr, f.(fn_code)!pc = Some instr -> wt_instr env f instr
+  }.
+
+(** * Type inference *)
+
+(** There are several ways to ensure that RTL code is well-typed and
+  to obtain the typing environment (type assignment for pseudo-registers)
+  needed for register allocation.  One is to start with well-typed Cminor
+  code and show type preservation for RTL generation and RTL optimizations.
+  Another is to start with untyped RTL and run a type inference algorithm
+  that reconstructs the typing environment, determining the type of
+  each pseudo-register from its uses in the code.  We follow the second
+  approach.
+
+  The algorithm and its correctness proof in this section were
+  contributed by Damien Doligez. *)
+
+(** ** Type inference algorithm *)
+
+Set Implicit Arguments.
+
+(** Type inference for RTL is similar to that for simply-typed 
+  lambda-calculus: we use type variables to represent the types
+  of registers that have not yet been determined to be [Tint] or [Tfloat]
+  based on their uses.  We need exactly one type variable per pseudo-register,
+  therefore type variables can be conveniently equated with registers.
+  The type of a register during inference is therefore either
+  [tTy t] (with [t = Tint] or [t = Tfloat]) for a known type,
+  or [tReg r] to mean ``the same type as that of register [r]''. *)
+
+Inductive myT : Set :=
+  | tTy : typ -> myT
+  | tReg : reg -> myT.
+
+(** The algorithm proceeds by unification of the currently inferred
+  type for a pseudo-register with the type dictated by its uses.
+  Unification builds on a ``union-find'' data structure representing
+  equivalence classes of types (see module [Union_find]).
+*)
+
+Module myreg.
+  Definition T := myT.
+  Definition eq : forall (x y : T), {x=y}+{x<>y}.
+  Proof.
+    destruct x; destruct y; auto;
+    try (apply right; discriminate); try (apply left; discriminate).
+    destruct t; destruct t0;
+    try (apply right; congruence); try (apply left; congruence).
+    elim (peq r r0); intros.
+    rewrite a; apply left; apply refl_equal.
+    apply right; congruence.
+  Defined.
+End myreg.
+
+Module mymap.
+  Definition elt := myreg.T.
+  Definition encode (t : myreg.T) : positive :=
+    match t with
+    | tTy Tint => xH
+    | tTy Tfloat => xI xH
+    | tReg r => xO r
+    end.
+  Definition decode (p : positive) : elt :=
+    match p with
+    | xH => tTy Tint
+    | xI _ => tTy Tfloat
+    | xO r => tReg r
+    end.
+
+  Lemma encode_decode : forall x : myreg.T, decode (encode x) = x.
+  Proof.
+    destruct x; try destruct t; simpl; auto.
+  Qed.
+
+  Lemma encode_injective :
+    forall (x y : myreg.T), encode x = encode y -> x = y.
+  Proof.
+    intros.
+    unfold encode in H. destruct x; destruct y; try congruence;
+    try destruct t; try destruct t0; congruence.
+  Qed.
+
+  Definition T := PTree.t positive.
+  Definition empty := PTree.empty positive.
+  Definition get (adr : elt) (t : T) :=
+    option_map decode (PTree.get (encode adr) t).
+  Definition add (adr dat : elt) (t : T) :=
+    PTree.set (encode adr) (encode dat) t.
+
+  Theorem get_empty : forall (x : elt), get x empty = None.
+  Proof.
+    intro.
+    unfold get. unfold empty.
+    rewrite PTree.gempty.
+    simpl; auto.
+  Qed.
+  Theorem get_add_1 :
+    forall (x y : elt) (m : T), get x (add x y m) = Some y.
+  Proof.
+    intros.
+    unfold add. unfold get.
+    rewrite PTree.gss.
+    simpl; rewrite encode_decode; auto.
+  Qed.
+  Theorem get_add_2 :
+    forall (x y z : elt) (m : T), z <> x -> get z (add x y m) = get z m.
+  Proof.
+    intros.
+    unfold get. unfold add.
+    rewrite PTree.gso; auto.
+    intro. apply H. apply encode_injective. auto.
+  Qed.
+End mymap.
+
+Module Uf := Unionfind (myreg) (mymap).
+
+Definition error := Uf.identify Uf.empty (tTy Tint) (tTy Tfloat).
+
+Fixpoint fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T)
+               (init : Uf.T) (la : list A) (lb : list B) {struct la}
+               : Uf.T :=
+  match la, lb with
+  | ha::ta, hb::tb => fold2 f (f init ha hb) ta tb
+  | nil, nil => init
+  | _, _ => error
+  end.
+
+Definition option_fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T)
+                        (init : Uf.T) (oa : option A) (ob : option B)
+                        : Uf.T :=
+  match oa, ob with
+  | Some a, Some b => f init a b
+  | None, None => init
+  | _, _ => error
+  end.
+
+Definition teq (ty1 ty2 : typ) : bool :=
+  match ty1, ty2 with
+  | Tint, Tint => true
+  | Tfloat, Tfloat => true
+  | _, _ => false
+  end.
+
+Definition type_rtl_arg (u : Uf.T) (r : reg) (t : typ) :=
+  Uf.identify u (tReg r) (tTy t).
+
+Definition type_rtl_ros (u : Uf.T) (ros : reg+ident) :=
+  match ros with
+  | inl r => Uf.identify u (tReg r) (tTy Tint)
+  | inr s => u
+  end.
+
+Definition type_of_sig_res (sig : signature) :=
+  match sig.(sig_res) with None => Tint | Some ty => ty end.
+
+(** This is the core type inference function.  The [u] argument is
+  the current substitution / equivalence classes between types.
+  An updated set of equivalence classes, reflecting unifications
+  possibly performed during the type-checking of [i], is returned.
+  Note that [type_rtl_instr] never fails explicitly.  However,
+  in case of type error (e.g. applying the [Oadd] integer operation
+  to float registers), the equivalence relation returned will
+  put [tTy Tint] and [tTy Tfloat] in the same equivalence class.
+  This fact will propagate through type inference for other instructions,
+  and be detected at the end of type inference, indicating a typing failure.
+*)
+
+Definition type_rtl_instr (rtyp : option typ)
+    (u : Uf.T) (_ : positive) (i : instruction) :=
+  match i with
+  | Inop _ => u
+  | Iop Omove (r1 :: nil) r0 _ => Uf.identify u (tReg r0) (tReg r1)
+  | Iop Omove _ _ _ => error
+  | Iop Oundef nil _ _ => u
+  | Iop Oundef _ _ _ => error
+  | Iop op args r0 _ =>
+      let (argtyp, restyp) := type_of_operation op in
+      let u1 := type_rtl_arg u r0 restyp in
+      fold2 type_rtl_arg u1 args argtyp
+  | Iload chunk addr args r0 _ =>  
+      let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in
+      fold2 type_rtl_arg u1 args (type_of_addressing addr)
+  | Istore chunk addr args r0 _ =>
+      let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in
+      fold2 type_rtl_arg u1 args (type_of_addressing addr)
+  | Icall sign ros args r0 _ =>
+      let u1 := type_rtl_ros u ros in
+      let u2 := type_rtl_arg u1 r0 (type_of_sig_res sign) in
+      fold2 type_rtl_arg u2 args sign.(sig_args)
+  | Icond cond args _ _ =>
+      fold2 type_rtl_arg u args (type_of_condition cond)
+  | Ireturn o => option_fold2 type_rtl_arg u o rtyp
+  end.
+
+Definition mk_env (u : Uf.T) (r : reg) :=
+  if myreg.eq (Uf.repr u (tReg r)) (Uf.repr u (tTy Tfloat))
+  then Tfloat
+  else Tint.
+
+Fixpoint member (x : reg) (l : list reg) {struct l} : bool :=
+  match l with
+  | nil => false
+  | y :: rest => if peq x y then true else member x rest
+  end.
+
+Fixpoint repet (l : list reg) : bool :=
+  match l with
+  | nil => false
+  | x :: rest => member x rest || repet rest
+  end.
+
+Definition type_rtl_function (f : function) :=
+  let u1 := PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
+                       f.(fn_code) Uf.empty in
+  let u2 := fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args) in
+  if repet f.(fn_params) then
+    None
+  else
+    if myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat))
+    then None
+    else Some (mk_env u2).
+
+Unset Implicit Arguments.
+
+(** ** Correctness proof for type inference *)
+
+(** General properties of the type equivalence relation. *)
+
+Definition consistent (u : Uf.T) :=
+  Uf.repr u (tTy Tint) <> Uf.repr u (tTy Tfloat).
+
+Lemma consistent_not_eq : forall (u : Uf.T) (A : Type) (x y : A),
+  consistent u ->
+  (if myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat)) then x else y)
+  = y.
+  Proof.
+    intros.
+    unfold consistent in H.
+    destruct (myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat)));
+    congruence.
+  Qed.
+
+Lemma equal_eq : forall (t : myT) (A : Type) (x y : A),
+  (if myreg.eq t t then x else y) = x.
+  Proof.
+    intros.
+    destruct (myreg.eq t t); congruence.
+  Qed.
+
+Lemma error_inconsistent : forall (A : Prop), consistent error -> A.
+  Proof.
+    intros.
+    absurd (consistent error); auto.
+    intro.
+    unfold error in H.  unfold consistent in H.
+    rewrite Uf.sameclass_identify_1 in H.
+    congruence.
+  Qed.
+
+Lemma teq_correct : forall (t1 t2 : typ), teq t1 t2 = true -> t1 = t2.
+  Proof.
+    intros; destruct t1; destruct t2; try simpl in H; congruence.
+  Qed.
+
+Definition included (u1 u2 : Uf.T) : Prop :=
+  forall (e1 e2: myT),
+    Uf.repr u1 e1 = Uf.repr u1 e2 -> Uf.repr u2 e1 = Uf.repr u2 e2.
+
+Lemma included_refl :
+  forall (e : Uf.T), included e e.
+  Proof.
+    unfold included. auto.
+  Qed.
+
+Lemma included_trans :
+  forall (e1 e2 e3 : Uf.T),
+  included e3 e2 -> included e2 e1 -> included e3 e1.
+  Proof.
+    unfold included. auto.
+  Qed.
+
+Lemma included_consistent :
+  forall (u1 u2 : Uf.T),
+  included u1 u2 -> consistent u2 -> consistent u1.
+  Proof.
+    unfold consistent. unfold included.
+    intros.
+    intro. apply H0. apply H.
+    auto.
+  Qed.
+
+Lemma included_identify :
+  forall (u : Uf.T) (t1 t2 : myT), included u (Uf.identify u t1 t2).
+  Proof.
+  unfold included.
+  intros.
+  apply Uf.sameclass_identify_2; auto.
+  Qed.
+
+Lemma type_arg_correct_1 :
+  forall (u : Uf.T) (r : reg) (t : typ),
+  consistent (type_rtl_arg u r t)
+  -> Uf.repr (type_rtl_arg u r t) (tReg r)
+     = Uf.repr (type_rtl_arg u r t) (tTy t).
+  Proof.
+    intros.
+    unfold type_rtl_arg.
+    rewrite Uf.sameclass_identify_1.
+    auto.
+  Qed.
+
+Lemma type_arg_correct :
+  forall (u : Uf.T) (r : reg) (t : typ),
+  consistent (type_rtl_arg u r t) -> mk_env (type_rtl_arg u r t) r = t.
+  Proof.
+    intros.
+    unfold mk_env. 
+    rewrite type_arg_correct_1.
+    destruct t.
+    apply consistent_not_eq; auto.
+    destruct (myreg.eq (Uf.repr (type_rtl_arg u r Tfloat) (tTy Tfloat)));
+    congruence.
+    auto.
+  Qed.
+
+Lemma type_arg_included :
+  forall (u : Uf.T) (r : reg) (t : typ), included u (type_rtl_arg u r t).
+  Proof.
+    intros.
+    unfold type_rtl_arg.
+    apply included_identify.
+  Qed.
+
+Lemma type_arg_extends :
+  forall (u : Uf.T) (r : reg) (t : typ),
+  consistent (type_rtl_arg u r t) -> consistent u.
+  Proof.
+    intros.
+    apply included_consistent with (u2 := type_rtl_arg u r t).
+    apply type_arg_included.
+    auto.
+  Qed.
+
+Lemma type_args_included :
+  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
+  consistent (fold2 type_rtl_arg u l1 l2)
+  -> included u (fold2 type_rtl_arg u l1 l2).
+  Proof.
+    induction l1; intros; destruct l2.
+    simpl in H; simpl; apply included_refl.
+    simpl in H. apply error_inconsistent. auto.
+    simpl in H. apply error_inconsistent. auto.
+    simpl.
+    simpl in H.
+    apply included_trans with (e2 := type_rtl_arg u a t).
+    apply type_arg_included.
+    apply IHl1.
+    auto.
+  Qed.
+
+Lemma type_args_extends :
+  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
+  consistent (fold2 type_rtl_arg u l1 l2) -> consistent u.
+  Proof.
+    intros.
+    apply (included_consistent _ _ (type_args_included l1 l2 u H)).
+    auto.
+  Qed.
+
+Lemma type_args_correct :
+  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
+  consistent (fold2 type_rtl_arg u l1 l2)
+  -> map (mk_env (fold2 type_rtl_arg u l1 l2)) l1 = l2.
+  Proof.
+    induction l1.
+    intros.
+    destruct l2.
+    unfold map; simpl; auto.
+    simpl in H; apply error_inconsistent; auto.
+    intros.
+    destruct l2.
+    simpl in H; apply error_inconsistent; auto.
+    simpl.
+    simpl in H.
+    rewrite (IHl1 l2 (type_rtl_arg u a t) H).
+    unfold mk_env.
+    destruct t.
+    rewrite (type_args_included _ _ _ H (tReg a) (tTy Tint)).
+    rewrite consistent_not_eq; auto.
+    apply type_arg_correct_1.
+    apply type_args_extends with (l1 := l1) (l2 := l2); auto.
+    rewrite (type_args_included _ _ _ H (tReg a) (tTy Tfloat)).
+    rewrite equal_eq; auto.
+    apply type_arg_correct_1.
+    apply type_args_extends with (l1 := l1) (l2 := l2); auto.
+  Qed.
+
+(** Correctness of [wt_params]. *)
+
+Lemma type_rtl_function_params :
+  forall (f: function) (env: regenv),
+  type_rtl_function f = Some env
+  -> List.map env f.(fn_params) = f.(fn_sig).(sig_args).
+  Proof.
+    destruct f; unfold type_rtl_function; simpl.
+    destruct (repet fn_params); simpl; intros; try congruence.
+    pose (u := PTree.fold (type_rtl_instr (sig_res fn_sig)) fn_code Uf.empty).
+    fold u in H.
+    cut (consistent (fold2 type_rtl_arg u fn_params (sig_args fn_sig))).
+    intro.
+    pose (R := Uf.repr (fold2 type_rtl_arg u fn_params (sig_args fn_sig))).
+    fold R in H.
+    destruct (myreg.eq (R (tTy Tint)) (R (tTy Tfloat))).
+    congruence.
+    injection H.
+    intro.
+    rewrite <- H1.
+    apply type_args_correct.
+    auto.
+    intro.
+    rewrite H0 in H.
+    rewrite equal_eq in H.
+    congruence.
+  Qed.
+
+(** Correctness of [wt_norepet]. *)
+
+Lemma member_correct :
+  forall (l : list reg) (a : reg), member a l = false -> ~In a l.
+  Proof.
+    induction l; simpl; intros; try tauto.
+    destruct (peq a0 a); simpl; try congruence.
+    intro. destruct H0; try congruence.
+    generalize H0; apply IHl; auto.
+  Qed.
+
+Lemma repet_correct :
+  forall (l : list reg), repet l = false -> list_norepet l.
+  Proof.
+    induction l; simpl; intros.
+     exact (list_norepet_nil reg).
+     elim (orb_false_elim (member a l) (repet l) H); intros.
+     apply list_norepet_cons.
+      apply member_correct; auto.
+      apply IHl; auto.
+  Qed.
+
+Lemma type_rtl_function_norepet :
+  forall (f: function) (env: regenv),
+  type_rtl_function f = Some env
+  -> list_norepet f.(fn_params).
+  Proof.
+    destruct f; unfold type_rtl_function; simpl.
+    intros. cut (repet fn_params = false).
+     intro. apply repet_correct. auto.
+     destruct (repet fn_params); congruence.
+  Qed.
+
+(** Correctness of [wt_instrs]. *)
+
+Lemma step1 :
+  forall (f : function) (env : regenv),
+  type_rtl_function f = Some env
+  -> exists u2 : Uf.T,
+       included (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
+                            f.(fn_code) Uf.empty)
+                u2
+       /\ env = mk_env u2
+       /\ consistent u2.
+  Proof.
+    intros f env.
+    pose (u1 := (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
+                            f.(fn_code) Uf.empty)).
+    fold u1.
+    unfold type_rtl_function.
+    intros.
+    destruct (repet f.(fn_params)).
+    congruence.
+    fold u1 in H.
+    pose (u2 := (fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args))).
+    fold u2 in H.
+    exists u2.
+    caseEq (myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat))).
+    intros.
+    rewrite e in H.
+    rewrite equal_eq in H.
+    congruence.
+    intros.
+    rewrite consistent_not_eq in H.
+    apply conj.
+    unfold u2.
+    apply type_args_included.
+    auto.
+    apply conj; auto.
+    congruence.
+    auto.
+  Qed.
+
+Lemma let_fold_args_res :
+  forall (u : Uf.T) (l : list reg) (r : reg) (e : list typ * typ),
+  (let (argtyp, restyp) := e in
+   fold2 type_rtl_arg (type_rtl_arg u r restyp) l argtyp)
+  = fold2 type_rtl_arg (type_rtl_arg u r (snd e)) l (fst e).
+  Proof.
+    intros. rewrite (surjective_pairing e). simpl. auto.
+  Qed.
+
+Lemma type_args_res_included :
+  forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2)
+  -> included u (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2).
+  Proof.
+  intros.
+  apply included_trans with (e2 := type_rtl_arg u r t).
+  apply type_arg_included.
+  apply type_args_included; auto.
+  Qed.
+
+Lemma type_args_res_ros_included :
+  forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ)
+         (ros : reg+ident),
+  consistent (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2)
+  -> included u (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2).
+Proof.
+  intros.
+  apply included_trans with (e2 := type_rtl_ros u ros).
+  unfold type_rtl_ros; destruct ros.
+  apply included_identify.
+  apply included_refl.
+  apply type_args_res_included; auto.
+Qed.
+
+Lemma type_instr_included :
+  forall (p : positive) (i : instruction) (u : Uf.T) (res_ty : option typ),
+  consistent (type_rtl_instr res_ty u p i)
+  -> included u (type_rtl_instr res_ty u p i).
+  Proof.
+    intros.
+    destruct i; simpl; simpl in H; try apply type_args_res_included; auto.
+    apply included_refl; auto.
+    destruct o; simpl; simpl in H; try apply type_args_res_included; auto.
+    destruct l; simpl; simpl in H; auto.
+    apply error_inconsistent; auto.
+    destruct l; simpl; simpl in H; auto.
+    apply included_identify.
+    apply error_inconsistent; auto.
+    destruct l; simpl; simpl in H; auto.
+    apply included_refl.
+    apply error_inconsistent; auto.
+    apply type_args_res_ros_included; auto.
+    apply type_args_included; auto.
+    destruct res_ty; destruct o; simpl; simpl in H;
+      try (apply error_inconsistent; auto; fail).
+    apply type_arg_included.
+    apply included_refl.
+   Qed.
+
+Lemma type_instrs_extends :
+  forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ),
+  consistent
+      (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u)
+  -> consistent u.
+Proof.
+  induction l; simpl; intros.
+  auto.
+  apply included_consistent
+     with (u2 := (type_rtl_instr res_ty u (fst a) (snd a))).
+  apply type_instr_included.
+  apply IHl with (res_ty := res_ty); auto.
+  apply IHl with (res_ty := res_ty); auto.
+Qed.
+
+Lemma type_instrs_included :
+  forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ),
+  consistent
+      (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u)
+  -> included u
+         (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u).
+  Proof.
+    induction l; simpl; intros.
+    apply included_refl; auto.
+    apply included_trans with (e2 := (type_rtl_instr res_ty u (fst a) (snd a))).
+    apply type_instr_included.
+    apply type_instrs_extends with (res_ty := res_ty) (l := l); auto.
+    apply IHl; auto.
+  Qed.
+
+Lemma step2 :
+  forall (res_ty : option typ) (c : code) (u0 : Uf.T),
+  consistent (PTree.fold (type_rtl_instr res_ty) c u0) ->
+  forall (pc : positive) (i : instruction),
+  c!pc = Some i
+  -> exists u : Uf.T,
+        consistent (type_rtl_instr res_ty u pc i)
+     /\ included (type_rtl_instr res_ty u pc i)
+                    (PTree.fold (type_rtl_instr res_ty) c u0).
+  Proof.
+    intros.
+    rewrite PTree.fold_spec.
+    rewrite PTree.fold_spec in H.
+    pose (H1 := PTree.elements_correct _ _ H0).
+    generalize H. clear H.
+    generalize u0. clear u0.
+    generalize H1. clear H1.
+    induction (PTree.elements c).
+    intros.
+    absurd (In (pc, i) nil).
+    apply in_nil.
+    auto.
+    intros.
+    simpl in H.
+    elim H1.
+    intro.
+    rewrite H2 in H.
+    simpl in H.
+    rewrite H2. simpl.
+    exists u0.
+    apply conj.
+    apply type_instrs_extends with (res_ty := res_ty) (l := l).
+    auto.
+    apply type_instrs_included.
+    auto.
+    intro.
+    simpl.
+    apply IHl.
+    auto.
+    auto.
+  Qed.
+
+Definition mapped (u : Uf.T) (r : reg) :=
+  Uf.repr u (tReg r) = Uf.repr u (tTy Tfloat)
+  \/ Uf.repr u (tReg r) = Uf.repr u (tTy Tint).
+
+Definition definite (u : Uf.T) (i : instruction) :=
+  match i with
+  | Inop _ => True
+  | Iop Omove (r1 :: nil) r0 _ => Uf.repr u (tReg r1) = Uf.repr u (tReg r0)
+  | Iop Oundef _ _ _ => True
+  | Iop _ args r0 _ =>
+         mapped u r0 /\ forall r : reg, In r args -> mapped u r
+  | Iload _ _ args r0 _ =>
+         mapped u r0 /\ forall r : reg, In r args -> mapped u r
+  | Istore _ _ args r0 _ =>
+         mapped u r0 /\ forall r : reg, In r args -> mapped u r
+  | Icall _ ros args r0 _ =>
+      match ros with inl r => mapped u r | _ => True end
+      /\ mapped u r0 /\ forall r : reg, In r args -> mapped u r
+  | Icond _ args _ _ =>
+      forall r : reg, In r args -> mapped u r
+  | Ireturn None => True
+  | Ireturn (Some r) => mapped u r
+  end.
+
+Lemma type_arg_complete :
+  forall (u : Uf.T) (r : reg) (t : typ),
+  mapped (type_rtl_arg u r t) r.
+Proof.
+  intros.
+  unfold type_rtl_arg.
+  unfold mapped.
+  destruct t.
+  right; apply Uf.sameclass_identify_1.
+  left; apply Uf.sameclass_identify_1.
+Qed.
+
+Lemma type_arg_mapped :
+  forall (u : Uf.T) (r r0 : reg) (t : typ),
+  mapped u r0 -> mapped (type_rtl_arg u r t) r0.
+Proof.
+  unfold mapped.
+  unfold type_rtl_arg.
+  intros.
+  elim H; intros.
+  left; apply Uf.sameclass_identify_2; auto.
+  right; apply Uf.sameclass_identify_2; auto.
+Qed.
+
+Lemma type_args_mapped :
+  forall (lr : list reg) (lt : list typ) (u : Uf.T) (r : reg),
+  consistent (fold2 type_rtl_arg u lr lt) ->
+  mapped u r ->
+    mapped (fold2 type_rtl_arg u lr lt) r.
+Proof.
+  induction lr; simpl; intros.
+  destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail).
+  destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail).
+  apply IHlr.
+  auto.
+  apply type_arg_mapped; auto.
+Qed.
+
+Lemma type_args_complete :
+  forall (lr : list reg) (lt : list typ) (u : Uf.T),
+  consistent (fold2 type_rtl_arg u lr lt)
+  -> forall r, (In r lr -> mapped (fold2 type_rtl_arg u lr lt) r).
+Proof.
+  induction lr; simpl; intros.
+  destruct lt; simpl; try tauto.
+  destruct lt; simpl.
+  apply error_inconsistent; auto.
+  elim H0; intros.
+  rewrite H1.
+  rewrite H1 in H.
+  apply type_args_mapped; auto.
+  apply type_arg_complete.
+  apply IHlr; auto.
+Qed.
+
+Lemma type_res_complete :
+  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
+  -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r.
+Proof.
+  intros.
+  apply type_args_mapped; auto.
+  apply type_arg_complete.
+Qed.
+
+Lemma type_args_res_complete :
+  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
+  -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r
+      /\ forall rr, (In rr lr -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t)
+                                                            lr lt)
+                                        rr).
+Proof.
+  intros.
+  apply conj.
+  apply type_res_complete; auto.
+  apply type_args_complete; auto.
+Qed.
+
+Lemma type_ros_complete :
+  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg
+                                    (type_rtl_ros u (inl ident r1)) r t) lr lt)
+  ->
+  mapped (fold2 type_rtl_arg (type_rtl_arg
+                                (type_rtl_ros u (inl ident r1)) r t) lr lt) r1.
+Proof.
+  intros.
+  apply type_args_mapped; auto.
+  apply type_arg_mapped.
+  unfold type_rtl_ros.
+  unfold mapped.
+  right.
+  apply Uf.sameclass_identify_1; auto.
+Qed.
+
+Lemma type_res_correct :
+  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
+  -> mk_env (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r = t.
+Proof.
+  intros.
+  unfold mk_env.
+  rewrite (type_args_included _ _ _ H (tReg r) (tTy t)).
+  destruct t.
+  apply consistent_not_eq; auto.
+  apply equal_eq; auto.
+  unfold type_rtl_arg; apply Uf.sameclass_identify_1; auto.
+Qed.
+
+Lemma type_ros_correct :
+  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ),
+  consistent (fold2 type_rtl_arg (type_rtl_arg
+                                    (type_rtl_ros u (inl ident r1)) r t) lr lt)
+  ->
+  mk_env (fold2 type_rtl_arg (type_rtl_arg
+                                (type_rtl_ros u (inl ident r1)) r t) lr lt) r1
+  = Tint.
+Proof.
+  intros.
+  unfold mk_env.
+  rewrite (type_args_included _ _ _ H (tReg r1) (tTy Tint)).
+  apply consistent_not_eq; auto.
+  rewrite (type_arg_included (type_rtl_ros u (inl ident r1)) r t (tReg r1) (tTy Tint)).
+  auto.
+  simpl.
+  apply Uf.sameclass_identify_1; auto.
+Qed.
+
+Lemma step3 :
+  forall (u : Uf.T) (f : function) (c : code) (i : instruction) (pc : positive),
+  c!pc = Some i ->
+  consistent (type_rtl_instr f.(fn_sig).(sig_res) u pc i)
+  ->    wt_instr (mk_env (type_rtl_instr f.(fn_sig).(sig_res) u pc i)) f i
+     /\ definite (type_rtl_instr f.(fn_sig).(sig_res) u pc i) i.
+  Proof.
+    Opaque type_rtl_arg.
+    intros.
+    destruct i; simpl in H0; simpl.
+     (* Inop *)
+     apply conj; auto. apply wt_Inop.
+     (* Iop *)
+     destruct o;
+       try (apply conj; [
+             apply wt_Iop; try congruence; simpl;
+               rewrite (type_args_correct _ _ _ H0);
+               rewrite (type_res_correct _ _ _ _ _ H0);
+               auto
+            |apply (type_args_res_complete _ _ _ _ _ H0)]).
+      (* Omove *)
+      destruct l; [apply error_inconsistent; auto | idtac].
+      destruct l; [idtac | apply error_inconsistent; auto].
+      apply conj.
+      apply wt_Iopmove.
+      simpl.
+      unfold mk_env.
+      rewrite Uf.sameclass_identify_1.
+      congruence.
+      simpl.
+      rewrite Uf.sameclass_identify_1; congruence.
+      (* Oundef *)
+      destruct l; [idtac | apply error_inconsistent; auto].
+      apply conj. apply wt_Iopundef.
+      unfold definite. auto.
+     (* Iload *)
+     apply conj.
+      apply wt_Iload.
+       rewrite (type_args_correct _ _ _ H0); auto.
+       rewrite (type_res_correct _ _ _ _ _ H0); auto.
+      simpl; apply (type_args_res_complete _ _ _ _ _ H0).
+     (* IStore *)
+     apply conj.
+      apply wt_Istore.
+       rewrite (type_args_correct _ _ _ H0); auto.
+       rewrite (type_res_correct _ _ _ _ _ H0); auto.
+      simpl; apply (type_args_res_complete _ _ _ _ _ H0).
+     (* Icall *)
+     apply conj.
+      apply wt_Icall.
+       destruct s0; auto. apply type_ros_correct. auto.
+       apply type_args_correct. auto.
+       fold (type_of_sig_res s). apply type_res_correct. auto.
+      destruct s0.
+       apply conj.
+        apply type_ros_complete. auto.
+        apply type_args_res_complete. auto.
+       apply conj; auto.
+         apply type_args_res_complete. auto.
+     (* Icond *) 
+     apply conj.
+      apply wt_Icond.
+       apply (type_args_correct _ _ _ H0).
+       simpl; apply (type_args_complete _ _ _ H0).
+     (* Ireturn *)
+     destruct o; simpl.
+      apply conj.
+       apply wt_Ireturn.
+         destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
+          rewrite type_arg_correct; auto.
+          apply error_inconsistent; auto.
+       destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
+          apply type_arg_complete.
+          apply error_inconsistent; auto.
+      apply conj; auto. apply wt_Ireturn.
+        destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
+         apply error_inconsistent; auto.
+         congruence.
+    Transparent type_rtl_arg.
+  Qed.
+
+Lemma mapped_included_consistent :
+  forall (u1 u2 : Uf.T) (r : reg),
+  mapped u1 r ->
+  included u1 u2 ->
+  consistent u2 ->
+  mk_env u2 r = mk_env u1 r.
+Proof.
+  intros.
+  unfold mk_env.
+  unfold mapped in H.
+  elim H; intros; rewrite H2; rewrite (H0 _ _ H2).
+  rewrite equal_eq; rewrite equal_eq; auto.
+  rewrite (consistent_not_eq u2).
+  rewrite (consistent_not_eq u1).
+  auto.
+  apply included_consistent with (u2 := u2).
+  auto.
+  auto.
+  auto.
+Qed.
+
+Lemma mapped_list_included :
+  forall (u1 u2 : Uf.T) (lr : list reg),
+  (forall r, In r lr -> mapped u1 r) ->
+  included u1 u2 ->
+  consistent u2 ->
+    map (mk_env u2) lr = map (mk_env u1) lr.
+Proof.
+  induction lr; simpl; intros.
+  auto.
+  rewrite (mapped_included_consistent u1 u2 a).
+  rewrite IHlr; auto.
+  apply (H a); intros.
+  left; auto.
+  auto.
+  auto.
+Qed.
+
+Lemma included_mapped :
+  forall (u1 u2 : Uf.T) (r : reg),
+  included u1 u2 ->
+  mapped u1 r ->
+    mapped u2 r.
+Proof.
+  unfold mapped.
+  intros.
+  elim H0; intros.
+  left; rewrite (H _ _ H1); auto.
+  right; rewrite (H _ _ H1); auto.
+Qed.
+
+Lemma included_mapped_forall :
+  forall (u1 u2 : Uf.T) (r : reg) (l : list reg),
+  included u1 u2 ->
+  mapped u1 r /\ (forall r, In r l -> mapped u1 r) ->
+    mapped u2 r /\ (forall r, In r l -> mapped u2 r).
+Proof.
+  intros.
+  elim H0; intros.
+  apply conj.
+  apply (included_mapped _ _ r H); auto.
+  intros.
+  apply (included_mapped _ _ r0 H).
+  apply H2; auto.
+Qed.
+
+Lemma definite_included :
+  forall (u1 u2 : Uf.T) (i : instruction),
+  included u1 u2 -> definite u1 i -> definite u2 i.
+Proof.
+  unfold definite.
+  intros.
+  destruct i; try apply (included_mapped_forall _ _ _ _ H H0); auto.
+  destruct o; try apply (included_mapped_forall _ _ _ _ H H0); auto.
+  destruct l; auto.
+  apply (included_mapped_forall _ _ _ _ H H0).
+  destruct l; auto.
+  apply (included_mapped_forall _ _ _ _ H H0).
+  destruct s0; auto.
+  elim H0; intros.
+  apply conj.
+  apply (included_mapped _ _ _ H H1).
+  apply (included_mapped_forall _ _ _ _ H H2).
+  elim H0; intros.
+  apply conj; auto.
+  apply (included_mapped_forall _ _ _ _ H H2).
+  intros.
+  apply (included_mapped _ _ _ H (H0 r H1)).
+  destruct o; auto.
+  apply (included_mapped _ _ _ H H0).
+Qed.
+
+Lemma step4 :
+  forall (f : function) (u1 u3 : Uf.T) (i : instruction),
+  included u3 u1 ->
+  wt_instr (mk_env u3) f i ->
+  definite u3 i ->
+  consistent u1 ->
+    wt_instr (mk_env u1) f i.
+  Proof.
+    intros f u1 u3 i H1 H H0 X.
+    destruct H; try simpl in H0; try (elim H0; intros).
+     apply wt_Inop.
+     apply wt_Iopmove. unfold mk_env. rewrite (H1 _ _ H0). auto.
+     apply wt_Iopundef.
+     apply wt_Iop; auto.
+       destruct op; try congruence; simpl; simpl in H3;
+       simpl in H0; elim H0; intros; rewrite (mapped_included_consistent _ _ _ H4 H1 X);
+       rewrite (mapped_list_included _ _ _ H5 H1); auto.
+     apply wt_Iload.
+      rewrite (mapped_list_included _ _ _ H4 H1); auto.
+      rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto.
+     apply wt_Istore.
+      rewrite (mapped_list_included _ _ _ H4 H1); auto.
+      rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto.
+     elim H5; intros; destruct ros; apply wt_Icall.
+      rewrite (mapped_included_consistent _ _ _ H4 H1 X); auto.
+      rewrite (mapped_list_included _ _ _ H7 H1); auto.
+      rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto.
+      auto.
+      rewrite (mapped_list_included _ _ _ H7 H1); auto.
+      rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto.
+     apply wt_Icond. rewrite (mapped_list_included _ _ _ H0 H1); auto.
+     apply wt_Ireturn.
+      destruct optres; destruct f.(fn_sig).(sig_res);
+        simpl in H; simpl; try congruence.
+        rewrite (mapped_included_consistent _ _ _ H0 H1 X); auto.
+  Qed.
+
+Lemma type_rtl_function_instrs :
+  forall (f: function) (env: regenv),
+  type_rtl_function f = Some env
+  -> forall pc i, f.(fn_code)!pc = Some i -> wt_instr env f i.
+  Proof.
+    intros.
+    elim (step1 _ _ H).
+    intros.
+    elim H1.
+    intros.
+    elim H3.
+    intros.
+    rewrite H4.
+    elim (step2 _ _ _ (included_consistent _ _ H2 H5) _ _ H0).
+    intros.
+    elim H6. intros.
+    elim (step3 x0 f _ _ _ H0); auto. intros.
+    apply (step4 f _ _ i H2); auto.
+    apply (step4 _ _ _ _ H8 H9 H10).
+    apply (included_consistent _ _ H2); auto.
+    apply (definite_included _ _ _ H8 H10); auto.
+  Qed.
+
+(** Combining the sub-proofs. *)
+
+Theorem type_rtl_function_correct:
+  forall (f: function) (env: regenv),
+  type_rtl_function f = Some env -> wt_function env f.
+  Proof.
+    intros.
+    exact (mk_wt_function env f (type_rtl_function_params f _ H)
+                                (type_rtl_function_norepet f _ H)
+                                (type_rtl_function_instrs f _ H)).
+  Qed.
+
+Definition wt_program (p: program) : Prop :=
+  forall i f, In (i, f) (prog_funct p) -> type_rtl_function f <> None.
+
+(** * Type preservation during evaluation *)
+
+(** The type system for RTL is not sound in that it does not guarantee
+  progress: well-typed instructions such as [Icall] can fail because
+  of run-time type tests (such as the equality between calle and caller's
+  signatures).  However, the type system guarantees a type preservation
+  property: if the execution does not fail because of a failed run-time
+  test, the result values and register states match the static
+  typing assumptions.  This preservation property will be useful
+  later for the proof of semantic equivalence between [Machabstr] and [Mach].
+  Even though we do not need it for [RTL], we show preservation for [RTL]
+  here, as a warm-up exercise and because some of the lemmas will be
+  useful later. *)
+
+Require Import Globalenvs.
+Require Import Values.
+Require Import Mem.
+Require Import Integers.
+
+Definition wt_regset (env: regenv) (rs: regset) : Prop :=
+  forall r, Val.has_type (rs#r) (env r).
+
+Lemma wt_regset_assign:
+  forall env rs v r,
+  wt_regset env rs ->
+  Val.has_type v (env r) ->
+  wt_regset env (rs#r <- v).
+Proof.
+  intros; red; intros. 
+  rewrite Regmap.gsspec.
+  case (peq r0 r); intro.
+  subst r0. assumption.
+  apply H.
+Qed.
+
+Lemma wt_regset_list:
+  forall env rs,
+  wt_regset env rs ->
+  forall rl, Val.has_type_list (rs##rl) (List.map env rl).
+Proof.
+  induction rl; simpl.
+  auto.
+  split. apply H. apply IHrl.
+Qed.  
+
+Lemma wt_init_regs:
+  forall env rl args,
+  Val.has_type_list args (List.map env rl) ->
+  wt_regset env (init_regs args rl).
+Proof.
+  induction rl; destruct args; simpl; intuition.
+  red; intros. rewrite Regmap.gi. simpl; auto. 
+  apply wt_regset_assign; auto.
+Qed.
+
+Section SUBJECT_REDUCTION.
+
+Variable p: program.
+
+Hypothesis wt_p: wt_program p.
+
+Let ge := Genv.globalenv p.
+
+Definition exec_instr_subject_reduction
+    (c: code) (sp: val)
+    (pc: node) (rs: regset) (m: mem)
+    (pc': node) (rs': regset) (m': mem) : Prop :=
+  forall env f
+         (CODE: c = fn_code f)
+         (WT_FN: wt_function env f)
+         (WT_RS: wt_regset env rs),
+  wt_regset env rs'.
+
+Definition exec_function_subject_reduction
+    (f: function) (args: list val) (m: mem) (res: val) (m': mem) : Prop :=
+  forall env,
+  wt_function env f ->  
+  Val.has_type_list args f.(fn_sig).(sig_args) ->
+  Val.has_type res
+    (match f.(fn_sig).(sig_res) with None => Tint | Some ty => ty end).
+
+Lemma subject_reduction:
+  forall f args m res m',
+  exec_function ge f args m res m' ->
+  exec_function_subject_reduction f args m res m'.
+Proof.
+  apply (exec_function_ind_3 ge
+           exec_instr_subject_reduction
+           exec_instr_subject_reduction
+           exec_function_subject_reduction);
+  intros; red; intros;
+  try (rewrite CODE in H;
+       generalize (wt_instrs env _ WT_FN pc _ H);
+       intro WT_INSTR;
+       inversion WT_INSTR).
+ 
+  assumption.
+
+  apply wt_regset_assign. auto. 
+  subst op. subst args. simpl in H0. injection H0; intro. 
+  subst v. rewrite <- H2. apply WT_RS.
+
+  apply wt_regset_assign. auto.
+  subst op; subst args; simpl in H0. injection H0; intro; subst v.
+  simpl; auto.
+
+  apply wt_regset_assign. auto.
+  replace (env res) with (snd (type_of_operation op)).
+  apply type_of_operation_sound with function ge rs##args sp; auto.
+  rewrite <- H7. reflexivity.
+
+  apply wt_regset_assign. auto. rewrite H8. 
+  eapply type_of_chunk_correct; eauto.
+
+  assumption.
+
+  apply wt_regset_assign. auto. rewrite H11. rewrite H1.
+  assert (type_rtl_function f <> None).
+    destruct ros; simpl in H0.
+    pattern f. apply Genv.find_funct_prop with function p (rs#r).
+    exact wt_p. exact H0. 
+    caseEq (Genv.find_symbol ge i); intros; rewrite H12 in H0.
+    pattern f. apply Genv.find_funct_ptr_prop with function p b.
+    exact wt_p. exact H0.
+    discriminate.
+  assert (exists env1, wt_function env1 f).
+    caseEq (type_rtl_function f); intros; try congruence.
+    exists t. apply type_rtl_function_correct; auto.
+  elim H13; intros env1 WT_FN1. 
+  eapply H3. eexact WT_FN1. rewrite <- H1. rewrite <- H10.
+  apply wt_regset_list; auto. 
+
+  assumption.
+  assumption.
+  assumption.
+  eauto.
+  eauto.
+
+  assert (WT_INIT: wt_regset env (init_regs args (fn_params f))).
+    apply wt_init_regs. rewrite (wt_params env f H4). assumption.
+  generalize (H1 env f (refl_equal (fn_code f)) H4 WT_INIT). 
+  intro WT_RS.
+  generalize (wt_instrs env _ H4 pc _ H2).
+  intro WT_INSTR; inversion WT_INSTR.
+  destruct or; simpl in H3; simpl in H7; rewrite <- H7.
+  rewrite H3. apply WT_RS. 
+  rewrite H3. simpl; auto.
+Qed. 
+
+End SUBJECT_REDUCTION.