Experiment with backtracking in rel_pure_l tactic

F_mu_ref_conc/examples/bit.v

@@ -141,7 +141,12 @@ Section heapify_refinement.
     rel_pure_r (Unpack (Pack _) _).
     rel_rec_l.
     rel_rec_r.
-    repeat rel_pure_l _.
+    rel_proj_l.
+    rel_rec_l.
+    rel_proj_l. rel_proj_l.
+    rel_rec_l.
+    rel_proj_l. rel_proj_l.
+    rel_rec_l.
     repeat rel_pure_r _.
     rel_alloc_l as x1 "Hx1".
     rel_alloc_r as x2 "Hx2".

F_mu_ref_conc/proofmode/rel_tactics.v

@@ -87,15 +87,13 @@ Qed.
 
 Tactic Notation "rel_pure_l" open_constr(ef) :=
   iStartProof;
-  rel_reshape_cont_l ltac:(fun K e' =>
-      unify e' ef;
-      simple eapply (tac_rel_pure_l K e');
-      [tac_bind_helper             (* e = fill K e1' *)
-      |apply _                     (* PureExec ϕ e1 e2 *)
-      |try (exact I || reflexivity || tac_rel_done)
-      |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
-      |simpl; reflexivity       (* eres = fill K e2 *)
-      |try iNext; simpl_subst/= (* new goal *)])
+  (simple eapply tac_rel_pure_l;
+   [tac_bind_helper ef          (* e = fill K e1' *)
+   |apply _                     (* PureExec ϕ e1 e2 *)
+   |try (exact I || reflexivity || tac_rel_done)
+   |first [left; split; reflexivity | right; reflexivity] (* E1 = E2? *)
+   |simpl; reflexivity       (* eres = fill K e2 *)
+   |try iNext; simpl_subst/= (* new goal *)])
   || fail "rel_pure_l: cannot find the reduct".
 
 Tactic Notation "rel_rec_l" := rel_pure_l (App (Rec _ _ _) _) || rel_pure_l (App _ _).
@@ -139,7 +137,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
   rel_reshape_cont_r ltac:(fun K e' =>
       unify e' ef;
       simple eapply (tac_rel_pure_r K e');
-      [tac_bind_helper             (* e = fill K e1 *)
+      [reflexivity                 (* e = fill K e1 *)
       |apply _                     (* PureExec ϕ e1 e2 *)
       |try (exact I || reflexivity || tac_rel_done)  (* φ *)
       |solve_ndisj                 (* ↑specN ⊆ E1 *)
@@ -249,9 +247,9 @@ Qed.
 Tactic Notation "rel_alloc_r" "as" ident(l) constr(H) :=
   iStartProof;
   eapply (tac_rel_alloc_r);
-    [solve_ndisj || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
+    [solve_ndisj     || fail "rel_alloc_r: cannot prove 'nclose specN ⊆ ?'"
     |tac_bind_helper || fail "rel_alloc_r: cannot find 'alloc'"
-    |solve_to_val (* to_val t' = Some v' *)
+    |solve_to_val    || fail "rel_alloc_r: argument not a value"
     |simpl; iIntros (l) H (* new goal *)].
 
 Tactic Notation "rel_alloc_r" :=

F_mu_ref_conc/proofmode/tactics.v

@@ -28,8 +28,7 @@ Ltac reshape_val e tac :=
 
 Ltac reshape_expr e tac :=
   let rec go K e :=
-  match e with
-  | _ => tac K e
+  tac K e + match e with
   | App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
   | App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
   | BinOp ?op ?e1 ?e2 =>
@@ -110,7 +109,7 @@ Lemma tac_rel_bind_r `{logrelG Σ} t' K ℶ E1 E2 Δ Γ e t τ :
   (ℶ ⊢ bin_log_related E1 E2 Δ Γ e t τ).
 Proof. intros. subst. eauto. Qed.
 
-Ltac tac_bind_helper :=
+Tactic Notation "tac_bind_helper" :=
   lazymatch goal with
   | |- fill ?K ?e = fill _ ?efoc =>
      reshape_expr e ltac:(fun K' e' =>
@@ -123,6 +122,19 @@ Ltac tac_bind_helper :=
        replace e with (fill K' e') by (by rewrite ?fill_app))
   end; reflexivity.
 
+Tactic Notation "tac_bind_helper" open_constr(efoc) :=
+  lazymatch goal with
+  | |- fill ?K ?e = fill _ _ =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       let K'' := eval cbn[app] in (K' ++ K) in
+       replace (fill K e) with (fill K'' e') by (by rewrite ?fill_app))
+  | |- ?e = fill _ _ =>
+     reshape_expr e ltac:(fun K' e' =>
+       unify e' efoc;
+       replace e with (fill K' e') by (by rewrite ?fill_app))
+  end; reflexivity.
+
 Tactic Notation "rel_bind_l" open_constr(efoc) :=
   iStartProof;
   eapply (tac_rel_bind_l efoc);