From b00665af60dc019c75e0f2a64099db163b4c3c26 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 10 Mar 2020 11:18:23 +0100 Subject: forward_move_rhs_sound --- backend/CSE3analysisproof.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'backend/CSE3analysisproof.v') diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index b9f4da44..2b963e39 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -421,4 +421,16 @@ Section SOUNDNESS. simpl in FIND. intuition congruence. Qed. + + Theorem forward_move_rhs_sound : + forall sop args rel rs m v, + (sem_rel rel rs m) -> + (sem_rhs sop args rs m v) -> + (sem_rhs sop (forward_move_l (ctx := ctx) rel args) rs m v). + Proof. + intros until v. + intros REL RHS. + destruct sop; simpl in *. + all: erewrite forward_move_l_sound by eassumption; assumption. + Qed. End SOUNDNESS. -- cgit