Draft: trying refinement

theories/tree_borrows/disjoint.v

@@ -566,6 +566,34 @@ Proof.
   + apply HEAD1'.
 Qed.
 
+From simuliris.tree_borrows Require Import lang examples.lib.
 
+Definition single_thread_step (P : prog) (st st' : expr * state) := prim_step P st.1 st.2 st'.1 st'.2 [].
 
+Definition refines P (e1 e2 : expr) :=
+  ∀ σ e' σ', rtc (single_thread_step P) (e1, σ) (e', σ') →
+    ( (* if the target can reach a stuck state, then so can the source *)
+      irreducible P e' σ' → ∃ e'' σ'', irreducible P e'' σ'' ∧ rtc (single_thread_step P) (e2, σ) (e', σ') ) ∧
+    ( (* if the target can reach a value, then the source can reach the same value in the same state *)
+      is_Some (to_val e') → rtc (single_thread_step P) (e2, σ) (e', σ')).
+
+Definition two_reads v1 x1 v2 x2 rest : expr :=
+  let: v1 := Copy *{sizeof_scalar} x1 in
+  let: v2 := Copy *{sizeof_scalar} x2 in
+  rest.
+
+Theorem basic_refinement {P rest} :
+  refines P
+    (two_reads "v1" "x1" "v2" "x2" rest)
+    (two_reads "v2" "x2" "v1" "x1" rest).
+Proof.
+  intros ? ? ? Reach. 
+  split.
+  + admit.
+  + unfold two_reads in *.
+    inversion Reach; intros; subst. { inversion H0. inversion H. }
+    destruct y; simpl in *; subst.
+    inversion H; simpl in *; subst.
+    destruct K; simpl in *.
+    * inversion H4.