From 7c6ce18466ed1de58a0f99c785c777d63a9a6149 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 14 Oct 2020 21:56:30 +0200
Subject: a bit of progress

---
 backend/CSE3analysisproof.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'backend/CSE3analysisproof.v')

diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index f4e3672d..0ddaa527 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -745,6 +745,25 @@ Section SOUNDNESS.
 
   Hint Resolve oper1_sound : cse3.
 
+  Lemma rel_idem_replace:
+    forall rel rs r m,
+      sem_rel rel rs m ->
+      sem_rel rel rs # r <- (rs # r) m.
+  Proof.
+    intros until m.
+    intro REL.
+    unfold sem_rel, sem_eq, sem_rhs in *.
+    intros.
+    specialize REL with (i:=i) (eq0:=eq).
+    rewrite Regmap.gsident.
+    replace ((rs # r <- (rs # r)) ## (eq_args eq)) with
+        (rs ## (eq_args eq)).
+    { apply REL; auto. }
+    apply list_map_exten.
+    intros.
+    apply Regmap.gsident.
+  Qed.
+      
   Lemma move_sound :
     forall no : node,
     forall rel : RELATION.t,
@@ -756,6 +775,10 @@ Section SOUNDNESS.
     unfold move.
     intros until m.
     intro REL.
+    destruct (peq src dst).
+    { subst dst.
+      apply rel_idem_replace; auto.
+    }
     pose proof (eq_find_sound no  {| eq_lhs := dst; eq_op := SOp Omove; eq_args := src :: nil |}) as EQ_FIND_SOUND.
     destruct eq_find.
     - intros i eq CONTAINS.
-- 
cgit