**Ugly** proof of simu_check_single_correct

1 files changed, 31 insertions, 8 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 40a05739..08a62202 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -1864,14 +1864,37 @@ Lemma simu_check_single_correct dm tf f pc1 pc2:
   sexec_simu dm f tf pc1 pc2.
 Proof.
   unfold sexec_simu; wlp_simplify.
-  exploit H2; clear H2. 1-3: wlp_simplify.
-  (* intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
-  exploit H3; clear H3. 1-3: wlp_simplify.
-  intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
-  eexists. eexists. split; eauto. split; eauto.
-  intros ctx.
-  eapply hsstate_simu_spec_correct; eauto. *)
-Admitted.
+  exploit H3. 1-5: wlp_simplify.
+  - simpl.
+    exploit H0; eauto.
+    wlp_simplify.
+    + assert (exta7 = true). { destruct exta7; auto. }
+      subst.
+      assert (exta8 = true). { destruct exta8; auto. } subst.
+      unfold hscond_set_hid.
+      rewrite H8.
+      assert (lhsv x = lhsv y). { apply H9. reflexivity. }
+      rewrite H12.
+      reflexivity.
+    + discriminate.
+  - intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
+    exploit H4; clear H4. 1-5: wlp_simplify.
+    + simpl.
+      exploit H0; eauto.
+      wlp_simplify. 2: { discriminate. }
+      assert (exta7 = true). { destruct exta7; auto. }
+      subst.
+      assert (exta8 = true). { destruct exta8; auto. } subst.
+      unfold hscond_set_hid.
+      rewrite H4.
+      assert (lhsv x = lhsv y). { apply H5. reflexivity. }
+      rewrite H9.
+      reflexivity.
+    + intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
+      eexists. eexists. split; eauto. split; eauto.
+      intros ctx.
+      eapply hsstate_simu_spec_correct; eauto.
+Qed.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.