Make eexact consistent with other e-tactics

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4045
From: @MatejKosik
Reported version: trunk
CC: coq-bugs-redist@lists.gforge.inria.fr

[coqbot]

Comment author: @MatejKosik

Concerning "eexact" tactic the Reference Manual says:

"This tactic behaves like exact but is able to handle terms and goals with meta-variables."

That sounds like "exact" wouldn't be able to cope with terms and goals with meta-variables. I do not think that is true (anymore):

Below, there is no need for "eexact" even though meta-variables are involved.

Require Import Arith.

(*
Nat.le_trans : forall n m p : nat, n <= m -> m <= p -> n <= p
mult_le_compat_r : forall n m p : nat, n <= m -> n * p <= m * p
mult_le_compat_l : forall n m p : nat, n <= m -> p * n <= p * m
*)

Theorem le_mult_mult : forall a b c d : nat, a <= c -> b <= d -> a * b <= c * d.
Proof.
(* forall a b c d : nat, a <= c -> b <= d -> a * b <= c * d ) intros a b c d a_le_c b_le_d.
( │ )
( │ a : nat )
( │ b : nat )
( │ c : nat )
( │ d : nat )
( │ a_le_c : a <= c )
( │ b_le_d : b <= d )
( │ )
( ╰─ a * b <= c * d ) eapply le_trans.
( │ )
( ├─ a * b <= ?m ) eapply mult_le_compat_r.
( │ │ )
( │ ╰─ a <= ?m0 ) exact a_le_c.
( │ )
( ╰─ c * b <= c * d ) apply mult_le_compat_l.
( │ )
( ╰─ b <= d *) exact b_le_d.
Qed.

[coqbot]

Comment author: @Zimmi48

Actually, I couldn't find any use-case where eexact is more powerful than exact. (BTW the tactic is not used in the standard library.)

In particular, eexact is strictly less powerful than eapply in cases where they should be equivalent:

Goal (nat -> True) -> True.
intro H.
Fail eexact (H _).
eapply (H _). (* all remaining goals are on the shelf *)

The implementation of eexact should be changed to succeed in this case in the same way as eapply, or the tactic should be simply removed.

Does anyone have an example where eexact is more powerful than exact as of today?

[JasonGross]

I found a case where exact is more powerful than eexact, strangely enough. I'll be reporting it soon.

[JasonGross]

Here is an example where exact succeeds but eexact fails: #9965 (comment)

[JasonGross]

Minimal-ish test-case:
This succeeds:

Class Foo := foo : True.

Goal forall (A B : Type) (F : A -> Type) (a : A),
    F a -> (Foo -> forall x, F x -> B) -> B.
  intros A B F a Fa H.
  let H' := open_constr:(H _ _) in
  refine (H' _); match goal with H'' : _ |- _ => exact H'' end.

but if I replace exact with eexact, then it fails.

[SkySkimmer]

I get the same results if I replace the match goal stuff with just (e)exact Fa btw