diff options
| -rw-r--r-- | scheduling/RTLpathWFcheck.v | 19 |
1 files changed, 3 insertions, 16 deletions
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index f5198e68..0ddc3142 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -88,24 +88,11 @@ Fixpoint exit_list_checker (pm: path_map) (l: list node): bool := | pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l' end. -Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. -Proof. - destruct o; simpl; intuition. - - eauto. - - firstorder. try_simplify_someHyps. -Qed. - -Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. -Proof. - intros; rewrite lazy_and_Some_true; firstorder. - destruct x; auto. -Qed. - Lemma exit_list_checker_correct pm l pc: exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt. Proof. intros EXIT PC; induction l; intuition. - simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT. + simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT. firstorder (subst; eauto). Qed. @@ -167,7 +154,7 @@ Lemma list_path_checker_correct f pm l: list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt. Proof. intros CHECKER e H; induction l as [|(pc & path) l]; intuition. - simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). + simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). Qed. Definition function_checker (f: RTL.function) (pm: path_map): bool := @@ -178,7 +165,7 @@ Lemma function_checker_correct f pm pc path: pm!pc = Some path -> path_checker f pm pc path = Some tt. Proof. - unfold function_checker; rewrite lazy_and_Some_true. + unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true. intros (ENTRY & PATH) PC. exploit list_path_checker_correct; eauto. - eapply PTree.elements_correct; eauto. |