Tactic to prove a boolean implication

Question

Is there a tactic similar to intros to prove a boolean implication such as

f : nat -> bool
g : nat -> bool
Lemma f_implies_g : forall n : nat, eq_true(implb (f n) (g n)).

This tactic would pull eq_true(f n) into the context and require to prove eq_true(g n).

Answer 1

Let me suggest to use SSReflect in this case. Because it already has the machinery you need. It does not use eq_true to embed bool into Prop, but rather is_true, which is an alternate way to do it.

From Coq Require Import ssreflect ssrbool.
Variables f g : nat -> bool.
Lemma f_implies_g n : (f n) ==> (g n).
Proof.
apply/implyP => Hfn.
Abort.

The snippet above does what you want, implicitly coercing f n and g n into Prop. Having executed the snippet you see this

  n : nat
  Hfn : f n
  ============================
  g n

but Set Printing Coercions. reveals that it's really

  n : nat
  Hfn : is_true (f n)
  ============================
  is_true (g n)

that you have.