diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 11:18:23 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 11:18:23 +0100 |
| commit | b00665af60dc019c75e0f2a64099db163b4c3c26 (patch) | |
| tree | 881bb849452f5414034d4face0839b4d2eb5dfdb /backend/CSE3analysisproof.v | |
| parent | f557bb9d9f264695a94cc598b3027c978eb5aca6 (diff) | |
| download | compcert-kvx-b00665af60dc019c75e0f2a64099db163b4c3c26.tar.gz compcert-kvx-b00665af60dc019c75e0f2a64099db163b4c3c26.zip | |
forward_move_rhs_sound
Diffstat (limited to 'backend/CSE3analysisproof.v')
| -rw-r--r-- | backend/CSE3analysisproof.v | 12 |
1 files changed, 12 insertions, 0 deletions
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. |