From 8603674da9e68529c5756591607d79f19c3fd98d Mon Sep 17 00:00:00 2001 From: Garo Brik Date: Thu, 27 Oct 2016 12:39:11 -0400 Subject: [PATCH] Proofs up to lemma 10 (skipping lemma 6) using no class_id --- newproof.v | 1707 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1707 insertions(+) create mode 100644 newproof.v diff --git a/newproof.v b/newproof.v new file mode 100644 index 0000000..067b7c6 --- /dev/null +++ b/newproof.v @@ -0,0 +1,1707 @@ +Require Import Coq.Init.Datatypes. +Require Import Coq.Lists.List. +Require Import Arith.EqNat. +Require Import Program.Equality. + +Module E. + Require Coq.Sets.Ensembles. + Include Ensembles. +End E. + +Section generic_defs. + Definition set := E.Ensemble. + Definition empty_set {A : Type} := E.Empty_set A. + Definition set_In {A : Type} (a : A) (s : set A) := E.In A s a. + Definition add {A : Type} (a : A) (s : set A) := E.Add A s a. + Definition union {A : Type} := E.Union A. + Definition union_introl {A : Type} := E.Union_introl A. + Definition union_intror {A : Type} := E.Union_intror A. + Definition subset {A : Type} := E.Included A. + Fixpoint set_from_list {A : Type} (l : list A) := + match l with + | nil => empty_set + | h :: l' => add h (set_from_list l') + end. + + (*Definition set (A : Type) := list A. + Definition union {A : Type} (a b : set A) := a ++ b. + Theorem union_introl : forall (A : Type) (s t : set A) (a : A), + In a s -> In a (s ++ t). + Proof. + intros. induction s. + - inversion H. + - simpl. simpl in H. destruct H. + + left. trivial. + + right. eauto. + Qed. *) + + Fixpoint index_of {A : Type} (f : A -> bool) (l : list A) : option nat := + match l with + | nil => None + | a :: l' => if f a then Some 0 else option_map S (index_of f l') + end. + Fixpoint first_n {A : Type} (l : list A) (n : nat) := + match n, l with + | S n', h :: l' => h :: (first_n l' n') + | _, _ => nil + end. + Fixpoint remove_last {A : Type} (l : list A) := + match l with + | nil => nil + | _ :: nil => nil + | h :: l' => h :: (remove_last l') + end. + + Fixpoint last_error {A : Type} (l : list A) := + match l with + | nil => None + | h :: nil => Some h + | _ :: l' => last_error l' + end. + + Fixpoint zip_with_ind_h {A : Type} (l : list A) (n : nat) := + match l with + | nil => nil + | h :: l' => (n, h) :: zip_with_ind_h l' (S n) + end. + Definition zip_with_ind {A : Type} (l : list A) := zip_with_ind_h l 0. + +End generic_defs. + +Notation "a 'U' b" := (union a b) (at level 65, right associativity). +Section generic_thms. + Theorem Forall_list_impl : forall (A : Type) (P Q : A -> Prop) (l : list A), + Forall P l -> Forall (fun a => P a -> Q a) l -> Forall Q l. + Proof. + intros A P Q l fp fimp. induction l. apply Forall_nil. + inversion fp. inversion fimp. + apply Forall_cons. + - apply H5; trivial. + - apply IHl; trivial. + Qed. + + Theorem Forall_map_swap : forall (A : Type) (P : A -> Prop) (f : A -> A) (l : list A), + Forall P (map f l) <-> Forall (fun a => P (f a)) l. + Proof. + intros A P f l. + induction l. + - simpl. split; intros; apply Forall_nil. + - simpl. split; intros; inversion H; apply Forall_cons; trivial; apply IHl; trivial. + Qed. + + Theorem Forall_In : forall (A : Type) (P : A -> Prop) (l : list A) (a : A), + Forall P l -> In a l -> P a. + Proof. + induction l. + - intros. inversion H0. + - intros. destruct H0; inversion H; eauto. + rewrite <- H0. eauto. + Qed. + + Theorem find_pair_in_zip : forall (A B : Type) (f : A -> bool) (la : list A) (lb lb' : list B) p p', + find (fun p => f (fst p)) (combine la lb) = Some p -> + find (fun p => f (fst p)) (combine la lb') = Some p' -> + In (snd p, snd p') (combine lb lb'). + Proof. + induction la. + - intros. inversion H. + - intros. destruct lb; destruct lb'. + + inversion H. + + inversion H. + + inversion H0. + + simpl in H. simpl in H0. destruct (f a). + * inversion H. inversion H0. simpl. left. reflexivity. + * simpl. right; eauto. + Qed. + + Theorem extract_combine : forall {A B : Type} (f : A -> bool) (la : list A) (lb : list B), + length la = length lb -> find (fun p => f (fst p)) (combine la lb) = None -> find f la = None. + Proof. + induction la. + - reflexivity. + - intros. destruct lb. + + inversion H. + + simpl in H0. simpl. destruct (f a). + * inversion H0. + * apply IHla with lb; eauto. + Qed. + + Theorem zip_In_l : forall {A B : Type} (la : list A) (lb : list B) a b, + In (a, b) (combine la lb) -> In a la. + Proof. + induction la; intros. + - inversion H. + - destruct lb. + + inversion H. + + simpl in H. simpl. destruct H. + * inversion H. eauto. + * right. apply IHla with lb b. eauto. + Qed. + + Theorem zip_In_r : forall {A B : Type} (la : list A) (lb : list B) a b, + In (a, b) (combine la lb) -> In b lb. + Proof. + intros A B la lb. generalize dependent la. induction lb; intros. + - destruct la; inversion H. + - destruct la. + + inversion H. + + simpl in H. simpl. destruct H. + * inversion H. eauto. + * right. apply IHlb with la a0. eauto. + Qed. + + Theorem get_nth : forall {A : Type} (l : list A) (m n : nat), + length l = n -> m < n -> exists a, nth_error l m = Some a. + Proof. + induction l; intros; simpl in H. + - rewrite <- H in H0. inversion H0. + - destruct n; inversion H. + destruct m. + + exists a. reflexivity. + + simpl. apply IHl with n; trivial. + apply Lt.lt_S_n. trivial. + Qed. + + Lemma union_comm : forall {A : Type} (s1 s2 : set A), + s1 U s2 = s2 U s1. + Proof. + intros. apply E.Extensionality_Ensembles. + unfold E.Same_set. unfold E.Included. + split; unfold union; intros; inversion H; + solve [apply union_introl; trivial | apply union_intror; trivial]. + Qed. + + Lemma union_addl : forall A (s1 s2 : set A) (a : A), + add a s1 U s2 = add a (s1 U s2). + intros. apply E.Extensionality_Ensembles. + unfold E.Same_set. unfold E.Included. unfold union. unfold add. + split; intros; inversion H; try (inversion H0); + solve [apply union_intror; trivial + | apply union_introl; solve [apply union_introl; trivial + | apply union_intror; solve [trivial | reflexivity]]]. + Qed. + + Lemma union_addr : forall A (s1 s2 : set A) (a : A), + s1 U add a s2 = add a (s1 U s2). + intros. apply E.Extensionality_Ensembles. + unfold E.Same_set. unfold E.Included. unfold union. unfold add. + split; intros; inversion H; try (inversion H0); + solve [ apply union_introl; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial] + | apply union_intror; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial]]. + Qed. + + Lemma union_assoc : forall {A: Type} (s1 s2 s3 : set A), + (s1 U s2) U s3 = s1 U s2 U s3. + Proof. + intros. apply E.Extensionality_Ensembles. unfold E.Same_set. unfold E.Included. unfold union. + split; intros; inversion H; try (inversion H0); + solve [ apply union_introl; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial] + | apply union_intror; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial]]. + Qed. + + Lemma union_same : forall {A : Type} (s : set A), + s U s = s. + Proof. + intros. apply E.Extensionality_Ensembles. unfold E.Same_set. unfold E.Included. unfold union. + split; intros; try (inversion H); trivial. apply union_introl. apply H. + Qed. + + Lemma union_include : forall {A : Type} (s1 s2 : set A), + subset s1 s2 -> s2 = s2 U s1. + Proof. + intros. apply E.Extensionality_Ensembles. + unfold E.Same_set. unfold subset in H. unfold E.Included. unfold E.Included in H. + split; intros. + - apply union_introl. apply H0. + - destruct H0. + + apply H0. + + apply H. apply H0. + Qed. + + Lemma In_list_set_In_list : forall {A : Type} (l : list A) (a : A), + In a l -> set_In a (set_from_list l). + Proof. + induction l; intros; inversion H. + - subst a0. simpl. apply union_intror. apply E.In_singleton. + - simpl. apply union_introl. apply IHl. apply H0. + Qed. + + Lemma nth_error_first_n : forall {A : Type} (l : list A) (a : A) (n : nat), + nth_error l n = Some a -> nth_error (first_n l (S n)) n = Some a. + Proof. + induction l; intros; destruct n; inversion H. + - subst a0. reflexivity. + - simpl. rewrite H1. apply IHl. apply H1. + Qed. + + Lemma remove_last_length : forall {A : Type} (l : list A) (n : nat), + length l = S n -> length (remove_last l) = n. + Proof. + induction l; intros; inversion H. + destruct l; try reflexivity. + simpl. simpl in IHl. rewrite IHl with (length l); reflexivity. + Qed. + + Lemma remove_last_first_n : forall {A : Type} (l : list A) (n : nat), + n < length l -> first_n l n = first_n (remove_last l) n. + Proof. + induction l; intros. + - inversion H. + - destruct l. + + simpl in H. inversion H. reflexivity. inversion H1. + + destruct n; try reflexivity. + simpl. f_equal. unfold first_n in IHl. fold (@first_n A) in IHl. + unfold remove_last in IHl. fold (@remove_last A) in IHl. + apply IHl. apply Lt.lt_S_n. apply H. + Qed. + + Lemma remove_last_nth_error : forall {A : Type} (l : list A) (n : nat), + S n < length l -> nth_error l n = nth_error (remove_last l) n. + Proof. + induction l; intros. + - inversion H. + - destruct n. + + destruct l. + * inversion H. inversion H1. + * reflexivity. + + destruct l. + * inversion H. inversion H1. + * simpl. simpl in IHl. apply IHl. apply Lt.lt_S_n. apply H. + Qed. + + Lemma first_n_length : forall {A : Type} (l : list A), + first_n l (length l) = l. + Proof. + induction l; try reflexivity. + simpl. rewrite IHl. reflexivity. + Qed. + Lemma last_error_In : forall {A : Type} (l : list A) (a : A), + last_error l = Some a -> In a l. + Proof. + induction l. + - intros. inversion H. + - destruct l. + + intros. inversion H. left. reflexivity. + + intros. right. apply IHl. apply H. + Qed. + + Lemma zip_with_ind_h_length : forall {A : Type} (l : list A) (n : nat), + length (zip_with_ind_h l n) = length l. + Proof. + induction l. + - reflexivity. + - intros. simpl. f_equal. apply IHl. + Qed. + + Lemma zip_with_ind_length : forall {A : Type} (l : list A), + length (zip_with_ind l) = length l. + Proof. intros. apply zip_with_ind_h_length. Qed. + + Lemma last_repeat : forall {A : Type} (a : A) (n : nat), + last_error (repeat a (S n)) = Some a. + Proof. + induction n. + - reflexivity. + - simpl. apply IHn. + Qed. + + Lemma last_error_map : forall {A B : Type} (f : A -> B) (l : list A) (a : A), + last_error l = Some a -> last_error (map f l) = Some (f a). + Proof. + induction l. + - intros. inversion H. + - intros. destruct l. + + inversion H. subst a0. reflexivity. + + simpl. apply IHl. apply H. + Qed. + + Lemma last_error_zip_with_ind_h : forall {A : Type} (l : list A) (n : nat) (m : nat) (a : A), + length l = S m -> last_error l = Some a -> + last_error (zip_with_ind_h l n) = Some (m + n, a). + Proof. + induction l. + - intros. inversion H. + - intros. destruct l. + + inversion H0. subst a0. inversion H. reflexivity. + + destruct m. inversion H. simpl. rewrite plus_n_Sm. apply IHl. + * simpl. f_equal. inversion H. reflexivity. + * apply H0. + Qed. + + Lemma last_error_zip_with_ind : forall {A : Type} (l : list A) (n : nat) (a : A), + length l = S n -> last_error l = Some a -> + last_error (zip_with_ind l) = Some (n, a). + Proof. + intros. unfold zip_with_ind. rewrite (plus_n_O n). apply last_error_zip_with_ind_h; trivial. + Qed. + + Lemma nth_error_map : forall {A B : Type} (l : list A) (f : A -> B) (a : A) (n : nat), + nth_error l n = Some a -> nth_error (map f l) n = Some (f a). + Proof. + induction l; intros; destruct n; inversion H. + - subst a0. reflexivity. + - rewrite <- IHl with (n := n); try reflexivity. apply H. + Qed. + + Lemma nth_error_zip_with_ind_h : forall {A : Type} (l : list A) (n : nat) (m : nat) (a : A), + nth_error l m = Some a -> nth_error (zip_with_ind_h l n) m = Some (n + m, a). + Proof. + induction l; intros; destruct m; inversion H. + - subst a0. rewrite PeanoNat.Nat.add_comm. reflexivity. + - simpl. rewrite <- plus_n_Sm. replace (S (n + m)) with (S n + m) by reflexivity. + apply IHl. trivial. + Qed. + + Lemma nth_error_zip_with_ind : forall {A : Type} (l : list A) (m : nat) (a : A), + nth_error l m = Some a -> nth_error (zip_with_ind l) m = Some (m, a). + Proof. + intros. apply nth_error_zip_with_ind_h. trivial. + Qed. + + Lemma nth_error_better_Some : forall {A : Type} (l : list A) (n : nat), + n < length l -> exists a, nth_error l n = Some a. + Proof. + intros. assert (nth_error l n <> None) by (apply nth_error_Some; trivial). + destruct (nth_error l n) eqn:ntherr. + - exists a. reflexivity. + - destruct H0; reflexivity. + Qed. + +End generic_thms. +Section defs. + Definition field_id := nat. + Definition var_id := nat. + Definition method_id := nat. + + Inductive var : Type := + | Var : var_id -> var + | This : var. + + Inductive class : Type := + | Obj : class + | C : class -> + list (class * field_id) -> + list (class * var_id) -> + list method -> class + with expr : Type := + | E_Var : var -> expr + | E_Field : expr -> field_id -> expr + | E_New : class -> list expr -> expr + | E_Invk : expr -> method_id -> list expr -> expr + | E_Cast : class -> expr -> expr + | E_Lib : expr + with method : Type := + | Method : class -> method_id -> list (class * var_id) -> expr -> method. + Definition exprlpt : Type := expr * set expr. + +End defs. +Section table_defs. + Definition empty_map : class -> Prop := fun c => False. + Definition class_table : Type := (class -> Prop) * (class -> Prop). + Definition in_app (ct : class_table) c := + match ct with (app, _) => app c end. + Definition in_lib (ct : class_table) c := + match ct with (_, lib) => lib c end. + Definition in_table ct c := in_app ct c \/ in_lib ct c. + Definition ct_lib (ct : class_table) : class_table := + match ct with (app, lib) => (empty_map, lib) end. + + Inductive expr_In : var -> expr -> Prop := + | EIn_Var : forall v, expr_In v (E_Var v) + | EIn_Field : forall v e f, expr_In v e -> expr_In v (E_Field e f) + | EIn_New : forall v le c, Exists (expr_In v) le -> expr_In v (E_New c le) + | EIn_Invk : forall v e m le, Exists (expr_In v) le \/ expr_In v e -> expr_In v (E_Invk e m le) + | EIn_Cast : forall v e c, expr_In v e -> expr_In v (E_Cast c e). + + Definition valid_method (m : method) : Prop := + match m with + | Method _ _ lcv e => + forall v, expr_In v e -> v = This \/ In v (map Var (map snd lcv)) + end. + + Inductive valid_class (ct : class_table) : class -> Prop := + | V_Obj : ~ in_app ct Obj -> in_lib ct Obj -> valid_class ct Obj + | V_Class : forall d l l' lm, + valid_class ct d -> + ~ (in_lib ct (C d l l' lm) /\ in_app ct (C d l l' lm)) -> + ((in_app ct d /\ in_app ct (C d l l' lm)) \/ (in_table ct (C d l l' lm) /\ in_lib ct d)) -> + Forall valid_method lm -> + valid_class ct (C d l l' lm). + Definition valid_table ct : Prop := + forall c, in_table ct c -> valid_class ct c. +End table_defs. +Section auxiliary_defs. + Definition beq_var (v v' : var) : bool := + match v, v' with + | This, This => true + | Var vi, Var vi' => beq_nat vi vi' + | _, _ => false + end. + + Theorem beq_var_refl : forall v, true = beq_var v v. + Proof. intros. destruct v; eauto. simpl. apply beq_nat_refl. Qed. + Theorem beq_var_true : forall v v', v = v' <-> true = beq_var v v'. + Proof. + intros. split; intro; destruct v; destruct v'; inversion H; eauto. + - apply beq_var_refl. + - symmetry in H1. apply beq_nat_true in H1. eauto. + Qed. + + Definition subst := list (var * expr). + Fixpoint do_sub (sig : subst) (e : expr) : expr := + match e with + | E_Var v => match find (fun p => beq_var (fst p) v) sig with + | Some (_, e') => e' + | None => e + end + | E_Field e' f => E_Field (do_sub sig e') f + | E_New c es => E_New c (map (do_sub sig) es) + | E_Invk e' m es => E_Invk (do_sub sig e') m (map (do_sub sig) es) + | E_Cast c e' => E_Cast c (do_sub sig e') + | E_Lib => E_Lib + end. + + Definition context := var -> class. + +End auxiliary_defs. +Section auxiliary_functions. + + Definition mid (m : method) : method_id := match m with Method _ mi _ _ => mi end. + Definition args (m : method) : list var := + match m with + | Method _ _ l _ => map Var (map snd l) + end. + Definition body (m : method) : expr := match m with Method _ _ _ e => e end. + Fixpoint fields (c : class) : list (class * field_id) := + match c with + | Obj => nil + | C d fs _ _ => fs ++ fields d + end. + + Definition dfields (c : class) : list (class * field_id) := + match c with + | Obj => nil + | C d fs _ _ => fs + end. + + Definition lookup_field (fi : field_id) (c : class) : option class := + option_map fst (find (fun p => match p with (_, fi') => beq_nat fi fi' end) (fields c)). + + Fixpoint declaring_class (fi : field_id) (c : class) : option class := + match c with + | Obj => None + | C d fs _ _ => if existsb (fun p => beq_nat fi (snd p)) fs + then Some c + else declaring_class fi d + end. + + Definition dmethods (c : class) : list method := + match c with + | Obj => nil + | C _ _ _ ms => ms + end. + + Definition dmethods_id (c : class) : list method_id := + match c with + | Obj => nil + | C _ _ _ ms => map (fun m => match m with Method _ mi _ _ => mi end) ms + end. + + Definition lookup_method (mi : method_id) (c : class) : option method := + match c with + | Obj => None + | C _ _ _ ms => find (fun m => match m with Method _ mi' _ _ => beq_nat mi mi' end) ms + end. + + Fixpoint find_method (mi : method_id) (c : class) : option method := + match c with + | Obj => None + | C d _ _ _ => match lookup_method mi c with + | Some m => Some m + | None => find_method mi d + end + end. + Fixpoint mtype (mi : method_id) (c : class) : option (list class * class) := + match find_method mi c with + | Some (Method ret _ par _) => Some (map fst par, ret) + | None => None + end. + + Fixpoint mparams (mi : method_id) (c : class) : option (list var_id) := + match find_method mi c with + | Some (Method ret _ par _) => Some (map snd par) + | None => None + end. + + Fixpoint mbody (mi : method_id) (c : class) : option (list var_id * expr) := + match find_method mi c with + | Some (Method _ _ par bod) => Some (map snd par, bod) + | None => None + end. + + Fixpoint mresolve (m : method_id) (c : class) : option class := + match c with + | Obj => None + | C d _ _ _ => + if (existsb (fun m' => beq_nat m m') (dmethods_id c)) + then Some c + else mresolve m d + end. + + Definition extends (c d : class) : Prop := + match c with + | Obj => False + | C d' _ _ _ => d = d' + end. + + (*Fixpoint subst_from_list (l : list (expr * var)) : subst := + match l with + | nil => fun _ => None + | (e, v) :: l' => fun v' => if beq_var v v' then Some e else subst_from_list l' v' + end.*) + +End auxiliary_functions. +Section auxiliary_lemmas. + Lemma decl_of_lib_in_lib : forall ct c d f, + valid_table ct -> in_lib ct c -> declaring_class f c = Some d -> in_lib ct d. + Proof. + intros ct c d f pft c_in_lib decl. + induction c. + - inversion decl. + - simpl in decl. destruct (existsb (fun p : class * nat => PeanoNat.Nat.eqb f (snd p)) l). + + inversion decl; trivial. + + assert (valid_class ct (C c l l0 l1)). + { apply pft. unfold in_table. right. trivial. } + inversion H. destruct H6 as [[par_app ch_app] | [ch_tab par_lib]]. + * destruct H5. split; trivial. + * apply IHc; trivial. + Qed. + + Lemma mresolve_in_methods : forall c d m, + mresolve m c = Some d -> In m (dmethods_id d). + Proof. + intros. induction c. + - inversion H. + - unfold mresolve in H. + destruct (existsb (fun m' : nat => PeanoNat.Nat.eqb m m') (dmethods_id (C c l l0 l1))) eqn:exst; eauto. + inversion H. rewrite existsb_exists in exst. destruct exst as [x [in_eqb]]. + apply beq_nat_true in H0. rewrite H0. trivial. + Qed. + +End auxiliary_lemmas. +Section props. + Definition ave_rel (ct ct' : class_table) : Prop := + valid_table ct /\ valid_table ct' /\ + (forall c, in_app ct c <-> in_app ct' c) /\ + (forall c d, extends c d -> in_lib ct d -> in_table ct' c -> in_lib ct' d). + + Inductive subtype : class -> class -> Prop := + | S_Ref : forall c, subtype c c + | S_Trans : forall c d e, subtype c d -> subtype d e -> subtype c e + | S_Sub : forall c d, extends c d -> subtype c d. + + Inductive type_of (gamma : context) : expr -> class -> Prop := + | T_Var : forall x, type_of gamma (E_Var x) (gamma x) + | T_Field : forall e c d f, + type_of gamma e c -> lookup_field f c = Some d -> + type_of gamma (E_Field e f) d + | T_New : forall c le lc ld, + map fst (fields c) = ld -> + length ld = length le -> length le = length lc -> + Forall (fun p => type_of gamma (fst p) (snd p)) (combine le lc) -> + Forall (fun p => subtype (fst p) (snd p)) (combine lc ld) -> + type_of gamma (E_New c le) c + | T_Invk : forall e0 c0 ld ret mi le lc, + type_of gamma e0 c0 -> mtype mi c0 = Some (ld, ret) -> + length ld = length le -> length le = length lc -> + Forall (fun p => type_of gamma (fst p) (snd p)) (combine le lc) -> + Forall (fun p => subtype (fst p) (snd p)) (combine lc ld) -> + type_of gamma (E_Invk e0 mi le) ret + | T_Cast : forall e0 c d, type_of gamma e0 d -> type_of gamma (E_Cast c e0) c. + + Inductive alpha (ct ct' : class_table) (gamma : context) : expr -> expr -> set expr -> Prop := + | Rel_Field : forall e e' f lpt, + alpha ct ct' gamma e e' lpt -> + alpha ct ct' gamma (E_Field e f) (E_Field e' f) lpt + | Rel_Lib_Field : forall e c d f lpt, + alpha ct ct' gamma e E_Lib lpt -> + declaring_class f c = Some d -> in_lib ct d -> + type_of gamma e c -> + alpha ct ct' gamma (E_Field e f) E_Lib lpt + | Rel_New : forall c le le' lpt, + in_table ct' c -> length le = length le' -> + Forall (fun p => alpha ct ct' gamma (fst p) (snd p) lpt) (combine le le') -> + alpha ct ct' gamma (E_New c le) (E_New c le') lpt + | Rel_Lib_New : forall c le lpt, + in_lib ct c -> Forall (fun e => alpha ct ct' gamma e E_Lib lpt) le -> + alpha ct ct' gamma (E_New c le) E_Lib lpt + | Rel_Invk : forall e e' le le' m lpt, + alpha ct ct' gamma e e' lpt -> + length le = length le' -> + Forall (fun p => alpha ct ct' gamma (fst p) (snd p) lpt) (combine le le') -> + alpha ct ct' gamma (E_Invk e m le) (E_Invk e' m le') lpt + | Rel_Lib_Invk : forall e le mi lpt, + (exists c, in_lib ct c /\ In mi (dmethods_id c)) -> + alpha ct ct' gamma e E_Lib lpt -> + Forall (fun e' => alpha ct ct' gamma e' E_Lib lpt) le -> + alpha ct ct' gamma (E_Invk e mi le) E_Lib lpt + | Rel_Cast : forall e e' c lpt, + alpha ct ct' gamma e e' lpt -> + alpha ct ct' gamma (E_Cast c e) (E_Cast c e') lpt + | Rel_Lib_Cast : forall e ci lpt, + alpha ct ct' gamma e E_Lib lpt -> alpha ct ct' gamma (E_Cast ci e) E_Lib lpt + | Rel_Lpt : forall e e' lpt, + alpha ct ct' gamma e e' lpt -> set_In e' lpt -> alpha ct ct' gamma e E_Lib lpt. + (*Inductive alpha (ct ct' : class_table) (gamma : context) : expr * (expr * set expr) -> Prop := + | Rel_Field : forall e e' f lpt, + alpha ct ct' gamma (e, (e', lpt)) -> + alpha ct ct' gamma ((E_Field e f), (E_Field e' f, lpt)) + | Rel_Lib_Field : forall e c d f lpt, + alpha ct ct' gamma (e, (E_Lib, lpt)) -> + declaring_class f c = Some d -> in_lib ct d -> + type_of gamma e c -> + alpha ct ct' gamma ((E_Field e f), (E_Lib, lpt)) + | Rel_New : forall c le le' lpt, + in_table ct' c -> length le = length le' -> + Forall (alpha ct ct' gamma) (combine le (combine le' (repeat lpt (length le')))) -> + alpha ct ct' gamma (E_New c le, (E_New c le', lpt)) + | Rel_Lib_New : forall c le lpt, + in_lib ct c -> Forall (fun e => alpha ct ct' gamma (e, (E_Lib, lpt))) le -> + alpha ct ct' gamma ((E_New c le), (E_Lib, lpt)) + | Rel_Invk : forall e e' le le' m lpt, + alpha ct ct' gamma (e, (e', lpt)) -> + length le = length le' -> + Forall (alpha ct ct' gamma) (combine le (combine le' (repeat lpt (length le')))) -> + alpha ct ct' gamma ((E_Invk e m le), (E_Invk e' m le', lpt)) + | Rel_Lib_Invk : forall e le mi lpt, + (exists c, in_lib ct c /\ In mi (dmethods_id c)) -> + alpha ct ct' gamma (e, (E_Lib, lpt)) -> + Forall (fun e' => alpha ct ct' gamma (e', (E_Lib, lpt))) le -> + alpha ct ct' gamma ((E_Invk e mi le), (E_Lib, lpt)) + | Rel_Cast : forall e e' c lpt, + alpha ct ct' gamma (e, (e', lpt)) -> + alpha ct ct' gamma ((E_Cast c e), (E_Cast c e', lpt)) + | Rel_Lib_Cast : forall e ci lpt, + alpha ct ct' gamma (e, (E_Lib, lpt)) -> alpha ct ct' gamma ((E_Cast ci e), (E_Lib, lpt)) + | Rel_Lpt : forall e e' lpt, + alpha ct ct' gamma (e, (e', lpt)) -> set_In e' lpt -> alpha ct ct' gamma (e, (E_Lib, lpt)).*) + + + Inductive type_checks (ct : class_table) (gamma : context) : expr -> Prop := + | TC_Var : forall x, in_table ct (gamma x) -> type_checks ct gamma (E_Var x) + | TC_Field : forall e f d, type_of gamma (E_Field e f) d -> in_table ct d -> type_checks ct gamma e -> + type_checks ct gamma (E_Field e f) + | TC_New : forall c le, in_table ct c -> Forall (type_checks ct gamma) le -> type_checks ct gamma (E_New c le) + | TC_Invk : forall e m le d, type_of gamma (E_Invk e m le) d -> in_table ct d -> + type_checks ct gamma e -> Forall (type_checks ct gamma) le -> + type_checks ct gamma (E_Invk e m le) + | TC_Cast : forall e d, in_table ct d -> type_checks ct gamma e -> type_checks ct gamma (E_Cast d e). + + Inductive fj_expr : expr -> Prop := + | FJ_Var : forall x, fj_expr (E_Var x) + | FJ_Field : forall e f, fj_expr e -> fj_expr (E_Field e f) + | FJ_New : forall c le, Forall fj_expr le -> fj_expr (E_New c le) + | FJ_Invk : forall e m le, + fj_expr e -> Forall fj_expr le -> + fj_expr (E_Invk e m le) + | FJ_Cast : forall e d, fj_expr e -> fj_expr (E_Cast d e). + + Inductive valid_expr (ct : class_table) (gamma : context) : expr -> Prop := + | Val_Var : forall x, type_checks ct gamma (E_Var x) -> valid_expr ct gamma (E_Var x) + | Val_Field : forall e f c, + type_checks ct gamma (E_Field e f) -> + type_of gamma e c -> + (exists d, declaring_class f c = Some d) -> + valid_expr ct gamma e -> + valid_expr ct gamma (E_Field e f) + | Val_New : forall c le, + type_checks ct gamma (E_New c le) -> + Forall (valid_expr ct gamma) le -> + valid_expr ct gamma (E_New c le) + | Val_Invk : forall e m le c, + type_checks ct gamma (E_Invk e m le) -> + valid_expr ct gamma e -> + Forall (valid_expr ct gamma) le -> + type_of gamma e c -> + (exists d, mresolve m c = Some d) -> + valid_expr ct gamma (E_Invk e m le) + | Val_Cast : forall c e, + type_checks ct gamma (E_Cast c e) -> valid_expr ct gamma e -> valid_expr ct gamma (E_Cast c e) + | Val_Lib : valid_expr ct gamma E_Lib. + + Definition calP (ct : class_table) (gamma : context) (e : expr) (lpt : set expr) := + type_checks ct gamma e /\ (forall e0, set_In e0 lpt -> type_checks ct gamma e0). + +End props. +Section prop_lemmas. + Axiom sub_keep_type : forall (gamma : context) (sig : subst) (e : expr) (c : class), + type_of gamma e c -> type_of gamma (do_sub sig e) c. + + Lemma type_of_fn : forall gamma e c d, + type_of gamma e c -> type_of gamma e d -> c = d. + Proof. + intros gamma e c d fc fd. generalize dependent d. + induction fc; intros d0 fd0; inversion fd0; trivial. + - assert (c = c0). apply IHfc; trivial. + rewrite <- H5 in H4. rewrite H4 in H. inversion H. trivial. + - assert (c0 = c1). apply IHfc; trivial. + rewrite H14 in H. rewrite H in H8. inversion H8; trivial. + Qed. + +End prop_lemmas. + +Section list_inductions. + Definition expr_rect_list := + fun (P : expr -> Type) (Q : list expr -> Type) + (g : Q nil) (h : forall e l, P e -> Q l -> Q (e :: l)) + (f : forall v : var, P (E_Var v)) + (f0 : forall e : expr, P e -> forall f0 : field_id, P (E_Field e f0)) + (f1 : forall (c : class) (l : list expr), Q l -> P (E_New c l)) + (f2 : forall e : expr, P e -> forall (m : method_id) (l : list expr), Q l -> P (E_Invk e m l)) + (f3 : forall (c : class) (e : expr), P e -> P (E_Cast c e)) (f4 : P E_Lib) => + fix F (e : expr) : P e := + match e as e0 return (P e0) with + | E_Var v => f v + | E_Field e0 f5 => f0 e0 (F e0) f5 + | E_New c l => f1 c l (list_rect Q g (fun u r => h u r (F u)) l) + | E_Invk e0 m l => f2 e0 (F e0) m l (list_rect Q g (fun u r => h u r (F u)) l) + | E_Cast c e0 => f3 c e0 (F e0) + | E_Lib => f4 + end. + + Definition expr_ind_list := + fun (P : expr -> Prop) + (f : forall v : var, P (E_Var v)) + (f0 : forall e : expr, P e -> forall f0 : field_id, P (E_Field e f0)) + (f1 : forall (c : class) (l : list expr), Forall P l -> P (E_New c l)) + (f2 : forall e : expr, P e -> forall (m : method_id) (l : list expr), Forall P l -> P (E_Invk e m l)) + (f3 : forall (c : class) (e : expr), P e -> P (E_Cast c e)) + (f4 : P E_Lib) => + fix F (e : expr) : P e := + match e as e0 return (P e0) with + | E_Var v => f v + | E_Field e0 f5 => f0 e0 (F e0) f5 + | E_New c l => f1 c l (list_rect (Forall P) (Forall_nil P) (fun u _ => (Forall_cons u (F u))) l) + | E_Invk e0 m l => f2 e0 (F e0) m l (list_rect (Forall P) (Forall_nil P) (fun u _ => Forall_cons u (F u)) l) + | E_Cast c e0 => f3 c e0 (F e0) + | E_Lib => f4 + end. + + Theorem alpha_ind_list : + forall (ct ct' : class_table) (gamma : context) (P : expr -> expr -> set expr -> Prop), + (forall (e e' : expr) (f : field_id) (lpt : set expr), + alpha ct ct' gamma e e' lpt -> P e e' lpt -> P (E_Field e f) (E_Field e' f) lpt) -> + (forall (e : expr) (c d : class) (f0 : field_id) (lpt : set expr), + alpha ct ct' gamma e E_Lib lpt -> + P e E_Lib lpt -> + declaring_class f0 c = Some d -> in_lib ct d -> type_of gamma e c -> P (E_Field e f0) E_Lib lpt) -> + (forall (c : class) (le le' : list expr) (lpt : set expr), + in_table ct' c -> + length le = length le' -> + Forall (fun p : expr * expr => alpha ct ct' gamma (fst p) (snd p) lpt) (combine le le') -> + Forall (fun p : expr * expr => P (fst p) (snd p) lpt) (combine le le') -> + P (E_New c le) (E_New c le') lpt) -> + (forall (c : class) (le : list expr) (lpt : set expr), + in_lib ct c -> + Forall (fun e : expr => alpha ct ct' gamma e E_Lib lpt) le -> + Forall (fun e : expr => P e E_Lib lpt) le -> + P (E_New c le) E_Lib lpt) -> + (forall (e e' : expr) (le le' : list expr) (m : method_id) (lpt : set expr), + alpha ct ct' gamma e e' lpt -> + P e e' lpt -> + length le = length le' -> + Forall (fun p : expr * expr => alpha ct ct' gamma (fst p) (snd p) lpt) (combine le le') -> + Forall (fun p : expr * expr => P (fst p) (snd p) lpt) (combine le le') -> + P (E_Invk e m le) (E_Invk e' m le') lpt) -> + (forall (e : expr) (le : list expr) (mi : method_id) (lpt : set expr), + (exists c : class, in_lib ct c /\ In mi (dmethods_id c)) -> + alpha ct ct' gamma e E_Lib lpt -> + P e E_Lib lpt -> + Forall (fun e' : expr => alpha ct ct' gamma e' E_Lib lpt) le -> + Forall (fun e' : expr => P e' E_Lib lpt) le -> + P (E_Invk e mi le) E_Lib lpt) -> + (forall (e e' : expr) (c : class) (lpt : set expr), + alpha ct ct' gamma e e' lpt -> P e e' lpt -> P (E_Cast c e) (E_Cast c e') lpt) -> + (forall (e : expr) (ci : class) (lpt : set expr), + alpha ct ct' gamma e E_Lib lpt -> P e E_Lib lpt -> P (E_Cast ci e) E_Lib lpt) -> + (forall (e e' : expr) (lpt : set expr), + alpha ct ct' gamma e e' lpt -> P e e' lpt -> set_In e' lpt -> P e E_Lib lpt) -> + forall (e e0 : expr) (s : set expr), alpha ct ct' gamma e e0 s -> P e e0 s. + Admitted. + + (*Theorem alpha_ind_list : forall (ct ct' : class_table) (gamma : context) (P : expr * (expr * set expr) -> Prop), + (forall (e e' : expr) (f : field_id) (lpt : set expr), + alpha ct ct' gamma (e, (e', lpt)) -> P (e, (e', lpt)) -> P (E_Field e f, (E_Field e' f, lpt))) -> + (forall (e : expr) (c d : class) (f0 : field_id) (lpt : set expr), + alpha ct ct' gamma (e, (E_Lib, lpt)) -> + P (e, (E_Lib, lpt)) -> + declaring_class f0 c = Some d -> in_lib ct d -> type_of gamma e c -> P (E_Field e f0, (E_Lib, lpt))) -> + (forall (c : class) (le le' : list expr) (lpt : set expr), + in_table ct' c -> + length le = length le' -> + Forall (alpha ct ct' gamma) (combine le (combine le' (repeat lpt (length le')))) -> + Forall P (combine le (combine le' (repeat lpt (length le')))) -> + P (E_New c le, (E_New c le', lpt))) -> + (forall (c : class) (le : list expr) (lpt : set expr), + in_lib ct c -> + Forall (fun e : expr => alpha ct ct' gamma (e, (E_Lib, lpt))) le -> + Forall (fun e : expr => P (e, (E_Lib, lpt))) le -> + P (E_New c le, (E_Lib, lpt))) -> + (forall (e e' : expr) (le le' : list expr) (m : method_id) (lpt : set expr), + alpha ct ct' gamma (e, (e', lpt)) -> + P (e, (e', lpt)) -> + length le = length le' -> + Forall (alpha ct ct' gamma) (combine le (combine le' (repeat lpt (length le')))) -> + Forall P (combine le (combine le' (repeat lpt (length le')))) -> + P (E_Invk e m le, (E_Invk e' m le', lpt))) -> + (forall (e : expr) (le : list expr) (mi : method_id) (lpt : set expr), + (exists c : class, in_lib ct c /\ In mi (dmethods_id c)) -> + alpha ct ct' gamma (e, (E_Lib, lpt)) -> + P (e, (E_Lib, lpt)) -> + Forall (fun e' : expr => alpha ct ct' gamma (e', (E_Lib, lpt))) le -> + Forall (fun e : expr => P (e, (E_Lib, lpt))) le -> + P (E_Invk e mi le, (E_Lib, lpt))) -> + (forall (e e' : expr) (c : class) (lpt : set expr), + alpha ct ct' gamma (e, (e', lpt)) -> P (e, (e', lpt)) -> P (E_Cast c e, (E_Cast c e', lpt))) -> + (forall (e : expr) (ci : class) (lpt : set expr), + alpha ct ct' gamma (e, (E_Lib, lpt)) -> P (e, (E_Lib, lpt)) -> P (E_Cast ci e, (E_Lib, lpt))) -> + (forall (e e' : expr) (lpt : set expr), + alpha ct ct' gamma (e, (e', lpt)) -> P (e, (e', lpt)) -> set_In e' lpt -> P (e, (E_Lib, lpt))) -> + forall p : expr * (expr * set expr), alpha ct ct' gamma p -> P p. + Proof. admit. Admitted.*) + +End list_inductions. +Section ct_lib_lemmas. + Lemma in_lib_in_ct_lib : forall ct c, + in_lib ct c -> in_table (ct_lib ct) c. + Proof. + intros ct c in_lib. destruct ct as [app lib]. + simpl in in_lib. unfold in_table. right. simpl. trivial. + Qed. + + Lemma in_ct_lib_in_lib : forall (ct : class_table) (c : class), + in_table (ct_lib ct) c -> in_lib ct c. + Proof. + intros ct c in_ct_lib. + unfold in_table in in_ct_lib. destruct ct as [app lib]. + destruct in_ct_lib. + - inversion H. + - simpl. simpl in H. trivial. + Qed. + + Lemma valid_table_valid_lib : forall (ct : class_table), + valid_table ct -> valid_table (ct_lib ct). + Proof. + unfold valid_table. intros ct val_ct c in_ct_lib. destruct ct as (app, lib). + apply in_ct_lib_in_lib in in_ct_lib as in_lib; trivial. + induction c as [|d]. + - apply V_Obj; eauto. + - simpl. + assert (valid_class (app, lib) (C d l l0 l1)) as pfc. + { apply val_ct. unfold in_table. right. trivial. } + dependent destruction pfc. + assert (lib d). + { destruct H0. + - destruct H0. destruct H. split; trivial. + - apply H0. } + apply V_Class; eauto. + + apply IHd; eauto. apply in_lib_in_ct_lib. eauto. + + unfold not. intros. destruct H3. contradiction. + Qed. + + Lemma type_checks_lib_ct : forall (ct : class_table) (gamma : context) (e : expr), + valid_table ct -> type_checks (ct_lib ct) gamma e -> type_checks ct gamma e. + Proof. + intros ct gamma e pft typ_lib. + induction e using expr_ind_list. + - inversion typ_lib. apply TC_Var. unfold in_table. right. apply in_ct_lib_in_lib; trivial. + - inversion typ_lib. apply TC_Field with d; trivial. + + unfold in_table. right. apply in_ct_lib_in_lib; trivial. + + apply IHe; trivial. + - inversion typ_lib. apply TC_New; trivial. + + unfold in_table. right. apply in_ct_lib_in_lib; trivial. + + apply Forall_list_impl with (P := type_checks (ct_lib ct) gamma); trivial. + - inversion typ_lib. apply TC_Invk with d; trivial. + + unfold in_table. right. apply in_ct_lib_in_lib; trivial. + + apply IHe. trivial. + + apply Forall_list_impl with (P := type_checks (ct_lib ct) gamma); trivial. + - inversion typ_lib. apply TC_Cast; trivial. + + unfold in_table. right. apply in_ct_lib_in_lib; trivial. + + apply IHe; trivial. + - inversion typ_lib. + Qed. + + Lemma valid_expr_lib_ct : forall (ct : class_table) (gamma : context) (e : expr), + valid_table ct -> valid_expr (ct_lib ct) gamma e -> valid_expr ct gamma e. + Proof. + intros ct gamma e pft val_lib. + induction e using expr_ind_list. + - inversion val_lib. apply Val_Var; trivial. apply type_checks_lib_ct; trivial. + - inversion val_lib. apply Val_Field with c; trivial. + + apply type_checks_lib_ct; trivial. + + apply IHe; trivial. + - inversion val_lib. apply Val_New; trivial. + + apply type_checks_lib_ct; trivial. + + apply Forall_list_impl with (P := valid_expr (ct_lib ct) gamma); trivial. + - inversion val_lib. apply Val_Invk with c; trivial. + + apply type_checks_lib_ct; trivial. + + apply IHe; trivial. + + apply Forall_list_impl with (P := valid_expr (ct_lib ct) gamma); trivial. + - inversion val_lib. apply Val_Cast; trivial. + + apply type_checks_lib_ct; trivial. + + apply IHe; trivial. + - apply Val_Lib. + Qed. + + Lemma typ_check_in_lib_typ_in_lib : forall ct gamma e c, + type_checks (ct_lib ct) gamma e -> type_of gamma e c -> in_lib ct c. + Proof. + intros ct gamma e c typ_chk typ. + destruct e; inversion typ; inversion typ_chk. + - apply in_ct_lib_in_lib; trivial. + - assert (c = d0). apply type_of_fn with gamma (E_Field e f); trivial. + rewrite H9. apply in_ct_lib_in_lib; trivial. + - rewrite <- H5. apply in_ct_lib_in_lib; trivial. + - assert (c = d). apply type_of_fn with gamma (E_Invk e m l); trivial. + rewrite H16. apply in_ct_lib_in_lib; trivial. + - rewrite <- H0. apply in_ct_lib_in_lib; trivial. + Qed. +End ct_lib_lemmas. +Section lemmas. + Lemma mres_lib_in_lib : forall (ct : class_table) (m : method_id) (c e : class), + valid_class ct c -> in_lib ct c -> mresolve m c = Some e -> in_lib ct e. + Proof. + intros ct m c e pfc c_in_app c_res_e. + induction c as [|d]. + - inversion c_res_e. + - unfold mresolve in c_res_e. destruct (existsb (fun m' : nat => beq_nat m m') (dmethods_id (C d l l0 l1))). + + inversion c_res_e; trivial. + + fold mresolve in c_res_e. dependent destruction pfc. apply IHd; trivial. + destruct H0 as [[_ con] | [_ x]]; trivial. + destruct H. split; trivial. + Qed. + + Lemma find_In_var : forall lv v, + In v lv <-> find (fun v' => beq_var v' v) lv <> None. + Proof. + split; induction lv; intros; eauto; simpl; simpl in H. + - destruct H. + + rewrite H. rewrite <- beq_var_refl. unfold not. intro. inversion H0. + + destruct (beq_var a v); eauto. unfold not. intro. inversion H0. + - apply H. reflexivity. + - destruct (beq_var a v) eqn:beq_av. + + left. apply beq_var_true. eauto. + + right. apply IHlv. trivial. + Qed. + +End lemmas. + +Section eq_dec. + Lemma eq_var_dec : forall v v' : var, {v = v'} + {v <> v'}. + Proof. + intros. destruct v; destruct v'. + - assert ({v = v0} + {v <> v0}) by apply PeanoNat.Nat.eq_dec. + destruct H. + + left. rewrite e. reflexivity. + + right. unfold not. intros. inversion H. contradiction. + - right. unfold not. intro. inversion H. + - right. unfold not. intro. inversion H. + - left. trivial. + Qed. + + + Inductive Forallt {A : Set} (P : A -> Set) : list A -> Set := + | Forallt_nil : Forallt P nil + | Forallt_cons : forall a l, P a -> Forallt P l -> Forallt P (a :: l). + + Lemma eq_expr_class_dech : forall (e e' : expr) (c c' : class), ({e = e'} + {e <> e'}) * ({c = c'} + {c <> c'}). + Proof. + induction e using expr_rect_list with (Q := fun l => forall e', Forallt (fun e : expr => {e = e'} + {e <> e'}) l). + - intros. apply Forallt_nil. + - intros. assert (({e = e'} + {e <> e'}) * ({Obj = Obj} + {Obj <> Obj})). apply IHe. + destruct H. apply Forallt_cons; eauto. + - intros. destruct e'. + + assert ({ v = v0 } + {v <> v0}) by apply eq_var_dec. + destruct H. + * Admitted. (*left. rewrite e. reflexivity. + * right. unfold not. intros. inversion H. contradiction. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + - intros. destruct e'. + + right. unfold not. intro. inversion H. + + assert ({f = f0} + {f <> f0}) by apply PeanoNat.Nat.eq_dec. + assert ({e = e'} + {e <> e'}) by apply IHe. + destruct H; destruct H0. + * left. rewrite e0. rewrite e1. reflexivity. + * right. unfold not. intros. inversion H. contradiction. + * right. unfold not. intros. inversion H. symmetry in H2. contradiction. + * right. unfold not. intros. inversion H. contradiction. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + - intros. destruct e'. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + (* assert ({c = c0} + {c <> c0}) by apply PeanoNat.Nat.eq_dec. *) +Admitted. *) + + Lemma eq_class_dec : forall c c' : class, {c = c'} + {c <> c'}. + Proof. + intros. + assert (({E_Var This = E_Var This} + {E_Var This <> E_Var This}) * ({c = c'} + {c <> c'})). + apply eq_expr_class_dech. + destruct H. + apply s0. + Qed. + + Lemma eq_expr_dec : forall e e' : expr, {e = e'} + {e <> e'}. + Proof. + intros e. + induction e using expr_rect_list with (Q := fun l => forall e', Forallt (fun e : expr => {e = e'} + {e <> e'}) l). + - intros. apply Forallt_nil. + - intros. apply Forallt_cons; eauto. + - intros. destruct e'. + + assert ({ v = v0 } + {v <> v0}) by apply eq_var_dec. + destruct H. + * left. rewrite e. reflexivity. + * right. unfold not. intros. inversion H. contradiction. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + - intros. destruct e'. + + right. unfold not. intro. inversion H. + + assert ({f = f0} + {f <> f0}) by apply PeanoNat.Nat.eq_dec. + assert ({e = e'} + {e <> e'}) by apply IHe. + destruct H; destruct H0. + * left. rewrite e0. rewrite e1. reflexivity. + * right. unfold not. intros. inversion H. contradiction. + * right. unfold not. intros. inversion H. symmetry in H2. contradiction. + * right. unfold not. intros. inversion H. contradiction. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + - intros. destruct e'. + + right. unfold not. intro. inversion H. + + right. unfold not. intro. inversion H. + + (* assert ({c = c0} + {c <> c0}) by apply PeanoNat.Nat.eq_dec. *) + Admitted. + +End eq_dec. +Section reduction_rules. + Inductive FJ_reduce : expr -> expr -> Prop := + | R_Field : forall c f le ei n, + index_of (fun p => beq_nat f (snd p)) (fields c) = Some n -> + nth_error le n = Some ei -> + FJ_reduce (E_New c le) ei + | R_Invk : forall c m mi le newle, + valid_method m -> find_method mi c = Some m -> + FJ_reduce (E_Invk (E_New c newle) mi le) + (do_sub ((This, (E_New c newle)) :: (combine (args m) le)) (body m)) + | R_Cast : forall c d le, + subtype c d -> FJ_reduce (E_Cast d (E_New c le)) (E_New c le) + | RC_Field : forall e e' f, + FJ_reduce e e' -> FJ_reduce (E_Field e f) (E_Field e' f) + | RC_Invk_Recv : forall e e' m le, + FJ_reduce e e' -> FJ_reduce (E_Invk e m le) (E_Invk e' m le) + | RC_Invk_Arg : forall e m le le' e0 e0' n, + nth_error le n = Some e0 -> nth_error le' n = Some e0' -> + FJ_reduce e0 e0' -> FJ_reduce (E_Invk e m le) (E_Invk e m le') + | RC_New_Arg : forall c le le' e0 e0' n, + nth_error le n = Some e0 -> nth_error le' n = Some e0' -> + FJ_reduce e0 e0' -> FJ_reduce (E_New c le) (E_New c le') + | RC_Cast : forall c e e', + FJ_reduce e e' -> FJ_reduce (E_Cast c e) (E_Cast c e'). + + Variable f : nat -> set nat. + Variable a : set nat. + Check (a U a). + Inductive AVE_reduce (ct : class_table) : expr -> set expr -> expr -> set expr -> Prop := + | RA_FJ : forall e e' lpt, + FJ_reduce e e' -> AVE_reduce ct e lpt e' lpt + | RA_Field : forall f c d e lpt, + declaring_class f c = Some d -> in_lib ct d -> + AVE_reduce ct e lpt e (add (E_Field E_Lib f) lpt) + | RA_New : forall c e lpt, + in_lib ct c -> + AVE_reduce ct e lpt e (add (E_New c (repeat E_Lib (length (fields c)))) lpt) + | RA_Invk : forall m c e lpt, + In m (dmethods c) -> in_lib ct c -> + AVE_reduce ct e lpt e (add (E_Invk E_Lib (mid m) (repeat E_Lib (length (args m)))) lpt) + | RA_Cast : forall c lpt, AVE_reduce ct (E_Cast c E_Lib) lpt E_Lib lpt + | RA_Lib_Invk : forall mi c newle largs d lpt, + mresolve mi c = Some d -> in_lib ct d -> + AVE_reduce ct + (E_Invk (E_New c newle) mi largs) + lpt + E_Lib + (add (E_New c newle) (set_from_list largs U lpt)) + | RA_Return : forall e lpt, + set_In e lpt -> AVE_reduce ct E_Lib lpt e lpt + | RA_Sub : forall e e' lpt lpt' d, + set_In e lpt -> AVE_reduce ct e lpt e' lpt' -> + AVE_reduce ct d lpt d (add e' (lpt' U lpt)) + | RAC_Field : forall e e' lpt lpt' f, + AVE_reduce ct e lpt e' lpt' -> + AVE_reduce ct (E_Field e f) lpt (E_Field e' f) (lpt' U lpt) + | RAC_Invk_Recv : forall e e' m le lpt lpt', + AVE_reduce ct e lpt e' lpt' -> + AVE_reduce ct (E_Invk e m le) lpt (E_Invk e' m le) (lpt' U lpt) + | RAC_Invk_Arg : forall e m le le' e0 e0' n lpt lpt', + nth_error le n = Some e0 -> nth_error le' n = Some e0' -> + AVE_reduce ct e0 lpt e0' lpt' -> + AVE_reduce ct (E_Invk e m le) lpt (E_Invk e m le') (lpt' U lpt) + | RAC_New_Arg : forall c le le' e0 e0' n lpt lpt', + nth_error le n = Some e0 -> nth_error le' n = Some e0' -> + AVE_reduce ct e0 lpt e0' lpt' -> + AVE_reduce ct (E_New c le) lpt (E_New c le') (lpt' U lpt) + | RAC_Cast : forall c e e' lpt lpt', + AVE_reduce ct e lpt e' lpt' -> + AVE_reduce ct (E_Cast c e) lpt (E_Cast c e') (lpt' U lpt). + + Inductive AVE_reduce' (ct : class_table) : expr -> set expr -> expr -> set expr -> Prop := + | RA'_refl : forall e lpt, AVE_reduce' ct e lpt e lpt + | RA'_step : forall e lpt e' lpt' e'' lpt'', + AVE_reduce ct e lpt e' lpt' -> + AVE_reduce' ct e' lpt' e'' lpt'' -> + AVE_reduce' ct e lpt e'' lpt''. + +End reduction_rules. +Lemma lemma1 : forall (ct : class_table) (c e : class) (m : method_id), + valid_class ct c -> mresolve m c = Some e -> in_app ct e -> in_app ct c. +Proof. + intros ct c e m pfc c_res_e e_in_app. induction c as [| d]. + - intros. inversion c_res_e. + - unfold mresolve in c_res_e. destruct (existsb (fun m' : nat => beq_nat m m') (dmethods_id (C d l l0 l1))). + + inversion c_res_e. rewrite H0. trivial. + + fold mresolve in c_res_e. dependent destruction pfc. + assert (in_app ct d). apply IHd; trivial. + destruct H0. + * apply H0. + * destruct d. + -- inversion pfc. contradiction. + -- inversion pfc. destruct H8. split; eauto. apply H0. +Qed. + +Lemma lemma2 : forall ct ct' c m e, + ave_rel ct ct' -> valid_class ct c -> valid_class ct' c -> + in_app ct c -> mresolve m c = Some e -> + in_app ct e \/ in_lib ct' e. +Proof. + intros ct ct' c m e rel pfc pfc' c_in_app c_res_e. + induction c as [|d]. + (* C is Obj *) + - inversion pfc. contradiction. + (* c extends d *) + - unfold mresolve in c_res_e. destruct (existsb (fun m' : nat => beq_nat m m') (dmethods_id (C d l l0 l1))). + (* m-res *) + + left. inversion c_res_e. trivial. + (* m-res-inh *) + + fold mresolve in c_res_e. dependent destruction pfc. dependent destruction pfc'. + destruct H0 as [[d_in_app _] | [_ d_in_lib]]. + (* d in app - use induction hypothesis *) + * apply IHd; trivial. + (* d in lib - use averroes transformation properties *) + * right. apply mres_lib_in_lib with m d; trivial. + inversion rel as [_ [_ [keep_app keep_lib]]]. + apply keep_lib with (C d l l0 l1); simpl; trivial. + unfold in_table. left. apply keep_app. trivial. +Qed. + +Lemma lemma3 : forall ct ct' lv le le' gamma e0 lpt, + ave_rel ct ct' -> + (length lv = length le) -> (length lv = length le') -> + (forall v, expr_In v e0 -> In v lv) -> + (Forall (fun p => alpha ct ct' gamma (fst p) (snd p) lpt) (combine le le')) -> + type_checks ct' gamma e0 -> fj_expr e0 -> + alpha ct ct' gamma (do_sub (combine lv le) e0) (do_sub (combine lv le') e0) lpt. +Proof. + intros ct ct' lv le le' gamma e0 lpt rel lenve lenve' valid_body sub_rel typ_chk fj_expr. + induction e0 using expr_ind_list. + (* Case Var *) + - simpl. destruct (find (fun p : var * expr => beq_var (fst p) v) (combine lv le)) eqn:sigv. + + destruct (find (fun p0 : var * expr => beq_var (fst p0) v) (combine lv le')) eqn:sigv'. + * assert (In (snd p, snd p0) (combine le le')). + { apply find_pair_in_zip with (la := lv) (f := (fun v' => beq_var v' v)); trivial. } + destruct p. destruct p0. simpl in H. + assert (alpha ct ct' gamma (fst (e, e0)) (snd (e, e0)) lpt). + { apply Forall_In with (l := combine le le') (a := (e, e0)); trivial. } + eauto. + * apply (extract_combine (fun v' => beq_var v' v) lv le' lenve') in sigv'. + assert (In v lv). apply valid_body. apply EIn_Var. + apply find_In_var in H. contradiction. + + apply (extract_combine (fun v' => beq_var v' v) lv le lenve) in sigv. + assert (In v lv). apply valid_body. apply EIn_Var. + apply find_In_var in H. contradiction. + (* Case Field *) + - simpl. inversion typ_chk. inversion fj_expr. apply Rel_Field; eauto. apply IHe0; eauto. + intros. apply EIn_Field with (f := f0) in H7. apply valid_body; trivial. + (* Case New *) + - simpl. inversion typ_chk. inversion fj_expr. apply Rel_New; eauto. + + rewrite map_length, map_length. reflexivity. + + clear typ_chk H1 H6 fj_expr. induction l. + * apply Forall_nil. + * inversion H. inversion H3. inversion H5. apply Forall_cons; eauto. + -- simpl. apply H7; eauto. + intros. apply valid_body; eauto. + apply EIn_New; eauto. + -- apply IHl; eauto. + intros. apply valid_body. apply EIn_New. inversion H17. + apply Exists_cons_tl; eauto. + (* Case Invk *) + - simpl. inversion typ_chk. inversion fj_expr. apply Rel_Invk; eauto. + + apply IHe0; eauto. intros. apply valid_body. apply EIn_Invk; eauto. + + rewrite map_length, map_length. reflexivity. + + clear H2 H3 typ_chk fj_expr H10. induction l. + * apply Forall_nil. + * inversion H. inversion H6. inversion H11. apply Forall_cons; eauto. + -- simpl. apply H10; eauto. + intros. apply valid_body; eauto. + apply EIn_Invk; eauto. + -- apply IHl; eauto. + intros. apply valid_body. apply EIn_Invk. inversion H21. destruct H24; eauto. + - simpl. inversion typ_chk. inversion fj_expr. apply Rel_Cast; eauto. + apply IHe0; eauto. intros. apply valid_body. apply EIn_Cast; eauto. + - inversion fj_expr. +Qed. + +Lemma lemma4 : forall ct ct' lv le gamma e0 lpt, + ave_rel ct ct' -> + length lv = length le -> + (forall v, expr_In v e0 -> In v lv) -> + (Forall (fun e => alpha ct ct' gamma e E_Lib lpt) le) -> + valid_expr (ct_lib ct) gamma e0 -> fj_expr e0 -> + alpha ct ct' gamma (do_sub (combine lv le) e0) E_Lib lpt. +Proof. + intros ct ct' lv le gamma e0 lpt rel lenve valid_body sub_rel val_in_lib fj_expr. + apply valid_expr_lib_ct in val_in_lib as val_in_ct. inversion rel as [pft [pft' [keep_app keep_lib]]]. + induction e0 using expr_ind_list; eauto. + - simpl. destruct (find (fun p : var * expr => beq_var (fst p) v) (combine lv le)) eqn:sigv. + + apply find_some in sigv. destruct sigv. destruct p. apply zip_In_r in H. + apply Forall_In with (l := le) (a := e); eauto. + + apply (extract_combine (fun v' => beq_var v' v) lv le lenve) in sigv. + assert (In v lv). apply valid_body. apply EIn_Var. + apply find_In_var in H. contradiction. + - simpl. inversion val_in_lib. inversion val_in_ct. inversion fj_expr. destruct H3 as [d decl]. + apply Rel_Lib_Field with c d; eauto. + + apply IHe0; eauto. + intros. apply valid_body. apply EIn_Field. eauto. + + assert (in_lib ct c). inversion H1. apply typ_check_in_lib_typ_in_lib with gamma e0; trivial. + apply decl_of_lib_in_lib with c f0; trivial. + + apply sub_keep_type; trivial. + - simpl. inversion val_in_lib. inversion val_in_ct. inversion fj_expr. + apply Rel_Lib_New; eauto. + + inversion H2. apply in_ct_lib_in_lib; trivial. + + assert (Forall (fun e0 => (forall v : var, expr_In v e0 -> In v lv)) l). + { apply Forall_forall. intros. apply valid_body. + apply EIn_New. apply Exists_exists; eauto. } + apply Forall_list_impl with (P := fun e0 => (forall v, expr_In v e0 -> In v lv)) in H; trivial. + apply Forall_list_impl with (P := valid_expr (ct_lib ct) gamma) in H; trivial. + apply Forall_list_impl with (P := valid_expr ct gamma) in H; trivial. + apply Forall_list_impl with (P := Top.fj_expr) in H; trivial. + rewrite Forall_map_swap. trivial. + - simpl. inversion val_in_lib. inversion val_in_ct. inversion fj_expr. + apply Rel_Lib_Invk; eauto. + + destruct H7 as [d mres_d]. exists d. + assert (in_lib ct c). + { inversion H3. apply typ_check_in_lib_typ_in_lib with gamma e0; trivial. } + split. + * apply mres_lib_in_lib with m c; trivial. + apply pft. unfold in_table. right; trivial. + * apply mresolve_in_methods with c; trivial. + + apply IHe0; eauto. intros. apply valid_body. apply EIn_Invk. eauto. + + assert (Forall (fun e0 => (forall v : var, expr_In v e0 -> In v lv)) l). + { apply Forall_forall. intros. apply valid_body. + apply EIn_Invk. left. apply Exists_exists; eauto. } + apply Forall_list_impl with (P := fun e0 => (forall v, expr_In v e0 -> In v lv)) in H; trivial. + apply Forall_list_impl with (P := valid_expr (ct_lib ct) gamma) in H; trivial. + apply Forall_list_impl with (P := valid_expr ct gamma) in H; trivial. + apply Forall_list_impl with (P := Top.fj_expr) in H; trivial. + rewrite Forall_map_swap. trivial. + - simpl. inversion val_in_lib. inversion val_in_ct. inversion fj_expr. + apply Rel_Lib_Cast. apply IHe0; eauto. + intros. apply valid_body. apply EIn_Cast. eauto. + - inversion fj_expr. + - inversion rel; trivial. +Qed. + +Lemma lemma5 : forall ct ct' gamma e e' lpt lpt', + alpha ct ct' gamma e e' lpt -> alpha ct ct' gamma e e' (lpt U lpt'). +Proof. + intros ct ct' gamma e e' lpt lpt' rel. + induction rel using alpha_ind_list; eauto. + - apply Rel_Field; trivial. + - apply Rel_Lib_Field with c d; trivial. + - apply Rel_New; trivial. + - apply Rel_Lib_New; trivial. + - apply Rel_Invk; trivial. + - apply Rel_Lib_Invk; trivial. + - apply Rel_Cast; trivial. + - apply Rel_Lib_Cast; trivial. + - apply Rel_Lpt with e'; trivial. + apply union_introl; trivial. +Qed. + +Definition not_derived_by_Rel_Lpt + {ct ct' : class_table} {gamma : context} + {e : expr} {y' : expr} {lpt : set expr} + (rel : alpha ct ct' gamma e y' lpt) : Prop := + match y' as y return alpha ct ct' gamma e y lpt -> Prop with + | E_Lib => fun rel => ~ exists pfe ine, rel = Rel_Lpt ct ct' gamma e E_Lib lpt pfe ine + | _ => fun _ => True + end rel. + +(* + +Inductive eg : nat -> Prop := +| eg1 : forall n, eg n +| eg2 : forall n, eg n. + +Lemma silly : eg1 0 <> eg2 0. +Proof. unfold not. intros. discriminate H. + +Definition eg_rect := +fun (P : forall n : nat, eg n -> Prop) (f : forall n : nat, P (S n) (eg1 n)) (f0 : P 5 eg2) (n : nat) (e : eg n) => +match e as e0 in (eg n0) return (P n0 e0) with +| eg1 x => f x +| eg2 => f0 +end. + +Definition silly (p : eg1 4 = eg2) := + match p in _ = e return match e as e0 in (eg 5) return Prop with + | eg2 => False + | _ => True + end + with + | eq_refl => I + end. + +Lemma aslkjasdg : forall ct ct' gamma e c d f lpt H0 e0 i t pfe ine, + Rel_Lib_Field ct ct' gamma e c d f lpt H0 e0 i t = Rel_Lpt ct ct' gamma (E_Field e f) E_Lib lpt pfe ine -> False. +Proof. intros. + +Lemma lemma6 : forall ct ct' gamma e e' lpt, + ave_rel ct ct' -> alpha ct ct' gamma e e' lpt -> calP ct' gamma e' lpt -> + exists y', calP ct' gamma e' lpt /\ + (exists pf : alpha ct ct' gamma e y' lpt, not_derived_by_Rel_Lpt pf) /\ + AVE_reduce' ct' e' lpt y' lpt. +Proof. + intros. + remember H0 as H0'. + remember e' as e'rem. + destruct H0. + + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. rewrite <- simpl. rewrite HeqH0'. simpl. + unfold not. intros exst. destruct exst as [pfe [ine abasdg]]. + rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists e'. split; eauto. split. rewrite <- Heqe'rem. exists H0'. apply I. rewrite <- Heqe'rem. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. + - exists (E_Field e' f). split; trivial. split. exists H0'. apply I. apply RA'_refl. *) +Lemma lemma7addextra : forall A (ns lpt' lpt : set A), + ns U lpt' U lpt = (ns U lpt') U ns U lpt. +Proof. + intros. + rewrite (union_comm ns lpt'). rewrite union_assoc. + rewrite <- (union_assoc ns ns lpt). rewrite union_same. + rewrite <- union_assoc. rewrite (union_comm ns lpt'). + rewrite union_assoc. reflexivity. +Qed. + +Lemma lemma7 : forall ct' e e' lpt lpt' ns, + AVE_reduce ct' e lpt e' lpt' -> AVE_reduce ct' e (union ns lpt) e' (union ns lpt'). +Proof. + intros ct' e e' lpt lpt' ns reduce. + induction reduce. + - apply RA_FJ; trivial. + - rewrite union_addr. apply RA_Field with c d; trivial. + - rewrite union_addr. apply RA_New; trivial. + - rewrite union_addr. apply RA_Invk with c; trivial. + - apply RA_Cast; trivial. + - rewrite union_addr. rewrite <- union_assoc. + rewrite (union_comm ns (set_from_list largs)). rewrite union_assoc. + apply RA_Lib_Invk with d; trivial. + - apply RA_Return; trivial. apply union_intror. apply H. + - rewrite union_addr. rewrite <- union_assoc. rewrite (union_comm ns lpt'). rewrite union_assoc. + assert (lpt' U ns U lpt = (ns U lpt') U ns U lpt). + { rewrite <- (union_assoc (ns U lpt') ns lpt). + rewrite (union_comm ns lpt'). rewrite (union_assoc lpt' ns ns). + rewrite union_same. rewrite union_assoc. reflexivity. } + rewrite H0. + apply RA_Sub with e; trivial. apply union_intror. apply H. + - rewrite lemma7addextra. apply RAC_Field; trivial. + - rewrite lemma7addextra. apply RAC_Invk_Recv; trivial. + - rewrite lemma7addextra. apply RAC_Invk_Arg with e0 e0' n; trivial. + - rewrite lemma7addextra. apply RAC_New_Arg with e0 e0' n; trivial. + - rewrite lemma7addextra. apply RAC_Cast; trivial. +Qed. + +Lemma lemma8 : forall ct' e e' lpt lpt', + AVE_reduce ct' e lpt e' lpt' -> subset lpt lpt'. +Proof. + intros. unfold subset. unfold E.Included. + induction H; intros; + solve [ apply union_introl; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial] + | apply union_intror; solve [ apply union_introl; reflexivity || trivial + | apply union_intror; reflexivity || trivial + | reflexivity || trivial] + | reflexivity || trivial]. +Qed. + + +Lemma lemma9setfromlist : forall {A : Type} (l : list A) (n : nat) (a : A), + length l = S n -> nth_error l n = Some a -> + set_from_list (first_n l (S n)) = add a (set_from_list (first_n l n)). +Proof. + induction l; intros; simpl; inversion H. + destruct n; rewrite H2; inversion H0. + - simpl. destruct l; simpl; reflexivity. + - simpl. rewrite IHl with n a0; trivial. + unfold add. unfold E.Add. rewrite union_assoc. rewrite (union_comm (E.Singleton A a0) (E.Singleton A a)). + rewrite <- union_assoc. reflexivity. +Qed. + +Lemma lemma9 : forall ct' n le e0 llpt lpt0, + length le = S n -> length llpt = S n -> + hd_error le = Some e0 -> hd_error llpt = Some lpt0 -> + e0 <> E_Lib -> set_In e0 lpt0 -> + (forall m e lpt e0 lpt0, + m < n -> nth_error le m = Some e -> nth_error llpt m = Some lpt -> + nth_error le (S m) = Some e0 -> nth_error llpt (S m) = Some lpt0 -> + AVE_reduce ct' e lpt e0 lpt0) -> + (forall m lpt lpt0, + m < n -> nth_error llpt m = Some lpt -> nth_error llpt (S m) = Some lpt0 -> + AVE_reduce ct' E_Lib (set_from_list (first_n le (S m)) U lpt) + E_Lib (set_from_list (first_n le (S (S m))) U lpt0)). +Proof. + induction n. + - intros le e0 llpt lpt0 len_le len_llpt hde0 hdlpt0 neq_lib_e0 in_e_lpt0 + n_reduce m lpt_m lpt_sm le_m_n index_lpt_m index_lpt_sm. + inversion le_m_n. + - intros le e0 llpt lpt0 len_le len_llpt hde0 hdlpt0 neq_lib_e0 in_e_lpt0 + n_reduce m lpt_m lpt_sm le_m_n index_lpt_m index_lpt_sm. + destruct le; inversion len_le. + destruct llpt; inversion len_llpt. + inversion hde0. inversion hdlpt0. + assert ({ m = n } + { m <> n }) by apply PeanoNat.Nat.eq_dec. destruct H. + + subst m. subst e0. + assert (exists e', nth_error (e :: le) n = Some e'). + { apply get_nth with (n0 := S (S n)); trivial. + apply le_S. apply le_m_n. } + destruct H as [e_m index_e_m]. + assert (exists e', nth_error (e :: le) (S n) = Some e'). + { apply get_nth with (n0 := S (S n)); trivial. + apply Lt.lt_n_S. apply le_m_n. } + destruct H as [e_Sm index_e_Sm]. + assert (AVE_reduce ct' e_m lpt_m e_Sm lpt_sm). + { apply n_reduce with n; trivial. } + assert (AVE_reduce ct' e_m (set_from_list (first_n (e :: le) (S n)) U lpt_m) + e_Sm (set_from_list (first_n (e :: le) (S n)) U lpt_sm)). + { apply lemma7; trivial. } + assert (set_from_list (first_n (e :: le) (S (S n))) = add e_Sm (set_from_list (first_n (e :: le) (S n)))). + { apply lemma9setfromlist; trivial. } + rewrite H4. rewrite union_addl. + assert (lpt_sm = lpt_sm U lpt_m). + { apply union_include. apply lemma8 with ct' e_m e_Sm; trivial. } + rewrite H5. rewrite (union_comm lpt_sm lpt_m). rewrite <- union_assoc. + remember (set_from_list (first_n (e :: le) (S n)) U lpt_m) as lpt_m'. + rewrite <- (union_same lpt_m'). + rewrite (union_comm (lpt_m' U lpt_m')). + rewrite <- union_assoc. + rewrite union_same. + apply RA_Sub with e_m; trivial. + * rewrite Heqlpt_m'. apply union_introl. apply In_list_set_In_list. apply nth_error_In with n. + apply nth_error_first_n. apply index_e_m. + * rewrite union_comm. rewrite Heqlpt_m'. rewrite union_assoc. rewrite (union_comm lpt_m). + rewrite <- (union_include lpt_m lpt_sm). rewrite <- Heqlpt_m'. apply H2. + apply lemma8 with ct' e_m e_Sm. trivial. + + subst e. subst s. + rewrite remove_last_first_n. + rewrite (remove_last_first_n (e0 :: le) (S (S m))). + apply IHn with e0 (remove_last (lpt0 :: llpt)) lpt0; trivial. + * rewrite <- (remove_last_length (e0 :: le)). reflexivity. trivial. + * rewrite <- (remove_last_length (lpt0 :: llpt)). reflexivity. trivial. + * destruct le. inversion len_le. reflexivity. + * destruct llpt. inversion len_llpt. reflexivity. + * intros. apply n_reduce with m0; eauto; + rewrite remove_last_nth_error; eauto; rewrite len_le || rewrite len_llpt; apply Lt.lt_n_S; + solve [apply Lt.lt_S; trivial | apply Lt.lt_n_S; trivial]. + * inversion le_m_n. contradiction. apply H2. + * rewrite <- remove_last_nth_error. trivial. rewrite len_llpt. apply Lt.lt_n_S. trivial. + * rewrite <- remove_last_nth_error. trivial. rewrite len_llpt. + apply Lt.lt_n_S. apply Lt.lt_n_S. inversion le_m_n. contradiction. apply H2. + * rewrite len_le. apply Lt.lt_n_S. apply Lt.lt_n_S. inversion le_m_n. contradiction. apply H2. + * rewrite len_le. apply Lt.lt_n_S. apply le_m_n. +Qed. + +Lemma E_Lib_dec : forall e, e = E_Lib \/ e <> E_Lib. +Proof. + intros. destruct e; solve [left; trivial | right; discriminate]. +Qed. + +Lemma use_lemma_9_1 : forall ct' e lpt e' lpt', + AVE_reduce' ct' e lpt e' lpt' -> exists le llpt n, + length le = S n /\ length llpt = S n /\ + hd_error le = Some e /\ hd_error llpt = Some lpt /\ + last_error le = Some e' /\ last_error llpt = Some lpt' /\ + (forall m e lpt e0 lpt0, + m < n -> nth_error le m = Some e -> nth_error llpt m = Some lpt -> + nth_error le (S m) = Some e0 -> nth_error llpt (S m) = Some lpt0 -> + AVE_reduce ct' e lpt e0 lpt0). +Proof. + intros. induction H. + - exists (e :: nil). exists (lpt :: nil). exists 0. + split; split; split; split; split; split; trivial || intros. inversion H. + - destruct IHAVE_reduce' as [le [llpt [n [len_le [len_llpt [hd_le [hd_llpt [last_le [last_llpt AVE_each]]]]]]]]]. + exists (e :: le). exists (lpt :: llpt). exists (S n). + split; try split; try split; try split; try split; try split. + + simpl. rewrite len_le. reflexivity. + + simpl. rewrite len_llpt. reflexivity. + + simpl. destruct le; inversion len_le. rewrite last_le. reflexivity. + + simpl. destruct llpt; inversion len_llpt. rewrite last_llpt. reflexivity. + + intros. destruct m. + * inversion H2. inversion H3. inversion H4. inversion H5. + destruct le; inversion len_le. destruct llpt; inversion len_llpt. + subst e0. subst lpt0. inversion hd_le. inversion hd_llpt. subst e2. subst s. + inversion H9. inversion H10. subst e1. subst lpt1. trivial. + * apply AVE_each with m; try assumption. + apply Lt.lt_S_n. apply H1. +Qed. + +Lemma unuse_lemma_9_1 : forall n ct' e lpt e' lpt' le llpt, + length le = S n -> length llpt = S n -> + hd_error le = Some e -> hd_error llpt = Some lpt -> + last_error le = Some e' -> last_error llpt = Some lpt' -> + (forall m e lpt e0 lpt0, + m < n -> nth_error le m = Some e -> nth_error llpt m = Some lpt -> + nth_error le (S m) = Some e0 -> nth_error llpt (S m) = Some lpt0 -> + AVE_reduce ct' e lpt e0 lpt0) -> + AVE_reduce' ct' e lpt e' lpt'. +Proof. + induction n. + - intros. + destruct le; inversion H1. destruct le; inversion H. + destruct llpt; inversion H4. destruct llpt; inversion H0. + subst e0. inversion H8. subst s. inversion H2. inversion H3. + subst e'. subst lpt'. apply RA'_refl. + - intros ct' e lpt e' lpt' le llpt len_le len_llpt hd_le hd_llpt last_le last_llpt AVE_each. + destruct le as [| e0 le']; inversion len_le as [len_le']. + destruct le' as [| e1 le'']; inversion len_le' as [len_le'']. + destruct llpt as [| lpt0 llpt']; inversion len_llpt as [len_llpt']. + destruct llpt' as [| lpt1 llpt'']; inversion len_llpt' as [len_llpt'']. + apply RA'_step with e1 lpt1. + + apply AVE_each with 0; trivial. unfold lt. apply le_n_S. apply le_0_n. + + apply IHn with (e1 :: le'') (lpt1 :: llpt''); trivial. + intros. apply AVE_each with (S m); try assumption. + apply Lt.lt_n_S. assumption. +Qed. + +Lemma lemma10 : forall ct ct' gamma e0 e0' e' lpt lpt', + alpha ct ct' gamma e0 E_Lib lpt -> alpha ct ct' gamma e0' e' lpt' -> + FJ_reduce e0 e0' -> AVE_reduce' ct' E_Lib lpt e' lpt' -> exists lpt'', + alpha ct ct' gamma e0' E_Lib lpt'' /\ AVE_reduce' ct' E_Lib lpt E_Lib lpt''. +Proof. + intros. destruct (E_Lib_dec e'). + - exists lpt'. subst e'. split; trivial. + - dependent induction H2; try (destruct H3; reflexivity). + destruct (E_Lib_dec e'). + + assert (exists lpt'' : set expr, + alpha ct ct' gamma e0' E_Lib lpt'' /\ AVE_reduce' ct' E_Lib lpt' E_Lib lpt''). + { apply IHAVE_reduce'; trivial. + - rewrite (union_include lpt lpt'). + + rewrite union_comm. apply lemma5. trivial. + + apply lemma8 with ct' E_Lib e'; trivial. } + destruct H6 as [lpt''0 [alph AVE_red]]. + exists lpt''0. split; trivial. + subst e'. apply RA'_step with E_Lib lpt'; trivial. + + inversion H2. + * inversion H6. + * symmetry in H10. contradiction. + * symmetry in H9. contradiction. + * symmetry in H10. contradiction. + * subst lpt. subst lpt'. subst e'. rename e'' into e'. rename lpt'' into lpt'. + assert (exists lpt''', AVE_reduce' ct' E_Lib lpt0 E_Lib lpt''' /\ + subset lpt' lpt''' /\ + set_In e' lpt'''). + { apply use_lemma_9_1 in H3 as H7. + destruct H7 as [le [llpt [n [len_le [len_llpt [hd_le [hd_llpt [last_le [last_llpt AVE_each]]]]]]]]]. + assert (forall m lpt lpt0, + m < n -> nth_error llpt m = Some lpt -> nth_error llpt (S m) = Some lpt0 -> + AVE_reduce ct' E_Lib (set_from_list (first_n le (S m)) U lpt) + E_Lib (set_from_list (first_n le (S (S m))) U lpt0)). + apply lemma9 with e lpt0; assumption. + exists (set_from_list (first_n le (S n)) U lpt'). split; try split. + - apply unuse_lemma_9_1 with n (repeat E_Lib (S n)) + (map (fun p => set_from_list (first_n le (S (fst p))) U (snd p)) + (zip_with_ind llpt)); trivial. + + apply repeat_length. + + rewrite map_length. rewrite zip_with_ind_length. trivial. + + destruct llpt; inversion hd_llpt. subst s. + simpl. f_equal. destruct le; inversion hd_le. subst e1. + replace (first_n (e :: le) 1) with (e :: nil) by (destruct le; reflexivity). + symmetry. rewrite union_comm. apply union_include. + unfold subset. unfold E.Included. intros. simpl in H8. destruct H8; inversion H8. + subst x. apply H6. + + apply last_repeat. + + remember (n, lpt') as p. + replace n with (fst p) by (rewrite Heqp; reflexivity). + replace lpt' with (snd p) by (rewrite Heqp; reflexivity). + apply last_error_map with (a := p). + rewrite Heqp. apply last_error_zip_with_ind; trivial. + + intros. destruct n. inversion H8. + assert (exists lpt_m, nth_error llpt m = Some lpt_m). + { apply nth_error_better_Some. rewrite len_llpt. apply le_S. apply H8. } + assert (exists lpt_Sm, nth_error llpt (S m) = Some lpt_Sm). + { apply nth_error_better_Some. rewrite len_llpt. apply le_n_S. apply H8. } + destruct H13 as [lpt_m Hlpt_m]. destruct H14 as [lpt_Sm Hlpt_Sm]. + replace lpt with (set_from_list (first_n le (S m)) U lpt_m). + replace lpt1 with (set_from_list (first_n le (S (S m))) U lpt_Sm). + replace e1 with E_Lib. replace e2 with E_Lib. + * apply H7; trivial. + * symmetry. apply repeat_spec with (S (S n)). apply nth_error_In with (S m). trivial. + * symmetry. apply repeat_spec with (S (S n)). apply nth_error_In with m. trivial. + * apply nth_error_zip_with_ind in Hlpt_Sm. + apply nth_error_map with (f := (fun p => set_from_list (first_n le (S (fst p))) U snd p)) in Hlpt_Sm. + assert (Some (set_from_list (first_n le (S (S m))) U lpt_Sm) = Some lpt1). + { rewrite <- H12. symmetry. apply Hlpt_Sm. } + inversion H13. trivial. + * apply nth_error_zip_with_ind in Hlpt_m. + apply nth_error_map with (f := (fun p => set_from_list (first_n le (S (fst p))) U snd p)) in Hlpt_m. + assert (Some (set_from_list (first_n le (S m)) U lpt_m) = Some lpt). + { rewrite <- H10. symmetry. apply Hlpt_m. } + inversion H13. trivial. + - unfold subset. unfold E.Included. intros. apply union_intror. assumption. + - rewrite <- len_le. rewrite first_n_length. apply union_introl. apply In_list_set_In_list. + apply last_error_In. apply last_le. } + destruct H7 as [lpt''' [AVE_red''' [sub_lpt'_lpt''' in_e_lpt''']]]. + exists lpt'''. split; trivial. + apply Rel_Lpt with e'; trivial. + rewrite (union_include lpt'); trivial. + rewrite union_comm. apply lemma5. trivial. + * symmetry in H10. contradiction. +Qed. \ No newline at end of file