factorize lazy_and_Some_* lemmas

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.