WIP: rework of naive_solver after discussion with Robbert

This is a slightly reworked version of naive_solver, which hopefully fails faster. @robbertkrebbers What do you think? What would be other kinds of goals I should try this version on?

theories/tactics.v

@@ -548,13 +548,14 @@ https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
 
 Ltac no_new_unsolved_evars tac := exact ltac:(tac).
 
-Tactic Notation "naive_solver" tactic(tac) :=
+Ltac naive_solver_prepare :=
   unfold iff, not in *;
   repeat match goal with
   | H : context [∀ _, _ ∧ _ ] |- _ =>
     repeat setoid_rewrite forall_and_distr in H; revert H
-  end;
-  let rec go n :=
+  end.
+
+Ltac naive_solver_go n tac :=
   repeat match goal with
   (**i solve the goal *)
   | |- _ => fast_done
@@ -588,21 +589,61 @@ Tactic Notation "naive_solver" tactic(tac) :=
   (**i use recursion to enable backtracking on the following clauses. *)
   match goal with
   (**i instantiation of the conclusion *)
-  | |- ∃ x, _ => no_new_unsolved_evars ltac:(eexists; go n)
-  | |- _ ∨ _ => first [left; go n | right; go n]
-  | |- Is_true (_ || _) => apply orb_True; first [left; go n | right; go n]
+  | |- ∃ x, _ => no_new_unsolved_evars ltac:(eexists; naive_solver_go n tac)
+  | |- _ ∨ _ => first [left; naive_solver_go n tac | right; naive_solver_go n tac]
+  | |- Is_true (_ || _) => apply orb_True; first [left; naive_solver_go n tac | right; naive_solver_go n tac]
   | _ =>
     (**i instantiations of assumptions. *)
     lazymatch n with
+    | O =>
+      match goal with
+      | H : ?P → ?Q |- _ =>
+        let H' := fresh "H" in
+        assert P as H'; [clear H; naive_solver_go n tac|];
+        specialize (H H'); clear H'; naive_solver_go n tac
+      end
     | S ?n' =>
       (**i we give priority to assumptions that fit on the conclusion. *)
       match goal with
       | H : _ → _ |- _ =>
         is_non_dependent H;
         no_new_unsolved_evars
-          ltac:(first [eapply H | efeed pose proof H]; clear H; go n')
+          ltac:(first [eapply H | efeed pose proof H]; clear H; naive_solver_go n' tac)
       end
     end
-  end
-  in iter (fun n' => go n') (eval compute in (seq 1 6)).
+  end.
+
+Tactic Notation "naive_solver0" tactic(tac) :=
+  naive_solver_prepare;
+  naive_solver_go 0 tac.
+Tactic Notation "naive_solver" tactic(tac) :=
+  naive_solver_prepare;
+  iter (fun n' => naive_solver_go n' tac) (eval compute in (seq 1 6)).
 Tactic Notation "naive_solver" := naive_solver eauto.
+
+Goal ∀ P, (0 < 1 → P) → P.
+  Fail lia.
+  naive_solver0 lia.
+  Undo.
+  naive_solver lia.
+Abort.
+
+Goal ∀ P x, 0 < x → (∀ x : nat, 0 < x → P) → P.
+  Fail lia.
+  Fail naive_solver0 lia.
+  naive_solver lia.
+Abort.
+
+Goal ∀ P,
+    (0 < 0 → P) →
+    (0 < 0 → P) →
+    (0 < 0 → P) →
+    (0 < 0 → P) →
+    (0 < 0 → P) →
+          (0 < 0 → P) → P.
+  Fail lia.
+  (* Finished transaction in 2.472 secs (2.469u,0.002s) (successful) *)
+  Time Fail naive_solver0 lia.
+  (* Finished transaction in 20.79 secs (20.786u,0.002s) (successful) *)
+  Time Fail naive_solver lia.
+Abort.

[Ralf Jung]

Is this an internal tactic, or some variant of naive_solver? Please add a coqdoc comment explaining that.

[Ralf Jung]

These look like testcases. Please move them to tests/naive_solver.v.

[Ralf Jung]

Indentation is off here.