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 FMapFacts. Require Import Natmap. Require Import Classical. Require Import base2. Require Import Max. Fixpoint gen_stmt_list_constr (g : G) (stmt_list : list_s) {struct stmt_list} : option (list ty_constraint) := match stmt_list with Nil_list_s => Some nil | Cons_list_s s' stmt_list' => match (gen_stmt_constr g s'), (gen_stmt_list_constr g stmt_list') with Some c_list, Some c_list' => Some (c_list ++ c_list') | _, _ => None end end with gen_stmt_constr (g : G) (stmt : s) : option (list ty_constraint) := match stmt with s_new var' cl' => match (XMap.find (x_var var') g) with Some ty' => Some ((sty_cl_constr (ty_def cl') ty') :: nil) | _ => None end | s_ass var' x' => match (XMap.find x' g), (XMap.find (x_var var') g) with Some ty', Some ty'' => Some ((sty_cl_constr ty' ty'') :: nil) | _, _ => None end | s_read var' x' f' => match (XMap.find x' g), (XMap.find (x_var var') g) with Some (ty_def cl'), Some ty' => Some ( (sty_field_rconstr cl' f' ty') :: nil) | _, _ => None end | s_write x' f' y => match (XMap.find x' g), (XMap.find y g) with Some (ty_def cl'), Some ty' => Some ((sty_field_wconstr ty' cl' f') :: nil) | _, _ => None end | s_call var' x' m' param_list => match (XMap.find x' g), (XMap.find (x_var var') g) with Some (ty_def cl'), Some ty' => match (fold_right (fun (y : x) (m: option (list ty)) => match (XMap.find y g), m with Some ty', Some m' => Some (ty' :: m') | _, _ => None end) (Some nil) param_list) with Some ty_list => Some ( (sty_meth_constr cl' m' ty' ty_list) :: nil) | _ => None end | _, _ => None end | s_if x' y s1 s2 => match (XMap.find x' g), (XMap.find y g) with Some ty', Some ty'' => match (gen_stmt_constr g s1), (gen_stmt_constr g s2) with Some c_list1, Some c_list2 => Some (sty_if_constr ty' ty'' :: (c_list1 ++ c_list2)) | _ , _ => None end | _, _ => None end | s_block s_list => gen_stmt_list_constr g s_list end. Lemma wf_stmt_if_gen_stmt_constr : forall (g : G) (s_list : list_s) (c_list : list ty_constraint), wf_stmt_list_constr g s_list c_list -> gen_stmt_list_constr g s_list = Some c_list. intros g s_list. elim s_list using s_list_ind with (P := fun s => (forall c_list', wf_stmt_constr g s c_list' -> gen_stmt_constr g s = Some c_list')); intros; simpl; auto; try inversion H; subst. rewrite H3; reflexivity. rewrite H2, H4; reflexivity. rewrite H4, H5; reflexivity. rewrite H4, H5; reflexivity. rewrite H5, H6, H7; reflexivity. inversion H1; subst; rewrite H6, H8, (H _ H9), (H0 _ H10); reflexivity. inversion H0; apply H; auto. reflexivity. inversion H1; subst; rewrite (H _ H4), (H0 _ H6); reflexivity. Qed. Lemma gen_stmt_constr_if_wf_stmt : forall (g : G) (s_list : list_s) (c_list : list ty_constraint), gen_stmt_list_constr g s_list = Some c_list -> wf_stmt_list_constr g s_list c_list. intros g s_list. elim s_list using s_list_ind with (P := fun s => (forall c_list', gen_stmt_constr g s = Some c_list' -> wf_stmt_constr g s c_list')); intros; simpl; auto; try simpl in H; subst. caseEq (XMap.find (elt:=ty) (x_var var) g); intros; rewrite H0 in H; inversion H; constructor; auto. caseEq (XMap.find (elt:=ty) (x_var var) g); intros; rewrite H0 in H. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H1 in H; inversion H; constructor; auto. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H1 in H; inversion H. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H0 in H. destruct t; caseEq (XMap.find (elt:=ty) (x_var var) g); intros; rewrite H1 in H; inversion H; constructor; auto. inversion H. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H0 in H. destruct t; caseEq (XMap.find (elt:=ty) y g); intros; rewrite H1 in H; inversion H; constructor; auto. inversion H. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H0 in H. destruct t; caseEq (XMap.find (elt:=ty) (x_var var) g); intros; rewrite H1 in H. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find (elt:=ty) y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None end | None => None end) (Some nil) l); intros; rewrite H2 in H; inversion H; subst; constructor; auto. inversion H. inversion H. simpl in H1. caseEq (XMap.find (elt:=ty) x g); intros; rewrite H2 in H1; try (inversion H1; fail); caseEq (XMap.find (elt:=ty) y g); intros; rewrite H3 in H1; try (inversion H1; fail); caseEq (gen_stmt_constr g s1); intros; rewrite H4 in H1; try (inversion H1; fail); caseEq (gen_stmt_constr g s2); intros; rewrite H5 in H1; inversion H1; subst; constructor; auto. simpl in H0; constructor; auto. inversion H; constructor. simpl in H1. caseEq (gen_stmt_constr g s); intros; rewrite H2 in H1; try (inversion H1; fail); caseEq (gen_stmt_list_constr g l); intros; rewrite H3 in H1; inversion H1; constructor; auto. Qed. Fixpoint distinct_list (v_list : list nat) {struct v_list} : bool := match v_list with nil => true | cons var' v_list' => (not_in_list var' v_list') && (distinct_list v_list') end. Definition gen_meth_constr (ty1: ty) (md' : md) : option (list ty_constraint) := match md' with md_def (ms_def ty' m' vd_list) (mb_def s_list y) => if (distinct_list (map (fun (vd' : vd) => match vd' with vd_def ty' var' => var' end) vd_list)) then let g := (fold_left (fun (m : XMap.t ty) (p : x*ty) => XMap.add (fst p) (snd p) m) (cons (x_this, ty1) (map (fun (vd' : vd) => match vd' with vd_def ty' var' => (x_var var', ty') end) vd_list)) (XMap.empty ty)) in match (gen_stmt_list_constr g (make_list_s s_list)), (XMap.find y g) with Some c_list, Some ty'' => Some ((sty_cl_constr ty'' ty') :: ( (map (fun (vd' : vd) => match vd' with vd_def (ty_def cl') var' => in_prog_constr cl' end) vd_list) ++ c_list)) | _, _ => None end else None end. Lemma not_in_list_In_list : forall (var' : nat) (v_list : list nat), not_in_list var' v_list = false <-> In var' v_list. induction v_list; intros; pa; intros. simpl in H; discriminate. simpl in H; contradiction. simpl in *|-*. unfold match_nat in H; generalize H; clear H; case (eq_nat_dec var' a); intros. po1; rewrite e; reflexivity. po2; applyI IHv_list. simpl in *|-*; bd H. rewrite H; unfold match_nat; case (eq_nat_dec var' var'); intros. rewrite andb_false_intro1; auto. congruence. rewrite (proj2 (IHv_list)); auto. destruct (match_nat var' a); auto. Qed. Lemma distinct_distinct_list : forall (l : list nat), distinct_list l = true <-> distinct _ l. induction l; intros; pa; intros; simpl; auto. pa. simpl in H. unfold not; intros; rewrite (proj2 (not_in_list_In_list a l)) in H. inversion H. exact H0. simpl in H; applyI IHl; import (andb_prop _ _ H); bd H0. simpl in H; bd H; rewrite (proj2 IHl). caseEq (not_in_list a l); intros; auto. elimtype False; apply H2; applyI not_in_list_In_list. exact H. Qed. Lemma wf_meth_if_gen_meth_constr : forall (ty' : ty) (md' : md) (c_list : list ty_constraint), wf_meth_constr ty' md' c_list -> gen_meth_constr ty' md' = Some c_list. intros ty' md' c_list; destruct md'; simpl; intros WF_meth; inversion WF_meth; subst. simpl in H6, H4; rewrite H6; rewrite (wf_stmt_if_gen_stmt_constr _ _ _ H4); rewrite ((proj2 (distinct_distinct_list _)) H1); reflexivity. Qed. Lemma gen_meth_constr_if_wf_meth : forall (ty' : ty) (md' : md) (c_list : list ty_constraint), gen_meth_constr ty' md' = Some c_list -> wf_meth_constr ty' md' c_list. intros ty' md' c_list; destruct md'; simpl; intros Gen_meth_c. destruct m; destruct m0. caseEq ( distinct_list (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) l)); intros; rewrite H in Gen_meth_c; try discriminate. caseEq (gen_stmt_list_constr (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.add x_this ty' (XMap.empty ty))) (make_list_s l0)); intros; rewrite H0 in Gen_meth_c; try discriminate. caseEq ( XMap.find (elt:=ty) x (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.add x_this ty' (XMap.empty ty)))); intros; rewrite H1 in Gen_meth_c; try discriminate. inversion Gen_meth_c; subst. eapply wf_method_constr; eauto. applyI distinct_distinct_list. apply gen_stmt_constr_if_wf_stmt; auto. Qed. Lemma wf_meth_list_if_gen_meth_list : forall (mds' : list md) (ty' : ty) (c_list : list ty_constraint), wf_meth_list_constr ty' mds' c_list -> (fold_right (fun (md' : md) (m : option (list ty_constraint)) => match m with Some c_list' => match (gen_meth_constr ty' md') with Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) mds') = Some c_list. induction mds'; intros. simpl; inversion H; reflexivity. inversion H; subst; simpl. rewrite (IHmds' _ _ H4). rewrite (wf_meth_if_gen_meth_constr _ _ _ H2); reflexivity. Qed. Lemma gen_meth_list_if_wf_meth_list : forall (mds' : list md) (ty' : ty) (c_list : list ty_constraint), (fold_right (fun (md' : md) (m : option (list ty_constraint)) => match m with Some c_list' => match (gen_meth_constr ty' md') with Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) mds') = Some c_list -> wf_meth_list_constr ty' mds' c_list. induction mds'; intros. simpl in H; inversion H; constructor. simpl in H; caseEq (fold_right (fun (md' : md) (m : option (list ty_constraint)) => match m with | Some c_list' => match gen_meth_constr ty' md' with | Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) mds'); intros; rewrite H0 in H; try discriminate; caseEq (gen_meth_constr ty' a); intros; rewrite H1 in H; try discriminate; inversion H; subst. constructor. eapply gen_meth_constr_if_wf_meth; eauto. eapply IHmds'; eauto. Qed. Definition gen_class_constr (cld': cld) : option (list ty_constraint) := match cld' with cld_def dcl' (cl_dcl dcl'') fds' mds' => if (eq_nat_dec dcl' dcl'') then None else let f_list := (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds') in let m_list := (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds') in if distinct_list f_list && distinct_list m_list then match (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 end | None => None end) (Some nil) mds') with Some c_list => Some ((in_prog_constr (cl_dcl dcl'')) :: (inherited_fields_constr f_list (cl_dcl dcl'')) :: (inherited_methods_constr mds' (cl_dcl dcl'')) :: ((map (fun (fd' : fd) => match fd' with fd_def (ty_def cl') _ => in_prog_constr cl' end) fds') ++ c_list)) | None => None end else None | cld_def dcl' cl_object fds' mds' => let f_list := (map (fun (fd' : fd) => match fd' with fd_def ty' f'=> f' end) fds') in let m_list := (map (fun (md' : md) => match md' with md_def (ms_def _ m' _) _=> m' end) mds') in if distinct_list f_list && distinct_list m_list then match (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 end | None => None end) (Some nil) mds') with Some c_list => Some ((map (fun (fd' : fd) => match fd' with fd_def (ty_def cl') _ => in_prog_constr cl' end) fds') ++ c_list) | None => None end else None end. Lemma wf_cld_if_gen_class_constr : forall (cld' : cld) (c_list : list ty_constraint), wf_cld_constr cld' c_list -> gen_class_constr cld' = Some c_list. intros cld' c_list; destruct cld'; simpl; intros WF_cld; inversion WF_cld; subst. destruct (eq_nat_dec d dcl''). congruence. rewrite (proj2 (distinct_distinct_list _ ) H7); rewrite (proj2 (distinct_distinct_list _ ) H8); simpl. rewrite (wf_meth_list_if_gen_meth_list _ _ _ H9); reflexivity. rewrite (proj2 (distinct_distinct_list _ ) H7); rewrite (proj2 (distinct_distinct_list _ ) H6); simpl. rewrite (wf_meth_list_if_gen_meth_list _ _ _ H8); reflexivity. Qed. Lemma gen_class_constr_if_wf_cld : forall (cld' : cld) (c_list : list ty_constraint), gen_class_constr cld' = Some c_list -> wf_cld_constr cld' c_list. intros cld' c_list Gen_class; destruct cld'; simpl in Gen_class; destruct c. destruct (eq_nat_dec d d0). discriminate. caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)); intros; rewrite H in Gen_class; try discriminate; caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)); intros; rewrite H0 in Gen_class; try 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 d)) md' with | Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) l0); intros; rewrite H1 in Gen_class; try discriminate; inversion Gen_class; subst; eapply wf_class_constraint; eauto; try applyI distinct_distinct_list; apply gen_meth_list_if_wf_meth_list; auto. caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)); intros; rewrite H in Gen_class; try discriminate; caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)); intros; rewrite H0 in Gen_class; try 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 d)) md' with | Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) l0); intros; rewrite H1 in Gen_class; try discriminate; inversion Gen_class; subst; eapply wf_class_constraint_obj; eauto; try applyI distinct_distinct_list; apply gen_meth_list_if_wf_meth_list; auto. Qed. Definition gen_cld_constr (cld_list : list cld) : option (list ty_constraint) := (fold_right (fun (cld' : cld) (m : option (list ty_constraint)) => match m with Some c_list' => match (gen_class_constr cld') with Some c_list'' => Some (c_list'' ++ c_list') | None => None end | None => None end) (Some nil) cld_list). Definition cl_eq (cl1 cl2 : cl) : bool := match cl1, cl2 with cl_object, cl_object => true | cl_dcl dcl1, cl_dcl dcl2 => if (eq_nat_dec dcl1 dcl2) then true else false | _, _ => false end. Lemma eq_cl_eq : forall (cl1 cl2 : cl), cl_eq cl1 cl2 = true <-> cl1 = cl2. destruct cl1; destruct cl2; simpl; pa; try congruence; case (eq_nat_dec d d0); intros; congruence. Qed. Definition in_cl_list (cl' : cl) (cl_list : list cl) : bool := existsb (cl_eq cl') cl_list. Fixpoint distinct_cl_list (cl_list : list cl) {struct cl_list} : bool := match cl_list with nil => true | cons cl' cl_list' => negb (in_cl_list cl' cl_list') && (distinct_cl_list cl_list') end. Lemma in_cl_list_In_cl_list : forall (cl' : cl) (cl_list : list cl), In cl' cl_list <-> in_cl_list cl' cl_list = true. induction cl_list; simpl; pa; intros. contradiction. discriminate. apply orb_true_intro; bd H. po1; applyI eq_cl_eq; auto. po2; applyI IHcl_list. destruct (orb_prop _ _ H). po1; import ((proj1 (eq_cl_eq _ _ )) H0); auto. po2; applyI IHcl_list. Qed. Lemma distinct_distinct_cl_list : forall (cl_list : list cl), distinct_cl_list cl_list = true <-> distinct _ cl_list. induction cl_list; simpl; pa; intros; auto. destruct (andb_prop _ _ H); pa. unfold not; intros; rewrite ((proj1 (in_cl_list_In_cl_list _ _)) H2) in H0; discriminate. applyI IHcl_list. bd H; apply andb_true_intro; pa. caseEq (in_cl_list a cl_list); intros; auto. import ((proj2 (in_cl_list_In_cl_list _ _ )) H0); contradiction. applyI IHcl_list. Qed. Fixpoint in_list_dcl (dcl' : dcl) (cld_list : list cld) {struct cld_list} : bool := match cld_list with nil => false | cld_def dcl'' _ _ _ :: cld_list'=> if (eq_nat_dec dcl' dcl'') then true else in_list_dcl dcl' cld_list' end. Definition in_list_parent (cld' : cld) (cld_list : list cld) : bool := match cld' with cld_def _ cl_object _ _ => true | cld_def _ (cl_dcl dcl') _ _ => in_list_dcl dcl' cld_list end. Lemma in_list_parent_In_names : forall (cl' : cl) (cld' : cld) (cld_list : list cld), get_parent cld' = cl' -> in_list_parent cld' cld_list = true -> In cl' (names cld_list). destruct cld'; intros; subst; destruct c; simpl. induction cld_list; simpl in *|-*. discriminate. destruct a; generalize H0; clear H0; case (eq_nat_dec d0 d1); intros. rewrite e; simpl; po1. simpl; po2; apply (IHcld_list H0). clear H0; induction cld_list; simpl; auto. destruct a; po2. Qed. Lemma In_names_in_list_parent : forall (cl' : cl) (cld' : cld) (cld_list : list cld), get_parent cld' = cl' -> In cl' (names cld_list) -> in_list_parent cld' cld_list = true. destruct cld'; intros; subst; destruct c; simpl. induction cld_list; simpl in *|-*. bd H0; congruence. destruct a; generalize H0; clear H0; case (eq_nat_dec d0 d1); intros. subst; simpl in H0; bd H0. simpl in H0; bd H0. congruence. apply (IHcld_list H0). reflexivity. Qed. Lemma snd_in_list_parent_map : forall (cld_list : list cld), snd (fold_right (fun (cld' : cld) (b : bool* list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: (snd b))) (true, nil) cld_list) = cld_list. induction cld_list; simpl; congruence. Qed. Definition gen_prog_constr (p : list cld) : option (list ty_constraint) := if distinct_cl_list (names p) then if (fst (fold_right (fun (cld' : cld) (b : bool* list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: (snd b))) (true, nil) p)) then gen_cld_constr p else None else None. Lemma wf_prog_if_gen_prog_constr : forall (p : P) (c_list : list ty_constraint), wf_prog_constr p c_list -> gen_prog_constr p = Some c_list. intros; inversion H; subst; unfold gen_prog_constr; rewrite ((proj2 (distinct_distinct_cl_list _)) H0). caseEq (fst (fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) p)); intros. generalize p c_list H1; clear. induction p; intros; inversion H1; subst. reflexivity. simpl; rewrite (IHp _ H4); rewrite (wf_cld_if_gen_class_constr _ _ H2); reflexivity. elimtype False; generalize p H2 H3; clear; induction p; simpl; intros. discriminate. inversion H2; subst. destruct (andb_false_elim _ _ H3) as [Not_In_a | Not_acyclic]. destruct a; simpl in H4. erewrite (In_names_in_list_parent) in Not_In_a. discriminate. simpl; eauto. generalize H4; clear; induction p. intros; destruct H4 as [cl' [Eq_cl' In_cl']]; subst; auto. destruct a; simpl; intros; destruct H4 as [cl' [Eq_cl' [Eq | In]]]; subst; auto. right; apply IHp; exists cl'; auto. auto. Qed. Lemma gen_prog_constr_if_wf_prog : forall (p : P) (c_list : list ty_constraint), gen_prog_constr p = Some c_list -> wf_prog_constr p c_list. unfold gen_prog_constr; intros. caseEq (distinct_cl_list (names p)); intros; rewrite H0 in H; try discriminate; caseEq (fst (fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) p)); intros; rewrite H1 in H; try discriminate. constructor. applyI distinct_distinct_cl_list. generalize c_list H; clear; induction p; intros. simpl in H; inversion H; subst; constructor. simpl in H; caseEq (gen_cld_constr p); intros; rewrite H0 in H; try discriminate; caseEq (gen_class_constr a); intros; rewrite H1 in H; try discriminate; inversion H; subst; constructor. apply gen_class_constr_if_wf_cld; auto. auto. revert H1; clear; induction p; simpl; intros; constructor. destruct ((proj1 (andb_true_iff _ _)) H1); apply IHp; auto. destruct ((proj1 (andb_true_iff _ _)) H1) as [H2 _]. generalize H2; clear; induction p. simpl; intros. destruct a; simpl in H2; destruct c; simpl in *|-*; auto. discriminate. exists cl_object; auto. destruct a; destruct a0; simpl; intros; destruct c. exists (cl_dcl d1); split; auto. destruct (eq_nat_dec d1 d0); auto. right. generalize H2; clear; induction p; simpl. intros; discriminate. destruct a; simpl; destruct (eq_nat_dec d1 d); intros; auto. exists cl_object; split; auto. right; apply cl_object_in_names. Qed. Lemma path_distinct_names : forall (p : P) (cl' : cl), distinct _ (names p) -> distinct _ (names (path p cl')). induction p; intros. simpl; tauto. simpl; destruct a; destruct cl'; try case (eq_nat_dec d0 d); intros. simpl in *|-*; bd H. pa. unfold not; intros; apply H2; clear H2. import (In_names_In_p _ _ H0); bd H1. apply (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H1)). apply IHp; auto. simpl in H; bd H; auto. simpl; tauto. Qed. Lemma in_path_In_path' : forall (p : P) (c : cl) (d : dcl), in_path (path p c) d = true -> exists cl', exists fds', exists mds', In (cld_def d cl' fds' mds') (path p c). induction p; intros. simpl in H; discriminate. simpl in H; destruct a; destruct c. generalize H; clear H; case (eq_nat_dec d1 d0); simpl; case (eq_nat_dec d d0); simpl; intros. exists c0; exists l; exists l0; subst. case (eq_nat_dec d0 d0); intros. simpl; po1. elimtype False; auto. import (IHp _ _ H); bd H0. exists x; exists x0; exists x1; subst. case (eq_nat_dec d0 d0); intros. simpl; po2; auto. elimtype False; auto. import (IHp _ _ H); bd H0. exists x; exists x0; exists x1; subst. case (eq_nat_dec d1 d0); intros. congruence. exact H0. import (IHp _ _ H); bd H0. exists x; exists x0; exists x1; subst. case (eq_nat_dec d1 d0); intros. congruence. exact H0. simpl in H; discriminate. Qed. Lemma in_path_In_path : forall (p : P) (d : dcl), in_path p d = true -> exists cl', exists fds', exists mds', In (cld_def d cl' fds' mds') p. induction p; intros. simpl in H; discriminate. simpl in H; destruct a. generalize H; clear H; case (eq_nat_dec d d0); simpl; intros. exists c; exists l; exists l0; subst. po1. import (IHp _ H); bd H0. exists x; exists x0; exists x1; subst. po2. Qed. Lemma In_path_in_path' : forall (p : P) (c cl': cl) (d : dcl) (fds' : list fd) (mds' : list md), In (cld_def d cl' fds' mds') (path p c) -> in_path (path p c) d = true. induction p; intros. simpl in H; contradiction. simpl in H; destruct a; destruct c. simpl; generalize H; clear H; case (eq_nat_dec d1 d0); simpl; case (eq_nat_dec d d0); simpl; intros. reflexivity. bd H. subst; congruence. apply (IHp _ _ _ _ _ H). subst. apply (IHp _ _ _ _ _ H). apply (IHp _ _ _ _ _ H). simpl in H; contradiction. Qed. Lemma In_path_in_path : forall (p : P) (c : cl) (d : dcl) (fds' : list fd) (mds' : list md), In (cld_def d c fds' mds') p -> in_path p d = true. induction p; intros. simpl in H; contradiction. simpl in H; destruct a. bd H. inversion H; subst; simpl. case (eq_nat_dec d d); intros; congruence. simpl; case (eq_nat_dec d d0); intros; try congruence. apply (IHp _ _ _ _ H). Qed. Lemma path_distinct_cld : forall (p : P) (dcl' : dcl) (c cl' cl'' : cl) (fds' fds'' : list fd) (mds' mds'': list md), distinct _ (names p) -> In (cld_def dcl' cl' fds' mds') (path p c) -> In (cld_def dcl' cl'' fds'' mds'') (path p c) -> (cl' = cl'' /\ fds' = fds'' /\ mds' = mds''). intros. import (path_distinct_names _ c H); clear H. induction (path p c). simpl in H0; contradiction. destruct a; simpl in *; bd H2; bd H1; bd H0; auto. rewrite H1 in H0; inversion H0; subst; repeat pa. inversion H1; subst. elimtype False; apply H4; apply (In_p_In_names _ _ _ _ _ H0). inversion H0; subst. elimtype False; apply H4; apply (In_p_In_names _ _ _ _ _ H1). Qed. Lemma ord_path_eq_parent : forall (p : P) (cl' : cl) (dcl' : dcl) (fds' : list fd) (md_list : list md), acyclic_hierarchy p -> In (cld_def dcl' cl' fds' md_list) p -> distinct _ (names p) -> path p (cl_dcl dcl') = (cld_def dcl' cl' fds' md_list) :: (path p cl'). intros. induction p. simpl in H0; elimtype False; apply H0. generalize (distinct_acyclic_hierarchy _ _ H0 H H1); intros H8; simpl in H8. destruct a. simpl in H0, H1; bd H1; bd H0. inversion H0; subst. clear H0. simpl. case (eq_nat_dec dcl' dcl'); intros H6; try (elimtype False; apply H6; reflexivity). destruct cl'. case (eq_nat_dec d dcl'); intros. rewrite e in H8; elimtype False; apply H8; reflexivity. reflexivity. rewrite path_cl_object; reflexivity. inversion H. generalize (IHp H5 H0 H1); clear IHp; intros. simpl. case (eq_nat_dec dcl' d); intros H9; try (elimtype False; apply H9; reflexivity). destruct cl'; rewrite H9 in H0; generalize (In_p_In_names _ _ _ _ _ H0); intros; elimtype False; apply H4; exact H10. rewrite H7. destruct cl'. case (eq_nat_dec d0 d); intros; subst. simpl in H7; rewrite <- H7 in *|-*; clear H7. import (list_ordered_parent _ _ H0 H5). bd H2. simpl in H10; rewrite <- H10 in H2. elimtype False; apply H4; exact H2. reflexivity. rewrite path_cl_object; apply refl_equal. Qed. Lemma in_path_sty : forall (p : P) (dcl' dcl'' : dcl) (cl'' : cl) (fds'' : list fd) (mds'' : list md), acyclic_hierarchy p -> distinct _ (names p) -> In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl dcl')) -> sty_one p (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')). intros p dcl'; assert (exists l, l = path p (cl_dcl dcl')). exists (path p (cl_dcl dcl')); reflexivity. bd H. intros; generalize p dcl' dcl'' cl'' fds'' mds'' H H0 H1 H2; clear. induction x; intros. rewrite <- H in H2; simpl in H2; contradiction. rewrite <- H in H2; destruct a; simpl in H2; bd H2. rewrite (path_eq_self _ _ _ _ _ _ _ (sym_eq H)) in |-*. assert (In (cld_def d c l l0) (path p (cl_dcl dcl'))). rewrite <- H; simpl; po1. inversion H2; subst. apply (sty_reflexive _ _ _ _ _ (in_path_in_prog _ _ _ H3)). assert (In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl dcl'))). rewrite <- H. simpl; po2. rewrite (path_eq_self _ _ _ _ _ _ _ (sym_eq H)); rewrite (path_eq_self _ _ _ _ _ _ _ (sym_eq H)) in H3, H. assert (In (cld_def d c l l0) (path p (cl_dcl d))). rewrite <- H; simpl; po1. rewrite (ord_path_eq_parent _ _ _ _ _ H0 (in_path_in_prog _ _ _ H4) H1) in H. inversion H; subst. destruct c. import (IHx p d0 _ _ _ _ (refl_equal _) H0 H1 H2). import (sty_from_direct _ _ _ (sty_dir _ _ _ _ _ (in_path_in_prog _ _ _ H4))). apply (sty_transitive _ _ _ _ H6 H5). rewrite path_cl_object in H2; simpl in H2; contradiction. Qed. Lemma path_eq_ancestor : forall (p : P) (dcl' dcl'' : dcl) (cl' : cl) (fds' : list fd) (mds' : list md), acyclic_hierarchy p -> distinct _ (names p) -> In (cld_def dcl' cl' fds' mds') (path p (cl_dcl dcl'')) -> exists l, path p (cl_dcl dcl'') = l ++ path p (cl_dcl dcl'). induction p; intros. simpl in H1; contradiction. simpl in H1. destruct a; generalize H1; simpl; clear H1; case (eq_nat_dec dcl'' dcl'); case (eq_nat_dec dcl'' d); intros. exists (nil : list cld); simpl; rewrite <- e0; rewrite e; auto. simpl; case (eq_nat_dec d d); intros; auto. congruence. case (eq_nat_dec dcl' d); intros. congruence. subst; exists (nil : list cld); auto. case (eq_nat_dec dcl' d); intros. congruence. simpl in H1; bd H1. inversion H1; congruence. inversion H; simpl in H0; bd H0; subst. destruct c. import (IHp _ _ _ _ _ H4 H0 H1). bd H2; rewrite H2; exists (cld_def d (cl_dcl d0) l l0 :: x); auto. rewrite path_cl_object in H1; simpl in H1; contradiction. case (eq_nat_dec dcl' d); intros. subst; import (in_path_in_prog _ _ _ H1). simpl in H0; bd H0. import (In_p_In_names _ _ _ _ _ H2). contradiction. inversion H; simpl in H0; bd H0; subst. import (IHp _ _ _ _ _ H4 H0 H1); bd H2. Qed. Lemma in_path_ancestor : forall (p : P) (d dcl' dcl'' : dcl) (cl' cl'' : cl) (fds' fds'' : list fd) (mds' mds'' : list md), acyclic_hierarchy p -> distinct _ (names p) -> In (cld_def dcl' cl' fds' mds') (path p (cl_dcl d)) -> In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl dcl')) -> In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl d)). intros. destruct (path_eq_ancestor _ _ _ _ _ _ H H0 H1). rewrite H3. apply in_or_app. po2. Qed. Lemma sty_cl_object : forall (p : P) (ty' : ty), sty_one p (ty_def cl_object) (ty') -> ty' = (ty_def cl_object). destruct ty'; destruct c; auto. assert (exists ty1, ty1 = ty_def (cl_object)). exists (ty_def cl_object); auto. assert (exists ty2, ty2 = ty_def (cl_dcl d)). exists (ty_def (cl_dcl d)); auto. bd H; bd H0; rewrite <- H; rewrite <- H0; intros. generalize d H H0; clear d H H0; induction H1; intros; subst. inversion H. reflexivity. discriminate. destruct ty'; destruct c. import (IHsty_one1 _ (refl_equal _) (refl_equal _)); discriminate. import (IHsty_one2 _ (refl_equal _) (refl_equal _)); discriminate. Qed. Lemma sty_cl_object' : forall (p : P) (dcl' : dcl), acyclic_hierarchy p -> distinct _ (names p) -> In (cl_dcl dcl') (names p) -> sty_one p (ty_def (cl_dcl dcl')) (ty_def cl_object). induction p; simpl; intros. bd H1; discriminate. destruct a. simpl in H1; bd H1. inversion H1. destruct c. assert (In (cld_def dcl' (cl_dcl d0) l l0) (cld_def dcl' (cl_dcl d0) l l0 :: p)). simpl; po1. rewrite H3 in *|-*. import (list_ordered_parent _ _ H2 H). bd H4. simpl in H7; rewrite <- H7 in *; simpl in H4. import (distinct_acyclic_hierarchy _ _ H2 H H0); simpl in H5. bd H4. congruence. simpl in H0; bd H0; inversion H; import (IHp _ H10 H0 H4). assert (sty_one ((cld_def dcl' (cl_dcl d0) l l0 :: p)) (ty_def (cl_dcl d0)) (ty_def cl_object)). generalize H12 H5; clear. intros. induction H12. apply sty_from_direct. inversion H. assert (In (cld_def dcl5 cl5 fds5 md_list) (cld_def dcl' (cl_dcl d0) l l0 :: P5) ). simpl; po2. apply (sty_dir _ _ _ _ _ H4). apply sty_opt_refl. assert ((In (cld_def dcl'0 cl' fds' mds) (cld_def dcl' (cl_dcl d0) l l0 :: P5) )). simpl; po2. apply (sty_reflexive _ _ _ _ _ H0). apply (sty_transitive _ _ _ _ IHsty_one1 IHsty_one2). assert (In (cld_def dcl' (cl_dcl d0) l l0) (cld_def dcl' (cl_dcl d0) l l0 :: p)). simpl; po1. apply (sty_transitive _ _ _ _ (sty_from_direct _ _ _ (sty_dir _ _ _ _ _ H14) ) H13). assert (In (cld_def dcl' cl_object l l0) (cld_def dcl' cl_object l l0 :: p)). simpl; po1. apply (sty_from_direct _ _ _ (sty_dir _ _ _ _ _ H2)). simpl in H0; bd H0; inversion H; import (IHp _ H5 H0 H1). cs (cl_dcl dcl' = cl_dcl d). congruence. generalize H7 H8; clear; intros H12 H5. induction H12. apply sty_from_direct. inversion H. assert (In (cld_def dcl5 cl5 fds5 md_list) (cld_def d c l l0 :: P5) ). simpl; po2. apply (sty_dir _ _ _ _ _ H4). apply sty_opt_refl. assert ((In (cld_def dcl'0 cl' fds' mds) (cld_def d c l l0 :: P5) )). simpl; po2. apply (sty_reflexive _ _ _ _ _ H0). apply (sty_transitive _ _ _ _ IHsty_one1 IHsty_one2). Qed. Lemma parent_in_path_sty' : forall (p : P) (dcl' dcl'' : dcl), acyclic_hierarchy p -> distinct _ (names p) -> sty_one p (ty_def (cl_dcl dcl')) (ty_def (cl_dcl dcl'')) -> exists cl'', exists fds'', exists mds'', In (cld_def dcl'' cl'' fds'' mds'') (path p (cl_dcl dcl')). intros. assert (exists ty1, ty1 = (ty_def (cl_dcl dcl'))). exists (ty_def (cl_dcl dcl')); auto. assert (exists ty2, ty2 = (ty_def (cl_dcl dcl''))). exists (ty_def (cl_dcl dcl'')); auto. bd H2; bd H3; rewrite <- H2 in H1; rewrite <- H3 in H1. generalize dcl' dcl'' H2 H3; clear dcl' dcl'' H2 H3; induction H1; intros; subst. inversion H1; subst. import (list_ordered_parent _ _ H5 H); bd H2. destruct x. import (In_names_In_p _ _ H2); bd H3. rewrite (ord_path_eq_parent _ _ _ _ _ H H5 H0). simpl in H6; inversion H6. rewrite (ord_path_eq_parent _ _ _ _ _ H H3 H0). exists x; exists x0; exists x1; po2; po1. simpl in H6; discriminate. discriminate. inversion H3; inversion H2; subst. exists cl'; exists fds'; exists mds. rewrite <- H6. apply In_prog_In_path; auto. destruct ty'; destruct c. import (IHsty_one2 H H0 d dcl'' (refl_equal _) (refl_equal _)). import (IHsty_one1 H H0 dcl' d (refl_equal _) (refl_equal _)). bd H1; bd H2; clear IHsty_one1 IHsty_one2. exists x; exists x0; exists x1; apply (in_path_ancestor _ _ _ _ _ _ _ _ _ _ H H0 H2 H1). import (sty_cl_object _ _ H1_0); discriminate. Qed. Lemma sat_fieldr_constr : forall (p : P) (ty' : ty) (dcl' : dcl) (f' : f), acyclic_hierarchy p -> distinct _ (names p) -> sat_constr p (sty_field_rconstr (cl_dcl dcl') f' ty') = true -> exists ty'', ftype p (cl_dcl dcl') f' = Some ty'' /\ sty_option p (Some ty'') (Some ty'). intros. inversion H1; destruct ty'. caseEq (ftype p (cl_dcl dcl') f'); intros; rewrite H2 in H3. exists t; pa. destruct t; destruct c; destruct c0. import (in_path_In_path _ _ H3); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H4)). discriminate. import (in_path_In_path _ _ H3); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H4)))). apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _ )). destruct c; discriminate. Qed. Lemma sat_fieldw_constr : forall (p : P) (ty' : ty) (dcl' : dcl) (f' : f), acyclic_hierarchy p -> distinct _ (names p) -> sat_constr p (sty_field_wconstr ty' (cl_dcl dcl') f' ) = true -> exists ty'', ftype p (cl_dcl dcl') f' = Some ty'' /\ sty_option p (Some ty') (Some ty''). intros. inversion H1; destruct ty'; caseEq (ftype p (cl_dcl dcl') f'); intros; rewrite H2 in H3. exists t; pa. destruct c; destruct t; destruct c. import (in_path_In_path _ _ H3); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H4)). import (in_path_In_path _ _ H3); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H4)))). discriminate. apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _ )). destruct c; discriminate. Qed. Lemma sat_meth_constr : forall (p : P) (dcl'': dcl) (cl' : cl) (m' : m) (ty_list : list ty), acyclic_hierarchy p -> distinct _ (names p) -> sat_constr p (sty_meth_constr (cl_dcl dcl'') m' (ty_def cl') ty_list) = true -> exists ty'', exists ty_list', mtype p (cl_dcl dcl'') m' = Some (mty_def ty_list' ty'') /\ sty_option p (Some ty'') (Some (ty_def cl')) /\ length ty_list = length ty_list' /\ sty_opt_list (map (fun (y : ty*ty) => (p, Some (fst y), Some (snd y))) (combine ty_list ty_list')). intros. inversion H1. caseEq (mtype p (cl_dcl dcl'') m'); intros. rewrite H2 in H3. caseEq m; intros. exists t; exists l; repeat pa. rewrite H4 in H3. generalize H3; clear H3; case (eq_nat_dec (length ty_list) (length l)); intros. destruct t; destruct c; destruct cl'. destruct (andb_prop _ _ H3); clear H3. import (in_path_In_path _ _ H5); bd H3. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H3)). destruct (andb_prop _ _ H3); clear H3. import (in_path_In_path _ _ H5); bd H3. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H3)))). discriminate. apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _)). destruct t; destruct c; destruct cl'; discriminate. generalize H3; clear H3; rewrite H4; case (eq_nat_dec (length ty_list) (length l)); intros. auto. destruct t; destruct c; destruct cl'; discriminate. rewrite H4 in H3. generalize H3; clear H3; case (eq_nat_dec (length ty_list) (length l)); intros. destruct cl'. destruct t; destruct c. destruct (andb_prop _ _ H3); clear H3. generalize l H6 H H0; clear; induction ty_list; intros t H H0 H1. simpl; apply Nil_sty_opt_list. destruct t; simpl in *|-*. apply Nil_sty_opt_list. destruct a; destruct t; destruct c0; destruct c; try (destruct (andb_prop _ _ H)). apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H0 H1 H4)). apply IHty_list; auto. discriminate. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. import (in_path_in_prog _ _ _ H4). apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H0 H1 (In_p_In_names _ _ _ _ _ H5))). apply IHty_list; auto. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _)). apply IHty_list; auto. discriminate. destruct t; destruct c. destruct (andb_prop _ _ H3); clear H3. generalize l H6 H H0; clear; induction ty_list; intros t H H0 H1. simpl; apply Nil_sty_opt_list. destruct t; simpl in *|-*. apply Nil_sty_opt_list. destruct a; destruct t; destruct c0; destruct c; try (destruct (andb_prop _ _ H)). apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H0 H1 H4)). apply IHty_list; auto. discriminate. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. import (in_path_in_prog _ _ _ H4). apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H0 H1 (In_p_In_names _ _ _ _ _ H5))). apply IHty_list; auto. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _)). apply IHty_list; auto. generalize l H3 H H0; clear; induction ty_list; intros t H H0 H1. simpl; apply Nil_sty_opt_list. destruct t; simpl in *|-*. apply Nil_sty_opt_list. destruct a; destruct t; destruct c0; destruct c; try (destruct (andb_prop _ _ H)). apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H0 H1 H4)). apply IHty_list; auto. discriminate. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). import (in_path_In_path _ _ H2); bd H4. import (in_path_in_prog _ _ _ H4). apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H0 H1 (In_p_In_names _ _ _ _ _ H5))). apply IHty_list; auto. apply Cons_sty_opt_list; try (apply (ty_def cl_object)). apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _)). apply IHty_list; auto. destruct t; destruct c; destruct cl'; discriminate. rewrite H2 in H3; discriminate. Qed. Lemma sat_cl_constr : forall (p : P) (ty' ty'': ty), acyclic_hierarchy p -> distinct _ (names p) -> (sat_constr p (sty_cl_constr ty' ty'') = true <-> sty_option p (Some ty') (Some ty'')). intros; pa; intros. inversion H1. destruct ty'; destruct ty''; destruct c0. destruct c. import (in_path_In_path _ _ H3); bd H2. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H2)). rewrite path_cl_object in H3; simpl in H3; discriminate. destruct c. import (in_path_In_path _ _ H3). bd H2. import (in_path_in_prog _ _ _ H2). apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ H4))). apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _ )). destruct ty'; destruct ty''; destruct c; destruct c0; simpl. inversion H1; inversion H2; inversion H3; subst. import (parent_in_path_sty' _ _ _ H H0 H4); bd H5. apply (In_path_in_path _ _ _ _ _ H5). inversion H1; inversion H2; inversion H3; subst. import (in_path_sty' _ _ _ H H0 H4); bd H5. apply (In_path_in_path _ _ _ _ _ H5). inversion H1; inversion H2; inversion H3; subst. import (sty_cl_object _ _ H4); discriminate. auto. Qed. Lemma in_path_sty_option : forall (p : P) (d : dcl) (c : cl), acyclic_hierarchy p -> distinct _ (names p) -> in_path (path p c) d = true -> sty_option p (Some (ty_def c)) (Some (ty_def (cl_dcl d))). intros. import (in_path_In_path _ _ H1); bd H2. destruct c. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H2)). rewrite path_cl_object in H2; contradiction. Qed. Lemma in_path_sty_option' : forall (p : P) (d : dcl) (c : cl), acyclic_hierarchy p -> distinct _ (names p) -> sty_option p (Some (ty_def c)) (Some (ty_def (cl_dcl d))) -> in_path (path p c) d = true. intros. inversion H1; inversion H2; inversion H3; subst. destruct c. import (parent_in_path_sty' _ _ _ H H0 H4); bd H5. apply (In_path_in_path _ _ _ _ _ H5). import (sty_cl_object _ _ H4); discriminate. Qed. Lemma sat_constr_list_app : forall (p : P) (c_list1 c_list2 : list ty_constraint), sat_constr_list p (c_list1 ++ c_list2) = true -> sat_constr_list p (c_list1) = true /\ sat_constr_list p (c_list2) = true. induction c_list1; intros. simpl in *|-*; pa. simpl in *|-*; destruct (andb_prop _ _ H); rewrite H0. destruct (IHc_list1 _ H1). pa; apply andb_true_intro; pa. Qed. Lemma sat_constr_list_app' : forall (p : P) (c_list1 c_list2 : list ty_constraint), sat_constr_list p (c_list1) = true /\ sat_constr_list p (c_list2) = true -> sat_constr_list p (c_list1 ++ c_list2) = true. induction c_list1; intros. simpl in *|-*; bd H; auto. bd H; simpl in H2. simpl in *|-*; destruct (andb_prop _ _ H2); rewrite H0. apply andb_true_intro; pa; apply IHc_list1; auto. Qed. Lemma sat_if_constr : forall (p : P) (ty' ty'': ty), acyclic_hierarchy p -> distinct _ (names p) -> (sat_constr p (sty_if_constr ty' ty'') = true <-> sty_option p (Some ty') (Some ty'') \/ sty_option p (Some ty'') (Some ty')). pa; intros. inversion H1. destruct ty'; destruct ty''; destruct c; destruct c0; try discriminate. destruct (orb_prop _ _ H3); import (in_path_In_path _ _ H2); bd H4. po1. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H4)). po2. apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (in_path_sty _ _ _ _ _ _ H H0 H4)). import (in_path_In_path _ _ H3); bd H2. po1; apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H2)))). import (in_path_In_path _ _ H3); bd H2. po2; apply (sty_opt _ _ _ _ _ (refl_equal _) (refl_equal _) (sty_cl_object' _ _ H H0 (In_p_In_names _ _ _ _ _ (in_path_in_prog _ _ _ H2)))). po1; apply (sty_opt p _ _ _ _ (refl_equal _) (refl_equal _) (sty_opt_refl _ )). destruct ty'; destruct ty''; destruct c; destruct c0; simpl; bd H1; inversion H1; inversion H2; inversion H3; subst. import (parent_in_path_sty' _ _ _ H H0 H4); bd H5. rewrite (In_path_in_path _ _ _ _ _ H5); auto. import (parent_in_path_sty' _ _ _ H H0 H4); bd H5. rewrite (In_path_in_path _ _ _ _ _ H5); destruct (in_path (path p (cl_dcl d)) d0); auto. import (in_path_sty' _ _ _ H H0 H4); bd H5. apply (In_path_in_path _ _ _ _ _ H5). import (sty_cl_object _ _ H4); discriminate. import (sty_cl_object _ _ H4); discriminate. import (in_path_sty' _ _ _ H H0 H4); bd H5. apply (In_path_in_path _ _ _ _ _ H5). Qed. Lemma sat_constr_wf : forall (g : G) (stmt_list : list_s) (p : P) (c_list : list ty_constraint), gen_stmt_list_constr g stmt_list = Some c_list -> sat_constr_list p c_list = true -> acyclic_hierarchy p -> distinct _ (names p) -> wf_stmt_list' p g stmt_list. intros g stmt_list p. elim stmt_list using s_list_ind with (P := fun s => forall c_list', acyclic_hierarchy p -> distinct _ (names p) -> gen_stmt_constr g s = Some c_list' ->sat_constr_list p c_list' = true -> wf_stmt p g s); intros. inversion H1; subst. caseEq (XMap.find (x_var var) g); intros; rewrite H3 in H4. inversion H4; rewrite <- H6 in H2. unfold sat_constr_list in H2. destruct (andb_prop _ _ H2). import (proj1 (sat_cl_constr _ _ _ H H0) H5). apply wf_new; congruence. discriminate. apply wf_var_assign. simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find (x_var var) g); intros; rewrite H4 in H1; try discriminate. inversion H1; rewrite <- H6 in H2; unfold sat_constr_list in H2. destruct (andb_prop _ _ H2). apply (proj1 (sat_cl_constr _ _ _ H H0) H5). simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find (x_var var) g); intros; rewrite H4 in H1; try discriminate. destruct t; inversion H1; rewrite <- H6 in H2. unfold sat_constr_list in H2; destruct (andb_prop _ _ H2). destruct c. import (sat_fieldr_constr _ _ _ _ H H0 H5); bd H8. rewrite <- H4 in H8; apply (wf_field_read _ _ _ _ _ _ _ H3 H11 H8). inversion H5. destruct t0; destruct c; unfold ftype in H9; try discriminate. rewrite path_cl_object in H9; simpl in H9; discriminate. rewrite path_cl_object in H9; simpl in H9; discriminate. destruct t; discriminate. simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find y g); intros; rewrite H4 in H1; try discriminate. destruct t; inversion H1; rewrite <- H6 in H2. unfold sat_constr_list in H2; destruct (andb_prop _ _ H2). destruct c. import (sat_fieldw_constr _ _ _ _ H H0 H5); bd H8. rewrite <- H4 in H8; apply (wf_field_write _ _ _ _ _ _ _ H3 H11 H8). inversion H5. destruct t0; destruct c; unfold ftype in H9; try discriminate; rewrite path_cl_object in H9; simpl in H9; discriminate. destruct t; discriminate. simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find (x_var var) g); intros; rewrite H4 in H1; try discriminate. destruct t. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H5 in H1. inversion H1; rewrite <- H7 in H2. unfold sat_constr_list in H2; destruct (andb_prop _ _ H2). destruct c; destruct t0. import (sat_meth_constr _ _ _ _ _ H H0 H6). bd H9. assert (length l = length l0). generalize l0 H5; clear; induction l; intros; destruct l0; simpl in *|-*; auto; try discriminate. destruct (XMap.find a g). caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H in *; discriminate. discriminate. rewrite (IHl l0). reflexivity. caseEq (XMap.find a g); intros; rewrite H in H5; try discriminate. caseEq (fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H0 in *. inversion H5; subst; auto. discriminate. assert (map (fun y : lj_definitions.x * ty => fst y) (combine l x1) = l). generalize l0 x1 H10 H14 ; clear; induction l; intros. auto. destruct l0; destruct x1; try discriminate. simpl. simpl in H10, H14. rewrite (IHl l0 x1); congruence. rewrite <- H11. apply (wf_mcall (combine l x1) p g var x m (cl_dcl d) x0 H3). assert (map (fun y : lj_definitions.x * ty => snd y) (combine l x1) = x1). rewrite H14 in H10; generalize x1 H10; clear; induction l; intros. destruct x1; simpl in *|-*; try discriminate. reflexivity. destruct x1; simpl in *|-*; try discriminate. rewrite IHl; congruence. rewrite H15; rewrite H12; reflexivity. generalize l0 x1 H10 H14 H5 H9; clear; induction l; intros; destruct l0; destruct x1; simpl in *|-*; try discriminate; auto. destruct (XMap.find a g). inversion H9; apply Cons_sty_opt_list; simpl in H5; auto. caseEq (fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H6 in H5; inversion H5; congruence. apply (IHl l0 x1); auto. caseEq (fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H6 in H5; inversion H5; congruence. discriminate. rewrite H4; auto. simpl in H6. inversion H6. inversion H6. unfold mtype in H10; unfold get_md in H10. rewrite path_cl_object in H10; simpl in H10; discriminate. discriminate. destruct t; discriminate. simpl in H3. caseEq (XMap.find x g); caseEq (XMap.find y g); intros; rewrite H5 in H3; rewrite H6 in H3; try discriminate. caseEq (gen_stmt_constr g s1); caseEq (gen_stmt_constr g s2); intros; rewrite H7 in H3; rewrite H8 in H3; try discriminate. inversion H3; rewrite <- H10 in H4; unfold sat_constr_list in H4. destruct (andb_prop _ _ H4); clear H4. import ((proj1 (sat_if_constr _ _ _ H1 H2)) H9); apply (wf_if p g x y s1 s2). congruence. apply (H l0); auto. fold sat_constr_list in H11. destruct (sat_constr_list_app _ _ _ H11); auto. apply (H0 l); auto. fold sat_constr_list in H11. destruct (sat_constr_list_app _ _ _ H11); auto. apply wf_block. applyI wf_stmt_list'_iff. apply (H c_list'); auto. apply Nil_wf_stmt_list'. apply Cons_wf_stmt_list'. caseEq (gen_stmt_constr g s); intros; simpl in H1; rewrite H5 in H1. destruct (gen_stmt_list_constr g l). inversion H1; rewrite <- H7 in H2. destruct (sat_constr_list_app _ _ _ H2). apply (H _ H3 H4 H5); auto. discriminate. discriminate. caseEq (gen_stmt_constr g s); intros; simpl in H1; rewrite H5 in H1. destruct (gen_stmt_list_constr g l). inversion H1; rewrite <- H7 in H2. destruct (sat_constr_list_app _ _ _ H2). apply (H0 _ (refl_equal _) H8 H3 H4); auto. discriminate. discriminate. Qed. Lemma fold_right_length : forall (g : G) (y_ty_list : list (x * ty)) (l0 : list ty), fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : x * ty => fst y) y_ty_list) = Some l0 -> length l0 = length y_ty_list. intros. generalize l0 H; clear; induction y_ty_list; intros l0 H5. destruct l0; simpl in *. congruence. discriminate. destruct l0; simpl in *. destruct a; destruct (XMap.find (fst (x, t)) g). caseEq(fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros; rewrite H in H5; discriminate. discriminate. rewrite IHy_ty_list; auto. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros; rewrite H in H5; try discriminate. destruct (XMap.find (fst a) g); inversion H5. auto. destruct (XMap.find (fst a) g); inversion H5. Qed. Lemma wf_sat_meth : forall (g : G) (p : P) (var : var) (x' : x) (m : m) (l : list x) (c_list' : list ty_constraint), acyclic_hierarchy p -> distinct cl (names p) -> gen_stmt_constr g (s_call var x' m l) = Some c_list' -> wf_stmt p g (s_call var x' m l) -> sat_constr_list p c_list' = true. intros. simpl in H1. caseEq (XMap.find x' g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find (x_var var) g); intros; rewrite H4 in H1; try discriminate. destruct t. caseEq (fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) l); intros; rewrite H5 in H1. inversion H1. inversion H2; subst. simpl. destruct t0; rewrite H3 in H13; inversion H13; subst; rewrite H14. destruct ty'; destruct c; destruct c0. case (eq_nat_dec (length l0) (length (map (fun y : x * ty => snd y) y_ty_list))); intros. rewrite H4 in H16; inversion H16; inversion H6; inversion H7; subst. import (parent_in_path_sty' _ _ _ H H0 H8); bd H9. rewrite (In_path_in_path _ _ _ _ _ H9); auto. repeat apply andb_true_intro; pa. repeat apply andb_true_intro; pa. generalize l0 y_ty_list H15 H5 H3 H1 H H0 e; clear; induction l0; intros. destruct y_ty_list; simpl; auto. destruct y_ty_list; simpl; auto. destruct a; destruct c; destruct p0; destruct t; destruct c; simpl. inversion H15; subst; apply andb_true_intro; pa. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. rewrite H2 in H6; inversion H6; inversion H7; inversion H8; subst. import (parent_in_path_sty' _ _ _ H H0 H10); bd H11. apply (In_path_in_path _ _ _ _ _ H11). rewrite H4 in H5; discriminate. rewrite H2 in H6; inversion H6; discriminate. apply IHl0; auto. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. auto. rewrite H4 in H5; discriminate. rewrite H2 in H6; inversion H6; discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. apply andb_true_intro; pa. import (in_path_sty' _ _ _ H H0 H14); bd H6. apply (In_path_in_path _ _ _ _ _ H6). apply IHl0; auto. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15; inversion H7; discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. import (sty_cl_object _ _ H14); discriminate. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15; inversion H7; discriminate. apply IHl0; auto. inversion H15; auto. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros; rewrite H4 in H5; inversion H5; auto. simpl in H5; rewrite H2 in H5; simpl in H5; discriminate. rewrite (fold_right_length _ _ _ H5) in n. elimtype False; apply n; clear; induction y_ty_list; simpl; try congruence. case (eq_nat_dec (length l0) (length (map (fun y : lj_definitions.x * ty => snd y) y_ty_list))); intros. apply andb_true_intro; pa. apply andb_true_intro; pa. inversion H16; inversion H6; inversion H7; subst. destruct ty'; import (in_path_sty' _ _ _ H H0 H8); bd H9. rewrite (In_path_in_path _ _ _ _ _ H9); auto. generalize l0 y_ty_list H15 H5 H3 H1 H H0 e; clear; induction l0; intros. destruct y_ty_list; simpl; auto. destruct y_ty_list; simpl; auto. destruct a; destruct c; destruct p0; destruct t; destruct c; simpl. inversion H15; subst; apply andb_true_intro; pa. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. rewrite H2 in H6; inversion H6; inversion H7; inversion H8; subst. import (parent_in_path_sty' _ _ _ H H0 H10); bd H11. apply (In_path_in_path _ _ _ _ _ H11). rewrite H4 in H5; discriminate. rewrite H2 in H6; inversion H6; discriminate. apply IHl0; auto. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. auto. rewrite H4 in H5; discriminate. rewrite H2 in H6; inversion H6; discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. apply andb_true_intro; pa. import (in_path_sty' _ _ _ H H0 H14); bd H6. apply (In_path_in_path _ _ _ _ _ H6). apply IHl0; auto. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15; inversion H7; discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. import (sty_cl_object _ _ H14); discriminate. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15; inversion H7; discriminate. apply IHl0; auto. inversion H15; auto. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros; rewrite H4 in H5; inversion H5; auto. simpl in H5; rewrite H2 in H5; simpl in H5; discriminate. rewrite (fold_right_length _ _ _ H5) in n. elimtype False; apply n; clear; induction y_ty_list; simpl; try congruence. rewrite H4 in H16; inversion H16; inversion H6; inversion H7; subst. import (sty_cl_object _ _ H8); discriminate. case (eq_nat_dec (length l0) (length (map (fun y : lj_definitions.x * ty => snd y) y_ty_list))); intros. rewrite H4 in H16; inversion H16; inversion H6; inversion H7; subst. generalize l0 y_ty_list H15 H5 H3 H1 H H0 e; clear; induction l0; intros. destruct y_ty_list; simpl; auto. destruct y_ty_list; simpl; auto. destruct a; destruct c; destruct p0; destruct t; destruct c; simpl. inversion H15; subst; apply andb_true_intro; pa. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. rewrite H2 in H6; inversion H6; inversion H7; inversion H8; subst. import (parent_in_path_sty' _ _ _ H H0 H10); bd H11. apply andb_true_intro; pa. apply (In_path_in_path _ _ _ _ _ H11). import (IHl0 y_ty_list). rewrite andb_true_r in H12. apply H12; auto. rewrite H4 in H5; discriminate. rewrite H2 in H6; inversion H6. discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. auto. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. apply andb_true_intro; pa. apply andb_true_intro; pa. import (in_path_sty' _ _ _ H H0 H14). bd H6; apply (In_path_in_path _ _ _ _ _ H6). import (IHl0 y_ty_list). rewrite andb_true_r in H6. apply H6; auto. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15. inversion H7; discriminate. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. auto. inversion H15; rewrite H2 in H8; inversion H8; inversion H12; inversion H13; subst. import (sty_cl_object _ _ H14); discriminate. rewrite H4 in H5; discriminate. simpl in H15; rewrite H2 in H15; inversion H15; inversion H7; discriminate. apply IHl0; auto. inversion H15; auto. caseEq (XMap.find x g); intros. simpl in H5; rewrite H2 in H5; simpl in H5. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros. rewrite H4 in H5. inversion H5; subst. auto. rewrite H4 in H5; discriminate. inversion H15. rewrite H2 in H7; inversion H7; discriminate. rewrite (fold_right_length _ _ _ H5) in n. elimtype False; apply n; clear; induction y_ty_list; simpl; congruence. discriminate. destruct t; discriminate. Qed. Lemma wf_sat_constr : forall (g : G) (stmt_list : list_s) (p : P) (c_list : list ty_constraint), gen_stmt_list_constr g stmt_list = Some c_list -> wf_stmt_list' p g stmt_list -> acyclic_hierarchy p -> distinct _ (names p) -> sat_constr_list p c_list = true. intros g stmt_list p. elim stmt_list using s_list_ind with (P := fun s => forall c_list', acyclic_hierarchy p -> distinct _ (names p) -> gen_stmt_constr g s = Some c_list' -> wf_stmt p g s -> sat_constr_list p c_list' = true); intros. simpl in H1. caseEq (XMap.find (x_var var) g); intros; rewrite H3 in H1; try discriminate. inversion H1; simpl. inversion H2; subst. destruct t; destruct c. rewrite H3 in H8; rewrite (in_path_sty_option'); auto. destruct cl; auto. destruct cl; auto. rewrite H3 in H8; inversion H8; inversion H4; inversion H5; subst. import (in_path_sty' _ _ _ H H0 H6); bd H7. rewrite (In_path_in_path _ _ _ _ _ H7). auto. simpl in H1. caseEq (XMap.find (x_var var) g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find x g); intros; rewrite H4 in H1; try discriminate. inversion H1; unfold sat_constr_list. inversion H2; subst. rewrite H4 in H9; rewrite H3 in H9. rewrite (proj2 (sat_cl_constr _ _ _ H H0) H9); auto. simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find (x_var var) g); intros; rewrite H4 in H1; try discriminate. destruct t; inversion H1; simpl. inversion H2; rewrite H11 in H3; inversion H3; subst. destruct t0. destruct c0; auto. rewrite H12. destruct ty5. rewrite H4 in H13; inversion H13; inversion H5; inversion H6; subst. destruct c0. import (parent_in_path_sty' _ _ _ H H0 H7); bd H8. rewrite (In_path_in_path _ _ _ _ _ H8); auto. import (sty_cl_object _ _ H7); discriminate. rewrite H4 in H13; inversion H13; inversion H5; inversion H6; subst. rewrite H12; destruct ty0; destruct c0; auto. import (in_path_sty' _ _ _ H H0 H7); bd H8. rewrite (In_path_in_path _ _ _ _ _ H8); auto. destruct t; discriminate. simpl in H1. caseEq (XMap.find x g); intros; rewrite H3 in H1; try discriminate; caseEq (XMap.find y g); intros; rewrite H4 in H1; try discriminate. destruct t; inversion H1; simpl. inversion H2; rewrite H11 in H3; inversion H3; subst. destruct t0. destruct c0; auto. rewrite H12. destruct ty5. rewrite H4 in H13; inversion H13; inversion H5; inversion H6; subst. destruct c0. import (parent_in_path_sty' _ _ _ H H0 H7); bd H8. rewrite (In_path_in_path _ _ _ _ _ H8); auto. import (in_path_sty' _ _ _ H H0 H7); bd H8. rewrite (In_path_in_path _ _ _ _ _ H8); auto. rewrite H4 in H13; inversion H13; inversion H5; inversion H6; subst. rewrite H12; destruct ty'; destruct c0; auto. import (sty_cl_object _ _ H7); discriminate. destruct t; discriminate. apply (wf_sat_meth _ _ _ _ _ _ _ H H0 H1 H2). simpl in H3. caseEq (XMap.find x g); intros; rewrite H5 in H3; try discriminate; caseEq (XMap.find y g); intros; rewrite H6 in H3; try discriminate. caseEq (gen_stmt_constr g s1); intros; rewrite H7 in H3; try discriminate; caseEq (gen_stmt_constr g s2); intros; rewrite H8 in H3; try discriminate. inversion H3. inversion H4; subst. unfold sat_constr_list; fold (sat_constr_list p (l ++ l0)). apply andb_true_intro; pa. applyI (sat_if_constr _ t t0 H1 H2); congruence. apply sat_constr_list_app'; pa. apply (H _ H1 H2 H7 H17). apply (H0 _ H1 H2 H8 H18). apply H; auto. inversion H3. applyI wf_stmt_list'_iff. simpl in H; inversion H; simpl; reflexivity. simpl in H1. caseEq (gen_stmt_constr g s); intros; rewrite H5 in H1. caseEq (gen_stmt_list_constr g l); intros; rewrite H6 in H1. inversion H1. apply sat_constr_list_app'; pa. apply H; auto. inversion H2; auto. apply H0; auto. inversion H2; auto. discriminate. discriminate. Qed. Lemma spurious_map_vd_constr : forall (ty_var_list : list (ty*var)), map (fun vd' : vd => match vd' with | vd_def (ty_def cl') var' => in_prog_constr cl' end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list) = map (fun ty_var : ty * var => match (fst ty_var) with ty_def cl' => in_prog_constr cl' end) ty_var_list. clear; induction ty_var_list; simpl; congruence. Qed. Lemma spurious_map_vd_reverse : forall (ty_var_list : list (ty*var)), map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list) = map (fun ty_var : ty * var => (x_var (snd ty_var), fst ty_var)) ty_var_list. clear; induction ty_var_list; simpl; congruence. Qed. Lemma sat_constr_inherited_meth_cons : forall (p : P) (mds' : list md) (md' : md) (cl' : cl), sat_constr p (inherited_methods_constr (md' :: mds') cl') = true -> sat_constr p (inherited_methods_constr mds' cl') = true. intros p mds' md' cl'; destruct md'; destruct m; caseEq (not_in_list m (methods p cl')); intro. simpl; rewrite H; simpl. auto. simpl; rewrite H; simpl. destruct (mtype p cl' m); intros H0; try discriminate. import (andb_prop _ _ H0); bd H1. Qed. Lemma eq_ty_eq : forall (ty1 ty2 : ty), eq_ty ty1 ty2 = true <-> ty1 = ty2. destruct ty1; destruct ty2; destruct c; destruct c0; simpl; try tauto. case (eq_nat_dec d d0); intros. rewrite e; tauto. pa; intros; congruence. pa; intros; congruence. pa; intros; congruence. Qed. Lemma neq_length_neq : forall (A : Type) (l1 l2 : list A), length l1 <> length l2 -> l1 <> l2. induction l1; intros. destruct l2; congruence. destruct l2; try congruence. Qed. Lemma eq_mty_eq : forall (mty1 mty2: mty), mty_eq mty1 mty2 = true <-> mty1 = mty2. destruct mty1 as [l t]; destruct mty2 as [l0 t0]; simpl. caseEq (eq_ty t t0); case (eq_nat_dec (length l) (length l0)). intros. rewrite ((proj1 (eq_ty_eq _ _)) H). generalize l0 e; clear; induction l. simpl; destruct l0; intros; try discriminate. tauto. destruct l0; intros; try discriminate. simpl. pa; intros. import (andb_prop _ _ H); bd H0. rewrite ((proj1 (eq_ty_eq _ _)) H3) in *|-*. simpl in e; inversion e. import ((proj1(IHl _ H2)) H0). inversion H1; congruence. apply andb_true_intro; pa. inversion H. applyI eq_ty_eq. inversion H. simpl in e; inversion e; subst; exact ((proj2(IHl _ H3)) (refl_equal _)). intros. import (neq_length_neq _ _ _ n); rewrite ((proj1 (eq_ty_eq _ _)) H). pa; intros; congruence. pa; intros. discriminate. inversion H0; subst; rewrite ((proj2 (eq_ty_eq t0 t0)) (refl_equal _)) in H; discriminate. intros. import (neq_length_neq _ _ _ n); pa; intros; congruence. Qed. Lemma wf_meth_sat_constr : forall (md' : md) (ty' : ty) (p : P) (c_list : list ty_constraint), acyclic_hierarchy p -> distinct _ (names p) -> gen_meth_constr ty' md' = Some c_list -> (wf_meth p ty' md' <-> sat_constr_list p c_list = true). intros. destruct md'; simpl in H1. destruct m; destruct m0. caseEq (distinct_list (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) l)); intros; rewrite H2 in H1. caseEq (gen_stmt_list_constr (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.add x_this ty' (XMap.empty ty))) (make_list_s l0)); intros; rewrite H3 in H1. caseEq (XMap.find x (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.add x_this ty' (XMap.empty ty)))); intros; rewrite H4 in H1. inversion H1. pa; intros. inversion H5. simpl; apply andb_true_intro; pa; subst. import (spurious_map_vd_reverse ty_var_list). destruct t0; destruct t; destruct c; destruct c0; subst; try rewrite H6 in H4; simpl in H18; try rewrite H4 in H18; clear H6 H1; inversion H18; inversion H1; inversion H6; subst. import (parent_in_path_sty' _ _ _ H H0 H7); bd H8. apply (In_path_in_path _ _ _ _ _ H8). import (in_path_sty' _ _ _ H H0 H7); bd H8; apply (In_path_in_path _ _ _ _ _ H8). import (sty_cl_object _ _ H7); discriminate. reflexivity. import (spurious_map_vd_constr ty_var_list). rewrite H6 in *|-*; clear H6 H1. rewrite sat_constr_list_app'; auto; pa; subst. generalize H14 H H0; clear; induction ty_var_list; intros H1 H H0. reflexivity. simpl. apply andb_true_intro; pa. inversion H1; subst. destruct (fst a); inversion H4; subst. simpl; destruct c. import (In_names_In_p _ _ H5); bd H2. apply (In_path_in_path _ _ _ _ _ H2). auto. inversion H1; apply IHty_var_list; auto. assert (wf_stmt_list' p (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list)) (XMap.add x_this (ty_def cl5) (XMap.empty ty))) (make_list_s (unmake_list_s s_list))). assert (make_list_s (unmake_list_s s_list) = s_list). clear; induction s_list; simpl; intros; auto. rewrite IHs_list; reflexivity. rewrite H1; generalize (proj1 (wf_stmt_list'_iff _ _ _ ) H17); clear; induction s_list; simpl; intros. apply Nil_wf_stmt_list'. inversion H; subst. apply Cons_wf_stmt_list'; rewrite spurious_map_vd_reverse; congruence. apply (wf_sat_constr _ _ _ _ H3 H1 H H0). unfold sat_constr_list in H5; fold sat_constr_list in H5. import (andb_prop _ _ H5); bd H7. import (sat_constr_list_app _ _ _ H7); bd H8. assert (wf_type_list (map (fun vd' : vd => match vd' with | vd_def ty' _ => (p, ty') end) l)). generalize H12; clear; induction l; simpl; intros. apply Nil_wf_type_list. destruct a; simpl; import (andb_prop _ _ H12); bd H; apply Cons_wf_type_list. destruct t; simpl in H2; destruct c; apply (wf_valid_dcl). import (in_path_In_path _ _ H2); bd H0. apply (In_p_In_names _ _ _ _ _ H0). clear; induction p; simpl; auto. destruct a; simpl; po2. apply IHl; auto. import (sat_constr_wf _ _ _ _ H3 H8 H H0). import ((proj1 (sat_cl_constr _ _ _ H H0)) H10). rewrite <- H4 in H13. import ((proj1 (distinct_distinct_list _ )) H2). assert (exists ty_list, exists var_list, l = (map (fun (tv: ty*var) => vd_def (fst tv) (snd tv) )) (combine ty_list var_list)). clear; induction l. exists (nil : list ty); exists (nil : list var); simpl; auto. bd IHl; destruct a. exists (t :: x); exists (v :: x0); rewrite IHl; auto. bd H15. rewrite H15. assert (unmake_list_s (make_list_s l0) = l0). clear; induction l0; simpl; intros; congruence. rewrite <- H16. destruct ty'. apply (wf_method (make_list_s l0) (combine x0 x1) p c t m x (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) (map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.add x_this (ty_def c) (XMap.empty ty)))); auto. rewrite H15 in H9. assert (map (fun vd' : vd => match vd' with | vd_def ty' _ => (p, ty') end) (map (fun tv : ty * var => vd_def (fst tv) (snd tv)) (combine x0 x1)) = (map (fun ty_var : ty * var => (p, fst ty_var)) (combine x0 x1))). generalize x1; clear; induction x0; intros; destruct x1; simpl; auto. rewrite IHx0; reflexivity. rewrite H17 in H9; exact H9. rewrite H15 in H14; generalize x1 H14; clear; induction x0; destruct x1; simpl; intros; auto. bd H14; pa. unfold not; intros; apply H1; generalize x1 H; clear; induction x0; destruct x1; simpl; intros; auto. bd H. inversion H; po1. po2; apply IHx0; auto. apply IHx0; auto. simpl. rewrite H15; rewrite spurious_map_vd_reverse; auto. applyI wf_stmt_list'_iff. discriminate. discriminate. discriminate. Qed. Lemma wf_class_sat_constr : forall (cld' : cld) (p : P) (c_list : list ty_constraint), acyclic_hierarchy p -> distinct _ (names p) -> gen_class_constr cld' = Some c_list -> (wf_class p cld' <-> sat_constr_list p c_list = true). intros; destruct cld'. unfold gen_class_constr in H1. destruct c. (*** c = cl_dcl d0 ***) generalize H1; clear H1; case (eq_nat_dec d d0); intros. discriminate. caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)); intros; rewrite H2 in H1. caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)); intros; rewrite H3 in H1; simpl in H1. 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 d)) 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) l0); intros; rewrite H4 in H1; inversion H1; generalize H4; intros G1; clear H1 H4 H6. pa; intros. (*** First conjunct**) simpl; apply andb_true_intro; pa. inversion H1; subst. inversion H8; subst. import (In_names_In_p _ _ H6); bd H4. apply (In_path_in_path _ _ _ _ _ H4). apply andb_true_intro; pa. inversion H1; subst. generalize H12; clear; intros. assert ((map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list)) = (map (fun tyf : ty * f => snd tyf) ty_f_list)). clear; induction ty_f_list; simpl; congruence. rewrite H; rewrite H12; auto. inversion H1; subst; apply andb_true_intro; pa. generalize H17; clear; induction l0; intros. simpl; reflexivity. simpl; destruct a; destruct m. caseEq (not_in_list m (methods p (cl_dcl d0))); intros; simpl; auto. apply IHl0; intros; auto. apply (H17 m' ty' vd_list mb'); auto. simpl; po2. rewrite <- (H17 m t l m0). import ((proj1 (not_in_list_In_list _ _)) H). destruct (mtype p (cl_dcl d0) m). apply andb_true_intro; pa. fold (get_vdstys l). applyI (eq_mty_eq (mty_def (get_vdstys l) t) (mty_def (get_vdstys l) t) ). apply IHl0; intros; auto. rewrite <- (H17 m' ty' vd_list mb'); auto. simpl; po2. apply andb_true_intro; pa. fold (get_vdstys l). applyI (eq_mty_eq (mty_def (get_vdstys l) t) (mty_def (get_vdstys l) t) ). apply IHl0; intros; auto. apply (H17 m' ty' vd_list mb'); simpl. po2. exact H2. simpl; po1. applyI (not_in_list_In_list). apply (sat_constr_list_app'); pa. generalize H14; clear; induction ty_f_list. simpl; auto. simpl; intros. apply andb_true_intro; pa. inversion H14; subst. destruct a; destruct t; simpl. inversion H1; destruct c. import (In_names_In_p _ _ H2). bd H4; apply (In_path_in_path _ _ _ _ _ H4). reflexivity. inversion H14; subst; apply IHty_f_list; auto. generalize l1 G1 H15 H H0; clear; induction l0; intros. simpl in G1; inversion G1; auto. simpl in G1. 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 d)) 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) l0); intros; rewrite H1 in G1. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H2 in G1. inversion G1. apply sat_constr_list_app'. pa. inversion H15; subst. applyI (wf_meth_sat_constr _ _ _ _ H H0 H2). apply IHl0; auto. inversion H15; auto. discriminate. discriminate. (*** Second Conjunct***) unfold sat_constr_list in H1; fold sat_constr_list in H1; import (andb_prop _ _ H1); bd H4; import (andb_prop _ _ H4); bd H5; import (andb_prop _ _ H5); bd H6; import (sat_constr_list_app _ _ _ H6); bd H8; clear H1 H4 H5 H6. apply (wf_cl (map (fun (fd' : fd) => match fd' with fd_def ty' f' => (ty',f') end) l)). simpl in H7. import (in_path_In_path _ _ H7); bd H1; apply wf_valid_dcl; apply (In_p_In_names _ _ _ _ _ H1). congruence. clear; induction l; simpl; auto; destruct a; simpl; congruence. generalize ((proj1 (distinct_distinct_list _)) H2); clear; simpl; induction l; simpl; auto; intros. bd H; pa. unfold not; intros; apply H2; generalize H0; clear; induction l; simpl; intros; auto. bd H0. destruct a0; destruct a; po1. po2; apply (IHl H0). apply (IHl H). generalize H9; clear; simpl; intros. assert (map (fun tyf : ty * f => snd tyf) (map (fun fd' : fd => match fd' with | fd_def ty' f' => (ty', f') end) l) = map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l). clear; induction l; simpl; auto; destruct a; simpl; congruence. rewrite H; caseEq ( list_inter f (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l) (fields p (cl_dcl d0)) in_nat_list); intros; rewrite H0 in H9. reflexivity. discriminate. generalize H13; clear; induction l; simpl; intros. apply Nil_wf_type_list. import (andb_prop _ _ H13); bd H; clear H13. apply Cons_wf_type_list. destruct a; simpl; destruct t; apply wf_valid_dcl. destruct c; simpl in H2. import (in_path_In_path _ _ H2); bd H0; apply (In_p_In_names _ _ _ _ _ H0). clear; induction p; simpl; auto. destruct a; simpl; po2. apply (IHl H). generalize l1 H H0 G1 H8; clear; induction l0; intros. simpl. apply Nil_wf_meth_list. simpl in G1. 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 d)) 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) l0); intros; rewrite H1 in G1; try discriminate. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H2 in G1; try discriminate. inversion G1; clear G1; rewrite <- H4 in H8. import (sat_constr_list_app _ _ _ H8); bd H3. simpl; apply Cons_wf_meth_list. applyI (wf_meth_sat_constr _ _ _ _ H H0 H2). apply (IHl0 l); auto. generalize H3; clear; induction l0; simpl; intros; auto. import (andb_prop _ _ H3); clear H3; bd H; pa. unfold not; intro; destruct a; destruct m. import ((proj2 (not_in_list_In_list _ _ )) H0). rewrite H1 in H2; discriminate. apply IHl0; auto. generalize H11; clear; induction l0; intros. simpl in H; contradiction. simpl in H; bd H. destruct a; inversion H; subst. simpl in H11. caseEq (not_in_list m' (methods p (cl_dcl d0))); intros; rewrite H1 in H11; simpl in H11. rewrite ((proj2 (not_in_list_In_list _ _ )) H0) in H1; discriminate. caseEq (mtype p (cl_dcl d0) m'); intros; rewrite H2 in H11. import (andb_prop _ _ H11); bd H3. destruct m. generalize l H6; clear; induction vd_list; simpl; unfold eq_ty at 1; destruct t; destruct ty'; destruct c; destruct c0; try tauto; try case (eq_nat_dec d d0). intros e l; case (eq_nat_dec (length l) 0); destruct l; intros; try discriminate; rewrite e; reflexivity. intros; try discriminate. intros; try discriminate. intros; try discriminate. intro l; case (eq_nat_dec (length l) 0); destruct l; intros; try discriminate; reflexivity. intros e l; (case (eq_nat_dec (length l) (S (length (map (fun vd' : vd => match vd' with | vd_def ty'' _ => ty'' end) vd_list))))); intros; try discriminate. destruct l; simpl in e0; try discriminate. destruct a; simpl; simpl in H6. import (andb_prop _ _ H6); bd H. destruct t; destruct t0; destruct c; destruct c0; try discriminate. generalize H2; simpl; case (eq_nat_dec d1 d2); intros; subst. simpl in *|-*; import (IHvd_list l); inversion e0; rewrite <- H4 in H1; rewrite H in H1; clear H4 IHvd_list e0. generalize H1; clear H1; case (eq_nat_dec d0 d0); case (eq_nat_dec (length l) (length l)); intros; try congruence. import (H1 (refl_equal _)); inversion H3; reflexivity. discriminate. simpl in *|-*; import (IHvd_list l); inversion e0. rewrite <- H3 in H0; rewrite H in H0; clear H3 IHvd_list e0. subst; generalize H0; clear H0; case (eq_nat_dec d0 d0); case (eq_nat_dec (length l) (length l)); intros; try congruence. import (H0 (refl_equal _)); inversion H1; reflexivity. intros; discriminate. intros; discriminate. intros; discriminate. intros t; (case (eq_nat_dec (length t) (S (length (map (fun vd' : vd => match vd' with | vd_def ty'' _ => ty'' end) vd_list))))); intros; try discriminate. destruct t; simpl in e; try discriminate. destruct a; simpl in *|-*. import (andb_prop _ _ H6); bd H. destruct t; destruct t1; destruct c; destruct c0; try discriminate. generalize H2; simpl; case (eq_nat_dec d0 d); intros; subst. import (IHvd_list t0); inversion e; rewrite <- H4 in H1; rewrite H in H1; clear H4 IHvd_list e. generalize H1; clear H1; case (eq_nat_dec d d); case (eq_nat_dec (length t0) (length t0)); intros; try congruence. import (H1 (refl_equal _)); inversion H3; reflexivity. generalize H0; case (eq_nat_dec d d0); intros; congruence. import (IHvd_list t0); inversion e; rewrite <- H3 in H0; rewrite H in H0; clear H3 IHvd_list e. generalize H0; clear H0; case (eq_nat_dec (length t0) (length t0)); intros; try congruence. import (H0 (refl_equal _)); inversion H1; reflexivity. discriminate. import (sat_constr_inherited_meth_cons _ _ _ _ H11). auto. apply (IHl0 H1 _ _ _ _ H H0). discriminate. simpl in H1; discriminate. (*** c = cl_object ***) caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)); intros; rewrite H2 in H1. caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)); intros; rewrite H3 in H1; simpl in H1. 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 d)) 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) l0); intros; rewrite H4 in H1; inversion H1; generalize H4; intros G1; clear H1 H4 H6. pa; intros. apply sat_constr_list_app'; pa. inversion H1; subst. generalize H14; clear; induction ty_f_list. simpl; auto. simpl; intros. apply andb_true_intro; pa. inversion H14; subst. destruct a; destruct t; simpl. inversion H1; destruct c. import (In_names_In_p _ _ H2). bd H4; apply (In_path_in_path _ _ _ _ _ H4). reflexivity. inversion H14; subst; apply IHty_f_list; auto. inversion H1; generalize l1 G1 H15 H H0; clear; induction l0; intros. simpl in G1; inversion G1; auto. simpl in G1. 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 d)) 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) l0); intros; rewrite H1 in G1. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H2 in G1. inversion G1. apply sat_constr_list_app'. pa. inversion H15; subst. applyI (wf_meth_sat_constr _ _ _ _ H H0 H2). apply IHl0; auto. inversion H15; auto. discriminate. discriminate. unfold sat_constr_list in H1; fold sat_constr_list in H1; import (sat_constr_list_app _ _ _ H1); bd H4; clear H1. apply (wf_cl (map (fun (fd' : fd) => match fd' with fd_def ty' f' => (ty',f') end) l)). apply wf_valid_dcl; clear; induction p; simpl; auto; try (destruct a; po2). congruence. assert (map (fun tyf : ty * f => snd tyf) (map (fun fd' : fd => match fd' with | fd_def ty' f' => (ty', f') end) l) = map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l). clear; induction l; simpl; auto; destruct a; simpl; congruence. clear; induction l; simpl; auto; destruct a; simpl; congruence. assert (map (fun tyf : ty * f => snd tyf) (map (fun fd' : fd => match fd' with | fd_def ty' f' => (ty', f') end) l) = map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l). clear; induction l; simpl; auto; destruct a; simpl; congruence. rewrite H1; applyI distinct_distinct_list. unfold fields; unfold ext_fs; rewrite path_cl_object; simpl. clear; induction l; simpl; auto; destruct a; simpl; congruence. generalize H7; clear; induction l; simpl; intros. apply Nil_wf_type_list. import (andb_prop _ _ H7); bd H; clear H7. apply Cons_wf_type_list. destruct a; simpl; destruct t; apply wf_valid_dcl. destruct c; simpl in H2. import (in_path_In_path _ _ H2); bd H0; apply (In_p_In_names _ _ _ _ _ H0). clear; induction p; simpl; auto. destruct a; simpl; po2. apply (IHl H). generalize l1 H H0 G1 H4; clear; induction l0; intros. simpl. apply Nil_wf_meth_list. simpl in G1. 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 d)) 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) l0); intros; rewrite H1 in G1; try discriminate. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H2 in G1; try discriminate. inversion G1; clear G1; rewrite <- H5 in H4. import (sat_constr_list_app _ _ _ H4); bd H3. simpl; apply Cons_wf_meth_list. applyI (wf_meth_sat_constr _ _ _ _ H H0 H2). apply (IHl0 l); auto. generalize H3; clear; induction l0; simpl; intros; auto. import (andb_prop _ _ H3); clear H3; bd H; pa. unfold not; intro; destruct a; destruct m. import ((proj2 (not_in_list_In_list _ _ )) H0). rewrite H1 in H2; discriminate. apply IHl0; auto. intros. unfold methods in H5; unfold get_md in H5; rewrite path_cl_object in H5. simpl in H5; contradiction. discriminate. simpl in H1; discriminate. Qed. Lemma in_list_parent_ordered : forall (cld_list : list cld), acyclic_hierarchy cld_list <-> (fold_right (fun (cld' : cld) (b : bool* list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: (snd b))) (true, nil) cld_list) = (true, cld_list). induction cld_list; simpl; pa; intros. reflexivity. apply nil_p. inversion H; bd H3; destruct a; subst. rewrite snd_in_list_parent_map. rewrite ((proj1 (IHcld_list)) H2). rewrite (In_names_in_list_parent c (cld_def d c l l0) cld_list); simpl in *|-*; auto. rewrite snd_in_list_parent_map in H. apply cons_p. caseEq (fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) cld_list); intros; rewrite H0 in *. simpl in H; inversion H; subst; applyI IHcld_list. import (andb_prop _ _ H2); bd H1; rewrite H1. import (snd_in_list_parent_map cld_list); rewrite H0 in H3; simpl in H3; rewrite H3; reflexivity. exists (get_parent a); simpl; pa. apply (in_list_parent_In_names (get_parent a) a cld_list); auto; destruct a. simpl; inversion H; destruct (andb_prop _ _ H1); subst. rewrite H0; rewrite H2. destruct c; auto. Qed. Lemma in_list_parent_ordered' : forall (cld_list : list cld), acyclic_hierarchy cld_list <-> fst (fold_right (fun (cld' : cld) (b : bool* list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: (snd b))) (true, nil) cld_list) = true. pa; intros. rewrite ((proj1 (in_list_parent_ordered _)) H); simpl; reflexivity. applyI in_list_parent_ordered. import (snd_in_list_parent_map cld_list). caseEq (fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) cld_list); intros; rewrite H1 in H; rewrite H1 in H0. simpl in H, H0; congruence. Qed. Lemma sat_constr_wf_class_list : forall (cld_list : list cld) (p : P) (c_list : list ty_constraint), acyclic_hierarchy p -> distinct _ (names p) -> gen_cld_constr cld_list = Some c_list -> acyclic_hierarchy cld_list -> distinct _ (names cld_list) -> (wf_class_list (map (fun cld_ : cld => (p, cld_)) cld_list) <-> sat_constr_list p c_list = true). induction cld_list; pa; intros. simpl in H1; inversion H1; simpl; auto. apply Nil_wf_class_list. unfold gen_cld_constr in H1; simpl in H1. caseEq (fold_right (fun (cld' : cld) (m : option (list ty_constraint)) => match m with | Some c_list' => match gen_class_constr cld' 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) cld_list); intros; rewrite H5 in H1. caseEq (gen_class_constr a); intros; rewrite H6 in H1. inversion H1; subst. apply sat_constr_list_app'; pa. applyI (wf_class_sat_constr _ _ _ H H0 H6). destruct a; simpl in H4. inversion H4; exact H10. applyI (IHcld_list _ _ H H0 H5). inversion H2; auto. destruct a; simpl in H3; bd H3. inversion H4; exact H11. discriminate. discriminate. unfold gen_cld_constr in H1; simpl in H1. caseEq (fold_right (fun (cld' : cld) (m : option (list ty_constraint)) => match m with | Some c_list' => match gen_class_constr cld' 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) cld_list); intros; rewrite H5 in H1. caseEq (gen_class_constr a); intros; rewrite H6 in H1. inversion H1; subst. import (sat_constr_list_app _ _ _ H4); bd H7. apply (Cons_wf_class_list p a (map (fun cld_ : cld => (p, cld_)) cld_list)). applyI (wf_class_sat_constr _ _ _ H H0 H6). fold (gen_cld_constr cld_list) in H5. applyI (IHcld_list _ _ H H0 H5). inversion H2; auto. destruct a; simpl in H3; bd H3. assert (In a (a :: cld_list)). simpl; po1. import (list_ordered_parent _ _ H8 H2). bd H9; subst; exists (get_parent a); pa. import (distinct_acyclic_hierarchy _ _ H8 H2 H3). destruct a; simpl in H9; bd H9. simpl in H11; congruence. rewrite names'_eq_names. simpl; exact H9. discriminate. discriminate. Qed. Lemma sat_constr_wf_prog : forall (p : P) (c_list : list ty_constraint), gen_prog_constr p = Some c_list -> (wf_prog p <-> sat_constr_list p c_list = true). intros p c_list; unfold gen_prog_constr; caseEq (distinct_cl_list (names p)); caseEq (fst (fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) p)); intros. import ((proj1 (distinct_distinct_cl_list _)) H0); import ((proj2 (in_list_parent_ordered' _)) H); clear H0 H. pa; intros. inversion H; subst. applyI (sat_constr_wf_class_list _ _ _ H3 H2 H1 H3 H2). apply (wf_program p p (refl_equal _) H2). applyI (sat_constr_wf_class_list _ _ _ H3 H2 H1 H3 H2). discriminate. discriminate. discriminate. Qed. Lemma gen_stmt_constr_fail : forall (g : G) (stmt_list : list_s) (p : P), gen_stmt_list_constr g stmt_list = None -> ~ (wf_stmt_list' p g stmt_list). intros g stmt_list p. elim stmt_list using s_list_ind with (P := fun s => gen_stmt_constr g s = None -> ~ (wf_stmt p g s)); unfold not; intros. simpl in H; inversion H0; subst. caseEq (XMap.find (x_var var) g); intros; rewrite H1 in H, H4; try discriminate. inversion H4; discriminate. simpl in H; inversion H0; subst. caseEq (XMap.find (x_var var) g); caseEq (XMap.find x g); intros; rewrite H1 in H, H4. rewrite H2 in H, H4; try discriminate. inversion H4; discriminate. rewrite H2 in H, H4; try discriminate. inversion H4; discriminate. inversion H4; discriminate. simpl in H; inversion H0; subst. caseEq (XMap.find (x_var var) g); caseEq (XMap.find x g); intros; rewrite H2 in H, H8. rewrite H1 in H; try discriminate. destruct t; discriminate. congruence. inversion H8; discriminate. inversion H8; discriminate. simpl in H; inversion H0; subst. rewrite H6 in H. caseEq (XMap.find y g); intros; rewrite H1 in H, H8. discriminate. inversion H8; discriminate. simpl in H; inversion H0; subst. rewrite H7 in H. inversion H10; subst; rewrite H2 in H. caseEq (fold_right (fun (y : lj_definitions.x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : lj_definitions.x * ty => fst y) y_ty_list)); intros; rewrite H4 in H. discriminate. generalize H9 H4; clear; induction y_ty_list; intros. simpl in H4; discriminate. simpl in H4; caseEq (XMap.find (fst a) g ); intros; rewrite H in H4. caseEq (fold_right (fun (y : x) (m : option (list ty)) => match XMap.find y g with | Some ty' => match m with | Some m' => Some (ty' :: m') | None => None (A:=list ty) end | None => None (A:=list ty) end) (Some nil) (map (fun y : x * ty => fst y) y_ty_list)); intros; rewrite H0 in H4. discriminate. inversion H9; subst; apply IHy_ty_list; auto. inversion H9; subst; rewrite H in H2; inversion H2; discriminate. inversion H2; simpl in H1; subst. caseEq (XMap.find x g); caseEq (XMap.find y g); intros; rewrite H3 in *; rewrite H4 in *. caseEq (gen_stmt_constr g s1); caseEq (gen_stmt_constr g s2); intros; rewrite H5 in *; rewrite H6 in *; auto. discriminate. bd H8; inversion H8; discriminate. bd H8; inversion H8; discriminate. bd H8; inversion H8; discriminate. simpl in H0; inversion H1; subst; auto. apply H; auto. applyI wf_stmt_list'_iff. simpl in H; discriminate. inversion H2; subst; simpl in H1. caseEq (gen_stmt_constr g s); caseEq (gen_stmt_list_constr g l); intros; rewrite H3 in *; try rewrite H4 in *. discriminate. auto. auto. auto. Qed. Lemma gen_meth_constr_fail : forall (md' : md) (ty' : ty) (p : P), gen_meth_constr ty' md' = None -> ~ (wf_meth p ty' md'). unfold not; intros. unfold gen_meth_constr in H. destruct md'; destruct m. caseEq (distinct_list (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) l)); intros; rewrite H1 in H. destruct m0. caseEq (gen_stmt_list_constr (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) ((x_this, ty') :: map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.empty ty)) (make_list_s l0)); intros; rewrite H2 in H. caseEq (XMap.find x (fold_left (fun (m : XMap.t ty) (p : lj_definitions.x * ty) => XMap.add (fst p) (snd p) m) ((x_this, ty') :: map (fun vd' : vd => match vd' with | vd_def ty' var' => (x_var var', ty') end) l) (XMap.empty ty))); intros; rewrite H3 in H. discriminate. inversion H0; subst. rewrite spurious_map_vd_reverse in H3. rewrite H3 in H15; inversion H15; discriminate. inversion H0; subst. rewrite spurious_map_vd_reverse in H2. assert (make_list_s (unmake_list_s s_list) = s_list). clear; induction s_list; simpl; congruence. rewrite H3 in H2. apply (gen_stmt_constr_fail _ _ _ H2 ((proj1 (wf_stmt_list'_iff _ _ _ )) H13)). inversion H0. generalize ty_var_list H1 H9 H4; clear; induction l; simpl; intros. discriminate. destruct ty_var_list; simpl in H4; try discriminate. destruct a; inversion H4; subst. caseEq (not_in_list (snd p0) (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list))); intros; rewrite H in H1. caseEq (distinct_list (map (fun vd' : vd => match vd' with | vd_def _ var' => var' end) (map (fun ty_var : ty * var => vd_def (fst ty_var) (snd ty_var)) ty_var_list))); intros; rewrite H0 in H1. simpl in H1; discriminate. simpl in H9; bd H9. apply (IHl ty_var_list); auto. simpl in H9; bd H9. apply H3; import ((proj1 (not_in_list_In_list _ _ )) H). generalize H0; clear; induction ty_var_list; intros. simpl in H0; contradiction. simpl in H0; bd H0. rewrite <- H0; simpl; po1. simpl; po2; auto. Qed. Lemma gen_class_constr_fail : forall (cld' : cld) (p : P), gen_class_constr cld' = None -> ~ (wf_class p cld'). unfold not; destruct cld'; destruct c; unfold gen_class_constr; try case (eq_nat_dec d d0). intros; subst; inversion H0; congruence. caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)). caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)). 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 d)) 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) l0). intros; simpl; discriminate. intros; inversion H3; subst. generalize H H15; clear; induction l0; simpl; 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 d)) 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) l0); intros; rewrite H0 in H. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H1 in H. discriminate. inversion H15; subst; apply (gen_meth_constr_fail _ _ _ H1 H4). inversion H15; subst; auto. simpl; intros. inversion H2; subst. generalize H15 H; clear; intros. rewrite ((proj2 (distinct_distinct_list _)) H15) in H. discriminate. simpl; intros; inversion H1; subst. generalize H H9; clear; induction ty_f_list; simpl; intros. discriminate. bd H9. caseEq ( not_in_list (snd a) (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list))); caseEq ( distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list))); intros; rewrite H0 in H; rewrite H1 in H. discriminate. apply IHty_f_list; auto. apply H2; applyI (not_in_list_In_list). rewrite <- H1; clear; induction ty_f_list; simpl; congruence. apply IHty_f_list; auto. caseEq (distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) l)). caseEq (distinct_list (map (fun md' : md => match md' with | md_def (ms_def _ m' _) _ => m' end) l0)). 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 d)) 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) l0). intros; simpl; discriminate. intros; inversion H3; subst. generalize H H15; clear; induction l0; simpl; 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 d)) 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) l0); intros; rewrite H0 in H. caseEq (gen_meth_constr (ty_def (cl_dcl d)) a); intros; rewrite H1 in H. discriminate. inversion H15; subst; apply (gen_meth_constr_fail _ _ _ H1 H4). inversion H15; subst; auto. simpl; intros. inversion H2; subst. generalize H15 H; clear; intros. rewrite ((proj2 (distinct_distinct_list _)) H15) in H. discriminate. simpl; intros; inversion H1; subst. generalize H H9; clear; induction ty_f_list; simpl; intros. discriminate. bd H9. caseEq ( not_in_list (snd a) (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list))); caseEq ( distinct_list (map (fun fd' : fd => match fd' with | fd_def _ f' => f' end) (map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) ty_f_list))); intros; rewrite H0 in H; rewrite H1 in H. discriminate. apply IHty_f_list; auto. apply H2; applyI (not_in_list_In_list). rewrite <- H1; clear; induction ty_f_list; simpl; congruence. apply IHty_f_list; auto. Qed. Lemma gen_cld_list_constr_fail : forall (cld_list : list cld) (p : P), gen_cld_constr cld_list = None -> ~ (wf_class_list (map (fun cld_ : cld => (p, cld_)) cld_list)). unfold not; induction cld_list; simpl; intros. discriminate. caseEq (gen_cld_constr cld_list); intros; rewrite H1 in H. caseEq (gen_class_constr a); intros; rewrite H2 in H. discriminate. inversion H0; subst. apply (gen_class_constr_fail _ _ H2 H6). inversion H0; subst. apply (IHcld_list _ H1 H6). Qed. Lemma sat_constr_wf' : forall (g : G) (stmt_list : list_s) (p : P) , acyclic_hierarchy p -> distinct _ (names p) -> ((exists c_list, gen_stmt_list_constr g stmt_list = Some c_list/\ sat_constr_list p c_list = true) <-> wf_stmt_list' p g stmt_list). pa; intros. bd H1. apply (sat_constr_wf _ _ _ _ H4 H1 H H0). caseEq (gen_stmt_list_constr g stmt_list); intros. exists l; pa. apply (wf_sat_constr _ _ _ _ H2 H1 H H0). import (gen_stmt_constr_fail _ _ _ H2 H1); contradiction. Qed. Lemma wf_meth_sat_constr' : forall (md' : md) (ty' : ty) (p : P), acyclic_hierarchy p -> distinct _ (names p) ->((exists c_list, gen_meth_constr ty' md' = Some c_list /\ sat_constr_list p c_list = true) <-> (wf_meth p ty' md')). pa; intros. bd H1; applyI (wf_meth_sat_constr _ _ _ _ H H0 H4). caseEq (gen_meth_constr ty' md'); intros. exists l; pa. applyI (wf_meth_sat_constr _ _ _ _ H H0 H2). import (gen_meth_constr_fail _ _ _ H2 H1); contradiction. Qed. Lemma wf_class_sat_constr' : forall (cld' : cld) (p : P), acyclic_hierarchy p -> distinct _ (names p) -> ((exists c_list, gen_class_constr cld' = Some c_list /\ sat_constr_list p c_list = true) <-> wf_class p cld'). pa; intros. bd H1; applyI (wf_class_sat_constr cld' _ x H H0). caseEq (gen_class_constr cld'); intros. exists l; pa. applyI (wf_class_sat_constr _ _ _ H H0 H2). import (gen_class_constr_fail _ _ H2 H1); contradiction. Qed. Lemma sat_constr_wf_class_list' : forall (cld_list : list cld) (p : P), acyclic_hierarchy p -> distinct _ (names p) -> acyclic_hierarchy cld_list -> distinct _ (names cld_list) -> ((exists c_list, gen_cld_constr cld_list = Some c_list /\ sat_constr_list p c_list = true) <-> wf_class_list (map (fun cld_ : cld => (p, cld_)) cld_list)). pa; intros. bd H3; applyI (sat_constr_wf_class_list _ _ _ H H0 H6 H1 H2). caseEq (gen_cld_constr cld_list); intros. exists l; pa. applyI (sat_constr_wf_class_list _ _ _ H H0 H4 H1 H2). import (gen_cld_list_constr_fail _ _ H4 H3); contradiction. Qed. Definition type_check (p : P) : bool := match gen_prog_constr p with Some c_list => sat_constr_list p c_list | None => false end. Theorem wf_iff_type_check : forall (p : P), type_check p = true <-> wf_prog p. unfold type_check; intros. caseEq (gen_prog_constr p). pa; intros; applyI (sat_constr_wf_prog _ _ H). pa; intros. discriminate. inversion H0; subst. unfold gen_prog_constr in H. caseEq (distinct_cl_list (names cld_list)); intros; rewrite H1 in H. caseEq (fst(fold_right (fun (cld' : cld) (b : bool * list cld) => (in_list_parent cld' (snd b) && fst b, cld' :: snd b)) (true, nil) cld_list)); intros; rewrite H4 in H. import (gen_cld_list_constr_fail _ _ H H3); contradiction. import (ordered_wf_prog _ _ H3). rewrite ((proj1 (in_list_parent_ordered' _)) H5) in H4; discriminate. rewrite ((proj2 (distinct_distinct_cl_list _ )) H2) in H1; discriminate. Qed. Lemma spurious_map_fst : forall (l : list x) (ty_list : list ty), length l = length ty_list -> map (fun y : lj_definitions.x * ty => fst y) (combine l ty_list) = l. induction l; simpl; intros; auto. destruct ty_list; simpl in H. discriminate. simpl; rewrite IHl; auto. Qed. Lemma spurious_map_snd : forall (l : list x) (ty_list : list ty), length l = length ty_list -> map (fun y : lj_definitions.x * ty => snd y) (combine l ty_list) = ty_list. induction l; simpl; intros; auto. destruct ty_list; auto. simpl in H; discriminate. destruct ty_list; auto. simpl; rewrite IHl; auto. Qed. Lemma Not_sty_cl_object_dcl : forall (dcl' : dcl) (p : P), ~sty_option p (Some (ty_def cl_object)) (Some (ty_def (cl_dcl dcl'))). unfold not; intros dcl' p H; inversion H; subst; inversion H0; inversion H1; subst; generalize (sty_cl_object _ _ H2); intros; discriminate. Qed. Lemma sty_option_in_path_self : forall (p : P) (dcl' : dcl) (ty_opt : option ty), acyclic_hierarchy p -> distinct _ (names p) -> sty_option p (Some (ty_def (cl_dcl dcl'))) ty_opt -> in_path (path p (cl_dcl dcl')) dcl' = true. intros; inversion H1; subst; inversion H2; clear H2 H1 H. revert dcl' H5; induction H4; intros; subst. inversion H; subst; eapply In_path_in_path; apply In_prog_In_path; auto; apply H3. discriminate. inversion H5; subst. eapply In_path_in_path; apply In_prog_In_path; auto; apply H. auto. Qed. Lemma vd_list_decomp : forall (vd_list : list vd), exists ty_list, exists var_list, vd_list = (map (fun (tv: ty*var) => vd_def (fst tv) (snd tv) )) (combine ty_list var_list). induction vd_list; intros. exists nil; exists nil; auto. destruct IHvd_list as [ty_list' [var_list' H]]; destruct a as [ty' var']. exists (ty' :: ty_list'); exists (var' :: var_list'); simpl; congruence. Qed. Lemma unmake_make_s_list_idem : forall (s_list : list s), unmake_list_s (make_list_s s_list) = s_list. induction s_list; simpl; congruence. Qed. Lemma make_unmake_s_list_idem : forall (s_list : list_s), make_list_s (unmake_list_s s_list) = s_list. induction s_list; simpl; congruence. Qed. Lemma fds_map_idem : forall (fds : list fd), fds = map (fun tyf : ty * f => fd_def (fst tyf) (snd tyf)) (map (fun fd => match fd with fd_def ty' f' => (ty', f') end) fds). induction fds; simpl; auto; destruct a; simpl; congruence. Qed.