Tactic Notation "apply" "->" open_constr(lemma) :=
bapply lemma ltac:(fun H => destruct H as [H _]; apply H).

Tactic Notation "eapply" "->" open_constr(lemma) :=
bapply lemma ltac:(fun H => destruct H as [H _]; eapply H).

Axiom foo : True <-> forall x y, x = 0 -> y = 0.
Goal 0 = 0.
Fail apply -> foo. (* Unable to find an instance for the variable x. *)
eapply -> foo. (* second goal is ?x = 0 *)

Axiom foo : forall x y, True <-> (x = 0 -> y = 0).
Goal 0 = 0.
  apply -> foo. (* second goal is ?a = 0 *)

From Ltac2 Require Import Ltac2.

Ltac2 Notation "rename" h(list1(seq(ident, "into", ident), ",")) := Std.rename h.
Ltac2 Notation "clearbody" ids(list1(ident)) := Std.clearbody ids.

Ltac2 rec find_equiv (h : ident) :=
  let hc := Control.hyp h in
  let t := Constr.type hc in
  lazy_match! t with
  | ?a -> ?b
    => Std.cut a
       > [ let h1 := Fresh.in_goal @H in
           intro h1;
           let h2 := Fresh.in_goal @H in
           (* work around COQBUG(https://github.com/coq/coq/issues/18179) *)
           pose ($hc &h1) as h2;
           Std.clearbody [h2];
           clear h h1;
           rename h2 into h;
           find_equiv h
         | clear h ]
  | forall x : ?t, _
    => let h1 := Fresh.in_goal @H in
       epose (&h _) as h1; clearbody h1;
       clear a; clear h; rename h1 into h; find_equiv h
  | ?a <-> ?b => ()
  | _ => Control.backtrack_tactic_failure "The given statement does not seem to end with an equivalence."
  end.

Ltac2 Notation "with_bindings:(" b(with_bindings) ")" := b.
Ltac2 Notation "constr_with_bindings:(" cb(seq(constr, with_bindings)) ")" := cb.

Ltac2 bapply ev lemma todo :=
  let h := Fresh.in_goal @H in
  Notations.enter_h
    ev
    (fun _ (lemma, bindings)
     => Std.pose (Some h) lemma;
        clearbody h;
        Std.specialize (constr_with_bindings:(&h)) None)
    lemma;
  find_equiv h > [todo h; clear h | .. ].

Ltac2 apply0 adv ev ocb cl :=
  let rec go adv ev cb_rev ocb cl :=
    match ocb with
    | [] => let cb := List.rev cb_rev in
            Std.apply adv ev cb cl
    | (ori, cb) :: ocb
      => match ori with
         | None => go adv ev (cb :: cb_rev) ocb cl
         | Some ori
           => let todo h
                := (match ori with
                    | Std.LTR => destruct h as [h _]
                    | Std.RTL => destruct h as [_ h]
                    end;
                    go adv ev ((fun () => constr_with_bindings:(&h)) :: cb_rev) ocb cl) in
              bapply ev cb todo
         end
    end in
  go adv ev [] ocb cl.

Ltac2 Notation "eapply"
  cb(list1(thunk(seq(opt(orient), open_constr, with_bindings)), ","))
  cl(opt(seq("in", ident, opt(seq("as", intropattern))))) :=
  apply0 true true cb cl.

Ltac2 Notation "apply"
  cb(list1(thunk(seq(opt(orient), open_constr, with_bindings)), ","))
  cl(opt(seq("in", ident, opt(seq("as", intropattern))))) :=
  apply0 true false cb cl.