Replace hypothesis with implication without adding its premise as subgoal

Question

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 fails 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.

SCappella SCappella · Accepted Answer · 2019-09-30T00:22:12

apply isn't what you want then. Quoting from the documentation,

The tactic apply tries to match the current goal against the conclusion of the type of term. If it succeeds, then the tactic returns as many subgoals as the number of non-dependent premises of the type of term.

Apply will generate subgoals for every (non-dependent) argument, which in your case includes Is_true x (in addition to the goal you already have: Is_true y).

Instead, what you can do is some trickery to emulate apply's hypothesis-replacing behavior but have better control over what the new hypothesis is.


Ltac elim_Is_true :=
  match goal with
  | H : Is_true (implb ?x ?y) |- _ =>
          (* Generate a new name for a temporary hypothesis *)
          let H' := fresh in
          (* rename the old hypothesis to this new name *)
          rename H into H';
          (* replace the goal with (Is_true x -> Is_true y) -> ?Goal *)
          generalize (proj2 (Is_true_implb_impl x y) H');
          (* intro (Is_true x -> Is_true y) with the old name *)
          intro H;
          (* Get rid of the old hypothesis *)
          clear H'
  | _ => idtac
  end.

We use proj2 (Is_true_implb_impl x y) H' because we want the <- part of the if and only if.

This can be abstracted with a tactic like this:

Tactic Notation "ng_apply" constr(X) "in" constr(H) :=
  let H' := fresh in
  rename H into H';
  generalize (X H'); intro H;
  clear H'.

Now elim_Is_true can be rewritten as

Ltac elim_Is_true :=
  lazymatch goal with
  | H : Is_true (implb ?x ?y) |- _ =>
          ng_apply (proj2 (Is_true_implb_impl x y)) in H
  end.

(the "ng" in ng_apply means no extra goals)

You can emulate some of the behavior of apply by using more complicated ltacs. For example, this version duplicates apply's behavior with tuple types (like <->). This means that we could simplify to ng_apply (Is_true_implb_impl x y) in H.

Ltac ng_apply X H :=
  first [
    let X' := fresh in let Y := fresh in let Z := fresh in
    set (X' := X);
    destruct X' as [Y Z] in X';
    first [ng_apply Y H | ng_apply Z H];
    clear Y; clear Z
  | let H' := fresh in
    rename H into H';
    generalize (X H');
    intro H;
    clear H'
  ].

It might be possible to let ng_apply supply some of the arguments, but I couldn't get it to work with tuple destructuring.

Replace hypothesis with implication without adding its premise as subgoal

1 Answers