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.