Lemma list_iblock_checker_correct

1 files changed, 20 insertions, 0 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 4d556711..62833dc3 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -100,6 +100,26 @@ Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
   | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl 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 list_iblock_checker_correct btl l: 
+  list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt.
+Proof.
+  intros CHECKER e H; induction l as [|(n & ibf) l]; intuition.
+  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
+Qed.
+
 Definition liveness_checker (f: BTL.function): res unit :=
   match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with
   | true => OK tt