diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-17 16:28:08 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-17 16:28:08 +0100 |
| commit | fca587ef6b13cef4c72423ed03709d296b3ed08a (patch) | |
| tree | 60bd66a037e2c52f96e65ed63ed2fedf0466321e | |
| parent | ffbc23971b75e96c0c3b5218c2aaa4c0376544ca (diff) | |
| download | compcert-kvx-fca587ef6b13cef4c72423ed03709d296b3ed08a.tar.gz compcert-kvx-fca587ef6b13cef4c72423ed03709d296b3ed08a.zip | |
seval_builtin_sval_preserved
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index c9033260..c9e272c0 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/scheduling/RTLpathSE_simu_specs.v @@ -748,7 +748,10 @@ Lemma seval_builtin_sval_preserved ge ge' sp sv rs0 m0: seval_builtin_sval ge sp sv rs0 m0 = seval_builtin_sval ge' sp sv rs0 m0. Proof. -Admitted. + induction sv; intro FIND; cbn. + all: try (erewrite seval_preserved by eauto); trivial. + all: erewrite IHsv1 by eauto; erewrite IHsv2 by eauto; reflexivity. +Qed. 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) -> |