diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 15:37:58 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-05 15:37:58 +0100 |
| commit | ad16517ee345e53398c69c62d975474475880799 (patch) | |
| tree | a988470a250ee713f86eba5e57cacc544f8dda0b /backend/CSE2proof.v | |
| parent | dabfcfe9aeffe4bcb3d2a27a46e2b10b5d725154 (diff) | |
| download | compcert-kvx-ad16517ee345e53398c69c62d975474475880799.tar.gz compcert-kvx-ad16517ee345e53398c69c62d975474475880799.zip | |
progress on wellformed reg
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 350cdb24..e0244518 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -171,6 +171,38 @@ Proof. Qed. Local Hint Resolve wellformed_mem_kill_reg : wellformed. +Lemma kill_sym_val_referenced: + forall dst, + forall sv, + (kill_sym_val dst sv)=true <-> In dst (referenced_by sv). +Proof. + intros. + destruct sv; simpl. + - destruct peq; intuition congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. + - rewrite existsb_exists. + split. + + intros [x [IN EQ]]. + destruct peq. + * subst x; trivial. + * discriminate. + + intro. + exists dst. + split; trivial. + destruct peq; trivial. + congruence. +Qed. + Lemma wellformed_mem_kill_mem: forall rel, (wellformed_mem rel) -> (wellformed_mem (kill_mem rel)). |