Add a `with_strategy` tactic

Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.

We have some timeouts in the strategy success file.  We should not run
into issues, because we are not really testing how long these take.  We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.

Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.

One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556

Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>

2 files changed, 614 insertions, 0 deletions

diff --git a/test-suite/success/strategy.v b/test-suite/success/strategy.v
new file mode 100644
index 0000000000..926ba54342
--- /dev/null
+++ b/test-suite/success/strategy.v
@@ -0,0 +1,87 @@
+Notation aid := (@id) (only parsing).
+Notation idn := id (only parsing).
+Ltac unfold_id := unfold id.
+
+Fixpoint fact (n : nat)
+  := match n with
+     | 0 => 1
+     | S n => (S n) * fact n
+     end.
+
+Opaque id.
+Goal id (fact 100) = fact 100.
+  Strategy expand [id].
+  Time Timeout 5 reflexivity. (* should be instant *)
+  (* Finished transaction in 0. secs (0.u,0.s) (successful) *)
+Time Timeout 5 Defined.
+(* Finished transaction in 0.001 secs (0.u,0.s) (successful) *)
+
+Goal True.
+  let x := smart_global:(id) in unfold x.
+  let x := smart_global:(aid) in unfold x.
+  let x := smart_global:(idn) in unfold x.
+Abort.
+
+Goal id 0 = 0.
+  Opaque id.
+  assert_fails unfold_id.
+  Transparent id.
+  assert_succeeds unfold_id.
+  Opaque id.
+  Strategy 0 [id].
+  assert_succeeds unfold_id.
+  Strategy 1 [id].
+  assert_succeeds unfold_id.
+  Strategy -1 [id].
+  assert_succeeds unfold_id.
+  Strategy opaque [id].
+  assert_fails unfold_id.
+  Strategy transparent [id].
+  assert_succeeds unfold_id.
+  Opaque id.
+  Strategy expand [id].
+  assert_succeeds unfold_id.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Opaque aid.
+  assert_fails unfold_id.
+  Transparent aid.
+  assert_succeeds unfold_id.
+  Opaque aid.
+  Strategy 0 [aid].
+  assert_succeeds unfold_id.
+  Strategy 1 [aid].
+  assert_succeeds unfold_id.
+  Strategy -1 [aid].
+  assert_succeeds unfold_id.
+  Strategy opaque [aid].
+  assert_fails unfold_id.
+  Strategy transparent [aid].
+  assert_succeeds unfold_id.
+  Opaque aid.
+  Strategy expand [aid].
+  assert_succeeds unfold_id.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Opaque idn.
+  assert_fails unfold_id.
+  Transparent idn.
+  assert_succeeds unfold_id.
+  Opaque idn.
+  Strategy 0 [idn].
+  assert_succeeds unfold_id.
+  Strategy 1 [idn].
+  assert_succeeds unfold_id.
+  Strategy -1 [idn].
+  assert_succeeds unfold_id.
+  Strategy opaque [idn].
+  assert_fails unfold_id.
+  Strategy transparent [idn].
+  assert_succeeds unfold_id.
+  Opaque idn.
+  Strategy expand [idn].
+  assert_succeeds unfold_id.
+  reflexivity.
+Qed.
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
new file mode 100644
index 0000000000..bf639ae6b9
--- /dev/null
+++ b/test-suite/success/with_strategy.v
@@ -0,0 +1,527 @@
+Notation aid := (@id) (only parsing).
+Notation idn := id (only parsing).
+Ltac unfold_id := unfold id.
+
+Fixpoint fact (n : nat)
+  := match n with
+     | 0 => 1
+     | S n => (S n) * fact n
+     end.
+
+Opaque id.
+Goal id 0 = 0.
+  with_strategy
+    opaque [id]
+    (with_strategy
+       opaque [id id]
+       (assert_fails unfold_id;
+        with_strategy
+          transparent [id]
+          (assert_succeeds unfold_id;
+           with_strategy
+             opaque [id]
+             (with_strategy
+                0 [id]
+                (assert_succeeds unfold_id;
+                 with_strategy
+                   1 [id]
+                   (assert_succeeds unfold_id;
+                    with_strategy
+                    -1 [id]
+                       (assert_succeeds unfold_id;
+                        with_strategy
+                          opaque [id]
+                          (assert_fails unfold_id;
+                           with_strategy
+                             transparent [id]
+                             (assert_succeeds unfold_id;
+                              with_strategy
+                                opaque [id]
+                                (with_strategy
+                                   expand [id]
+                                   (assert_succeeds unfold_id;
+                                    let l := strategy_level:(expand) in
+                                    with_strategy
+                                      l [id]
+                                      (let idx := smart_global:(id) in
+                                       cbv [idx];
+                                       (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *)
+                                       assert_fails
+                                         (let idx := smart_global:(id) in
+                                          with_strategy
+                                            expand [idx]
+                                            idtac);
+                                       reflexivity)))))))))))).
+Qed.
+Goal id 0 = 0.
+  with_strategy
+    opaque [aid]
+    (assert_fails unfold_id;
+     with_strategy
+       transparent [aid]
+       (assert_succeeds unfold_id;
+        with_strategy
+          opaque [aid]
+          (with_strategy
+             0 [aid]
+             (assert_succeeds unfold_id;
+              with_strategy
+                1 [aid]
+                (assert_succeeds unfold_id;
+                 with_strategy
+                 -1 [aid]
+                    (assert_succeeds unfold_id;
+                     with_strategy
+                       opaque [aid]
+                       (assert_fails unfold_id;
+                        with_strategy
+                          transparent [aid]
+                          (assert_succeeds unfold_id;
+                           with_strategy
+                             opaque [aid]
+                             (with_strategy
+                                expand [aid]
+                                (assert_succeeds unfold_id;
+                                 reflexivity)))))))))).
+Qed.
+Goal id 0 = 0.
+  with_strategy
+    opaque [idn]
+    (assert_fails unfold_id;
+     with_strategy
+       transparent [idn]
+       (assert_succeeds unfold_id;
+        with_strategy
+          opaque [idn]
+          (with_strategy
+             0 [idn]
+             (assert_succeeds unfold_id;
+              with_strategy
+                1 [idn]
+                (assert_succeeds unfold_id;
+                 with_strategy
+                 -1 [idn]
+                    (assert_succeeds unfold_id;
+                     with_strategy
+                       opaque [idn]
+                       (assert_fails unfold_id;
+                        with_strategy
+                          transparent [idn]
+                          (assert_succeeds unfold_id;
+                           with_strategy
+                             opaque [idn]
+                             (with_strategy
+                                expand [idn]
+                                (assert_succeeds unfold_id;
+                                 reflexivity)))))))))).
+Qed.
+
+(* test that strategy tactic does not persist after the execution of the tactic *)
+Opaque id.
+Goal id 0 = 0.
+  assert_fails unfold_id;
+    (with_strategy transparent [id] assert_succeeds unfold_id);
+    assert_fails unfold_id.
+  assert_fails unfold_id.
+  with_strategy transparent [id] assert_succeeds unfold_id.
+  assert_fails unfold_id.
+  reflexivity.
+Qed.
+
+(* test that the strategy tactic does persist through abstract *)
+Opaque id.
+Goal id 0 = 0.
+  Fail Time Timeout 5
+       with_strategy
+       expand [id]
+       assert (id (fact 100) = fact 100) by abstract reflexivity.
+  reflexivity.
+Time Timeout 5 Defined.
+
+(* check that module substitutions happen correctly *)
+Module F.
+  Definition id {T} := @id T.
+  Opaque id.
+  Ltac with_transparent_id tac := with_strategy transparent [id] tac.
+End F.
+Opaque F.id.
+
+Goal F.id 0 = F.id 0.
+  Fail unfold F.id.
+  (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *)
+  Fail F.with_transparent_id ltac:(progress unfold F.id).
+  F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x).
+Abort.
+
+Module Type Empty. End Empty.
+Module E. End E.
+Module F2F (E : Empty).
+  Definition id {T} := @id T.
+  Opaque id.
+  Ltac with_transparent_id tac := with_strategy transparent [id] tac.
+End F2F.
+Module F2 := F2F E.
+Opaque F2.id.
+
+Goal F2.id 0 = F2.id 0.
+  Fail unfold F2.id.
+  (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *)
+  Fail F2.with_transparent_id ltac:(progress unfold F2.id).
+  F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x).
+Abort.
+
+(* test the tactic notation entries *)
+Tactic Notation "with_strategy0" strategy_level(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac.
+Tactic Notation "with_strategy1" strategy_level_or_var(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac.
+Tactic Notation "with_strategy2" strategy_level(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac.
+Tactic Notation "with_strategy3" strategy_level_or_var(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac.
+
+(* [with_strategy0] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *)
+Opaque id.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [id id] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy0 0 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 1 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 -1 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy0 expand [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *)
+  Fail let idx := smart_global:(id) in
+       with_strategy0 expand [idx] idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac.
+  Fail (* should work, not Fail *) with_strategy0 0 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 1 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 -1 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac.
+  Fail (* should work, not Fail *) with_strategy0 expand [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac.
+  Fail (* should work, not Fail *) with_strategy0 0 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 1 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 -1 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac.
+  Fail (* should work, not Fail *) with_strategy0 expand [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  reflexivity.
+Qed.
+
+(* [with_strategy1] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *)
+Opaque id.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [id id] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy1 0 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 1 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 -1 [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac.
+  Fail (* should work, not Fail *) with_strategy1 expand [id] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) let l := strategy_level:(expand) in
+                                   with_strategy1 l [id] idtac.
+  (* This should succeed, but doesn't, basically due to https://github idtac.com/coq/coq/issues/11202 *)
+  Fail let idx := smart_global:(id) in
+       with_strategy1 expand [idx] idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac.
+  Fail (* should work, not Fail *) with_strategy1 0 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 1 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 -1 [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac.
+  Fail (* should work, not Fail *) with_strategy1 expand [aid] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac.
+  Fail (* should work, not Fail *) with_strategy1 0 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 1 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 -1 [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac.
+  assert_fails unfold_id.
+  Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac.
+  Fail (* should work, not Fail *) with_strategy1 expand [idn] idtac.
+  Fail (* should work, not Fail *) assert_succeeds unfold_id idtac.
+  reflexivity.
+Qed.
+
+Opaque id.
+Goal id 0 = 0.
+  with_strategy2
+    opaque [id]
+    (with_strategy2
+       opaque [id]
+       (assert_fails unfold_id;
+        with_strategy2
+          transparent [id]
+          (assert_succeeds unfold_id;
+           with_strategy2
+             opaque [id]
+             (with_strategy2
+                0 [id]
+                (assert_succeeds unfold_id;
+                 with_strategy2
+                   1 [id]
+                   (assert_succeeds unfold_id;
+                    with_strategy2
+                    -1 [id]
+                       (assert_succeeds unfold_id;
+                        with_strategy2
+                          opaque [id]
+                          (assert_fails unfold_id;
+                           with_strategy2
+                             transparent [id]
+                             (assert_succeeds unfold_id;
+                              with_strategy2
+                                opaque [id]
+                                (with_strategy2
+                                   expand [id]
+                                   (assert_succeeds unfold_id))))))))))).
+  (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *)
+  Fail let idx := smart_global:(id) in
+       with_strategy2 expand [idx] idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  with_strategy2
+    opaque [aid]
+    (with_strategy2
+       opaque [aid]
+       (assert_fails unfold_id;
+        with_strategy2
+          transparent [aid]
+          (assert_succeeds unfold_id;
+           with_strategy2
+             opaque [aid]
+             (with_strategy2
+                0 [aid]
+                (assert_succeeds unfold_id;
+                 with_strategy2
+                   1 [aid]
+                   (assert_succeeds unfold_id;
+                    with_strategy2
+                    -1 [aid]
+                       (assert_succeeds unfold_id;
+                        with_strategy2
+                          opaque [aid]
+                          (assert_fails unfold_id;
+                           with_strategy2
+                             transparent [aid]
+                             (assert_succeeds unfold_id;
+                              with_strategy2
+                                opaque [aid]
+                                (with_strategy2
+                                   expand [aid]
+                                   (assert_succeeds unfold_id))))))))))).
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  with_strategy2
+    opaque [idn]
+    (with_strategy2
+       opaque [idn]
+       (assert_fails unfold_id;
+        with_strategy2
+          transparent [idn]
+          (assert_succeeds unfold_id;
+           with_strategy2
+             opaque [idn]
+             (with_strategy2
+                0 [idn]
+                (assert_succeeds unfold_id;
+                 with_strategy2
+                   1 [idn]
+                   (assert_succeeds unfold_id;
+                    with_strategy2
+                    -1 [idn]
+                       (assert_succeeds unfold_id;
+                        with_strategy2
+                          opaque [idn]
+                          (assert_fails unfold_id;
+                           with_strategy2
+                             transparent [idn]
+                             (assert_succeeds unfold_id;
+                              with_strategy2
+                                opaque [idn]
+                                (with_strategy2
+                                   expand [idn]
+                                   (assert_succeeds unfold_id))))))))))).
+  reflexivity.
+Qed.
+
+Opaque id.
+Goal id 0 = 0.
+  with_strategy3
+    opaque [id]
+    (with_strategy3
+       opaque [id]
+       (assert_fails unfold_id;
+        with_strategy3
+          transparent [id]
+          (assert_succeeds unfold_id;
+           with_strategy3
+             opaque [id]
+             (with_strategy3
+                0 [id]
+                (assert_succeeds unfold_id;
+                 with_strategy3
+                   1 [id]
+                   (assert_succeeds unfold_id;
+                    with_strategy3
+                    -1 [id]
+                       (assert_succeeds unfold_id;
+                        with_strategy3
+                          opaque [id]
+                          (assert_fails unfold_id;
+                           with_strategy3
+                             transparent [id]
+                             (assert_succeeds unfold_id;
+                              with_strategy3
+                                opaque [id]
+                                (with_strategy3
+                                   expand [id]
+                                   (assert_succeeds unfold_id))))))))))).
+  (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *)
+  Fail let idx := smart_global:(id) in
+       with_strategy3 expand [idx] idtac.
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  with_strategy3
+    opaque [aid]
+    (with_strategy3
+       opaque [aid]
+       (assert_fails unfold_id;
+        with_strategy3
+          transparent [aid]
+          (assert_succeeds unfold_id;
+           with_strategy3
+             opaque [aid]
+             (with_strategy3
+                0 [aid]
+                (assert_succeeds unfold_id;
+                 with_strategy3
+                   1 [aid]
+                   (assert_succeeds unfold_id;
+                    with_strategy3
+                    -1 [aid]
+                       (assert_succeeds unfold_id;
+                        with_strategy3
+                          opaque [aid]
+                          (assert_fails unfold_id;
+                           with_strategy3
+                             transparent [aid]
+                             (assert_succeeds unfold_id;
+                              with_strategy3
+                                opaque [aid]
+                                (with_strategy3
+                                   expand [aid]
+                                   (assert_succeeds unfold_id))))))))))).
+  reflexivity.
+Qed.
+Goal id 0 = 0.
+  with_strategy3
+    opaque [idn]
+    (with_strategy3
+       opaque [idn]
+       (assert_fails unfold_id;
+        with_strategy3
+          transparent [idn]
+          (assert_succeeds unfold_id;
+           with_strategy3
+             opaque [idn]
+             (with_strategy3
+                0 [idn]
+                (assert_succeeds unfold_id;
+                 with_strategy3
+                   1 [idn]
+                   (assert_succeeds unfold_id;
+                    with_strategy3
+                    -1 [idn]
+                       (assert_succeeds unfold_id;
+                        with_strategy3
+                          opaque [idn]
+                          (assert_fails unfold_id;
+                           with_strategy3
+                             transparent [idn]
+                             (assert_succeeds unfold_id;
+                              with_strategy3
+                                opaque [idn]
+                                (with_strategy3
+                                   expand [idn]
+                                   (assert_succeeds unfold_id))))))))))).
+  reflexivity.
+Qed.