From 3f305f0f8035b9de9ef048910afa9840766c8498 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 1 Jan 2023 18:28:13 +0000 Subject: Add all_evaluable lemma for seq_app --- src/hls/GiblePargenproof.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src') 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) -> -- cgit