Library collect
Require Export syntax.
Require Export List.
Section collect.
Variable Constraint : Set.
Variable gen : Program -> MethodName ->
progCount -> Instruction -> list Constraint.
Lemma inf_log_prop1 : forall (i:Instruction) q pc,
inf_log (Ppred (nat2pos (length (i :: q)) + pc)) 32 ->
inf_log pc 32.
Proof.
intros.
apply inf_log_le with (1:=H); simpl.
rewrite Pplus_succ_permute_l.
rewrite Ppred_succ.
rewrite nat_of_P_plus_morphism; omega.
Qed.
Implicit Arguments inf_log_prop1 [i q pc].
Lemma inf_log_prop2 : forall (i:Instruction) q pc,
inf_log (Ppred (nat2pos (length (i :: q)) + pc)) 32 ->
inf_log (Ppred (nat2pos (length q) + Psucc pc)) 32.
Proof.
intros.
simpl in H; rewrite Pplus_succ_permute_l in H.
rewrite <- Pplus_succ_permute_r in H; auto.
Qed.
Implicit Arguments inf_log_prop2 [i q pc].
Lemma gen_instructions_rec :
forall (P:Program) (m:MethodName) (l:list Instruction) (pc:positive),
inf_log (Ppred (Pplus (nat2pos (length l)) pc)) (32) -> (list Constraint).
Proof.
intros P m; induction l as [|i q]; intros.
exact nil.
refine (app (gen P m (exP pc(inf_log_prop1 H)) i) (IHq (Psucc pc) (inf_log_prop2 H))).
Defined.
Lemma in_gen_instructions_rec_intro : forall P m i l pc n
(H:inf_log (Ppred (Pplus (nat2pos (length l)) pc)) (32)),
(nth_error l n)=(Some i) ->
exists pc', (word2pos pc') = (Ppred (Pplus (nat2pos n) pc)) /\
(incl (gen P m pc' i)
(gen_instructions_rec P m l pc H)).
Proof.
induction l; simpl; intros.
destruct n; discriminate H0.
destruct n; simpl in H0.
injection H0; intros; subst; clear H0.
exists (exP pc (inf_log_prop1 (i:=i) (q:=l) (pc:=pc) H)); split.
simpl; destruct pc.
rewrite xI_succ_xO.
rewrite xO_succ_permute.
rewrite Ppred_succ; auto.
rewrite xI_succ_xO.
rewrite Ppred_succ; auto.
auto.
auto with datatypes.
destruct (IHl (Psucc pc) n (inf_log_prop2 (i:=a) (q:=l) (pc:=pc) H) H0)
as [pc' (H1,H2)].
exists pc'; split.
rewrite H1; simpl.
rewrite Pplus_succ_permute_l; rewrite Pplus_succ_permute_r; auto.
auto with datatypes.
Qed.
Lemma in_gen_instructions_rec_elim : forall P m l pc c
(H:inf_log (Ppred (Pplus (nat2pos (length l)) pc)) (32)),
In c (gen_instructions_rec P m l pc H) ->
exists n, exists i, exists pc',
(word2pos pc') = (Ppred (Pplus (nat2pos n) pc)) /\
(nth_error l n)=(Some i) /\ In c (gen P m pc' i).
Proof.
induction l; simpl; intros.
elim H0.
elim (in_app_or _ _ _ H0); clear H0; intros H0.
exists 0; exists a; exists (exP pc (inf_log_prop1 (i:=a) (q:=l) (pc:=pc) H)); split.
simpl; destruct pc.
rewrite xI_succ_xO.
rewrite xO_succ_permute.
rewrite Ppred_succ; auto.
rewrite xI_succ_xO.
rewrite Ppred_succ; auto.
auto.
split; auto.
elim (IHl _ _ _ H0); intros n (i,(pc',(H1,(H2,H3)))).
exists (S n); exists i; exists pc'; split; auto.
rewrite H1; simpl.
rewrite Pplus_succ_permute_l; rewrite Pplus_succ_permute_r; auto.
Qed.
Lemma inf_logM : forall M,
inf_log (Ppred (Pplus (nat2pos (length (instructions M))) xH)) (32).
Proof.
intros.
rewrite <- Pplus_one_succ_r.
rewrite Ppred_succ.
apply instructions_nb.
Qed.
Definition gen_instructions (P:Program) (M:Method) : list Constraint :=
gen_instructions_rec P (nameMethod M) (instructions M) xH (inf_logM M).
Lemma in_gen_instructions_intro : forall P M i pc,
(nth_positive (instructions M) (word2pos pc))=(Some i) ->
exists pc', eq_word pc pc' /\
incl (gen P (nameMethod M) pc' i) (gen_instructions P M).
Proof.
unfold gen_instructions, nth_positive; intros.
destruct (in_gen_instructions_rec_intro P (nameMethod M) i (instructions M) xH _ (inf_logM M) H)
as [pc' (H1,H2)].
exists pc'; split; simpl.
apply eq_word_def'.
rewrite H1.
rewrite Pplus_comm.
rewrite <- Pplus_one_succ_l.
rewrite Ppred_succ.
unfold nat2pos.
apply nat_of_P_inj.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
generalize (lt_O_nat_of_P pc); omega.
auto.
Qed.
Lemma in_gen_instructions_elim : forall P M c,
In c (gen_instructions P M) ->
exists pc, exists i,
(nth_positive (instructions M) (word2pos pc))=(Some i) /\
In c (gen P (nameMethod M) pc i).
Proof.
unfold gen_instructions, nth_positive; intros.
destruct (in_gen_instructions_rec_elim P (nameMethod M) (instructions M) xH c (inf_logM M) H)
as [n (i,(pc,(H1,(H2,H3))))].
exists pc; exists i; split; auto.
rewrite H1.
rewrite <- Pplus_one_succ_r.
rewrite Ppred_succ.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl; auto.
Qed.
Fixpoint gen_methods_rec
(P:Program) (l:list Method) {struct l} : (list Constraint) :=
match l with
nil => nil
| M::q => app (gen_instructions P M) (gen_methods_rec P q)
end.
Lemma in_gen_methods_rec_intro : forall P M pc i l,
In M l ->
nth_positive (instructions M) (word2pos pc) = Some i ->
exists pc', eq_word pc pc' /\
incl (gen P (nameMethod M) pc' i) (gen_methods_rec P l).
Proof.
induction l; simpl; intros.
elim H.
destruct H; subst.
destruct (in_gen_instructions_intro P _ _ _ H0) as [pc' (H1,H2)].
exists pc'; split; auto with datatypes.
destruct (IHl H H0) as [pc' (H1,H2)].
exists pc'; split; auto with datatypes.
Qed.
Lemma in_gen_methods_rec_elim : forall P l c,
In c (gen_methods_rec P l) ->
exists M, exists pc, exists i,
In M l /\
(nth_positive (instructions M) (word2pos pc))=(Some i) /\
In c (gen P (nameMethod M) pc i).
Proof.
induction l; simpl; intros.
elim H.
destruct (in_app_or _ _ _ H); clear H; intros.
destruct (in_gen_instructions_elim _ _ _ H0) as [pc (i,(H1,H2))].
exists a; exists pc; exists i; split; auto.
destruct (IHl _ H0) as [M (pc,(i,(H1,(H2,H3))))].
exists M; exists pc; exists i; split; auto.
Qed.
Definition collect (P:Program) : list Constraint :=
gen_methods_rec P (main P :: methods P).
Lemma in_collect_intro : forall P m pc i,
instructionAt P m pc = Some i ->
exists m', exists pc', eq_word pc pc' /\ eq_word m m' /\
incl (gen P m' pc' i) (collect P).
Proof.
unfold instructionAt, collect; intros P m pc i.
CaseEq (searchMethod P m); intros.
destruct (in_gen_methods_rec_intro P _ _ _ _ (searchMethod_some_in _ _ _ H) H0)
as [pc' (H1,H2)].
exists (nameMethod m0); exists pc'; split; auto.
split; auto.
apply (searchMethod_some _ _ _ H).
discriminate H0.
Qed.
Lemma in_collect_elim : forall P c,
In c (collect P) -> exists m, exists pc, exists i,
instructionAt P m pc = Some i /\ In c (gen P m pc i).
Proof.
unfold instructionAt, collect; intros P c H.
destruct (in_gen_methods_rec_elim _ _ _ H) as [M (pc,(i,(H1,(H2,H3))))].
exists (nameMethod M); exists pc; exists i; split; auto.
rewrite (searchMethod_eq_some _ _ H1); auto.
Qed.
Lemma prop_on_collect : forall (Q:Constraint->Prop) P,
(forall m pc i c, instructionAt P m pc = Some i ->
In c (gen P m pc i) -> Q c) ->
forall c, In c (collect P) -> Q c.
Proof.
intros.
destruct (in_collect_elim _ _ H0) as [m (pc,(i,(H1,H2)))].
eauto.
Qed.
End collect.
Section collectM.
Variable Constraint : Set.
Variable gen : Program -> MethodName -> list Constraint.
Fixpoint genM_methods_rec
(P:Program) (l:list Method) {struct l} : (list Constraint) :=
match l with
nil => nil
| M::q => app (gen P (nameMethod M)) (genM_methods_rec P q)
end.
Lemma in_genM_methods_rec_intro : forall P M l,
In M l ->
incl (gen P (nameMethod M)) (genM_methods_rec P l).
Proof.
induction l; simpl; intros.
elim H.
destruct H; subst; auto with datatypes.
Qed.
Lemma in_genM_methods_rec_elim : forall P l c,
In c (genM_methods_rec P l) ->
exists M,
In M l /\
In c (gen P (nameMethod M)).
Proof.
induction l; simpl; intros.
elim H.
destruct (in_app_or _ _ _ H); clear H; intros.
exists a; auto.
destruct (IHl _ H0) as [M (H2,H3)].
exists M; split; auto.
Qed.
Definition collectM (P:Program) : list Constraint :=
genM_methods_rec P (main P :: methods P).
Lemma in_collectM_intro : forall P M,
In M (main P :: methods P) ->
incl (gen P (nameMethod M)) (collectM P).
Proof.
unfold instructionAt, collectM; intros P m pc i H.
apply in_genM_methods_rec_intro with m; auto.
Qed.
Lemma in_collectM_elim : forall P c,
In c (collectM P) -> exists M,
In M (main P :: methods P) /\ In c (gen P (nameMethod M)).
Proof.
unfold instructionAt, collectM; intros P c H.
destruct (in_genM_methods_rec_elim _ _ _ H) as [M (H2,H3)].
eauto.
Qed.
Lemma prop_on_collectM : forall (Q:Constraint->Prop) P,
(forall M c, In M (main P :: methods P) ->
In c (gen P (nameMethod M)) -> Q c) ->
forall c, In c (collectM P) -> Q c.
Proof.
intros.
destruct (in_collectM_elim _ _ H0) as [m (H1,H2)].
eauto.
Qed.
End collectM.
Index
This page has been generated by coqdoc