diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-17 16:23:12 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-17 16:23:12 +0100 |
| commit | ffbc23971b75e96c0c3b5218c2aaa4c0376544ca (patch) | |
| tree | e0fb193c4805274fbc0cabb63ae5e9ed35ff80c9 | |
| parent | 25e9903b5cf250c70316c21f2f94df3e0a876937 (diff) | |
| download | compcert-kvx-ffbc23971b75e96c0c3b5218c2aaa4c0376544ca.tar.gz compcert-kvx-ffbc23971b75e96c0c3b5218c2aaa4c0376544ca.zip | |
a little lemma on list of builtins
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index 48f5f65d..c9033260 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -743,10 +743,23 @@ Proof. erewrite list_sval_eval_preserved; eauto. Qed. +Lemma seval_builtin_sval_preserved ge ge' sp sv rs0 m0: + (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> + seval_builtin_sval ge sp sv rs0 m0 = + seval_builtin_sval ge' sp sv rs0 m0. +Proof. +Admitted. + Lemma seval_list_builtin_sval_preserved ge ge' sp lsv rs0 m0: (forall s : ident, Genv.find_symbol ge' s = Genv.find_symbol ge s) -> - seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv rs0 m0. -Admitted. (* TODO *) + seval_list_builtin_sval ge sp lsv rs0 m0 = + seval_list_builtin_sval ge' sp lsv rs0 m0. +Proof. + induction lsv; intro FIND; cbn. { trivial. } + erewrite seval_builtin_sval_preserved by eauto. + erewrite IHlsv by eauto. + reflexivity. +Qed. Lemma barg_proj_refines_eq ge ge' sp rs0 m0: (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> |