diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-16 22:39:56 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-16 22:39:56 +0100 |
| commit | 25e9903b5cf250c70316c21f2f94df3e0a876937 (patch) | |
| tree | 2a55b28addd8cc97f1f4c2eb5b33ff2c1f3582f5 | |
| parent | a00d05e5336d208238b169ee6abf651398a130e2 (diff) | |
| download | compcert-kvx-25e9903b5cf250c70316c21f2f94df3e0a876937.tar.gz compcert-kvx-25e9903b5cf250c70316c21f2f94df3e0a876937.zip | |
there remains two tricky cases
| -rw-r--r-- | scheduling/RTLpathSE_theory.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index 06b3a646..c43c530e 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -1785,13 +1785,24 @@ Proof. + constructor; assumption. Qed. -Lemma seval_builtin_sval_correct ge sp m rs0 m0 v bs2: forall bs1, +Lemma seval_builtin_sval_correct ge sp m rs0 m0: forall bs1 v bs2, seval_builtin_arg ge sp m rs0 m0 bs1 v -> (seval_builtin_sval ge sp bs1 rs0 m0) = (seval_builtin_sval ge sp bs2 rs0 m0) -> seval_builtin_arg ge sp m rs0 m0 bs2 v. Proof. - induction 1. - - simpl. rewrite H. intros. destruct bs2; simpl in *; try congruence. + induction bs1. + all: try(destruct bs2; + intros Hinv Hrew; + inv Hinv; + cbn in *; + try constructor; + repeat (destruct seval_sval; [idtac | discriminate]); + repeat (destruct seval_builtin_sval; [idtac | discriminate]); + try congruence; + inv Hrew; + constructor). + - admit. + - admit. Admitted. Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1, |