From ad16517ee345e53398c69c62d975474475880799 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 5 Feb 2020 15:37:58 +0100 Subject: progress on wellformed reg --- backend/CSE2proof.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'backend/CSE2proof.v') 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)). -- cgit