Commit 52faac32 authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

factorize lazy_and_Some_* lemmas

parent f9ea38dc
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment