From fe286deeb5c8a81aad20b81cd2ce9a586cc99dca Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 May 2023 15:46:48 +0100 Subject: Add proof about preds_empty --- src/hls/GiblePargenproofBackward.v | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'src/hls/GiblePargenproofBackward.v') diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 3434eba..f3fdacd 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -862,10 +862,19 @@ Proof. constructor. constructor. cbn. constructor. constructor. Qed. +Lemma all_preds_in_empty: + all_preds_in empty (PTree.empty unit). +Proof. + unfold all_preds_in; split; intros; apply NE.Forall_forall; intros. + - rewrite get_empty in H. inv H. inv H0. + - cbn in *. inv H. inv H0. +Qed. + Lemma abstr_seq_reverse_correct: - forall sp x i i' ti cf x' l, - abstract_sequence' x = Some (x', l) -> + forall sp x i i' ti cf x' l lm, + abstract_sequence' x = Some (x', l, lm) -> evaluable_pred_list (mk_ctx i sp ge) x'.(forest_preds) l -> + evaluable_pred_list_m (mk_ctx i sp ge) x'.(forest_preds) lm -> sem (mk_ctx i sp ge) x' (i', (Some cf)) -> state_lessdef i ti -> exists ti', SeqBB.step ge sp (Iexec ti) x (Iterm ti' cf) @@ -874,7 +883,7 @@ Proof. intros. unfold abstract_sequence' in H. unfold Option.map, Option.bind in H. repeat destr. inv H. inv Heqo. eapply abstr_seq_reverse_correct_fold; - try eassumption; try reflexivity; apply sem_empty. + try eassumption; try reflexivity; auto using sem_empty, all_preds_in_empty. Qed. (*| -- cgit