Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Natmap.
Require Import FMaps.
Require Import EqNat.
Require Import lj_definitions.
Require Import lj_infrastructure.
Require Import lj_soundness.
Require Import lj_constraint_definitions.
Require Import lj_constraint_infrastructure.
Require Import lj_constraint_soundness.
Require Import LFJ_definitions.
Require Import LFJ_infrastructure.
Require Import base2.

Lemma sat_comp_ps_sat_psel : forall (c_list : list comp_constraint) (ps : PSel) (p : P),
  sat_comp_constr_psel c_list ps = true -> compose ps = Some p -> 
  sat_comp_constr_p c_list p = true.
  induction c_list.
  simpl; intros; reflexivity.
  destruct a; simpl; intros; destruct (andb_prop _ _ H);
    rewrite (IHc_list ps p); auto; apply andb_true_intro; pa;
      generalize p H1 H0; clear; induction ps; intros.
  simpl in H1; discriminate.
  destruct a.
  simpl in H1.
  caseEq (in_path l0 d); intros H; rewrite H in H1.
  simpl in H0.
  destruct (compose ps);
    try destruct (fold_right
      (fun (rcld' : rcld) (op : option P) =>
        match op with
          | Some p' => compose_refines_class p' rcld'
          | None => None (A:=P)
        end) (Some p0)); inversion H0.
  generalize p1 H1; clear; induction l0.
  unfold sat_meth_constr_clds; simpl; intros; discriminate.
  destruct a; unfold sat_meth_constr_clds; unfold sat_meth_constr_p; 
    simpl; case (eq_nat_dec d d0); simpl.
  auto.
  fold (sat_meth_constr_clds l0 d m).
  intros; fold (sat_meth_constr_p d m (rm_dcl (introduce_classes p1 l0) (cld_def d0 c l l1))).
  generalize (IHl0 p1 H1) n; clear; induction (introduce_classes p1 l0).
  simpl; auto.
  destruct a; simpl; case (eq_nat_dec d0 d1); simpl.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); simpl.
  congruence.
  intros; apply IHl2; auto.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); simpl; auto.
  caseEq (sat_meth_constr_rclds l d m); intros; rewrite H2 in H1.
  generalize p H0 H H2; clear; induction l; intros.
  simpl in H; discriminate.
  destruct a; simpl in H2; generalize H2; clear H2; case (eq_nat_dec d d0); intros; subst.
  simpl in H0.
  caseEq (compose ps); intros; rewrite H1 in H0.
  caseEq (fold_right (fun (rcld' : rcld) (op : option P) =>
              match op with
              | Some p' => compose_refines_class p' rcld'
              | None => None (A:=P)
              end) (Some p0) l); intros; rewrite H3 in H0.
  caseEq (compose_refines_class p1 (refines_cld_def d0 c l1 l2 l3)); intros; rewrite H4 in H0.
  inversion H0; clear H0.
  caseEq (meth_in_mds l2 m); intros G1; rewrite G1 in H2.
  simpl in G1.
  destruct (in_mds_In_mds _ _ G1).
  import (in_rclds_mds_in_p _ _ _ _ _ _ _ _ _ H4 H0).
  bd H5.
  import (distinct_compose_names _ _ H1).
  assert (distinct _ (names p1)).
  generalize p1 H3 H7; clear; induction l; simpl; intros.
  congruence.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H in H3.
  apply (distinct_refines_class _ _ _  (IHl _ H H7) H3).
  discriminate.
  simpl in H3.
  generalize H H5 H9 (distinct_refines_class _ _ _ H8 H4); clear; induction l0.
  simpl; intros _ H H0 H1.
  induction p2; simpl in H0.
  contradiction.
  bd H0; subst.
  unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d0); simpl.
  intros; apply (In_mds_in_mds _ _ _ H).
  congruence.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); simpl.
  simpl in H1; bd H1; intros; subst.
  import (In_names _ _ _ _ _ H0); tauto.
  intros; fold (sat_meth_constr_p d0 m p2).
  simpl in H1; bd H1; auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); intros.
  congruence.
  fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p2 l0) (cld_def d c0 l l1))); bd H1.
  generalize (IHl0 H H5 H9 H0) n; clear; induction (introduce_classes p2 l0); simpl.
  auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d d1); 
    case (eq_nat_dec d0 d1); simpl; intros.
  congruence.
  fold (sat_meth_constr_p d0 m l2) in H; fold (sat_meth_constr_p d0 m  (rm_dcl l2 (cld_def d c0 l l1))); auto.
  case (eq_nat_dec d0 d1); simpl; intros; auto.
  case (eq_nat_dec d0 d1); simpl; intros; auto.
  unfold compose in IHl; fold (compose ps) in IHl; rewrite H1 in IHl; 
    unfold compose_fd in IHl; rewrite H3 in IHl; import (IHl _ (refl_equal _) H H2).
  generalize p2 H H4 G1 H0; clear; induction l0.
  simpl; induction p1.
  simpl; intros; discriminate.
  destruct a; simpl; case (eq_nat_dec d d0).
  caseEq (compose_refined_mds l0 l3); intros.
  inversion H4; subst; clear H4; generalize H1; unfold sat_meth_constr_p; simpl;
    case (eq_nat_dec d0 d0); simpl; intros.
  apply in_mds_in_introduce.
  apply (in_mds_in_compose _ _ _ _ H2 H).
  auto.
  discriminate.
  intros n p2 H H0 H1 H2; destruct (cons_option_Some _ _ _ _ H0); rewrite H3 in H0;
    simpl in H0; inversion H0; subst.
  generalize H2; clear H2; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); auto.
  intros; apply (IHp1 x); auto.
  destruct a; unfold sat_meth_constr_p; simpl; case (eq_nat_dec d0 d); simpl; auto.
  fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p1 l0) (cld_def d c0 l l4))); intros;
    fold (sat_meth_constr_p d0 m (rm_dcl (introduce_classes p2 l0) (cld_def d c0 l l4))).
  applyI (sat_meth_rm_dcl _ _ c0 l l4 m (introduce_classes p2 l0) n).
  apply (IHl0 _ H H4 G1).
  applyI (sat_meth_rm_dcl _ _ c0 l l4 m (introduce_classes p1 l0) n).
  discriminate.
  discriminate.
  discriminate.
  simpl in H0, IHl; destruct (compose ps).
  destruct ( fold_right
    (fun (rcld' : rcld) (op : option P) =>
      match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
      end) (Some p0) l).
  import (IHl _ (refl_equal _) H H2).
  caseEq (compose_refines_class p1 (refines_cld_def d0 c l1 l2 l3)); intros; rewrite H3 in H0.
  inversion H0.
  apply (sat_not_introduced d p2 l0 m H).
  import (sat_not_introduced' _ _ _ _ H H1).
  import (sat_p_sat_compose 0 (refines_cld_def d0 c l1 l2 l3) d m p1 p2).
  simpl in H6; rewrite H4 in H6; simpl in H6; bd (andb_prop _ _ (H6 (refl_equal _) H3)).
  discriminate.
  discriminate.
  discriminate.
  simpl in H0; destruct (compose ps).
  import (IHps _ H1 (refl_equal _)).
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H4 in H0.
  inversion H0.
  apply (sat_not_introduced d p1 l0 m H).
  generalize p1 H3 H4; clear; induction l.
  simpl; congruence.
  destruct a; simpl; intros.
  caseEq (fold_right
           (fun (rcld' : rcld) (op : option P) =>
            match op with
            | Some p' => compose_refines_class p' rcld'
            | None => None (A:=P)
            end) (Some p0) l); intros; rewrite H in H4.
  import (IHl _ H3 H).
  import (sat_p_sat_compose 0 (refines_cld_def d0 c l0 l1 l2) d m p p1).
  simpl in H1; rewrite H0 in H1; simpl in H1; bd (andb_prop _ _ (H1 (refl_equal _) H4)).
  discriminate.
  discriminate.
  discriminate.  
  simpl in H1; discriminate.
  destruct a; simpl in H1.
  caseEq (in_clds d l0); intros; rewrite H in H1; simpl in H0.
  destruct (compose ps).
  destruct (fold_right
    (fun (rcld' : rcld) (op : option P) =>
      match op with
        | Some p' => compose_refines_class p' rcld'
        | None => None (A:=P)
      end) (Some p0) l).
  generalize p H0 H; clear; induction l0.
  unfold in_clds; simpl; intros; discriminate.
  destruct a; simpl; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl;
    intros e p H H0; inversion H.
  simpl; case (eq_nat_dec d d0); simpl; congruence.
  simpl; case (eq_nat_dec d d0); simpl; try congruence.
  fold (in_clds d (rm_dcl (introduce_classes p1 l0) (cld_def d0 c l l1))).
  fold (in_clds d l0) in H0.
  import (IHl0 _ (refl_equal _) H0).
  generalize H1; clear; induction (introduce_classes p1 l0).
  simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  discriminate.
  discriminate.
 import (distinct_compose_names ps).
 destruct (compose ps).
 import (H2 _ (refl_equal _)); clear H2.
 import (IHps _ H1 (refl_equal _)).
  generalize p H H2 H0; clear; induction l; simpl.
 induction l0.
 simpl; congruence.
 destruct a; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl; intros.
 discriminate.
 fold (in_clds d p0) in H2; fold (in_clds d p); fold (in_clds d l0) in H.
 import (IHl0 _ H H2 (refl_equal _)).
 inversion H0.
 unfold in_clds; simpl; case (eq_nat_dec d d0); simpl.
 reflexivity.
 fold (in_clds d  (rm_dcl (introduce_classes p0 l0) (cld_def d0 c l l1) )).
 generalize H1; clear; induction  (introduce_classes p0 l0).
 simpl; auto.
 destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
 congruence.
 fold (in_clds d l2); fold (in_clds d (rm_dcl l2 (cld_def d0 c l l1))); auto.
 case (eq_nat_dec d d1); intros; subst.
 simpl; auto.
 congruence.
 case (eq_nat_dec d d1); simpl.
 congruence.
 fold (in_clds d l2); fold (in_clds d (rm_dcl l2 (cld_def d0 c l l1))); auto. 
 caseEq (       fold_right
         (fun (rcld' : rcld) (op : option P) =>
          match op with
          | Some p' => compose_refines_class p' rcld'
          | None => None (A:=P)
          end) (Some p0) l); intros.
 rewrite H in IHl; import (IHl _ H0 H2 (refl_equal _)).
 assert (in_clds d p = true).
 generalize H0 H3; clear; induction l0.
 unfold in_clds; simpl; auto.
 unfold in_clds; destruct a; simpl; case (eq_nat_dec d d0); simpl.
 intros; discriminate.
 fold (in_clds d p); fold (in_clds d l0); 
   fold (in_clds d (rm_dcl (introduce_classes p l0) (cld_def d0 c l l1))); intros.
 apply IHl0; auto.
 generalize n H3; clear; induction (introduce_classes p l0).
 simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  caseEq (compose_refines_class p a); intros; rewrite H5 in H1; inversion H1; clear H1.
  assert (in_clds d p2 = true).
  destruct a; cs (d = d0); subst.
  apply (in_clds_compose' _ _ _ _ _ _ _ H4 H5).
  apply (in_clds_compose _ _ _ _ _ _ _ _ H4 H5 H1).
  generalize H0 H1; clear; induction l0.
  simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d d0); simpl.
  intros; discriminate.
  fold (in_clds d l0); fold (in_clds d p2); fold (in_clds d (rm_dcl (introduce_classes p2 l0) (cld_def d0 c l l1))).
  intros n H H0; generalize n (IHl0 H H0); clear; induction (introduce_classes p2 l0).
 simpl; auto.
  destruct a; unfold in_clds; simpl; case (eq_nat_dec d0 d1); case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  case (eq_nat_dec d d1); simpl; congruence.
  case (eq_nat_dec d d1); simpl.
  congruence.
  auto.
  discriminate.
  discriminate.
Qed.

Lemma safe_compose_compose_ps : forall (ps : PSel), safe_comp_ps ps -> exists p, compose ps = Some p.
  induction ps; intros SC_ps.
  exists nil; reflexivity.
  destruct a; simpl; inversion SC_ps; subst.
  destruct (IHps H3) as [p' Comp_ps]; rewrite Comp_ps.
  generalize (sat_comp_ps_sat_psel _ _ _ H2 Comp_ps); intro Sat_cc_p'.
  fold (compose_fd (feature_def l l0) p').
  inversion H1; subst.
  eapply sat_comp_valid_compose; eauto.        
Qed.                                           
                                               
Theorem sat_comp_build_p : Sound_Composition.  
  unfold Sound_Composition; intros until c_list; intros WF_ft Sat_cl WF_PS. 
  destruct (sat_ps_safe_comp _ _ _ WF_ft Sat_cl WF_PS) as [ps' [Bld_ps SC_ps']].
  unfold build_p; rewrite Bld_ps.
  apply (safe_compose_compose_ps _ SC_ps').
Qed.

Theorem sat_wf_PSpec_sat_gen : forall (ft : FT) (fc_list : list feature_constraint)
  (ps : PSpec) (p : P),
  wf_FT 0 ft fc_list -> wf_PSpec ft ps -> sat_feature_unique_constr ps fc_list -> build_p ft ps = Some p ->
  forall (dcl' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md), In (cld_def dcl' cl' fds' mds') p -> 
  distinct _ (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds') /\
  distinct _ (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds').
  intros until p; intros WF_ft WF_ps Sat_ps Bld_p; intros until mds'; intro In_cld.
  destruct (wf_PSpec_build_p _ _ WF_ps) as [ps' [Bld_ps _]].
  unfold build_p in Bld_p; rewrite Bld_ps in Bld_p.
  apply (sat_constr_distinct' ps' p dcl' cl' fds' mds' Bld_p); auto.
  destruct (sat_wf_PSel _ _ _ _ WF_ft Sat_ps Bld_ps) as [fc_list' [WF_ps' Sat_ps']].
  rewrite wf_PSel_gen_unique with (fc_list := fc_list'); auto.
  destruct (sat_wf_PSel _ _ _ _ WF_ft Sat_ps Bld_ps) as [fc_list' [WF_ps' _]].
  generalize fc_list' WF_ps'; clear; induction ps'.
  simpl; auto.
  intros; inversion WF_ps'; subst.
  destruct a; simpl; apply andb_true_intro; rewrite (IHps' _ H3); split; auto.
  inversion H1; subst.
  generalize uc_list1 tyc_list1 H2; clear; induction l0.
  simpl; reflexivity.
  intros; inversion H2; subst; inversion H1; subst; simpl.
  apply andb_true_intro; split.
  apply andb_true_intro; split; apply (proj2 (distinct_distinct_list _)); auto.
  eauto.
  apply andb_true_intro; split.
  apply andb_true_intro; split; apply (proj2 (distinct_distinct_list _)); auto.
  eauto.
Qed.  

Theorem sat_ps_sat_p : forall (ps : PSel) (p p' : P) (dcl' : dcl) (cl' : cl) (fds' : fds) (mds' : list md) (t_list : list ty_constraint), 
  get_refined_cld ps (cl_dcl dcl') = Some (cld_def dcl' cl' fds' mds') -> Permutation p p' -> acyclic_hierarchy p' ->
  sat_unique_constraint (ps_gen_unique_constraint ps) = true -> PS_distinct_fds_mds ps = true -> compose ps = Some p ->
  gen_ps_constr ps = Some t_list -> ps_sat_constr_list ps t_list (length (introduce_all ps)) = true ->
  exists t_list', gen_cld_constr (cld_def dcl' cl' fds' mds' :: nil) = Some t_list' /\
    sat_constr_list p' t_list' = true.
  intros.
  destruct (ex_gen_ps_gen_p _ _ _ _ _ _ _ H4 H5 H2 H3 H).
  exists x; pa.
  generalize H7; simpl gen_cld_constr.
  destruct cl'; destruct (distinct_list
           (map (fun fd' : fd => match fd' with
                                 | fd_def _ f' => f'
                                 end) fds') &&
         distinct_list
           (map
              (fun md' : md =>
               match md' with
               | md_def (ms_def _ m' _) _ => m'
               end) mds')); try (intros; discriminate).
  case (eq_nat_dec dcl' d); try (intros; discriminate).
  caseEq (fold_right
         (fun (md' : md) (m : option (list ty_constraint)) =>
          match m with
          | Some c_list' =>
              match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
              | Some c_list'' => Some (c_list'' ++ c_list')
              | None => None (A:=list ty_constraint)
              end
          | None => None (A:=list ty_constraint)
          end) (Some nil) mds'); intros; try discriminate.
  inversion H9; subst; clear H9.
  import (in_prog_gen_p_gen_ps _ _ _ _ _ _ _ H H5 H7).
  simpl in H9; import (H9 (or_introl _ (refl_equal _))); clear H9.
  assert (forall fd',  In fd' fds' -> exists fds', In fd' fds' /\
    In (inherited_fields_constr (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds') (cl_dcl dcl')) t_list).
  intros.  
  apply (inherit_fds_gen_p_gen_ps _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H9).
  assert (forall ms' mb', In (md_def ms' mb') mds' -> exists mb'', exists mds'', In (md_def ms' mb'') mds'' /\
    In (inherited_methods_constr mds'' (cl_dcl dcl')) t_list).
  intros; apply (inherit_mds_gen_p_gen_ps _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H11).
  assert (forall cl'' f', In (fd_def (ty_def cl'') f') fds' -> In (in_prog_constr cl'') t_list).
  intros; apply (in_prog_fds_gen_p_gen_ps _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H12).
  simpl; repeat (apply andb_true_intro; pa).
  import (in_sat_ps_list _ _ _ _ H10 H6).
  rewrite (ps_sat_constr_in_prog _ _ _ (cl_dcl d) H4 H0 H1) in H13.
  apply H13.
  rewrite <- (ps_fields_eq_fields _ (cl_dcl d) _ _ H4 H0 H1).
  assert (get_ps_parent ps (cl_dcl dcl') = Some (cl_dcl d)).
  unfold get_ps_parent; rewrite H; simpl; reflexivity.
  clear H; rename H13 into H.
  generalize H9 H6 H; clear.
  induction fds'; intros.
  simpl; auto.
  simpl.
  destruct a.
  simpl in H9; import (H9 _ (or_introl _ (refl_equal _))).
  bd H0.
  import (in_sat_ps_list _ _ _ _ H0 H6).
  simpl in H1.
  rewrite H in H1.
  assert (in_nat_list f (ps_fields ps (cl_dcl d) (length (introduce_all ps))) = false).
  generalize H1 H3; clear; induction x.
  simpl; intros; contradiction.
  destruct a; simpl.
  intros.
  bd H3.
  inversion H3; subst; clear H3.
  destruct (in_nat_list f
               (ps_fields ps (cl_dcl d) (length (introduce_all ps)))).
  discriminate.
  auto.
  apply IHx; auto.
   destruct (in_nat_list f0
               (ps_fields ps (cl_dcl d) (length (introduce_all ps)))).
   discriminate.
   auto.
   rewrite H2.
   apply IHfds'; auto.
   rewrite <- (ps_methods_eq_methods _ (cl_dcl d) _ _ H4 H0 H1).
   assert (forall m', ps_mtype ps (cl_dcl d) m' (length (introduce_all ps)) = mtype p' (cl_dcl d) m').
   intros; apply (ps_mtype_eq_mtype _ (cl_dcl d) m' _ _ H4 H0 H1).
   assert (get_ps_parent ps (cl_dcl dcl') = Some (cl_dcl d)).
   unfold get_ps_parent; rewrite H; simpl; reflexivity.
   clear H H0; rename H13 into H; rename H14 into H0.
   generalize H11 H6 H H0; clear.
   induction mds'; intros.
   simpl; auto.
   simpl.
   destruct a.
   simpl in H11; import (H11 _ _ (or_introl _ (refl_equal _))).
   bd H1.
   import (in_sat_ps_list _ _ _ _ H1 H6).
   simpl in H2.
   destruct m.
   rewrite <- H.
   rewrite H0 in H2.
   assert ((if negb
     (not_in_list m
       (ps_methods ps (cl_dcl d)
         (length (introduce_all ps))))
     then
       match
         ps_mtype ps (cl_dcl d) m (length (introduce_all ps))
         with
         | Some mty' =>
           mty_eq mty'
           (mty_def
             (map
               (fun vd' : vd =>
                 match vd' with
                   | vd_def ty'' _ => ty''
                 end) l) t) && true
         | None => false
       end
     else true) = true).
   revert H2 H4; clear; induction x0.
   simpl; intros; contradiction.
   simpl; intros.
   bd H4; subst.
   destruct (negb (not_in_list m
     (ps_methods ps (cl_dcl d) (length (introduce_all ps))))); auto.
   destruct (ps_mtype ps (cl_dcl d) m (length (introduce_all ps))).
   destruct (andb_prop _ _ H2); auto.
   rewrite H; auto.
   discriminate.
   apply IHx0; auto.
   destruct a; simpl.
   destruct m0.
   destruct (negb
     (not_in_list m0
       (ps_methods ps (cl_dcl d) (length (introduce_all ps))))).
   destruct (ps_mtype ps (cl_dcl d) m0 (length (introduce_all ps))).
   destruct (andb_prop _ _ H2).
   exact H0.
   discriminate.
   exact H2.
   destruct (negb
     (not_in_list m
       (ps_methods ps (cl_dcl d) (length (introduce_all ps))))).
   destruct (ps_mtype ps (cl_dcl d) m (length (introduce_all ps))); try discriminate.
   rewrite (proj1 (andb_prop _ _ H3)).
   simpl.
   apply IHmds'; auto.
   intros; apply (H11 _ _ (or_intror _ H5)).
   apply IHmds'; auto.
   intros; apply (H11 _ _ (or_intror _ H5)).
   rewrite <- app_nil_end.
   cut (sat_constr_list p' l = true).
   revert H12 H6 H0 H1 H4; clear; induction fds'.
   simpl; auto.
   destruct a; intros.
   simpl.
   destruct t; simpl in H12; import (H12 _ _ (or_introl _ (refl_equal _))).
   rewrite <- (ps_sat_constr_in_prog _ _ _ c H4 H0 H1).
   rewrite (in_sat_ps_list _ _ _ _ H2 H6); simpl.
   apply IHfds'; auto.
   intros; apply (H12 _ _ (or_intror _ H3)).
   assert (forall md', In md' mds' -> 
     exists t_list', gen_meth_constr (ty_def (cl_dcl dcl')) md' = Some t_list').
   generalize l H8; clear; induction mds'.
   simpl; intros.
   contradiction.
   simpl; intros; destruct (fold_right
     (fun (md' : md) (m : option (list ty_constraint)) =>
            match m with
            | Some c_list' =>
                match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
                | Some c_list'' => Some (c_list'' ++ c_list')
                | None => None (A:=list ty_constraint)
                end
            | None => None (A:=list ty_constraint)
            end) (Some nil) mds'); bd H; subst.
   destruct (gen_meth_constr (ty_def (cl_dcl dcl')) md'); try discriminate.
   exists l1; auto.
   apply (IHmds' l0); auto.
   discriminate.
   discriminate.
   assert (forall md', In md' mds' -> 
     exists t_list', gen_meth_constr (ty_def (cl_dcl dcl')) md' = Some t_list' /\
   (forall tyc', In tyc' t_list' -> (ps_sat_constr ps tyc' (length (introduce_all ps)) = true /\
   (forall l cl'', tyc' <> inherited_fields_constr l cl'') /\ 
   (forall md' cl', tyc' <> inherited_methods_constr md' cl')))).
   intros.
   destruct (H13 _ H14).
   exists x.
   pa.
   intros.
   import (In_stmt_gen_p_gen_ps _ _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H14 H15 H16).
   import (In_gen_meth_constr _ _ _ _ H15 H16).
   bd H18; pa.
   apply (in_sat_ps_list _ _ _ _ H17 H6).
   pa.
   assert (forall tyc', In tyc' l -> (ps_sat_constr ps tyc' (length (introduce_all ps)) = true /\
   (forall l cl'', tyc' <> inherited_fields_constr l cl'') /\ 
   (forall md' cl', tyc' <> inherited_methods_constr md' cl'))).
   generalize l H8 H14; clear; induction mds'.
   simpl; intros.
   inversion H8; subst; simpl in H; contradiction.
   intros.
   simpl in H8.
   destruct (fold_right
             (fun (md' : md) (m : option (list ty_constraint)) =>
              match m with
              | Some c_list' =>
                  match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
                  | Some c_list'' => Some (c_list'' ++ c_list')
                  | None => None (A:=list ty_constraint)
                  end
              | None => None (A:=list ty_constraint)
              end) (Some nil) mds').
   simpl in H14; import (H14 a (or_introl _ (refl_equal _))).
   bd H0.
   rewrite H3 in H8.
   inversion H8; subst; clear H8.
   import (in_app_or _ _ _ H).
   bd H1; clear H.
   apply (H0 _ H1).
   apply (IHmds' l0); auto.
   discriminate.
   assert (forall tyc', In tyc' l -> sat_constr p' tyc' = true).
   intros.
   import (H15 _ H16).
   bd H17.
   destruct tyc'.
   rewrite <- (ps_sat_constr_in_prog _ _ _ c H4 H0 H1).
   exact H20.
   rewrite <- (ps_sat_constr_compos_sty_field_r _ _ _ c f t H4 H0 H1).
   exact H20.
   rewrite <- (ps_sat_constr_compos_sty_field_w _ _ _ c f t H4 H0 H1).
   exact H20.
   rewrite <- (ps_sat_constr_compose_sty_meth _ _ _ c m t l0 H4 H0 H1).
   exact H20.
   rewrite <- (ps_sat_constr_compos_sty_cl _ _ _ t t0 H4 H0 H1).
   exact H20.
   rewrite <- (ps_sat_constr_compos_sty_if _ _ _ t t0 H4 H0 H1).
   exact H20.
   import (H21 l0 c); congruence.
   import (H17 l0 c); congruence.
   generalize H16; clear; induction l.
   simpl; auto.
   simpl; intros.
   bd H16.
   rewrite (H16 _ (or_introl _ (refl_equal _))).
   rewrite IHl; auto.
   case (eq_nat_dec dcl' d); intros; discriminate.
  caseEq (fold_right
         (fun (md' : md) (m : option (list ty_constraint)) =>
          match m with
          | Some c_list' =>
              match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
              | Some c_list'' => Some (c_list'' ++ c_list')
              | None => None (A:=list ty_constraint)
              end
          | None => None (A:=list ty_constraint)
          end) (Some nil) mds'); intros; try discriminate.
  inversion H9; subst; clear H9.
  assert (forall fd',  In fd' fds' -> exists fds', In fd' fds' /\
    In (inherited_fields_constr (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds') (cl_dcl dcl')) t_list).
  intros.  
  apply (inherit_fds_gen_p_gen_ps _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H9).
  assert (forall ms' mb', In (md_def ms' mb') mds' -> exists mb'', exists mds'', In (md_def ms' mb'') mds'' /\
    In (inherited_methods_constr mds'' (cl_dcl dcl')) t_list).
  intros; apply (inherit_mds_gen_p_gen_ps _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H10).
  assert (forall cl'' f', In (fd_def (ty_def cl'') f') fds' -> In (in_prog_constr cl'') t_list).
  intros; apply (in_prog_fds_gen_p_gen_ps _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H11).
  rewrite <- app_nil_end.
   cut (sat_constr_list p' l = true).
   revert H11 H6 H0 H1 H4; clear; induction fds'.
   simpl; auto.
   destruct a; intros.
   simpl.
   destruct t; simpl in H11; import (H11 _ _ (or_introl _ (refl_equal _))).
   rewrite <- (ps_sat_constr_in_prog _ _ _ c H4 H0 H1).
   rewrite (in_sat_ps_list _ _ _ _ H2 H6); simpl.
   apply IHfds'; auto.
   intros; apply (H11 _ _ (or_intror _ H3)).
   assert (forall md', In md' mds' -> 
     exists t_list', gen_meth_constr (ty_def (cl_dcl dcl')) md' = Some t_list').
   generalize l H8; clear; induction mds'.
   simpl; intros.
   contradiction.
   simpl; intros; destruct (fold_right
     (fun (md' : md) (m : option (list ty_constraint)) =>
            match m with
            | Some c_list' =>
                match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
                | Some c_list'' => Some (c_list'' ++ c_list')
                | None => None (A:=list ty_constraint)
                end
            | None => None (A:=list ty_constraint)
            end) (Some nil) mds'); bd H; subst.
   destruct (gen_meth_constr (ty_def (cl_dcl dcl')) md'); try discriminate.
   exists l1; auto.
   apply (IHmds' l0); auto.
   discriminate.
   discriminate.
   assert (forall md', In md' mds' -> 
     exists t_list', gen_meth_constr (ty_def (cl_dcl dcl')) md' = Some t_list' /\
   (forall tyc', In tyc' t_list' -> (ps_sat_constr ps tyc' (length (introduce_all ps)) = true /\
   (forall l cl'', tyc' <> inherited_fields_constr l cl'') /\ 
   (forall md' cl', tyc' <> inherited_methods_constr md' cl')))).
   intros.
   destruct (H12 _ H13).
   exists x.
   pa.
   intros.
   import (In_stmt_gen_p_gen_ps _ _ _ _ _ _ _ _ _ _ H H2 H3 H4 H5 H13 H14 H15).
   import (In_gen_meth_constr _ _ _ _ H14 H15).
   bd H17; pa.
   apply (in_sat_ps_list _ _ _ _ H16 H6).
   pa.
   assert (forall tyc', In tyc' l -> (ps_sat_constr ps tyc' (length (introduce_all ps)) = true /\
   (forall l cl'', tyc' <> inherited_fields_constr l cl'') /\ 
   (forall md' cl', tyc' <> inherited_methods_constr md' cl'))).
   generalize l H8 H13; clear; induction mds'.
   simpl; intros.
   inversion H8; subst; simpl in H; contradiction.
   intros.
   simpl in H8.
   destruct (fold_right
             (fun (md' : md) (m : option (list ty_constraint)) =>
              match m with
              | Some c_list' =>
                  match gen_meth_constr (ty_def (cl_dcl dcl')) md' with
                  | Some c_list'' => Some (c_list'' ++ c_list')
                  | None => None (A:=list ty_constraint)
                  end
              | None => None (A:=list ty_constraint)
              end) (Some nil) mds').
   simpl in H13; import (H13 a (or_introl _ (refl_equal _))).
   bd H0.
   rewrite H3 in H8.
   inversion H8; subst; clear H8.
   import (in_app_or _ _ _ H).
   bd H1; clear H.
   apply (H0 _ H1).
   apply (IHmds' l0); auto.
   discriminate.
   assert (forall tyc', In tyc' l -> sat_constr p' tyc' = true).
   intros.
   import (H14 _ H15).
   bd H16.
   destruct tyc'.
   rewrite <- (ps_sat_constr_in_prog _ _ _ c H4 H0 H1).
   exact H19.
   rewrite <- (ps_sat_constr_compos_sty_field_r _ _ _ c f t H4 H0 H1).
   exact H19.
   rewrite <- (ps_sat_constr_compos_sty_field_w _ _ _ c f t H4 H0 H1).
   exact H19.
   rewrite <- (ps_sat_constr_compose_sty_meth _ _ _ c m t l0 H4 H0 H1).
   exact H19.
   rewrite <- (ps_sat_constr_compos_sty_cl _ _ _ t t0 H4 H0 H1).
   exact H19.
   rewrite <- (ps_sat_constr_compos_sty_if _ _ _ t t0 H4 H0 H1).
   exact H19.
   import (H20 l0 c); congruence.
   import (H16 l0 c); congruence.
   generalize H15; clear; induction l.
   simpl; auto.
   simpl; intros.
   bd H15.
   rewrite (H15 _ (or_introl _ (refl_equal _))).
   rewrite IHl; auto.
 Qed.

Corollary sat_ps_sat_cld : forall (ps : PSel) (p p' : P) (t_list : list ty_constraint), 
  Permutation p p' -> acyclic_hierarchy p' -> sat_unique_constraint (ps_gen_unique_constraint ps) = true -> 
  PS_distinct_fds_mds ps = true -> compose ps = Some p -> gen_ps_constr ps = Some t_list -> 
  ps_sat_constr_list ps t_list (length (introduce_all ps)) = true -> exists c_list,
    gen_cld_constr p' = Some c_list /\ sat_constr_list p' c_list = true.
  intros.
  assert (forall cld', In cld' p' -> 
    exists t_list', gen_cld_constr (cld' :: nil) = Some t_list' /\ sat_constr_list p' t_list' = true).
  intros.
  import (distinct_compose_names _ _ H3).
  import (distinct_permute_names _ _ H7 H).
  destruct cld'.
  import (in_p_get_cld _ _ _ _ _ H6 H8).
  import (get_cld_eq_get_refined_cld (cl_dcl d) _ _ H3). 
  rewrite (permute_get_cld_eq _ _ (cl_dcl d) H7 H) in H10.
  rewrite H10 in H9.
  exact (sat_ps_sat_p _ _ _ _ _ _ _ _ H9 H H0 H1 H2 H3 H4 H5).
  assert (forall p'', (forall cld',
    In cld' p' ->
    exists t_list' : list ty_constraint,
      gen_cld_constr (cld' :: nil) = Some t_list' /\
      sat_constr_list p'' t_list' = true) -> 
  exists c_list : list ty_constraint,
    gen_cld_constr p' = Some c_list /\ sat_constr_list p'' c_list = true).
  clear; induction p'; intros.
  simpl; exists (nil : list ty_constraint); pa; auto.
  simpl; intros.
  simpl in H; import (H _ (or_introl _ (refl_equal _))).
  bd H0.
  destruct (gen_class_constr a); simpl in H3; try discriminate.
  rewrite <- app_nil_end in H3.
  inversion H3; subst; clear H3.
  assert ( forall cld' : cld,
    In cld' p' ->
      exists t_list' : list ty_constraint,
        match gen_class_constr cld' with
        | Some c_list'' => Some (c_list'' ++ nil)
        | None => None (A:=list ty_constraint)
        end = Some t_list' /\ sat_constr_list p'' t_list' = true).
  intros; apply H; auto.
  import (IHp' _ H1).
  bd H2.
  rewrite H5.
  exists (x ++ x0); pa; auto.
  revert H0 H2; clear; induction x.
  simpl; auto.
  intros.
  simpl in H0.
  simpl.
  destruct (andb_prop _ _ H0); clear H0; apply andb_true_intro; pa; auto.
  apply H7.
  exact H6.
Qed.

Corollary sat_ps_type_check  : forall (ps : PSel) (p p' : P) (t_list : list ty_constraint), 
  Permutation p p' -> acyclic_hierarchy p' -> sat_unique_constraint (ps_gen_unique_constraint ps) = true -> 
  PS_distinct_fds_mds ps = true -> compose ps = Some p -> gen_ps_constr ps = Some t_list -> 
  ps_sat_constr_list ps t_list (length (introduce_all ps)) = true -> type_check p' = true.
  intros.
  import (distinct_compose_names _ _ H3).
  import (distinct_permute_names _ _ H6 H).
  generalize H0 (sat_ps_sat_cld _ _ _ _ H H0 H1 H2 H3 H4 H5)
    H7; clear.
  intros.
  unfold type_check.
  unfold gen_prog_constr.
  rewrite ((proj2 (distinct_distinct_cl_list _ )) H7).
  cut (fst
           (fold_right
              (fun (cld' : cld) (b : bool * list cld) =>
               (in_list_parent cld' (snd b) && fst b, cld' :: snd b))
              (true, nil) p') = true).
  intros.
  rewrite H1.
  bd H.
  rewrite H4; rewrite H; auto.
  applyI in_list_parent_ordered'.
Qed.
  
Corollary sat_ps_compose_wf_prog  : forall (ps : PSel) (p p' : P) (t_list : list ty_constraint), 
  Permutation p p' -> acyclic_hierarchy p' -> sat_unique_constraint (ps_gen_unique_constraint ps) = true -> 
  PS_distinct_fds_mds ps = true -> compose ps = Some p -> gen_ps_constr ps = Some t_list -> 
  ps_sat_constr_list ps t_list (length (introduce_all ps)) = true -> wf_prog p'.
  intros; applyI wf_iff_type_check.
  apply (sat_ps_type_check _ _ _ _ H H0 H1 H2 H3 H4 H5).
Qed.

Theorem wf_composition  : WF_Composition.
  unfold WF_Composition; intros.
  destruct (sat_comp_build_p _ _ _ H H1 H0) as [p Bld_p].
  exists p; split; intros.
  assumption.
  unfold build_p in Bld_p; caseEq (build_PSel ft ps); intros; rewrite H6 in Bld_p; try discriminate;
    rename p0 into ps'.
  import (WF_FT_PS_distinct _ _ _ _ _ H H6).
  destruct (sat_wf_PSel _ _ _ _ H H2 H6) as [fc_list' [wf_PSel Sat_uc_PSel]].
  rewrite <- (wf_PSel_gen_unique _ _ wf_PSel) in Sat_uc_PSel.
  destruct (wf_FT_sat_constr_list''' _ _ _ _ H H6 H3) as [tyc_list [Gen_tcl Sat_tcl]].
  eapply sat_ps_compose_wf_prog; eauto.
Qed.