Require syntax.
Require semantic.
Require Omega.
Require Wf_nat.
Lemma reachable_is_Valid : (P: Program ; st : State)
(reachable_State P st) -> (valid_State st).
Intros.
NewInduction H.
Unfold valid_State.
Inversion H.
Split.
Intros.
Discriminate H2.
Intros.
Simpl in H2.
Elim H2 ; Intros ; Trivial.
Clear H2.
Rewrite <- H3.
Split.
Intros.
Generalize (H0 x) ; Intros H4.
Rewrite H2 in H4 ; Discriminate H4.
Intros.
Simpl in H2 ; Auto.
Elim H3.
Generalize IHreachable_State ; Inversion_clear H0.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L S)).
Rewrite <- H0.
Simpl.
Intros.
Intuition.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L S)).
Rewrite <- H0.
Simpl.
Intros.
Cut (frame m pc L S)=(frame m pc L S)\/(In (frame m pc L S) SF) ; Intuition.
Discriminate H11.
EApply H9 ; EAuto.
Discriminate H12.
EApply H10 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Simpl in IHreachable_State''.
Generalize (IHreachable_State'' (frame m pc L v::S)).
Rewrite <- H0.
Simpl.
Intros.
Cut (frame m pc L v::S)=(frame m pc L v::S)\/(In (frame m pc L S) SF) ; Intuition.
EApply H9 ; EAuto.
EApply H9 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L (num n1)::(num n2)::S)).
Rewrite <- H0.
Simpl.
Intros.
Cut (frame m pc L (num n1)::(num n2)::S)
=(frame m pc L (num n1)::(num n2)::S)\/(In
(frame m pc L
(num n1)::
(num n2)::S) SF) ; Intuition.
Discriminate H11.
EApply H9 ; EAuto.
Discriminate H12.
EApply H9 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L S)).
Rewrite <- H0.
Simpl.
Intros.
Cut (frame m pc L S)=(frame m pc L S)\/(In (frame m pc L S) SF) ; Intuition.
EApply H4 ; EAuto.
EApply H9 ; EAuto.
EApply H4 ; EAuto.
EApply H9 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L v::S)).
Rewrite <- H0.
Simpl.
Intros.
Cut (frame m pc L v::S)=(frame m pc L v::S)\/(In (frame m pc L S) SF) ; Intuition.
Case (Var_dec i x) ; Intros ; Subst.
Generalize H3 ; Unfold substLocalVar ; Case Var_dec ; Intros.
EApply H9 ; EAuto.
Elim n ; Auto.
Generalize H3 ; Unfold substLocalVar ; Case Var_dec ; Intros.
Elim n ; Auto.
EApply H4 ; EAuto.
EApply H9 ; EAuto.
Generalize H3 ; Unfold substLocalVar ; Case Var_dec ; Intros.
EApply H9 ; EAuto.
EApply H4 ; EAuto.
EApply H9 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H4) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L (num n)::S)).
Rewrite <- H0.
Simpl.
Intros.
Cut(frame m pc L (num n)::S)=(frame m pc L (num n)::S)\/(In
(
frame m pc
L
(num n)::
S) SF) ; Intuition.
EApply H10 ; EAuto.
EApply H10 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H4 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L (num (0))::S)).
Rewrite <- H0.
Simpl.
Intros.
Cut(frame m pc L (num (0))::S)=(frame m pc L (num (0))::S)\/(In
(
frame m pc
L
(num (0))::
S) SF) ; Intuition.
EApply H9 ; EAuto.
EApply H9 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Case (Location_dec loc loc0) ; Intros ; Subst.
Rewrite substHeap_equal in H0.
Injection H0 ; Intros H' ; Rewrite H'.
Case (Location_dec loc0 loc1) ; Intros ; Subst.
Rewrite substHeap_equal.
Red ; Intro Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Rewrite <-H' in H5.
Case (Field_dec f f0) ; Intro; Subst.
Rewrite <-substfield_equal in H5.
Generalize (H6 (frame m pc L v::(ref loc0)::S)) ; Intros.
Simpl in H7.
Cut (frame m pc L v::(ref loc0)::S)=(frame m pc L v::(ref loc0)::S)\/(
In (frame m pc L v::(ref loc0)::S) SF) ; Intuition.
EApply H14 ; EAuto.
EApply H14 ; EAuto.
Rewrite <-substfield_diff in H5.
EApply IHreachable_State' ; EAuto.
Trivial.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff; Auto.
Rewrite substHeap_diff in H0; Auto.
EApply IHreachable_State' ; EAuto.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' g
H5.
Simpl in H5.
Elim H5.
Intros H6 ; Rewrite <-H6.
Split.
Intros.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Generalize (IHreachable_State'' (frame m pc L v::(ref loc)::S)) ; Intros.
Simpl in H7.
Cut (frame m pc L v::(ref loc)::S)=(frame m pc L v::(ref loc)::S)\/(
In (frame m pc L v::(ref loc)::S) SF) ; Intuition.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Generalize (IHreachable_State'' (frame m pc L v::(ref loc)::S)) ; Intros.
Simpl in H7.
Cut (frame m pc L v::(ref loc)::S)=(frame m pc L v::(ref loc)::S)\/(
In (frame m pc L v::(ref loc)::S) SF) ; Intuition.
EApply H14 with loc2 ; EAuto.
EApply H14 with loc2 ; EAuto.
EApply H14 with loc2 ; EAuto.
EApply H14 with loc2 ; EAuto.
Intros.
Generalize (IHreachable_State'' g) ; Intros ; Auto.
Simpl in H6.
Cut (frame m pc L v::(ref loc)::S)=g\/(In g SF) ; Auto ; Intros.
Generalize (H6 H7) ; Intros.
Clear H6 H5.
CaseEq g ; Intros.
Rewrite H5 in H8.
Split.
Intros.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim H8 ; Intros.
EApply H5 ; EAuto.
Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim H8 ; Intros.
EApply H9 ; EAuto.
Unfold valid_State.
Elim H3 ; Intros.
Generalize (newObject_specif P x H1 H' loc) ; Intros.
Elim (searchClass_some P cl x); Intros ; Subst ; Auto.
Elim (H5 H6 H4) ; Intros ; Clear H5.
Rewrite H8.
Split ; Intros.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Case (Location_dec loc loc0) ; Intros ; Subst.
Rewrite substHeap_equal in H5; Auto.
Injection H5 ; Clear H5 ; Intro H5 ; Cut (o = (def x)) ; Intros ; Auto ; Subst.
Clear H5.
Unfold def in H9.
Unfold initField in H9.
Generalize H9 ; Clear H9.
Simpl.
CaseEq ' (searchField x f).
Do 2 Intro.
CaseEq '(typeField f0) ; Intros.
Discriminate H9.
Discriminate H9.
Intros.
Discriminate H9.
Generalize H5 ; Clear H5 ; Rewrite substHeap_diff ; Auto.
Intros.
Elim IHreachable_State0 ; Clear IHreachable_State0 ; Intros.
Red ; Intro.
Elim (H8 ? ? ? ? H5 H9 H11).
Simpl in H5.
Elim H5 ; Intros.
Clear H5.
Rewrite <- H9.
Split.
Intros.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim IHreachable_State0 ; Clear IHreachable_State0 ; Intros.
Generalize (H10 (frame m pc L S)) ; Clear H10 ; Intro H10.
Simpl in H10.
Cut (frame m pc L S)=(frame m pc L S)\/(In (frame m pc L S) SF) ; Auto ; Intros.
Generalize (H10 H11) ; Clear H10 ; Intro H10.
Elim H10 ; Clear H10 ; Intros.
EApply H10 ; EAuto.
Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim IHreachable_State0 ; Clear IHreachable_State0 ; Intros.
Simpl in H5.
Elim H5 ; Intros.
Injection H11 ; Clear H11 ; Intro H11 ; Elim n ; Auto.
Clear H5.
Generalize (H10 (frame m pc L S)) ; Clear H10 ; Intro H10.
Simpl in H10 ;
Cut (frame m pc L S)=(frame m pc L S)\/(In (frame m pc L S) SF) ; Auto ; Intros.
Generalize (H10 H5) ; Clear H10 H5 ; Intro H5.
Elim H5 ; Clear H5 ; Intros.
EApply H10 ; EAuto.
CaseEq f ; Intros.
Split.
Intros.
Elim IHreachable_State0 ; Clear IHreachable_State0 ; Intros.
Generalize (H13 f) ; Clear H13 ; Intro H13.
Simpl in H13.
Cut (frame m pc L S)=f\/(In f SF) ; Intros ; Auto.
Generalize (H13 H14) ; Clear H13 H14 ; Intro H13.
Rewrite H10 in H13.
Case (Location_dec loc loc1) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim H13 ; Intros.
EApply H8; EAuto.
Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Rewrite substHeap_equal ; Auto.
Red ; Intros Hdisc ; Discriminate Hdisc.
Rewrite substHeap_diff ; Auto.
Elim IHreachable_State0 ; Clear IHreachable_State0 ; Intros.
Generalize (H10 (frame m0 p l o)) ; Clear H10 ; Intro H10.
Simpl in H10.
Cut (frame m pc L S)=(frame m0 p l o)\/(In (frame m0 p l o) SF); Intros ; Auto.
Generalize (H10 H12) ; Clear H10 H12 ; Intros.
Elim H10 ; Clear H10 ; Intros.
EApply H12 ; EAuto.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Intros.
Generalize (IHreachable_State' ? ? ? ? H0 H5) ; Intros; Assumption.
Intros.
Simpl in H0 ; Elim H0 ; Intros.
Clear H0 ; Rewrite <- H5.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Generalize (H7 (frame m pc L (ref loc)::S)) ; Clear H7 ; Intro H7.
Simpl in H7.
Cut (frame m pc L (ref loc)::S)=(frame m pc L (ref loc)::S)\/(
In (frame m pc L (ref loc)::S) SF) ; Intros ; Auto.
Generalize (H7 H8) ; Clear H7 H8 ; Intros.
Elim H7 ; Intros.
EApply H8 ; EAuto.
Simpl in H0 ; Elim H0 ; Clear H0 ; Intros.
Elim IHreachable_State ; Clear IHreachable_State; Intros.
Apply (H6 ? ? ? ? H3 H0) ; Auto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Generalize (H7 (frame m pc L (ref loc2)::S)) ; Clear H7 ; Intro H7.
Cut (frame m pc L (ref loc2)::S)=(frame m pc L (ref loc2)::S)\/(
In (frame m pc L (ref loc2)::S) SF) ; Intros ; Auto.
Generalize (H7 H8) ; Clear H7 H8 ; Intros.
Elim H7 ; Intros.
EApply H9 ; EAuto.
Simpl ; Left ; Auto.
Generalize (H7 (frame m pc L (ref loc)::S)) ; Intros.
Simpl in H8 ; Cut (In (frame m pc L (ref loc)::S) (frame m pc L (ref loc)::S)::SF) ;
Intros ; Auto.
Generalize (H8 H9) ; Clear H8 H9 ; Intros.
Elim H8 ; Intros.
EApply H10 ; EAuto.
Simpl; Left; Auto.
Clear H0.
CaseEq f0 ; Intros.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Generalize (H8 f0) ; Clear H8 ; Intro H8.
Simpl in H8.
Cut (frame m pc L (ref loc)::S)=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H8 H9) ; Clear H8 H9 ; Intros.
Rewrite H0 in H8 ; Elim H8 ; Intros.
EApply H9 ; EAuto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Case (Location_dec loc loc2) ; Intros ; Subst.
Generalize (H8 (frame m pc L (ref loc2)::S)) ; Clear H8 ; Intro H8.
Simpl in H8.
Cut (frame m pc L (ref loc2)::S)=(frame m pc L (ref loc2)::S)\/(
In (frame m pc L (ref loc2)::S) SF) ; Intros ; Auto.
Generalize (H8 H0) ; Clear H8 H0 ; Intros.
Elim H0 ; Intros.
EApply H9 ; EAuto.
Generalize (H8 (frame m0 p l o0)) ; Clear H8 ; Intro H8.
Simpl in H8.
Cut (frame m pc L (ref loc)::S)=(frame m0 p l o0)\/(In
(frame m0 p l
o0) SF) ; Intros; Auto.
Generalize (H8 H0) ; Clear H8 H0 ; Intros.
Elim H0 ; Intros.
EApply H9 ; EAuto.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros.
EApply H10 ; EAuto.
Intros.
Simpl in H0 ; Elim H0 ; Clear H0 ; Intros.
Rewrite <-H0.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Generalize (H11 (frame m pc L (ref loc)::(app A S))) ; Clear H11 ; Intro H11.
LetTac S' := (ref loc)::(app A S).
Simpl in H11.
Cut (frame m pc L S') = (frame m pc L S') \/(
In (frame m pc L S') SF) ; Intros ; Auto.
Generalize (H11 H12) ; Clear H11 H12 ; Intros.
Elim H11 ; Intros.
Apply H13.
Case (Location_dec loc loc1) ; Intros ; Subst.
Left; Trivial.
Right.
Generalize nth_in_or_default ; Intros.
Generalize (H6 Value (pred (convert x)) (ref loc)::A null); Clear H6 ; Intros.
Rewrite H9 in H6.
Elim H6 ; Intros.
Simpl in a ; Apply in_or_app ; Intuition.
Injection H6 ; Intros ; Subst ; Auto ; Elim n0 ; Auto.
Discriminate b.
Discriminate b.
Simpl in H9 ; Auto.
Elim H0 ; Clear H0 ; Intros.
Rewrite <- H0.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
LetTac f0 := (frame m pc L (ref loc)::(app A S)).
Generalize (H11 f0) ; Clear H11 ; Intro H11.
Simpl in H11;
Cut f0=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H11 H12) ; Clear H11 H12 ; Intros.
Elim H11 ; Intros.
EApply H12 ; EAuto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
LetTac f0 := (frame m pc L (ref loc)::(app A S)).
Generalize (H11 f0) ; Clear H11 ; Intro H11.
Simpl in H11;
Cut f0=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H11 H12) ; Clear H11 H12 ; Intros.
Elim H11 ; Intros.
EApply H13 ; EAuto.
Right.
Apply in_or_app ; Auto.
CaseEq f ; Intros.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Generalize (H12 f) ; Clear H12 ; Intro H12.
Simpl in H12.
Cut (frame m pc L (ref loc)::(app A S)) = f\/(In f SF) ; Intros ; Auto.
Generalize (H12 H13) ; Clear H12 H13 ; Intros.
Rewrite H9 in H12.
Elim H12 ; Intros.
EApply H13 ; EAuto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Generalize (H12 f) ; Clear H12 ; Intro H12.
Simpl in H12.
Cut (frame m pc L (ref loc)::(app A S)) = f\/(In f SF) ; Intros ; Auto.
Generalize (H12 H13) ; Clear H12 H13 ; Intros.
Rewrite H9 in H12.
Elim H12 ; Intros.
EApply H14 ; EAuto.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros.
EApply H4 ; EAuto.
Intros.
Simpl in H0 ; Elim H0 ; Clear H0 ; Intros.
Rewrite <-H0.
Split ; Intros.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Simpl in H5.
LetTac f0 := (frame m pc L S).
Generalize (H5 f0) ; Clear H5 ; Intro H5.
Cut (frame m' pc' L' v::S')=f0\/f0=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H5 H6) ; Clear H5 H6 ; Intros.
Simpl in H5 ; Elim H5 ; Clear H5 ; Intros.
EApply H5 ; EAuto.
Simpl in H3 ; Elim H3 ; Clear H3 ; Intro H3.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Simpl in H5.
LetTac f0 := (frame m' pc' L' v::S').
Generalize (H5 f0) ; Clear H5 ; Intro H5.
Cut f0=f0\/(frame m pc L S)=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H5 H6) ; Clear H5 H6 ; Intros.
Simpl in H5 ; Elim H5 ; Clear H5 ; Intros.
EApply H6 ; EAuto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Simpl in H5.
LetTac f0 := (frame m pc L S).
Generalize (H5 f0) ; Clear H5 ; Intro H5.
Cut (frame m' pc' L' v::S')=f0\/f0=f0\/(In f0 SF) ; Intros ; Auto.
Generalize (H5 H6) ; Clear H5 H6 ; Intros.
Simpl in H5 ; Elim H5 ; Clear H5 ; Intros.
EApply H6 ; EAuto.
Elim IHreachable_State ; Clear IHreachable_State ; Intros.
Simpl in H4.
Generalize (H4 f) ; Clear H4 ; Intro H4.
CaseEq f ; Intros.
Split ; Intros.
Cut (frame m' pc' L' v::S')=f\/(frame m pc L S)=f\/(In f SF) ; Intros ; Auto.
Generalize (H4 H7) ; Clear H4 H7 ; Intros.
Rewrite H5 in H4 ; Elim H4 ; Clear H4 ; Intros.
EApply H4 ; EAuto.
Cut (frame m' pc' L' v::S')=f\/(frame m pc L S)=f\/(In f SF) ; Intros ; Auto.
Generalize (H4 H7) ; Clear H4 H7 ; Intros.
Rewrite H5 in H4 ; Elim H4 ; Clear H4 ; Intros.
EApply H7 ; EAuto.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L v::S)).
Rewrite <- H0.
Simpl.
Intros.
Intuition.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L S)).
Rewrite <- H0.
Simpl.
Intros.
Intuition.
Clear H5.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L v1::v2::S)).
Rewrite <- H0.
Simpl.
Intros.
Intuition.
Clear H5.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Unfold valid_State.
Clear IHreachable_State;
Intros IHreachable_State.
Split.
Intros.
Elim IHreachable_State ; Intros IHreachable_State'.
Generalize (IHreachable_State' loc loc0 o f H0 H3) ; Intros; Assumption.
Elim IHreachable_State ; Intros IHreachable_State' ; Intros IHreachable_State'' f
H5.
Simpl in H5 ; Elim H5 ; Intros.
Clear H5.
Generalize (IHreachable_State'' (frame m pc L v1::v2::S)).
Rewrite <- H0.
Simpl.
Intros.
Intuition.
Clear H5.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
EApply H8 ; EAuto.
Generalize (IHreachable_State'' f) ; Intros.
Simpl in H3 ; Intuition.
Qed.
Lemma smallstep_instruction_only :
(P:Program;h:Heap;m:MethodName;pc:progCount;l:LocalVar;s:OperandStack;sf:CallStack;
st:State)
(SmallStepSem P (config h <m,pc,l,s>::sf) st) ->
(EX I:Instruction | (instructionAt P m pc)= (Some I)).
Intros.
Inversion_clear H; EAuto.
Qed.
Lemma referred_class : (P : Program ; h : Heap ; m : MethodName ;
pc : progCount ; l : LocalVar ; s : OperandStack ; sf : CallStack;
loc : Location ; o : ClassInst)
(reachable_State P (config h <m , pc, l, s>::sf)) ->
(h loc) = (Some o) ->
(inf_log (class o) (max_log_ClassName P)).
Proof.
LetTac valid_State2 :=
[P: Program; St: State]let (h,sf)=St in
((loc : Location ; o : ClassInst)
(h loc) = (Some o) ->(inf_log (class o) (max_log_ClassName P))).
Intros.
Cut (reachable_State P (config h (frame m pc l s)::sf)) -> (valid_State2 P
(config h (frame m pc l s)::sf)) ; Intros.
Generalize (H1 H) ; Clear H1 H ; Intros.
Cbv Iota Beta Delta [valid_State2] in H.
Intuition.
EApply H ; EAuto.
NewInduction H1.
Inversion H1.
Cbv Iota Beta Delta [valid_State2].
Intros.
Discriminate H4.
Inversion H2 ; (Cbv Iota Beta Delta [valid_State2] ;
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State ;
Rewrite <-H5 in IHreachable_State ;
Intuition ; EApply H7 ; EAuto) Orelse Idtac.
Cbv Iota Beta Delta [valid_State2];
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2 ;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State;
Rewrite <-H6 in IHreachable_State ;
Intuition ; EApply H8 ; EAuto.
Cbv Iota Beta Delta [valid_State2];
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2 ;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State.
Rewrite <-H7 in IHreachable_State ;
Intuition.
CaseEq '(Location_dec loc0 loc1) ; Intros.
Clear H10 ; Subst.
Rewrite substHeap_equal in H9.
Injection H9 ; Intros ; Clear H9.
Rewrite <- H10 ; Unfold substField ; Simpl.
EApply IHreachable_State ; EAuto.
Clear H10.
Rewrite substHeap_diff in H9; Auto.
EApply IHreachable_State ; EAuto.
Cbv Iota Beta Delta [valid_State2];
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2 ;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State.
Rewrite <-H7 in IHreachable_State ;
Intuition.
Elim H5 ; Intros.
Cut (In x (classes P)) ; Intros.
Generalize (newObject_specif ? ? H3 H' loc0 H11) ; Intros.
Generalize (searchClass_some ? ? ? H10) ; Intuition.
Subst.
Generalize (H12 H6) ; Clear H12 ; Intros ; Intuition.
Subst.
Case (Location_dec loc0 loc1) ; Intros ; Subst.
Clear H6.
Rewrite substHeap_equal in H9.
Injection H9 ; Intros ; Clear H9.
Rewrite <-H6.
Unfold def ; Simpl.
Generalize in_inf_log ; Intros.
Unfold max_log_ClassName ; EApply H9 ; EAuto.
Rewrite substHeap_diff in H9 ; Auto.
EApply IHreachable_State ; EAuto.
Generalize (searchClass_some ? ? ? H10) ; Intuition.
Cbv Iota Beta Delta [valid_State2];
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2 ;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State.
Rewrite <-H7 in IHreachable_State ;
Intuition.
Cbv Iota Beta Delta [valid_State2];
Cbv Iota Beta Delta [valid_State2] in IHreachable_State ;
Clear valid_State2 ;
Generalize (IHreachable_State H1) ; Clear IHreachable_State ;
Intro IHreachable_State.
Rewrite <-H11 in IHreachable_State ;
Intuition.
Qed.
Lemma Nonempty_reachable_frame : (P : Program )(h : Heap ; c : CallStack)
(reachable_State P (config h c)) -> ~(c = (nil ?)).
Cut (P: Program ; h : Heap ; c: CallStack ; x : nat) (reachable_in P (config h c) x) -> ~(c = (nil ?)).
Intros.
Generalize (reachable_reachable_in P (config h c) H0) ; Intros.
Elim H1 ; Intros.
Apply (H P h c x H2).
Intro P.
LetTac PP := [w : nat](h : Heap ; c : CallStack)
(reachable_in P (config h c) w)->~c=(nil Frame).
Cut (w : nat) (PP w) ; Intros.
Cbv Iota Beta Delta [PP] in H.
EApply H ; EAuto.
NewInduction w.
Cbv Iota Beta Delta [PP].
Intros.
Inversion H.
Inversion H0.
Red ; Intros.
Discriminate H5.
Cbv Iota Beta Delta [PP] in IHw ;Cbv Iota Beta Delta [PP].
Clear PP.
Intros.
Inversion H.
Subst.
Inversion H3 ; Subst ; Try (Red ; Intros ;Discriminate H0).
Red ; Intros ;Discriminate H9.
Red; Intros ; Discriminate H2.
Qed.
Tactic Definition ElimEX x:=
Match Context With
[
id : (EX x : ? | ?) |- ?
] -> Elim id ; Clear id ; Intro x ; Intros ; Intuition.
Lemma Two_frames_in_CallStack : (P : Program ; h' : Heap ; m,m': MethodName ;
pc,pc' : progCount; s,s' : OperandStack ; l,l' : LocalVar ; sf : CallStack;n: nat)
(reachable_in P (config h' <m',pc',l',s'>::<m,pc,l,s>::sf) n) ->
(EX j : nat | (EX h'' : Heap | (EX s'' : OperandStack |
(lt j n) /\ (reachable_in P (config h'' <m,pc,l,s''>::sf) j)))).
Intro P.
LetTac PP:= [n: nat]
(h':Heap; m,m':MethodName; pc,pc':progCount; s,s':OperandStack;
l,l':LocalVar; sf:CallStack)
(reachable_in P
(config h' (frame m' pc' l' s')::(frame m pc l s)::sf) n)
->(EX j : nat | (EX h'' : Heap | (EX s'' : OperandStack |(
(lt j n) /\ (reachable_in P (config h'' <m,pc,l,s''>::sf) j))))).
Cut (n : nat) (PP n) ; Intros.
Cbv Iota Beta Delta [PP] in H ; Clear PP ; EApply H ; EAuto.
Generalize (lt_wf_ind n PP) ; Intro wf_ind.
Apply wf_ind ; Clear wf_ind ; Intros.
Cbv Iota Beta Delta [PP] in H ; Cbv Iota Beta Delta [PP] ; Clear PP.
Intros.
Inversion H0 ; Subst.
Inversion_clear H1 ; Subst ; Auto.
Cut (n0 = (S n1)) ; Intros ; Auto ; Subst.
Clear H4.
Inversion H0 ; Subst.
Cut (lt n1 (S n1)) ; [Intros Hlt | Auto with arith].
Tactic Definition TrivialCases st H Hlt Hreach j h s:=
Match Context With
[id : ?1 = st |- ?]-> Cut (st = ?1) ; Intros ; Auto ; Subst;
Solve [Generalize (H ? Hlt ? ? ? ? ? ? ? ? ? ? Hreach) ; Intros;
ElimEX j ; ElimEX h ; ElimEX s ;
Exists j ; Exists h ; Exists s ;
Split ; Trivial ; Auto with arith].
Inversion H6 ; Subst ; Try TrivialCases st0 H Hlt H4 j h'' s''.
Cut (st0 = (config h' (frame m pc l (ref loc)::(app A s))::sf)) ; Intros ;
Subst; Auto.
Exists n1 ; Exists h' ; Exists (ref loc)::(app A s) ; Split ; Auto.
Cut (st0 = (config h'
(frame m'0 pc'0 L' v::S')::
(frame m' pc0 l' S)::(frame m pc l s)::sf)) ; Intros ; Subst ; Auto.
Clear H7.
Generalize (H ? Hlt ? ? ? ? ? ? ? ? ? ? H4) ; Intros.
ElimEX j ; ElimEX h'' ; ElimEX s'' ; Intuition.
Rename S into AbS.
Cut (lt j (S n1)) ; [Intro | Auto with arith].
Generalize (H ? H3 ? ? ? ? ? ? ? ? ? ? H7) ; Intros.
ElimEX j0 ; ElimEX h''' ; ElimEX s''' ; Intuition.
Exists j0 ; Exists h''' ; Exists s''' ; Split ; Auto ; Omega.
Qed.
Lemma Frame_in_main : (P : Program ; h : Heap ; m: MethodName ; pc : progCount;
s : OperandStack ; l : LocalVar ; n : nat)
(reachable_in P (config h <m,pc,l, s>::(nil ?)) n) ->
m = (main P).
Intro P.
LetTac PP := [n:nat]
(h:Heap; m:MethodName; pc:progCount; s:OperandStack; l:LocalVar)
(reachable_in P (config h (frame m pc l s)::(nil Frame)) n)
->m=(main P).
Cut (n : nat) (PP n) ; Intros.
Cbv Iota Beta Delta [PP] in H ; Clear PP ; EApply H ; EAuto.
Generalize (lt_wf_ind n PP) ; Intro wf_ind.
Apply wf_ind ; Clear wf_ind ; Intros.
Cbv Iota Beta Delta [PP] in H ; Cbv Iota Beta Delta [PP] ; Clear PP.
Intros.
Inversion H0 ; Subst.
Inversion_clear H1 ; Subst ; Auto.
Cut (n0 = (S n1)) ; Intros ; Auto ; Subst.
Clear H4.
Inversion H0 ; Subst.
Cut (lt n1 (S n1)) ; [Intros Hlt | Auto with arith].
Tactic Definition TrivialCases' st H Hlt Hreach:=
Match Context With
[id : ?1 = st |- ?]-> Cut (st = ?1) ; Intros ; Auto;
Subst;
Apply (H ? Hlt ? ? ? ? ? Hreach).
Inversion H6 ; Subst ; Try (TrivialCases' st0 H Hlt H4).
Cut (st0 = (config h
(frame m' pc' L' v::S')::(frame m pc0 l S)::(nil Frame))) ; Intros ;
Auto.
Subst.
Clear H7.
Generalize (Two_frames_in_CallStack ? ? ? ? ? ? ? ? ? ? ? ? H4) ; Intros.
ElimEX j ; ElimEX h''; ElimEX s''.
Rename S into AbS.
Cut (lt j (S n1)) ; [Clear H5 ; Intro H5 | Auto with arith].
Apply (H ? H5 ? ? ? ? ? H7).
Qed.
Lemma return_inv2: (P :Program ; h : Heap ; m: MethodName ; pc : progCount;
s : OperandStack ; l : LocalVar ; sf : CallStack ; n : nat)
(reachable_in P (config h <m,pc,l, s>::sf) n) ->
(instructionAt P m pc)=(Some return)->
(EX m' : MethodName | (EX pc' : progCount | (EX l' : LocalVar |
(EX s' : OperandStack | (EX sf' : CallStack | sf = ((<m',pc',l', s'>)::sf')))))).
Intros.
CaseEq sf ; Intros ; Subst.
Generalize (Frame_in_main ? ? ? ? ? ? ? H) ; Intros.
Cut (main P) = m ; Intros ; Auto.
Elim (No_return_in_main ? ? pc H2) ; Auto.
CaseEq f ; Intros.
Exists m0 ; Exists p ; Exists l1 ; Exists o ; Exists l0 ; Auto.
Qed.
Lemma return_inv: (P :Program ; h : Heap ; m, m' : MethodName ; pc, pc' : progCount;
s, s' : OperandStack ; l, l' : LocalVar ; sf : CallStack ; n : nat)
(reachable_in P (config h <m,pc,l, s>::<m',pc',l',s'>::sf) n) ->
(EX j : nat | (lt j n) /\ (EX h' : Heap |
(EX s'' : OperandStack | (reachable_in P (config h' <m',pc',l',s''>::sf) j) /\
(EX mID : MethodID |(instructionAt P m' pc')=(Some (invokevirtual mID)) /\
(EX loc : Location | (EX A : OperandStack | (EX B : OperandStack|
(EX o : ClassInst | (EX M : Method |
s'' = (((ref loc))::(app A B)) /\ (h' loc) = (Some o) /\
(methodLookup P mID (class o) ) = (Some M) /\
(searchMethod P m) = (Some M) /\
(length A) = (nbArguments M)))))))))).
LetTac PP := [w: nat] (P:Program; h:Heap; m,m':MethodName; pc,pc':progCount;
s,s':OperandStack; l,l':LocalVar; sf:CallStack)
(reachable_in P
(config h (frame m pc l s)::(frame m' pc' l' s')::sf) w)
->(EX j:
nat|(lt j w)
/\(EX h':
Heap|(EX s'':
OperandStack|(reachable_in P
(config h'
(frame m' pc' l' s'')::sf)
j)
/\(EX mID:
MethodID|(instructionAt
P m' pc')
=(Some
(
invokevirtual
mID))
/\(EX loc:
Location|(
EX A:
OperandStack|(
EX B:
OperandStack|(
EX o:
ClassInst|(
EX M:
Method|
s''
=(
(ref loc)::
(app A B))
/\
(h' loc)
=(
Some o)
/\
(methodLookup
P mID
(class o))
=(
Some M)
/\
(searchMethod
P m)
=(
Some M)
/\
(length A)
=(
nbArguments
M)))))))))).
Cut (w : nat) (PP w) ; Intros.
Generalize (H n) ; Clear H.
Replace PP with [w:nat]
(P:Program; h:Heap; m,m':MethodName; pc,pc':progCount;
s,s':OperandStack; l,l':LocalVar; sf:CallStack)
(reachable_in P
(config h (frame m pc l s)::(frame m' pc' l' s')::sf) w)
->(EX j:
nat|(lt j w)
/\(EX h':
Heap|(EX s'':
OperandStack|(reachable_in P
(config h'
(frame m' pc' l' s'')::
sf) j)
/\(EX mID:
MethodID|
(instructionAt P
m' pc')
=(Some
(invokevirtual
mID))
/\(EX loc:
Location|(
EX A:
OperandStack|(
EX B:
OperandStack|(
EX o:
ClassInst|(
EX M:
Method|
s''
=(
(ref loc)::
(app A B))
/\
(h' loc)
=(
Some o)
/\
(methodLookup
P mID
(class o))
=(
Some M)
/\
(searchMethod
P m)
=(
Some M)
/\
(length A)
=(
nbArguments
M)))))))))) ; Auto.
Intros H ; EApply H ; EAuto.
Generalize (lt_wf_ind w PP) ; Intro wf_ind.
Apply wf_ind ; Clear wf_ind.
Intros n Hind.
Clear w.
Cbv Iota Beta Delta [PP].
Intros.
Inversion H.
Inversion H0.
Cut (n = (S n0)) ; Intros ; Subst ; Auto.
Clear H3.
CaseEq st ; Intros.
CaseEq c ; Intros.
Generalize (reachable_in_reachable P st n0 H0); Intros.
Rewrite H2 in H4.
Generalize (Nonempty_reachable_frame P h0 c H4) ; Intros.
Red in H5 ; Elim (H5 H3).
Rewrite H3 in H2 ; Rewrite H2 in H1.
Cut (lt n0 (S n0)) ; [Intro Hlt | Omega].
Cbv Iota Beta Delta [PP] in Hind ; Clear PP.
Tactic Definition InjFrame :=
Match Context With
[id : (frame ? ? ? ?) = (frame ? ? ? ?)|- ?] -> Injection id ; Intros ; Subst.
Inversion H1 ; Try (Intros ; Subst ; CaseEq f ; Intros ; Subst ; InjFrame ;
Generalize (Hind n0 Hlt ? ? ? ? ? ? ? ? ? ? ? H0) ; Clear Hind ; Intros ;
ElimEX j ; Exists j ; Split ; Try Omega ; ElimEX h' ; Exists h' ;
ElimEX s'' ; Exists s'' ; Split ; Try Omega ; Auto).
CaseEq f ; Intros ; Subst.
Injection H6 ; Intros ; Subst.
Clear H6.
Exists n0.
Split ; Auto with arith.
Exists h.
Exists o0.
Split ; Auto.
Exists mID ; Split ; Auto.
Exists loc.
Exists A ; Exists s'.
Exists o.
Exists M'.
Intuition ; Auto.
Clear Hind.
EApply searchMethod_some_inv.
Unfold methodLookup in H21.
CaseEq '(searchClass P (class o)) ; Intros.
Rewrite H3 in H21.
CaseEq '(searchWithMethodID (list_methods_lookup c) mID) ; Intros.
Rewrite H4 in H21.
CaseEq '(searchMethod P m0) ; Intros.
Rewrite H5 in H21.
Injection H21 ; Intros ; Subst.
Clear H21.
Generalize (searchMethod_some P m0 M') ; Intros; Intuition.
Rewrite H5 in H21; Discriminate H21.
Rewrite H4 in H21 ; Discriminate H21.
Cut (EX c:Class|(In c (classes P))/\(class o) = (nameClass c)) ; Intros.
Generalize (searchClass_find P (class o) H4); Intros.
Red in H5 ; Elim (H5 H3).
Elim H20 ; Intuition.
Exists x ; Auto.
CaseEq f ; Intros ; Subst.
Injection H7 ; Intros ; Subst.
Clear H7.
Rename S into AbS.
Rewrite <-H8 in H0.
Generalize (Hind n0 Hlt ? ? ? ? ? ? ? ? ? ? ? H0) ; Intros.
Elim H3 ; Clear H3 ; Intros.
Elim H3 ; Clear H3; Intros.
Elim H4 ; Clear H4 ; Intros.
Elim H4 ; Clear H4; Intros.
Elim H4 ; Clear H4; Intros.
Clear H0 H5.
Cut (lt x (S n0)) ; [Intro Hlt' | Omega].
Generalize (Hind x Hlt' ? ? ? ? ? ? ? ? ? ? ? H4) ; Clear Hind ; Intros.
ElimEX x2 ; ElimEX x3 ; ElimEX x4 ; ElimEX x5 ; ElimEX x6 ; ElimEX x7 ; ElimEX x8 ; ElimEX x9;
ElimEX x10 ; Subst.
Cut (lt x2 (S n0)) ; Intros ; Try Omega.
Exists x2 ; Split ; Auto.
Exists x3 ; Exists (ref x6)::(app x7 x8) ; Split ; Auto.
Exists x5 ; Split ; Auto.
Exists x6 ; Exists x7 ; Exists x8 ; Exists x9 ; Exists x10.
Intuition ; Auto.
Qed.