diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-01-01 18:28:13 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-01-01 18:28:13 +0000 |
| commit | 3f305f0f8035b9de9ef048910afa9840766c8498 (patch) | |
| tree | f5c81b4f762acc0cd257f93b0f1138bd2b68959a /src/hls/GiblePargenproof.v | |
| parent | de9ebbc8e34be60bcb023bec3cfdb5f33c8cd56b (diff) | |
| download | vericert-3f305f0f8035b9de9ef048910afa9840766c8498.tar.gz vericert-3f305f0f8035b9de9ef048910afa9840766c8498.zip | |
Add all_evaluable lemma for seq_app
Diffstat (limited to 'src/hls/GiblePargenproof.v')
| -rw-r--r-- | src/hls/GiblePargenproof.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 104d1f4..8754ce5 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1976,6 +1976,15 @@ all be evaluable. eapply all_evaluable2_cons in H0. eauto. Qed. + 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). + Proof. + intros. + Lemma eval_predf_update_evaluable : forall A (ctx: @ctx A) curr_p next_p f f_next instr, update (curr_p, f) instr = Some (next_p, f_next) -> |