Perform `fast_done` first in `naive_solver`.

This avoids naive_solver tearing whole goals apart, even if the goal appears exactly as a hypothesis.

In Iris/C I ran into this problem after the recent set_solver changes (4ff965b2). Since set_unfold unfolds more stuff than it used to do, naive_solver essentially had to solve P → P. However, since it was tearing the entire goal apart, and trying to reestablish it while there were other assumptions in the context that influenced instantiation of existentials, it was not able to solve P again. By performing fast_done eagerly, it will not simply solve P → P immediately without tearing the entire goal apart.

It appears that the impact on e.g. LambdaRust is in the noise range: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=4ad3f8b08c1ff4481d0fab41f878b215257a6462&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fnaive_solver&var-commit2=11c5f900bf7b1f9fdaf4ba8cfc36d601bb5abdbf&var-config2=coq-8.9.0&var-group=().*&var-metric=instructions

theories/tactics.v

@@ -506,6 +506,8 @@ Tactic Notation "naive_solver" tactic(tac) :=
   end;
   let rec go n :=
   repeat match goal with
+  (**i solve the goal *)
+  | |- _ => fast_done
   (**i intros *)
   | |- ∀ _, _ => intro
   (**i simplification of assumptions *)
@@ -522,8 +524,6 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
   (**i simplify and solve equalities *)
   | |- _ => progress simplify_eq/=
-  (**i solve the goal *)
-  | |- _ => fast_done
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | |- Is_true (bool_decide _) => apply (bool_decide_pack _)