diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 15:46:48 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-05-21 15:47:00 +0100 |
| commit | fe286deeb5c8a81aad20b81cd2ce9a586cc99dca (patch) | |
| tree | f9e39a896033f98271e74c82409b02c18478ffad /src/hls/GiblePargenproofBackward.v | |
| parent | 78026c97881e4500fd3e46283f2e59e5e57973fb (diff) | |
| download | vericert-fe286deeb5c8a81aad20b81cd2ce9a586cc99dca.tar.gz vericert-fe286deeb5c8a81aad20b81cd2ce9a586cc99dca.zip | |
Add proof about preds_empty
Diffstat (limited to 'src/hls/GiblePargenproofBackward.v')
| -rw-r--r-- | src/hls/GiblePargenproofBackward.v | 15 |
1 files changed, 12 insertions, 3 deletions
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. (*| |