From a0529ae7a4eb991c39f258a8dbc003dd83ad3d36 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 9 Dec 2020 11:02:56 +0100
Subject: apply_cond_sound

---
 backend/CSE3analysisproof.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'backend')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index a012771c..29d171eb 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1341,6 +1341,20 @@ Section SOUNDNESS.
     unfold sem_rel in REL.
     eapply REL; eassumption.
   Qed.
+
+  Lemma apply_cond_sound :
+    forall pc cond args rel rs m
+      (COND : (eval_condition cond (rs ## args) m) = Some true)
+      (REL : (sem_rel rel rs m)),
+      (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    unfold apply_cond.
+    intros.
+    pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
+    destruct apply_cond1 eqn:COND1.
+    { apply apply_cond0_sound; auto. }
+    exact SOUND1.
+  Qed.
   
   (*
   Section INDUCTIVENESS.
-- 
cgit