Require syntax.
Require Lattice.
Require SumLattice.
Require func.
Require StackLattice.
Require AbVal.
Require FiniteSet.
Require semantic.
Require analysis.
Require rel_correct.
Lemma R_Val_subst_def_ref : (P:Program;h:Heap;x:Class;loc,loc0:Location;V:(AbVal P))
(R_Val P h (ref loc0) V) ->
~(h loc0)=(None ?) ->
(h loc)=(None ?) ->
(R_Val P (substHeap h loc (def x)) (ref loc0) V).
Intros P h x loc loc0 V.
Unfold R_Val betaVal; Simpl; Unfold betaRef; Intros.
Case (Location_dec loc loc0); Intros.
Subst.
Elim (H0 H1).
Rewrite substHeap_diff; Auto.
Qed.
Lemma R_Val_subst_def_num : (P:Program;h:Heap;x:Class;loc:Location;n:integer;V:(AbVal P))
(R_Val P h (num n) V) ->
(R_Val P (substHeap h loc (def x)) (num n) V).
Unfold R_Val betaVal; Simpl; Intros; Auto.
Qed.
Lemma R_Stack_subst_def: (P:Program;h:Heap;c:Class;loc:Location ;
s : OperandStack ; S : (AbStack P))
(h loc)=(None ?)->
((loc2:Location)
(In (ref loc2) s)->~(h loc2)=(None ClassInst))->
(R_Stack P h s S)->
(R_Stack P (substHeap h loc (def c)) s S).
NewInduction s.
Intros.
Unfold R_Stack betaStack.
Simpl ; Auto.
Intros.
Inversion H1.
Constructor.
Unfold R_Stack betaStack.
Simpl.
Constructor.
Rewrite <-H5 in H1.
Generalize H4.
Unfold betaVal.
CaseEq a ; Do 2 Intro ; Auto.
Unfold betaRef.
CaseEq '(h r) ; Intros.
Case (Location_dec loc r) ; Intro ; Subst.
Rewrite H8 in H ; Discriminate H.
Rewrite substHeap_diff ; Auto.
Elim (H0 r) ; Simpl ; Intuition.
Generalize (IHs (some ? l2)).
Cut (loc2:Location)(In (ref loc2) s)->~(h loc2)=(None ClassInst) ; Intros.
Generalize (H8 H H7).
Unfold R_Stack betaStack.
Simpl.
Intros.
Apply H9.
Apply H6.
Apply H0.
Simpl ; Right ; Auto.
Qed.
Lemma R_PopCallStack_monotonicity2 : (P : Program ; h : Heap ; m :
MethodName ; pc1, pc2 : progCount ; l : LocalVar ;s : OperandStack ;
sf : CallStack; L:(AbFuncLocalVar P);AbS:(AbFuncStack P))
(R_PopCallStack P h (frame m pc1 l s)::sf (L,AbS)) ->
(order (LatAbLocalVar P) (L (add m pc1)) (L (add m pc2))) ->
(R_PopCallStack P h (frame m pc2 l s)::sf (L,AbS)).
Intros.
Inversion H.
Subst.
Constructor.
EApply R_PopCallStack_2 ; EAuto.
Qed.
Lemma apply_apply_tree : (A: Set ; PA: (Lattice A); max: nat;
f:(funcTree A max);p:positive)
(apply_tree A (bottom PA) (tr A max f) p) = (apply PA f p).
Unfold apply ; Auto.
Qed.
Lemma map_length : (A, B : Set ; f : A->B ; l : (list A))
(length (PolyList.map f l)) = (length l).
NewInduction l ; Simpl ; Auto.
Qed.
Lemma map_nil : (A,B: Set ; l : (list A) ; f : A->B)
(PolyList.map f l) = (nil B) -> l = (nil A).
NewInduction l ; Intros ; Auto.
Simpl in H ; Discriminate H.
Qed.
Lemma map_app : (A,B: Set ; l,l' : (list A) ; f : A->B)
(PolyList.map f (app l l')) = (app (PolyList.map f l) (PolyList.map f l')).
NewInduction l.
Simpl ; Auto.
Simpl ; Intros ; Rewrite IHl ; Auto.
Qed.
Lemma length_app : (A: Set ; l1, l2 : (list A))
(le (length l1) (length (app l1 l2))).
NewInduction l1 ; Simpl ; Intros ; Auto with arith.
Qed.
Lemma length_app_sum : (A: Set ; l1, l2 : (list A))
(length (app l1 l2)) = (plus (length l1) (length l2)).
NewInduction l1 ; Simpl ; Intros ; Auto with arith.
Qed.
Lemma methodLookUp_prop :
(P :Program ; mID : MethodID ; o : ClassInst ; M : Method)
(methodLookup P mID (class o))=(Some M) ->
(inf_log (nameMethod M) (max_log_MethodName P)).
Intros P mID o M.
Unfold methodLookup.
CaseEq '(searchClass P (class o)) ; Do 2 Intro.
CaseEq '(searchWithMethodID (list_methods_lookup c) mID) ; Do 2 Intro.
CaseEq '(searchMethod P m) ; Intros.
Injection H2 ; Intros ; Subst.
Generalize (searchMethod_some P m M) ; Intros; Intuition.
2: Discriminate H2.
2: Discriminate H1.
2: Discriminate H0.
Generalize in_inf_log ; Intros.
Unfold max_log_MethodName.
EApply in_inf_log ; EAuto.
Qed.
Lemma orderS_order:
(P:Program; A,A':OperandStack; h:Heap; l:(list (AbVal P)))
(orderS (AbVal P) (LatAbVal P)
(some (AbVal P) (PolyList.map (betaVal P h) (app A A')))
(some (AbVal P) l))
->(n1:nat)
(order (LatAbVal P) (betaVal P h (nth n1 A null))
(nth n1 l (bot_sum (AbRef P)+AbNum))).
Intro P.
Generalize (orderS_ind (AbVal P) (LatAbVal P) [S1, S2 : (stack (AbVal P))]
(A,A' : OperandStack; h: Heap ; l : (list (AbVal P)))
S1 = (some (AbVal P) (PolyList.map (betaVal P h) (app A A'))) ->
S2 = (some (AbVal P) l) ->
(orderS (AbVal P) (LatAbVal P)
(some (AbVal P) (PolyList.map (betaVal P h) (app A A')))
(some (AbVal P) l))
->(n1:nat)
(order (LatAbVal P) (betaVal P h (nth n1 A null))
(nth n1 l (bot_sum (AbRef P)+AbNum))) ) ; Intros.
EApply H.
Intros.
Discriminate H1.
Intros.
Discriminate H2.
Intros.
Injection H2 ; Clear H2 ; Intro H2.
Rewrite <- H2.
Injection H1 ; Clear H1 ; Intro H1.
Rewrite map_app in H1.
Cut (app (PolyList.map (betaVal P h0) A0)
(PolyList.map (betaVal P h0) A'0)) = (nil (AbVal P)) ; Intros ; Auto.
Generalize (app_eq_nil H4 ) ; Intros ; Intuition.
Clear H7 H4 H1.
Generalize (map_nil Value (AbVal P) A0 (betaVal P h0) H6) ; Intros.
Rewrite H1.
Simpl.
Transparent bottom.
CaseEq n0 ; Intros; Unfold betaVal betaRef; Simpl ; Constructor.
Intros.
CaseEq A0 ; Intros.
Simpl.
CaseEq n0 ; Intros; Unfold betaVal betaRef; Simpl ; Constructor.
Subst.
Injection H5 ; Clear H5 ; Intro H5.
Cut l0 = (x2::l2) ; Intros ; Auto ; Subst.
Clear H5.
Simpl in H4 H6.
Injection H4; Clear H4 ; Intros; Subst.
CaseEq n0 ; Intros.
Simpl ;Simpl in H1 ; Auto.
Simpl.
Simpl in H3.
Apply H3 with A'0 ; Auto.
Apply H0.
Auto.
Auto.
Auto.
Qed.
Lemma nth_notIn :
(A:Set ; n:nat ; l:(list A) ; d:A)
(le (length l) n)-> (nth n l d) = d.
NewInduction n.
Simpl ; Intros.
Generalize (lel_nil H) ; Unfold lel ; Intros.
Rewrite <- H0.
Unfold nth ; Auto.
Generalize IHn ; Clear IHn.
NewInduction l.
Intros; Unfold nth ; Auto.
Intros ; Simpl.
Apply IHn ; Simpl in H ; Auto with arith.
Qed.
Lemma AbTop_n_length : (P :Program ; l : (list (AbVal P)))
(AbTop_n P (some (AbVal P) l) (length l)) = l.
NewInduction l.
Simpl; Auto.
Simpl ; Rewrite IHl; Auto.
Qed.
Lemma AbTop_n_app_first : (P :Program ; l1, l2: (list (AbVal P)))
(AbTop_n P (some (AbVal P) (app l1 l2)) (length l1)) =
(AbTop_n P (some (AbVal P) l1) (length l1)).
NewInduction l1.
Simpl ; Intros; Auto.
Simpl ; Intros ; Rewrite IHl1 ; Auto.
Qed.
Lemma app_exists : (A:Set ; l : (list A) ; m: nat)
(le m (length l)) ->
(EX l' : (list A) | (EX l'' : (list A) | l = (app l' l'') /\ (length l') =m)).
Intro A.
Generalize rev_ind ; Intro.
Generalize (H A [l :(list A)]
(m:nat) (le m (length l))
->(EX l':list A|(EX l'':list A|l=(app l' l'')/\(length l')=m))); Clear H; Intros.
Apply H ; Simpl ; Intros ; Auto.
Cut (m0 = (0)) ; Intros ; Try Omega.
Subst.
Exists (nil A) ; Intros ; Subst ; Exists (nil A) ; Intros ; Subst ; Auto.
Case (le_gt_dec m0 (length l0)) ; Intros ; Auto.
Generalize (H1 m0 l1) ; Clear H1 ; Intros H1 ; Elim H1 ; Clear H1 ; Intros.
Elim H1 ; Clear H1 ; Intros ; Intuition.
Subst.
Exists x0; Exists (app x1 x::(nil A)); Split ; Try Rewrite app_ass ; Auto.
Cut m0 = (length (app l0 x::(nil A))) ; Intros.
Exists (app l0 x::(nil A)) ; Exists (nil A) ; Split; Try Rewrite <-app_nil_end ; Auto.
Generalize H2 ; Rewrite length_app_sum; Simpl ; Intros.
LetTac ll := (length l0) ; Omega.
Qed.
Lemma AbTop_n_app : (P :Program ; l1, l2 : (list (AbVal P)) ; m : nat)
(le m (length l1)) ->
(AbTop_n P (some (AbVal P) (app l1 l2)) m) = (AbTop_n P (some (AbVal P) l1) m).
Intro P.
Generalize rev_ind ; Intro.
Generalize (H (AbVal P)
[l1 : (list (AbVal P))]
(l2 : (list (AbVal P)))
(m: nat)
(le m (length l1))
->(AbTop_n P (some (AbVal P) (app l1 l2)) m)
=(AbTop_n P (some (AbVal P) l1) m)) ; Clear H ; Intros.
Apply H ; Auto.
Simpl ; Intros.
Cut (m0 = (0)) ; Intros ; Try Omega.
Subst ; Simpl ; Auto.
Simpl ; Intros.
Case (le_gt_dec m0 (length l)) ; Intros ; Auto.
Clear H2.
Rewrite app_ass.
Rewrite H1 ; Auto.
Generalize (app_exists (AbVal P) l m0 l3) ; Intros.
Elim H2 ; Clear H2 ; Intros.
Elim H2 ; Clear H2 ; Intros ; Intuition.
Rewrite H3.
Rewrite <- H4.
Rewrite AbTop_n_app_first.
Rewrite app_ass.
Rewrite AbTop_n_app_first ; Auto.
Cut m0 = (length (app l x::(nil (AbVal P)))) ; Intros.
Subst.
Rewrite AbTop_n_app_first ; Auto.
Generalize H2 ; Rewrite length_app_sum.
Simpl.
LetTac ll := (length l) ; Intros ; Omega.
Qed.
Lemma nth_last : (A: Set ; l: (list A) ; x,d : A)
(nth (length l) (app l x::(nil A)) d) = x.
NewInduction l.
Simpl; Auto.
Simpl ; Apply IHl; Auto.
Qed.
Lemma nth_last_app : (A: Set ; l,l': (list A) ; x,d : A)
(nth (length l) (app (app l x::(nil A)) l') d) = x.
NewInduction l.
Simpl; Auto.
Simpl ; Apply IHl; Auto.
Qed.
Lemma nth_app : (A: Set ; l1, l2 : (list A) ; n : nat; d : A)
(lt n (length l1)) ->
(nth n (app l1 l2) d) = (nth n l1 d).
Intro A.
Generalize rev_ind ; Intro.
Generalize (H A [l1 : (list A)] (l2:(list A); n:nat; d:A)
(lt n (length l1))->(nth n (app l1 l2) d)=(nth n l1 d)) ; Clear H ; Intros.
Apply H ;Auto ; Simpl ; Intros.
Apply False_ind ; Omega.
Case (le_gt_dec (length l) n0) ; Intros ; Auto.
Cut n0 = (length l) ; Intros.
Subst.
Rewrite nth_last.
Rewrite nth_last_app; Auto.
Generalize H2 ; Rewrite length_app_sum.
Simpl.
LetTac ll := (length l) ; Intros ; Omega.
Cut (le n0 (length l)) ; Intros.
Generalize (app_exists A l n0 H3) ; Intros.
Do 2 (Elim H4 ; Clear H4 ; Intros) ; Intuition.
Rewrite H5.
Rewrite <- H6.
CaseEq x1 ; Intros ; Subst.
Simpl.
Rewrite <-app_nil_end.
Rewrite nth_last.
Rewrite nth_last_app ; Auto.
Rewrite app_ass.
Replace (app (app x0 a::l3) (app x::(nil A) l0)) with
(app (app x0 a::(nil A)) (app (app l3 x::(nil A)) l0)).
Replace (app (app x0 a::l3) x::(nil A)) with
(app (app x0 a::(nil A)) (app l3 x::(nil A))).
Do 2 Rewrite nth_last_app ; Auto.
Do 2 Rewrite app_ass.
Replace (app a::(nil A) (app l3 x::(nil A))) with
(app a::l3 x::(nil A)) ; Auto.
Do 3 Rewrite app_ass.
Replace (app a::(nil A) (app l3 (app x::(nil A) l0)))
with (app a::l3 (app x::(nil A) l0)) ; Auto.
Generalize H2 ; Rewrite length_app_sum.
Simpl.
LetTac ll := (length l) ; Intros ; Omega.
Qed.
Lemma nth_AbTop_n :
(P:Program; n,m:nat; l:(list (AbVal P)))
(lt n m) -> (le m (length l)) ->
(nth n (AbTop_n P (some (AbVal P) l) m)
(bottom (LatAbVal P))) = (nth n l (bottom (LatAbVal P))).
Intro P.
Generalize rev_ind ; Intros.
Generalize (H (AbVal P)
[l : (list (AbVal P))]
(n,m:nat)
(lt n m)
->(le m (length l))
->(nth n (AbTop_n P (some (AbVal P) l) m) (bottom (LatAbVal P)))
=(nth n l (bottom (LatAbVal P)))) ; Clear H ; Intros.
Transparent nth AbTop_n.
Apply H ; Auto.
Simpl.
Intros.
Apply False_ind ; Omega.
Intros.
Rewrite length_app_sum in H4 ; Simpl in H4.
Case (le_gt_dec m0 (length l0)) ; Intros.
Clear H4.
Rewrite (AbTop_n_app ? l0 x::(nil ?) m0 l1).
Rewrite (nth_app ? l0 x::(nil ?) n0 (bottom (LatAbVal P))).
Apply H2 ; Auto.
LetTac ll := (length l0); Omega.
Cut m0 = (S (length l0)) ; Intros.
Subst.
Cut (length (app l0 x::(nil (AbVal P)))) = (S (length l0)) ; Intros.
Rewrite <- H5.
Rewrite AbTop_n_length ; Auto.
Rewrite length_app_sum ; Simpl ; Auto with arith.
LetTac ll := (length l0) ; Omega.
LetTac ll := (length l0) ; Omega.
Qed.
Definition apply_nat :
(A:Set)(Lattice A)->(max:nat)(funcTree A max)->nat->A :=
[A,L,max,f,p](apply L f (anti_convert p)).
Implicits apply_nat [1 3].
Lemma anti_convert_pred_convert : (p:positive)
(anti_convert (pred (convert p)))=p.
Intros p.
Elim (ZL4 p); Intros.
Rewrite H; Simpl.
Cut (anti_convert (S x))=(add_un p); Intros.
Simpl in H0.
Replace (anti_convert x) with (sub_un (add_un (anti_convert x))).
Replace p with (sub_un (add_un p)).
Rewrite H0; Auto.
Rewrite sub_add_one; Auto.
Rewrite sub_add_one; Auto.
Rewrite <- H.
Apply bij2.
Qed.
Lemma nth_subst_n_nat:
(P:Program;l:(list (AbVal P)); x:nat; p:positive)
(inf_log (anti_convert (plus x (pred (convert p)))) (max_log_Var P)) ->
(apply_nat (LatAbVal P) (subst_n_rec P p (bottom (LatAbLocalVar P)) l) (plus x (pred (convert p))))
=(nth x l (bottom (LatAbVal P))).
NewInduction l; Simpl; Intros.
Unfold apply_nat.
Rewrite apply_bottom.
Case x; Auto.
Generalize H; Clear H; Case x; Simpl; Intros.
Unfold apply_nat.
Rewrite anti_convert_pred_convert.
Rewrite apply_subst1; Auto.
Rewrite anti_convert_pred_convert in H; Auto.
Unfold apply_nat.
Rewrite apply_subst2; Auto.
Generalize (IHl n (add_un p)); Unfold apply_nat.
Simpl.
Replace (anti_convert (plus n (pred (convert (add_un p))))) with
(add_un (anti_convert (plus n (pred (convert p))))); Intros.
Apply H0; Auto.
Replace (add_un (anti_convert (plus n (pred (convert p))))) with
(anti_convert (S (plus n (pred (convert p))))).
Rewrite plus_sym.
Replace (S (plus (pred (convert p)) n)) with (plus (S (pred (convert p))) n).
Rewrite plus_sym.
Replace (S (pred (convert p))) with (pred (convert (add_un p)));Auto.
Replace (pred (convert (add_un p))) with (convert (sub_un (add_un p))).
Rewrite sub_add_one.
Elim (ZL4 p); Intros.
Rewrite H0; Auto.
Replace (convert (add_un p)) with (S (convert p)).
Rewrite sub_add_one ;Simpl; Auto.
Unfold convert.
Rewrite convert_add_un; Auto.
Auto.
Auto.
Apply inf_log_trans with (add_un (anti_convert (plus n (pred (convert p))))); Auto.
Replace (add_un (anti_convert (plus n (pred (convert p))))) with
(anti_convert (S (plus n (pred (convert p))))).
Case n; Intros.
Rewrite plus_sym.
Replace (S (plus (pred (convert p)) (0))) with (plus (S (pred (convert p))) (0)).
Rewrite plus_sym.
Simpl.
Rewrite anti_convert_pred_convert.
Apply convert_compare_INFERIEUR.
Replace (convert (add_un p)) with (S (convert p)).
Omega.
Unfold convert.
Rewrite convert_add_un; Auto.
Auto.
Rewrite <- (bij1 n0).
Rewrite plus_sym.
Replace (S (plus (pred (convert p)) (convert (anti_convert n0)))) with
(plus (S (pred (convert p))) (convert (anti_convert n0))).
Rewrite plus_sym.
Replace (S (pred (convert p))) with (convert p).
Rewrite <- convert_add.
Rewrite bij2.
Apply convert_compare_INFERIEUR.
Rewrite add_sym.
Rewrite <- ZL14.
Apply ZL17.
Elim (ZL4 p); Intros.
Rewrite H0; Auto.
Auto.
Auto.
Red; Intros.
Elim (lt_n_n (convert p)).
Pattern 2 p; Rewrite <- H0.
Rewrite bij1.
Rewrite plus_sym.
Replace (S (plus (pred (convert p)) n)) with
(plus (S (pred (convert p))) n).
Replace (S (pred (convert p))) with (convert p).
Apply le_lt_trans with (plus (convert p) n).
Auto with zarith.
Auto with zarith.
Elim (ZL4 p); Intros.
Rewrite H1; Auto.
Auto.
Qed.
Lemma nth_subst_n:
(P:Program; x:positive; l:(list (AbVal P)))
(inf_log x (max_log_Var P)) ->
(apply (LatAbVal P) (subst_n P l) x)
=(nth (pred (convert x)) l (bottom (LatAbVal P))).
Intros.
Unfold subst_n.
Generalize (nth_subst_n_nat P l (pred (convert x)) xH).
Replace (plus (pred (convert x)) (pred (convert xH))) with (pred (convert x)).
Unfold apply_nat.
Rewrite anti_convert_pred_convert.
Intros.
Apply H0 ;Auto.
Simpl.
Rewrite plus_sym.
Auto.
Qed.
Lemma R_Stack_AbPop: (P: Program ; h : Heap ; s: OperandStack ; AbS :(AbStack P);
a: Value)
(R_Stack P h a::s AbS) -> (R_Stack P h s (AbPop AbS)).
Do 5 Intro.
Unfold R_Stack betaStack.
Simpl.
Intros.
Inversion H.
Simpl.
Constructor.
Simpl ; Auto.
Qed.
Lemma AbPop_AbPop_n : (P : Program ; AbS : (AbStack P) ; n : nat)
(AbPop_n P (AbPop AbS) n) = (AbPop (AbPop_n P AbS n)).
NewInduction n.
Simpl ; Auto.
Simpl.
Rewrite IHn ; Auto.
Qed.
Lemma R_Stack_AbPop_n: (P: Program ; h : Heap ; s,s': OperandStack ; AbS :(AbStack P))
(R_Stack P h (app s s') AbS) -> (R_Stack P h s' (AbPop_n P AbS (length s))).
NewInduction s.
Simpl ; Auto.
Simpl ; Intros.
Generalize (R_Stack_AbPop P h (app s s') AbS a H ) ; Intros.
Generalize (IHs s' (AbPop AbS) H0) ; Intros.
Rewrite <- AbPop_AbPop_n ; Auto.
Qed.
Lemma AbPop_n_bot : (P : Program ; n :nat)
(AbPop_n P (StackLattice.bot (AbVal P)) n) =
(StackLattice.bot (AbVal P)).
NewInduction n.
Simpl ; Auto.
Simpl ; Rewrite IHn ; Auto.
Qed.
Lemma AbPop_n_AbPop: (P : Program ; n :nat ; AbS : (AbStack P))
(AbPop (AbPop_n P AbS n)) = (AbPop_n P (AbPop AbS) n).
NewInduction n.
Simpl; Auto.
Simpl ;Intros ; Rewrite IHn ; Auto.
Qed.