diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-01-02 21:36:00 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-01-02 21:36:00 +0000 |
| commit | 7f35332a5a8e47ec685c6309ea99416d19a5fb2f (patch) | |
| tree | ea3fc5bb0f35869892bceeb1390a942309e183ac /src/hls/GiblePargenproof.v | |
| parent | 3f305f0f8035b9de9ef048910afa9840766c8498 (diff) | |
| download | vericert-7f35332a5a8e47ec685c6309ea99416d19a5fb2f.tar.gz vericert-7f35332a5a8e47ec685c6309ea99416d19a5fb2f.zip | |
Work on simplifying seq_app evaluation lemma
Diffstat (limited to 'src/hls/GiblePargenproof.v')
| -rw-r--r-- | src/hls/GiblePargenproof.v | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 8754ce5..f53cb87 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1976,14 +1976,19 @@ all be evaluable. eapply all_evaluable2_cons in H0. eauto. Qed. + Lemma all_evaluable_pred_ret : + forall A B G (ctx: @ctx G) (sem: @Abstr.ctx G -> A -> B -> Prop) + (a: A) (b: B), + sem ctx a b -> + all_evaluable2 ctx sem (pred_ret a). + Admitted. + Lemma eval_predf_seq_app_evaluable : - forall A B C D (ctx: @ctx A) (sem: @Abstr.ctx A -> C -> D -> Prop) - (a: predicated (B -> C)) b, - all_evaluable2 ctx sem a -> - all_evaluable2 ctx sem b -> - all_evaluable2 ctx sem (seq_app a b). + forall A B G (ctx: @ctx G) (sem: @Abstr.ctx G -> A -> B -> Prop) (l: predicated A) a, + all_evaluable2 ctx sem l -> + all_evaluable2 ctx sem (seq_app a l). Proof. - intros. + intros. unfold seq_app. Lemma eval_predf_update_evaluable : forall A (ctx: @ctx A) curr_p next_p f f_next instr, |