We currently have 2 versions of `eexact`

(ltac1 and ltac2). They are not the same:

```
Goal nat. eexact _.
```

fails with

```
Unable to satisfy the following constraints:
?y : "?T"
```

in ltac1 and succeeds producing a shelved `nat`

goal in ltac2.

In fact WTF is ltac1 `eexact`

for? the stdlib contains 1 instance (https://github.com/coq/coq/blob/e4df3622ec23a540e4f800a45e5aab8c375e12e5/theories/Numbers/NatInt/NZSqrt.v#L359) but `exact`

works fine there

the test suite contains a couple instances but `exact`

behaves the same there too (with better error message in the test for https://github.com/coq/coq/issues/3461)

meanwhile the ltac2 version is somewhat equivalent to `refine; shelve`

(ltac2 refine which is like ltac1 `simple refine`

) modulo subtilities about the difference between shelved evar and future goal evar (ie

```
Require Import Ltac2.Ltac2.
Axiom foo : bool -> nat -> nat.
Goal nat.
unshelve (refine '(foo _ _); Control.shelve()). (* goals bool, nat *)
exact true.
unshelve (eexact (foo _ _)). (* goals bool, nat *)
exact true.
unshelve (refine '(foo _ ltac:(shelve)); Control.shelve()). (* goals nat, bool *)
2:exact true.
unshelve (eexact (foo _ ltac:(shelve))). (* goals bool, nat *)
exact true.
```

) so is it really useful?

and the doc says https://coq.inria.fr/doc/master/refman/proof-engine/tactics.html#coq:tacn.eexact

```
Tactic exact one_term
Directly gives the exact proof term for the goal. exact p succeeds if and only if one_term and the type of p are unifiable (see Conversion rules).
Error Not an exact proof.
Tactic eexact one_term
Behaves like exact but can handle terms and goals with existential variables.
```

leaving unclear what "can handle" means. possibly `exact`

used to have trouble with goals that have evars? but on

```
Goal exists n m:nat, n = m.
do 2 eexists.
exact eq_refl.
```

8.4 fails with "cannot infer the implicit parameter x of eq_refl" both with exact and eexact, after 8.5 both exact and eexact succeed so IDK

A good chunk of the e-tactic business is legacy behaviour, so we could probably just deprecate eexact

ideally the non-e variants should all be defined as a call to the tclWITHOLES wrapper around the base e-tactic

I have a piece of Ltac where I was forced to use `eexact`

instead of `exact`

, and it is only two year old. But I do not remember the reason. From what I can infer from the code, it tries to match a term of type `?P -> ?Q`

with a goal of type `foo -> ?R`

. So, perhaps `eexact`

behaves better when unifying types that mix arrows and evars.

definition of eexact: https://github.com/coq/coq/blob/cf2842d9e4a62455a8c7ed692c14ade84bc235d1/plugins/ltac/g_auto.mlg#L32 and https://github.com/coq/coq/blob/cf2842d9e4a62455a8c7ed692c14ade84bc235d1/tactics/eauto.ml#L30-L40

so eexact takes a `constr`

(not open_constr AFAICT) but uses old unification when the goal or inferred type of the term have undefined evars

In my case, both the goal and the inferred type have undefined evars. So, I guess it is a case where the old unification works better.

is your code public?

Sure. But it is in a user-facing tactic. So just changing `eexact`

into `exact`

will not cause any apparent issue, unless you can recover the originally failing user testcase (which I don't remember). https://gitlab.inria.fr/coqinterval/interval/-/blob/master/src/Tactic.v?ref_type=heads#L244

There, `cut_root`

has type `forall (x y : R) (G P : Prop), ((P -> G) -> x = y -> G) -> ((x = y -> P) -> G) -> G`

. So, in `eexact K`

, `K`

has type `(?P -> ?G) -> x = y -> ?G`

, if I am not mistaken.

Last updated: Oct 13 2024 at 01:02 UTC