diff options
| -rw-r--r-- | backend/CSE3analysisproof.v | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v index 75dae91a..a012771c 100644 --- a/backend/CSE3analysisproof.v +++ b/backend/CSE3analysisproof.v @@ -1317,7 +1317,31 @@ Section SOUNDNESS. } exact REL. Qed. - + + Lemma apply_cond0_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 (apply_cond0 (ctx:=ctx) pc cond args rel) rs m). + Proof. + intros. + unfold apply_cond0. + destruct eq_find as [eq_id | ] eqn:FIND; cbn. + 2: assumption. + pose proof (eq_find_sound pc (Cond cond args) eq_id FIND) as FIND_SOUND. + intros eq_id' eq' CONTAINS CATALOG. + destruct (peq eq_id eq_id'). + { subst eq_id'. + unfold sem_eq. + rewrite FIND_SOUND in CATALOG. + inv CATALOG. + assumption. + } + rewrite PSet.gaddo in CONTAINS by assumption. + unfold sem_rel in REL. + eapply REL; eassumption. + Qed. + (* Section INDUCTIVENESS. Variable fn : RTL.function. |