From 53e6b782b65f3b6777c3a21b2b061baab7e319e6 Mon Sep 17 00:00:00 2001 From: Garo Brik Date: Wed, 14 Sep 2016 14:22:22 -0400 Subject: [PATCH] Finished lemma 3 --- proof.v | 643 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 322 insertions(+), 321 deletions(-) diff --git a/proof.v b/proof.v index 4ea9625..cbfa4dd 100644 --- a/proof.v +++ b/proof.v @@ -1,211 +1,317 @@ (* Test *) -Require Import Lists.List. +Require Import Coq.Init.Datatypes. +Require Import Coq.Lists.List. Require Import Arith.EqNat. Require Import Maps. -Definition method := id. - -(* -Inductive lib : Type := . -Inductive app : Type := . - -Inductive class (T : Type) : Type := -| Obj : class lib -| Lib_Clazz : class lib -> list method -> class lib -| Ext_Lib : class lib -> list method -> class app -| Ext_App : class app -> list method -> class app. - -Inductive app_class : Type := -| Ext_Lib : lib_class -> list method -> app_class -| Ext_App : app_class -> list method -> app_class. - *) - -(** Definition of class objects which contain their parent class, - and class table which just says whether class is in app. - *) -Module Rec. - - Inductive class : Type := - | Obj : class - | C : class -> list method -> class. - - Inductive class_table : Type := - | CT : (class -> Prop) -> class_table. - - Definition in_app (ct : class_table) (c : class) : Prop := - match ct with - | CT f => f c - end. - -End Rec. - -Module ParId. - - Inductive class : Type := - | Obj : class - | C : id -> list method -> class. - - Definition class_table : Type := partial_map class * partial_map class. - - Definition extends_id (ct : class_table) (i : id) (d : class) : Prop := - match ct with (app, lib) => app i = Some d \/ lib i = Some d end. - - Definition extends (ct : class_table) (c d : class) : Prop := - match c with - | Obj => False - | C i _ => extends_id ct i d - end. - - - Definition in_lib_id (ct : class_table) (i : id) : Prop := - match ct with (_, lib) => lib i <> None end. - - Definition in_app_id (ct : class_table) (i : id) : Prop := - match ct with (app, _) => app i <> None end. - - Definition in_table_id (ct : class_table) (i : id) : Prop := - in_lib_id ct i \/ in_app_id ct i. - - Definition in_lib (ct : class_table) (c : class) : Prop := - match c with - | Obj => True - | C i _ => in_lib_id ct i - end. - Definition in_app (ct : class_table) (c : class) : Prop := - match c with - | Obj => False - | C i _ => in_app_id ct i - end. - Definition in_table (ct : class_table) (c : class) : Prop := - match c with - | Obj => True - | C i _ => in_table_id ct i - end. - Lemma in_table_app_or_lib : forall (ct : class_table) (c : class), - in_table ct c <-> in_lib ct c \/ in_app ct c. - Proof. - intros. destruct c. - - simpl. split. auto. auto. - - unfold in_table, in_lib, in_app. unfold in_table_id. reflexivity. - Qed. - Lemma in_app_in_table : forall (ct : class_table) (c : class), - in_app ct c -> in_table ct c. - Proof. intros. rewrite in_table_app_or_lib. right. apply H. Qed. - Lemma in_lib_in_table : forall (ct : class_table) (c : class), - in_lib ct c -> in_table ct c. - Proof. intros. rewrite in_table_app_or_lib. left. apply H. Qed. +Fixpoint list_rel { A : Type } (rel : A -> A -> Prop) (l l' : list A) : Prop := + match l, l' with + | nil, nil => True + | nil, _ => False + | _, nil => False + | x::xs, y::ys => rel x y /\ list_rel rel xs ys + end. + +Definition var_id := id. +Definition class_id := id. +Definition obj_id : class_id := Id 0. +Inductive var : Type := +| Var : var_id -> var +| This : var. +Definition field_id := id. +Definition method_id := id. +Inductive expr : Type := +| E_Var : var -> expr +| E_Field : expr -> field_id -> expr +| E_Invk : expr -> method_id -> list expr -> expr +| E_New : class_id -> list expr -> expr +| E_Cast : class_id -> expr -> expr. + +Theorem expr_ind_list : + forall P : expr -> Prop, + (forall v : var, P (E_Var v)) -> + (forall e : expr, P e -> forall f0 : field_id, P (E_Field e f0)) -> + (forall e : expr, P e -> forall (m : method_id) (l : list expr), Forall P l -> P (E_Invk e m l)) -> + (forall (c : class_id) (l : list expr), Forall P l -> P (E_New c l)) -> + (forall (c : class_id) (e : expr), P e -> P (E_Cast c e)) -> forall e : expr, P e. + intros P H H0 H1 H2 H3 e. apply expr_rect. + - apply H. + - apply H0. + - admit. + - admit. + - admit. +Admitted. + +Definition context := var -> class_id. + +Definition params := list (class_id * var_id). +Inductive constr : Type := +| Constr : class_id -> params -> list var_id -> list (field_id * var_id) -> constr. +Inductive method := Method : class_id -> method_id -> params -> expr -> method. + +Inductive class : Type := +| Obj : class +| C : class_id -> class_id -> list (class_id * field_id) -> constr -> list method -> class. + +Definition class_table : Type := partial_map class * partial_map class. + + +Definition lookup (ct : class_table) (i : class_id) : option class := + match ct with (app, lib) => + match app i with + | Some c => Some c + | None => lib i + end + end. +Definition lookup_field (c : class) (f : field_id) : option class_id := + match c with + | Obj => None + | C _ _ fs _ _ => match find (fun fp => beq_id (snd fp) f) fs with + | None => None + | Some (ci, _) => Some ci + end + end. +Definition lookup_method (c : class) (mi : method_id) : option method := + match c with + | Obj => None + | C _ _ _ _ ms => find (fun m => match m with Method _ mi' _ _ => beq_id mi mi' end) ms + end. +Definition id_of (c : class) : class_id := + match c with + | Obj => obj_id + | C ci _ _ _ _ => ci + end. + +Definition par_id_of (c : class) : option class_id := + match c with + | Obj => None + | C _ di _ _ _ => Some di + end. + +Definition in_lib_id (ct : class_table) (i : class_id) : Prop := + match ct with (_, lib) => lib i <> None end. + +Definition in_app_id (ct : class_table) (i : class_id) : Prop := + match ct with (app, _) => app i <> None end. + +Definition in_lib (ct : class_table) (c : class) : Prop := + match ct with (_, lib) => lib (id_of c) <> None end. + +Definition in_app (ct : class_table) (c : class) : Prop := + match ct with (app, _) => app (id_of c) <> None end. + +Definition in_table_id (ct : class_table) (i : class_id) : Prop := + in_app_id ct i \/ in_lib_id ct i. + +Definition in_table (ct : class_table) (c : class) : Prop := + in_app ct c \/ in_lib ct c. + +Lemma in_app_in_table : forall (ct : class_table) (c : class), + in_app ct c -> in_table ct c. +Proof. intros. unfold in_table. left. apply H. Qed. +Lemma in_lib_in_table : forall (ct : class_table) (c : class), + in_lib ct c -> in_table ct c. +Proof. intros. unfold in_table. right. apply H. Qed. + +Definition extends (ct : class_table) (c d : class) : Prop := + match c with + | Obj => False + | C _ di _ _ _ => lookup ct di = Some d + end. + +Definition extends_id (ct : class_table) (ci di : class_id) : Prop := + match lookup ct ci with + | None => False + | Some Obj => False + | Some (C _ di' _ _ _) => di = di' + end. + +Inductive subtype (ct : class_table) : class -> class -> Prop := +| S_Ref : forall (c : class), subtype ct c c +| S_Trans : forall (c d e : class), subtype ct c d -> subtype ct d e -> subtype ct c e +| S_Sub : forall (c d : class), extends ct c d -> subtype ct c d. + +Inductive subtype_id (ct : class_table) : class_id -> class_id -> Prop := +| SI_Ref : forall ci, in_table_id ct ci -> subtype_id ct ci ci +| SI_Sub : forall ci di, extends_id ct ci di -> subtype_id ct ci di +| SI_Trans : forall ci di ei, subtype_id ct ci di -> subtype_id ct di ei -> subtype_id ct ci ei. + +Inductive valid_class (ct : class_table) : class -> Type := +| ValidObj : in_lib ct Obj -> ~ in_app ct Obj -> lookup ct obj_id = Some Obj -> valid_class ct Obj +| ValidParent : forall c d, + valid_class ct d -> extends ct c d -> + ~ (in_lib ct c /\ in_app ct c) -> + (in_lib ct d /\ in_table ct c) \/ (in_app ct d /\ in_app ct c) -> + lookup ct (id_of c) = Some c -> + valid_class ct c. + +Fixpoint mtype (ct : class_table) (mi : method_id) (c : class) (pfc : valid_class ct c) : + option (list class_id * class_id) := + match pfc with + | ValidObj _ _ _ _ => None + | ValidParent _ d pfd _ _ _ _ _ => + match lookup_method c mi with + | None => None + | Some (Method ci _ l_arg _) => Some (map fst l_arg, ci) + end + end. + +Fixpoint fields (ct : class_table) (c : class) (pfc : valid_class ct c) : list class_id := + match pfc, c with + | ValidObj _ _ _ _, _ => nil + | ValidParent _ _ d pfd _ _ _ _ , C _ _ fs _ _ => map fst fs ++ fields ct d pfd + | _, _ => nil + end. + +Inductive type_of (ct : class_table) (gamma : context) : expr -> class_id -> Prop := +| T_Var : forall x, type_of ct gamma (E_Var x) (gamma x) +| T_Field : forall e c di f, + type_of ct gamma e (id_of c) -> lookup_field c f = Some di -> + type_of ct gamma (E_Field e f) di +| T_Invk : forall e0 c0 ci0 pfc0 ld ret mi le lc, + id_of c0 = ci0 -> type_of ct gamma e0 ci0 -> mtype ct mi c0 pfc0 = Some (ld, ret) -> + length ld = length le -> length le = length lc -> + Forall (fun p => type_of ct gamma (fst p) (snd p)) (combine le lc) -> + Forall (fun p => subtype_id ct (fst p) (snd p)) (combine lc ld) -> + type_of ct gamma (E_Invk e0 mi le) ci0 +| T_New : forall c ci pfc le lc ld, + id_of c = ci -> fields ct c pfc = ld -> + length ld = length le -> length le = length lc -> + Forall (fun p => type_of ct gamma (fst p) (snd p)) (combine le lc) -> + Forall (fun p => subtype_id ct (fst p) (snd p)) (combine lc ld) -> + type_of ct gamma (E_New ci le) ci +| T_Cast : forall e0 ci di, type_of ct gamma e0 di -> type_of ct gamma (E_Cast ci e0) ci. + +Inductive type_checks (ct : class_table) (gamma : context) : expr -> Prop := +| TC_Var : forall x, in_table_id ct (gamma x) -> type_checks ct gamma (E_Var x) +| TC_Field : forall e f di, type_of ct gamma (E_Field e f) di -> in_table_id ct di -> type_checks ct gamma e -> + type_checks ct gamma (E_Field e f) +| TC_Invk : forall e m le di, type_of ct gamma (E_Invk e m le) di -> in_table_id ct di -> + type_checks ct gamma e -> Forall (type_checks ct gamma) le -> + type_checks ct gamma (E_Invk e m le) +| TC_New : forall ci le, in_table_id ct ci -> Forall (type_checks ct gamma) le -> type_checks ct gamma (E_New ci le) +| TC_Cast : forall e di, in_table_id ct di -> type_checks ct gamma e -> type_checks ct gamma (E_Cast di e). +(* exists c, type_of ct gamma e c /\ in_table_id ct c. *) + - Inductive valid_class (ct : class_table) : class -> Type := - | ValidObj : valid_class ct Obj - | ValidParent : forall i ms d, - valid_class ct d -> extends ct (C i ms) d -> - ~ (in_lib ct (C i ms) /\ in_app ct (C i ms)) -> - (in_lib ct d /\ in_table ct (C i ms)) \/ (in_app ct d /\ in_app ct (C i ms)) -> - valid_class ct (C i ms). - - - Definition valid_table (ct : class_table) : Type := - forall c, in_table ct c -> valid_class ct c. - - Lemma extends_injective : forall ct c d d', - valid_class ct c -> extends ct c d -> extends ct c d' -> d = d'. - Proof. - intros ct c d d' pfc c_ext_d c_ext_d'. - unfold extends in c_ext_d, c_ext_d'. destruct c as [| i ms]. - - inversion c_ext_d. - - unfold extends_id in c_ext_d, c_ext_d'. remember ct as ct'. destruct ct' as [app lib]. inversion pfc. - destruct c_ext_d as [d_in_app | d_in_lib], c_ext_d' as [d'_in_app | d'_in_lib]. - + rewrite d_in_app in d'_in_app. inversion d'_in_app. reflexivity. - + assert (in_lib (app, lib) (C i ms)) as c_in_lib. - { unfold in_lib, in_lib_id, not. intros. rewrite d'_in_lib in H5. inversion H5. } - assert (in_app (app, lib) (C i ms)) as c_in_app. - { unfold in_app, in_app_id, not. intros. rewrite d_in_app in H5. inversion H5. } - unfold not in H3. assert False. apply H3. split. apply c_in_lib. apply c_in_app. inversion H5. - + assert (in_lib (app, lib) (C i ms)) as c_in_lib. - { unfold in_lib, in_lib_id, not. intros. rewrite d_in_lib in H5. inversion H5. } - assert (in_app (app, lib) (C i ms)) as c_in_app. - { unfold in_app, in_app_id, not. intros. rewrite d'_in_app in H5. inversion H5. } - unfold not in H3. assert False. apply H3. split. apply c_in_lib. apply c_in_app. inversion H5. - + rewrite d_in_lib in d'_in_lib. inversion d'_in_lib. reflexivity. - Qed. - - - Fixpoint mresolve (ct : class_table) (m : method) (c : class) (pfc : valid_class ct c) : option class := - match pfc with - | ValidObj _ => None - | ValidParent _ _ ms d pfd _ _ _ => if (existsb (fun m' => beq_id m m') ms) - then Some c - else mresolve ct m d pfd - end. - - Lemma mres_lib_in_lib : forall (ct : class_table) (m : method) (c e : class) (pfc : valid_class ct c), - in_lib ct c -> mresolve ct m c pfc = Some e -> in_lib ct e. - admit. - Admitted. - Lemma lemma1 : forall (ct : class_table) (c e : class) (m : method) (pfc : valid_class ct c), - mresolve ct m c pfc = Some e -> in_app ct e -> in_app ct c. - Proof. - intros. induction pfc. - - unfold mresolve in H. inversion H. - - unfold mresolve in H. destruct (existsb (fun m' : id => beq_id m m') ms) in H. - + inversion H. rewrite H2. apply H0. - + fold mresolve in H. apply IHpfc in H. destruct o. - * inversion pfc. - -- rewrite <- H2 in H. unfold in_app in H. inversion H. - -- rewrite H6 in H4. destruct H4. split. destruct H1. apply H1. apply H. - * destruct H1. apply H2. - Qed. - - Inductive ave_rel (ct ct' : class_table) : Prop := - | AveRel : valid_table ct -> valid_table ct' -> - (forall c, in_app ct c <-> in_app ct' c) -> - (forall c d, extends ct c d -> in_table ct' c -> extends ct' c d) -> - (forall c d, extends ct c d -> in_lib ct d -> in_table ct' c -> in_lib ct' d) -> - ave_rel ct ct'. - - Lemma lib'_subset_lib : forall (ct ct' : class_table) (c : class), - ave_rel ct ct' -> in_table ct' c -> in_lib ct c -> in_lib ct' c. - Proof. - intros. inversion H. rewrite in_table_app_or_lib in H0. destruct H0. - - apply H0. - - apply H2 in H0. unfold valid_table in X. - assert (in_table ct c). { apply in_app_in_table. apply H0. } - apply X in H5. inversion H5. - + rewrite <- H6 in H0. inversion H0. - + rewrite H10 in H8. destruct H8. split. apply H1. apply H0. - Qed. - - (*Lemma ext_in_ct_ext_in_ct' : forall (ct ct' : class_table) (c d : class), - ave_rel ct ct' -> in_table ct c -> in_table ct' c -> extends ct c d -> extends ct' c d. - Proof. - intros ct ct' c d ave cin cin' ext.*) - - - - Lemma lemma2 : forall (ct ct' : class_table) (c e e' : class) (m : method) (pfc : valid_class ct c) (pfc' : valid_class ct' c), - in_app ct c -> mresolve ct m c pfc = Some e -> mresolve ct' m c pfc' = Some e' -> ave_rel ct ct' -> - in_app ct e \/ in_lib ct' e'. +Definition valid_table (ct : class_table) : Type := + forall c, in_table ct c -> valid_class ct c. + +Lemma extends_injective : forall ct c d d', + valid_class ct c -> extends ct c d -> extends ct c d' -> d = d'. +Proof. + intros ct c d d' pfc c_ext_d c_ext_d'. + unfold extends in c_ext_d, c_ext_d'. destruct c as [| ci di k ms fs]. + - inversion c_ext_d. + - rewrite c_ext_d in c_ext_d'. inversion c_ext_d'. reflexivity. +Qed. + +Definition dmethods (c : class) : list method_id := + match c with + | Obj => nil + | C _ _ _ _ ms => map (fun m => match m with Method _ id _ _ => id end) ms + end. + +Fixpoint mresolve (ct : class_table) (m : method_id) (c : class) (pfc : valid_class ct c) : option class := + match pfc with + | ValidObj _ _ _ _ => None + | ValidParent _ _ d pfd _ _ _ _ => if (existsb (fun m' => beq_id m m') (dmethods c)) + then Some c + else mresolve ct m d pfd + end. + +Lemma mres_lib_in_lib : forall (ct : class_table) (m : method_id) (c e : class) (pfc : valid_class ct c), + in_lib ct c -> mresolve ct m c pfc = Some e -> in_lib ct e. + intros ct m c e pfc c_in_lib c_res_e. + induction pfc. + - inversion c_res_e. + - unfold mresolve in c_res_e. destruct (existsb (fun m' : id => beq_id m m') (dmethods c)) in c_res_e. + + inversion c_res_e. rewrite <- H0. apply c_in_lib. + + fold mresolve in c_res_e. apply IHpfc. + * destruct o. + -- destruct H. apply H. + -- destruct n. split. apply c_in_lib. destruct H. apply H0. + * apply c_res_e. +Qed. + +Inductive ave_rel (ct ct' : class_table) : Prop := + | AveRel : valid_table ct -> valid_table ct' -> + (forall c, in_app ct c <-> in_app ct' c) -> + (forall c d, extends ct c d -> in_table ct' c -> extends ct' c d) -> + (forall c d, extends ct c d -> in_lib ct d -> in_table ct' c -> in_lib ct' d) -> + ave_rel ct ct'. + +Lemma lib'_subset_lib : forall (ct ct' : class_table) (c : class), + ave_rel ct ct' -> in_table ct' c -> in_lib ct c -> in_lib ct' c. +Proof. + intros. inversion H. unfold in_table in H0. destruct H0. + - apply H2 in H0. unfold valid_table in X. + assert (in_table ct c). { apply in_app_in_table. apply H0. } + apply X in H5. inversion H5. + + rewrite <- H9 in H0. unfold not in H7. apply H7 in H0. inversion H0. + + destruct H8. split. apply H1. apply H0. + - apply H0. +Qed. + +Inductive alpha (ct ct' : class_table) (pft : ave_rel ct ct') : expr * expr -> Prop := +| Rel_Field : forall e e' f, alpha ct ct' pft (e, e') -> alpha ct ct' pft (E_Field e f, E_Field e' f) +| Rel_Invk : forall e e' le le' m, alpha ct ct' pft (e, e') -> length le = length le' -> Forall (alpha ct ct' pft) (combine le le') -> + alpha ct ct' pft (E_Invk e m le, E_Invk e' m le') +| Rel_New : forall ci le le', in_table_id ct' ci -> length le = length le' -> + Forall (alpha ct ct' pft) (combine le le') -> + alpha ct ct' pft (E_New ci le, E_New ci le') +| Rel_Cast : forall e e' c, alpha ct ct' pft (e, e') -> alpha ct ct' pft (E_Cast c e, E_Cast c e'). + +Definition subst := var -> expr. + +Fixpoint do_sub (sig : subst) (e : expr) : expr := + match e with + | E_Var v => sig v + | E_Field e' f => E_Field (do_sub sig e') f + | E_Invk e' m es => E_Invk (do_sub sig e') m (map (do_sub sig) es) + | E_New c es => E_New c (map (do_sub sig) es) + | E_Cast c e' => E_Cast c (do_sub sig e') + end. + +Lemma lemma1 : forall (ct : class_table) (c e : class) (m : method_id) (pfc : valid_class ct c), + mresolve ct m c pfc = Some e -> in_app ct e -> in_app ct c. +Proof. + intros ct c e m pfc c_res_e e_in_app. induction pfc as [ | c d pfd IHd c_ext_d not_lib_app sca look]. + - unfold mresolve in c_res_e. inversion c_res_e. + - unfold mresolve in c_res_e. destruct (existsb (fun m' : id => beq_id m m') (dmethods c)) in c_res_e. + + inversion c_res_e. apply e_in_app. + + fold mresolve in c_res_e. apply IHd in c_res_e. destruct sca. + * inversion pfd. + -- rewrite <- H3 in c_res_e. unfold not in H1. apply H1 in c_res_e. inversion c_res_e. + -- destruct H2. split. destruct H. apply H. apply c_res_e. + * destruct H. apply H0. +Qed. + +Lemma lemma2 : forall (ct ct' : class_table) (c e e' : class) (m : method_id) + (pfc : valid_class ct c) (pfc' : valid_class ct' c), + in_app ct c -> mresolve ct m c pfc = Some e -> mresolve ct' m c pfc' = Some e' -> ave_rel ct ct' -> + in_app ct e \/ in_lib ct' e'. Proof. intros ct ct' c e e' m pfc pfc' c_in_app c_res_e c_res_e' rel. - induction pfc as [| i ms d pfd IHd c_ext_d not_lib_app app_ext_app]. + induction pfc as [| c d pfd IHd c_ext_d not_lib_app app_ext_app]. (* c is Obj *) - unfold mresolve in c_res_e. inversion c_res_e. (* c extends d *) - - unfold mresolve in c_res_e. fold mresolve in c_res_e. - destruct (existsb (fun m' : id => beq_id m m') ms) eqn:m_res. + - unfold mresolve in c_res_e; fold mresolve in c_res_e. + destruct (existsb (fun m' : id => beq_id m m') (dmethods c)) eqn:m_res. (* m-res *) - + inversion c_res_e. left. apply c_in_app. + + inversion c_res_e; left; rewrite <- H0; eauto. (* m-res-inh *) + inversion rel as [ct_val ct'_val keep_app keep_ext keep_lib]. - remember (C i ms) as c. unfold mresolve in c_res_e'. - (* can't induct on pfc and pfc' simultaneously, so manually destruct pfc' and show that it's the same d *) - destruct pfc' as [_ | i0 ms0 d0 pfd' c_ext_d'] eqn:pfc''. + unfold mresolve in c_res_e'. + (* can't induct on pfc and pfc' simultaneously, + so manually destruct pfc' and show that it's the same parent *) + destruct pfc' as [| c0 d0 pfd' c_ext_d'] eqn:pfc''. * inversion c_res_e'. - * fold mresolve in c_res_e'. inversion Heqc. - rewrite H1 in c_res_e'. rewrite m_res in c_res_e'. + * fold mresolve in c_res_e'. rewrite m_res in c_res_e'. assert (d = d0) as deq. - { apply extends_injective with (ct := ct') (c := (C i0 ms0)). + { apply extends_injective with (ct := ct') (c := c0). -- apply pfc'. -- apply keep_ext. ++ apply c_ext_d. @@ -214,7 +320,7 @@ Proof. destruct app_ext_app as [[d_in_lib _] | [d_in_app _]]. (* d in lib - use averroes transformation properties *) -- right. apply mres_lib_in_lib with (m := m) (c := d0) (pfc := pfd'). - ++ apply keep_lib with (c := (C i0 ms0)). + ++ apply keep_lib with (c := c0). ** rewrite <- deq. apply c_ext_d. ** rewrite <- deq. apply d_in_lib. ** apply in_app_in_table. apply keep_app. apply c_in_app. @@ -225,138 +331,33 @@ Proof. mresolve ct' m d pfc' = Some e' -> in_app ct e \/ in_lib ct' e') as IHd'. { intros pfc'0 _ mres'. apply IHd with (pfc' := pfc'0). apply d_in_app. apply c_res_e. apply mres'. } - rewrite deq in IHd'. + rewrite deq in IHd'. apply IHd' with (pfc' := pfd'). ++ rewrite <- deq. apply d_in_app. ++ apply c_res_e'. Qed. - - -End ParId. - -Module ParC. - - Inductive class : Type := - | Obj : class - | C : class -> list method -> class. - - (** application classes * library classes *) - Definition class_table : Type := list class * list class. - - Definition in_table (ct : class_table) (c : class) : Prop := - match ct with (app, lib) => In c app \/ In c lib end. - - Definition in_app (ct : class_table) (c : class) : Prop := - match ct with (app, _) => In c app end. - - Definition in_lib (ct : class_table) (c : class) : Prop := - match ct with (_, lib) => In c lib end. - - Inductive valid_class (ct : class_table) : class -> Type := - | ValidObj : valid_class ct Obj - | ValidParent : forall c ms, - valid_class ct c -> - ~ (in_lib ct (C c ms) /\ in_app ct (C c ms)) -> - (in_lib ct c /\ in_table ct (C c ms)) \/ (in_app ct c /\ in_app ct (C c ms)) -> - valid_class ct (C c ms). - - Definition extends (c d : class) : Prop := - match c with - | Obj => False - | C c' _ => c' = d - end. - - Definition valid_table (ct : class_table) : Type := - match ct with - | (app, lib) => forall c, in_table ct c -> valid_class ct c - end. - - Fixpoint mresolve (m : method) (c : class) : option class := - match c with - | Obj => None - | C d ms => if (existsb (fun m' => beq_id m m') ms) then Some c else mresolve m d - end. - - Lemma lemma1 : forall (ct : class_table) (pft : valid_table ct) (c e : class) (pfc : valid_class ct c) (pfe : valid_class ct e) (m : method), - mresolve m c = Some e -> in_app ct e -> in_app ct c. - Proof. - intros. induction pfc. - - unfold mresolve in H. inversion H. - - unfold mresolve in H. destruct (existsb (fun m' : id => beq_id m m') ms) in H. - + inversion H. rewrite H2. apply H0. - + fold mresolve in H. apply IHpfc in H. destruct o. - * destruct n. destruct H1. split. apply H1. apply H. - * destruct H1. apply H2. - Qed. - -End ParC. -(* -Definition extends (c d : class) : Prop := - match c with - | Obj => False - | C d' ms => d' = d - end. -Definition parent (c : class) : class := - match c with - | Obj => Obj - | C d _ => d - end. -*) -Axiom obj_in_lib : forall (ct : class_table), ~ (in_app ct Obj). - -Axiom no_lib_ext_app : forall (ct : class_table) (c : class) (ms : list method), - in_app ct c -> in_app ct (C c ms). - -Module NonInductive. - Fixpoint mresolve (ct : class_table) (m : method) (c : class) : class := - match c with - | Obj => Obj - | C d ms => if (existsb (fun m' => beq_id m m') ms) then c else mresolve ct m d - end. - - Lemma lemma1 : forall (ct : class_table) (c : class) (m : method), - in_app ct (mresolve ct m c) -> in_app ct c. - Proof. - intros. induction c as [| d ms]. - - simpl in H. apply obj_in_lib in H. inversion H. - - simpl in H. destruct (existsb (fun m' : id => beq_id m m') l) in H. - + apply H. - + apply ms in H. apply no_lib_ext_app. apply H. - Qed. - -End NonInductive. - -Module Induct. - Inductive mresolve (ct : class_table) : method -> class -> class -> Prop := - | Mres : forall (m : method) (c : class) (ms : list method), - In m ms -> mresolve ct m (C c ms) (C c ms) - | Mres_Inh : forall (m : method) (c d : class) (ms : list method), - ~ In m ms -> mresolve ct m c d -> mresolve ct m (C c ms) d. - - Lemma lemma1 : forall (ct : class_table) (c d : class) (m : method), - mresolve ct m c d -> in_app ct d -> in_app ct c. - Proof. - intros. induction H. - - (* Mres *) apply H0. - - (* Mres-Inh *) apply no_lib_ext_app. auto. - Qed. -End Induct. - -Module InductOpt. - Inductive mresolve (ct : class_table) : method -> class -> option class -> Prop := - | M_Res_None : forall (m : method), mresolve ct m Obj None - | M_Res : forall (m : method) (c : class) (ms : list method), - In m ms -> mresolve ct m (C c ms) (Some (C c ms)) - | M_Res_Inh : forall (m : method) (c : class) (d : option class) (ms : list method), - ~ In m ms -> mresolve ct m c d -> mresolve ct m (C c ms) d. - -Lemma lemma1 : forall (ct : class_table) (c d : class) (m : method), - mresolve ct m c (Some d) -> in_app ct d -> in_app ct c. +(* Lemma Forall_imp : forall (A : type) (l : list A) *) + +Lemma lemma3 : forall (ct ct' : class_table) (pft : ave_rel ct ct') + (sig sig' : subst) (gamma : context) (e0 : expr), + (forall v, alpha ct ct' pft (sig v, sig' v)) -> type_checks ct' gamma e0 -> + alpha ct ct' pft (do_sub sig e0, do_sub sig' e0). Proof. - intros. remember (Some d) as sd. induction H. - - (* Obj *) inversion Heqsd. - - (* Mres *) inversion Heqsd. rewrite <- H2 in H0. apply H0. - - (* Mres-Inh *) apply IHmresolve in Heqsd. apply no_lib_ext_app. apply Heqsd. + intros ct ct' pft sig sig' gamma e0 rel typ_chk. induction e0 using expr_ind_list. + - eauto. + - simpl; apply Rel_Field. inversion typ_chk; eauto. + - simpl; apply Rel_Invk. + + inversion typ_chk; eauto. + + rewrite map_length, map_length; reflexivity. + + inversion typ_chk. clear H2; clear H3; clear typ_chk; induction l. + * apply Forall_nil. + * inversion H; inversion H6. apply Forall_cons; eauto; eauto. + - simpl. inversion typ_chk. apply Rel_New. + + eauto. + + rewrite map_length, map_length; reflexivity. + + clear typ_chk; clear H1; induction l. + * apply Forall_nil. + * inversion H; inversion H3. apply Forall_cons; eauto; eauto. + - apply Rel_Cast; inversion typ_chk; eauto. Qed. -End InductOpt. \ No newline at end of file