Decouple Ltac2 from Corelib

[patrick-nicodemus]

Is your feature request related to a problem?

This is a feature request to remove the dependencies of Ltac2 on Corelib so that Corelib is not loaded when Ltac2 is loaded, motivated by the desire to be as compatible as possible with the CoqHoTT library.

Ideally Require Ltac2.Ltac2 would not cause Corelib.Init.Logic to be loaded. The modules are all qualified so it's unlikely that the Prop-valued equality would be used accidentally, but it would still be preferable not to load the files defining Prop-valued equality at all.

I'm not sure how realistic this is. Probably an easier target would be to remove the dependence of Ltac2 on the various plugins implementing powerful tactics:

[Loading ML file rocq-runtime.plugins.tauto ...
[Loading ML file rocq-runtime.plugins.cc_core ...
[Loading ML file rocq-runtime.plugins.cc ...
[Loading ML file rocq-runtime.plugins.firstorder_core ...
[Loading ML file rocq-runtime.plugins.firstorder ...

Proposed solution

No response

Alternative solutions

No response

Additional context

No response

[SkySkimmer]

I think currently the main obstacle is that Ltac2 provides now which needs Logic etc
https://github.com/coq/coq/blob/89b24b812f89a1a8e8fd72ea10182b46f220e75e/user-contrib/Ltac2/Notations.v#L624
https://github.com/coq/coq/blob/89b24b812f89a1a8e8fd72ea10182b46f220e75e/theories/Init/Tactics.v#L158

Maybe we could reduce the ltac2 dependency to just Corelib.Init.Ltac using an indirection, something like

(* Corelib.Init.Ltac *)
(* current content + *)
Ltac easy := fail "Corelib.Init.Tactics not loaded".

(* Corelib.Init.Tactics *)
(* after Ltac easy := big code: *)
Ltac Ltac.easy ::= easy.

and use Corelib.Init.Ltac in Ltac2.Notations.

[patrick-nicodemus]

Okay, cool. I see the use of conjunction in that tactic. Are any other tactics in easy heavily dependent on Init stuff? (inversion strikes me as complicated so i'm wondering if that relies on anything in Init)

Or maybe the Ltac2 easy could be rewritten slightly differently, so that instead of [ |- _ /\ _ ] => it was something like "if the goal is an inductive type with a single constructor that takes two arguments, apply the constructor". It would probably be difficult to do that in a backwards compatible way.

[SkySkimmer]

#20387