Replace hypothesis with implication without adding its premise as subgoal

Using Rocq
1

This is part of some automation I am trying to build for working with Is_true. I have that Lemma Is_true_implb_impl : (Is_true x -> Is_true y) <-> Is_true (implb x y). and I have a hypothesis H of the form Is_true (implb ?x ?y) that I match using Ltac elim_Is_true := match goal with .... When I apply Is_true_implb_impl x y in H (if I do not instantiate with x and y it failt to match), then the hypothesis is changed into Is_true y and I get Is_true x as a new subgoal. (I tried to get around this by writing a tactic that asserts Is_true x -> Is_true y but this also fails because I couldn’t figure out how to prove the assert, using assumption after the assert does not work). Is there some way such that I can change H into Is_true x -> Is_true y? Another problem with doing this in a loop with other Is_true elimination is that the new subgoal of the form Is_true _ is matched by match goal with but the tactic cannot apply any rules to it.

An example snippet demonstrating what I am trying to do:

From Coq Require Export Init.Datatypes.
From Coq Require Export Bool.Bool.

Lemma Is_true_implb_impl x y :
  (Is_true x -> Is_true y) <-> Is_true (implb x y).
Proof.
  destruct x; simpl; split; intros H.
  - apply H. apply I.
  - intros H'. assumption.
  - apply I.
  - intros H'. exfalso. assumption.
Qed.

Ltac elim_Is_true :=
  match goal with
  (* FAILS: *)
  (* | [H : Is_true (implb ?x ?y) |- _] => apply Is_true_implb_impl in H *)
  | [H : Is_true (implb ?x ?y) |- _] => apply (Is_true_implb_impl x y) in H
  | _ => idtac
  end.

Example test x y :
  Is_true x -> Is_true (implb x y) -> Is_true y.
Proof.
  intros H1 H2. elim_Is_true.
  (* In this case this is useful but in other cases I do not yet want to add
     the premise as a subgoal *)
Abort.
2

rewrite might do what you’re looking for.

From Coq Require Export Init.Datatypes.
From Coq Require Export Bool.Bool.
From Coq Require Import Setoid. (* needed to rewrite with iff *)

Lemma Is_true_implb_impl x y :
  (Is_true x -> Is_true y) <-> Is_true (implb x y).
Proof.
  destruct x; simpl; split; intros H.
  - apply H. apply I.
  - intros H'. assumption.
  - apply I.
  - intros H'. exfalso. assumption.
Qed.

Ltac elim_Is_true :=
  match goal with
  | [H : Is_true (implb ?x ?y) |- _] => rewrite <- (Is_true_implb_impl x y) in H
  | _ => idtac
  end.

Example test x y :
  Is_true x -> Is_true (implb x y) -> Is_true y.
Proof.
  intros H1 H2. elim_Is_true.
Abort.