Quelle  with_strategy.v   Sprache: Coq

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.
  Time Timeout 5
       with_strategy
       expand [id]
       assert (id (fact 100) = fact 100) by abstract reflexivity.
  reflexivity.
Time Timeout 5 Defined.

(* test that it works even with [Qed] *)
Goal id 0 = 0.
Proof using Type.
  Time Timeout 5
       abstract
       (with_strategy
          expand [id]
          assert (id (fact 100) = fact 100) by abstract reflexivity;
       reflexivity).
Time Timeout 5 Qed.

(* test that the strategy is correctly reverted after closing the goal completely *)
Goal id 0 = 0.
  assert (id 0 = 0) by with_strategy expand [id] reflexivity.
  Fail unfold id.
  reflexivity.
Qed.

(* test that the strategy is correctly reverted after failure *)
Goal id 0 = 0.
  let id' := id in
  (try with_strategy expand [id] fail); assert_fails unfold id'.
  Fail unfold id.
  (* a more complicated test involving a success and then a failure after backtracking *)
  let id' := id in
  ((with_strategy expand [id] (unfold id' + fail)) + idtac);
    lazymatch goal with |- id 0 = 0 => idtac end;
    assert_fails unfold id'.
  Fail unfold id.
  reflexivity.
Qed.

(* test multi-success *)
Goal id (fact 100) = fact 100.
  Timeout 1
          (with_strategy -1 [id] (((idtac + (abstract reflexivity))); fail)).
  Undo.
  Timeout 1
          let id' := id in
          (with_strategy -1 [id] (((idtac + (unfold id'; reflexivity))); fail)).
  Undo.
  Timeout 1
          (with_strategy -1 [id] (idtac + (abstract reflexivity))); fail. (* should not time out *)
  Undo.
  with_strategy -1 [id] abstract reflexivity.
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.
  F.with_transparent_id ltac:(progress unfold F.id).
  Undo.
  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.
  F2.with_transparent_id ltac:(progress unfold F2.id).
  Undo.
  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.

(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *)
Reset Initial.